diff --git a/DynamicalSystems/Basic/Documentation.lean b/DynamicalSystems/Basic/Documentation.lean
index 97c908d..1f8ef93 100644
--- a/DynamicalSystems/Basic/Documentation.lean
+++ b/DynamicalSystems/Basic/Documentation.lean
@@ -33,7 +33,7 @@ tag := "lploc"
 For autonomous equations, the solution operator can be represented using {name}`Flow` as a map
 `ℝ → E → E`.
 For non-autonomous systems, the solution operator is not time-covariant, therefore one has to take
-the initial time into account. We prove a bundled map
+the initial time into account. We define a bundled map
 
 {docstring NonautonomousFlow}
 
diff --git a/DynamicalSystems/Basic/LpLoc.lean b/DynamicalSystems/Basic/LpLoc.lean
index 54e34f2..df58a04 100644
--- a/DynamicalSystems/Basic/LpLoc.lean
+++ b/DynamicalSystems/Basic/LpLoc.lean
@@ -16,186 +16,244 @@ public import Mathlib.MeasureTheory.SpecificCodomains.WithLp
 
 @[expose] public noncomputable section
 
-open MeasureTheory Filter
+open MeasureTheory Filter Topology Bornology
 open scoped NNReal ENNReal
 
-variable {α 𝕜 𝕜' E F : Type*} {m : MeasurableSpace α} {p : ℝ≥0∞} {μ : Measure α}
+variable {α 𝕜 𝕜' ε ε' E F : Type*} {m : MeasurableSpace α} {p : ℝ≥0∞} {μ ν : Measure α}
   [NormedAddCommGroup E] [NormedAddCommGroup F]
 
 namespace MeasureTheory
 
-variable {s : Set α} {f : α →ₘ[μ] E}
+variable {s : Set α}
 
-open Bornology
+section eLpNorm
 
-section MemLpLoc
+@[simp]
+theorem lpAddConst_top : ∞.LpAddConst = 1 := rfl
+
+variable [ENorm ε]
+
+/-- Addition of measures -/
+theorem eLpNorm_add_measure {f : α → ε} :
+    eLpNorm f p (μ + ν) ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm f p ν) := by
+  rcases p.trichotomy with (rfl | rfl | hp)
+  · simp
+  · simp only [eLpNorm_exponent_top]
+    refine eLpNormEssSup_le_of_ae_enorm_bound ?_
+    simp only [ae_add_measure_iff]
+    constructor
+    · have : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ eLpNormEssSup f μ :=
+        ENNReal.ae_le_essSup (fun y ↦ ‖f y‖ₑ)
+      filter_upwards [this] with x hx
+      grw [hx]
+      simp
+    · have : ∀ᵐ (x : α) ∂ν, ‖f x‖ₑ ≤ eLpNormEssSup f ν :=
+        ENNReal.ae_le_essSup (‖f ·‖ₑ)
+      filter_upwards [this] with x hx
+      grw [hx]
+      simp
+  · rw [ENNReal.toReal_pos_iff] at hp
+    simp_rw [eLpNorm_eq_eLpNorm' hp.1.ne' hp.2.ne, eLpNorm'_eq_lintegral_enorm, one_div,
+      lintegral_add_measure]
+    apply ENNReal.rpow_add_le_mul_rpow_add_rpow''
+
+end eLpNorm
+
+namespace MemLp
 
-attribute [fun_prop] MemLp MemLp.add MemLp.sub MemLp.neg
+attribute [fun_prop] MemLp MemLp.add MemLp.sub MemLp.neg MemLp.aestronglyMeasurable
+
+variable [TopologicalSpace ε] [TopologicalSpace.PseudoMetrizableSpace ε] [ENorm ε]
+
+theorem add_measure {f : α → ε} (hμ : MemLp f p μ) (hν : MemLp f p ν) : MemLp f p (μ + ν) := by
+  constructor
+  · simp only [aestronglyMeasurable_add_measure_iff]
+    exact ⟨hμ.aestronglyMeasurable, hν.aestronglyMeasurable⟩
+  · grw [eLpNorm_add_measure]
+    rw [ENNReal.mul_lt_top_iff, ENNReal.add_lt_top]
+    exact Or.inl ⟨p.LpAddConst_lt_top, ⟨hμ.2, hν.2⟩⟩
+
+end MemLp
+
+variable [TopologicalSpace ε]
+
+section MemLpLoc
 
 /-- A function `u` is locally in `Lp` if for every bounded measurable set `s`, `u` is in `Lp` with
 respect to measure `μ` restricted to `s`. -/
 @[fun_prop]
-def MemLpLoc [Bornology α] (u : α → E) (p : ℝ≥0∞) (μ : Measure α := by volume_tac) : Prop :=
-  ∀ s : Set α, MeasurableSet s ∧ IsBounded s → MemLp u p (μ.restrict s)
+def MemLpLoc [ENorm ε] [TopologicalSpace α] (f : α → ε) (p : ℝ≥0∞)
+    (μ : Measure α := by volume_tac) : Prop :=
+  ∀ x, ∀ᶠ s in (𝓝 x).smallSets, MemLp f p (μ.restrict s)
 
-section Bornology
+section ENorm
 
-variable [Bornology α]
+variable [TopologicalSpace α] [ENorm ε] {f g : α → ε}
 
-variable {u v : α → E}
+theorem memLpLoc_prod_iff {f : α → E × F} :
+    MemLpLoc f p μ ↔ MemLpLoc (fun x ↦ (f x).1) p μ ∧ MemLpLoc (fun x ↦ (f x).2) p μ := by
+  simp_rw [MemLpLoc, ← forall_and, ← eventually_and]
+  congrm (∀ x, ∀ᶠ s in (𝓝 x).smallSets, ?_)
+  exact memLp_prod_iff
+
+theorem memLpLoc_withLp_prod_iff [Fact (1 ≤ p)] {f : α → WithLp p (E × F)} :
+    MemLpLoc f p μ ↔ MemLpLoc (WithLp.fst <| f ·) p μ ∧ MemLpLoc (WithLp.snd <| f ·) p μ := by
+  simp_rw [MemLpLoc, ← forall_and, ← eventually_and]
+  congrm (∀ x, ∀ᶠ s in (𝓝 x).smallSets, ?_)
+  exact memLp_prodLp_iff
+
+theorem memLpLoc_congr_ae (huv : f =ᵐ[μ] g) : MemLpLoc f p μ ↔ MemLpLoc g p μ := by
+  congrm (∀ x, ∀ᶠ s in (𝓝 x).smallSets, ?_)
+  exact memLp_congr_ae huv.restrict
+
+theorem MemLpLoc.congr_ae (hu : MemLpLoc f p μ) (huv : f =ᵐ[μ] g) : MemLpLoc g p μ :=
+  (memLpLoc_congr_ae huv).mp hu
 
 @[fun_prop]
-theorem MemLpLoc.memLp {s : Set α} (hs : MeasurableSet s) (hs' : IsBounded s)
-    (hu : MemLpLoc u p μ) : MemLp u p (μ.restrict s) := hu s ⟨hs, hs'⟩
+theorem MemLpLoc.indicator [TopologicalSpace ε'] [ESeminormedAddMonoid ε'] (hs : MeasurableSet s)
+    {f : α → ε'} (hf : MemLpLoc f p μ) :
+    MemLpLoc (s.indicator f) p μ := by
+  intro x
+  filter_upwards [hf x] with s' hf
+  exact hf.indicator hs
+
+end ENorm
+
+section ContinuousENorm
+
+variable [TopologicalSpace α] [ContinuousENorm ε] {f g : α → ε}
+
+theorem MemLp.memLpLoc (hf : MemLp f p μ) : MemLpLoc f p μ := by
+  intro x
+  refine eventually_smallSets.mpr ?_
+  use Set.univ
+  simp only [univ_mem, Set.subset_univ, forall_const, true_and]
+  intro s
+  apply hf.restrict
+
+theorem memLpLoc_iff {f : α → ε} : MemLpLoc f p μ ↔
+    ∀ x, ∃ s : Set α, s ∈ 𝓝 x ∧ MemLp f p (μ.restrict s) := by
+    congrm (∀ x, ?_)
+    rw [eventually_smallSets']
+    intro s t hst hf
+    exact hf.mono_measure (μ.restrict_mono_set hst)
+
+variable [TopologicalSpace.PseudoMetrizableSpace ε]
+
+/-- If a function is locally integrable on a compact set, then it is integrable on that set. -/
+theorem MemLpLoc.memLp_restrict_isCompact (hf : MemLpLoc f p μ) (hs : IsCompact s) :
+    MemLp f p (μ.restrict s) := by
+  refine hs.induction_on ?_ ?_ ?_ ?_
+  · simp [μ.restrict_empty]
+  · intro s t hst h
+    exact h.mono_measure (μ.restrict_mono_set hst)
+  · intro s t hs ht
+    apply (hs.add_measure ht).mono_measure
+    exact Measure.restrict_union_le s t
+  · intro x hx
+    rw [memLpLoc_iff] at hf
+    obtain ⟨s', hs', hs''⟩ := hf x
+    exact ⟨s', mem_nhdsWithin_of_mem_nhds hs', hs''⟩
+
+theorem memLpLoc_iff_memLp_isCompact [WeaklyLocallyCompactSpace α] :
+    MemLpLoc f p μ ↔ ∀ s (_hs : IsCompact s), MemLp f p (μ.restrict s) := by
+  constructor
+  · intro h s hs
+    exact h.memLp_restrict_isCompact hs
+  · rw [memLpLoc_iff]
+    intro h x
+    obtain ⟨s, hs₁, hs₂⟩ := WeaklyLocallyCompactSpace.exists_compact_mem_nhds x
+    use s, hs₂
+    exact h s hs₁
+
+theorem memLpLoc_iff_memLp_indicator [WeaklyLocallyCompactSpace α] [TopologicalSpace ε']
+    [TopologicalSpace.PseudoMetrizableSpace ε'] [ESeminormedAddMonoid ε']
+    [OpensMeasurableSpace α] [T2Space α]
+    {f : α → ε'} :
+    MemLpLoc f p μ ↔ ∀ s (_hs : IsCompact s), MemLp (s.indicator f) p μ := by
+  rw [memLpLoc_iff_memLp_isCompact]
+  congrm (∀ s hs, ?_)
+  refine Iff.symm (memLp_indicator_iff_restrict ?_)
+  apply hs.measurableSet
+
+theorem MemLpLoc.memLp_indicator [OpensMeasurableSpace α] [T2Space α]
+    [TopologicalSpace ε'] [TopologicalSpace.PseudoMetrizableSpace ε'] [ESeminormedAddMonoid ε']
+    {f : α → ε'} (hf : MemLpLoc f p μ) (hs : IsCompact s) :
+    MemLp (s.indicator f) p μ := by
+  rw [memLp_indicator_iff_restrict hs.measurableSet]
+  exact hf.memLp_restrict_isCompact hs
 
 @[fun_prop]
-theorem MemLpLoc.aestronglyMeasurable {s : Set α} (hs : MeasurableSet s) (hs' : IsBounded s)
-    (hu : MemLpLoc u p μ) : AEStronglyMeasurable u (μ.restrict s) :=
-  (hu s ⟨hs, hs'⟩).aestronglyMeasurable
+theorem MemLpLoc.aestronglyMeasurable (hs : IsCompact s) (hf : MemLpLoc f p μ) :
+    AEStronglyMeasurable f (μ.restrict s) :=
+  (hf.memLp_restrict_isCompact hs).aestronglyMeasurable
 
-theorem memLpLoc_prod_iff {u : α → E × F} :
-    MemLpLoc u p μ ↔ MemLpLoc (fun x ↦ (u x).1) p μ ∧ MemLpLoc (fun x ↦ (u x).2) p μ := by
-  constructor
-  · intro h
-    exact ⟨(h · · |>.fst), (h · · |>.snd)⟩
-  · intro ⟨h₁, h₂⟩ s hs
-    exact MemLp.of_fst_snd ⟨h₁ s hs, h₂ s hs⟩
+end ContinuousENorm
 
-theorem memLpLoc_withLp_prod_iff {p : ℝ≥0∞} [Fact (1 ≤ p)] {u : α → WithLp p (E × F)} :
-    MemLpLoc u p μ ↔ MemLpLoc (WithLp.fst <| u ·) p μ ∧ MemLpLoc (WithLp.snd <| u ·) p μ := by
-  constructor
-  · intro h
-    exact ⟨(h · · |>.prodLp_fst), (h · · |>.prodLp_snd)⟩
-  · intro ⟨h₁, h₂⟩ s hs
-    exact MemLp.of_fst_of_snd_prodLp ⟨h₁ s hs, h₂ s hs⟩
+variable [TopologicalSpace α] {f g : α → E}
 
 @[to_fun (attr := fun_prop)]
-theorem MemLpLoc.add (hu : MemLpLoc u p μ) (hv : MemLpLoc v p μ) : MemLpLoc (u + v) p μ := by
-  intro s ⟨hs, hs'⟩
-  fun_prop
+theorem MemLpLoc.add (hf : MemLpLoc f p μ) (hg : MemLpLoc g p μ) : MemLpLoc (f + g) p μ := by
+  intro x
+  filter_upwards [hf x, hg x] with x hf hg
+  exact hf.add hg
 
 @[to_fun (attr := fun_prop)]
-theorem MemLpLoc.sub (hu : MemLpLoc u p μ) (hv : MemLpLoc v p μ) : MemLpLoc (u - v) p μ := by
-  intro s ⟨hs, hs'⟩
-  fun_prop
+theorem MemLpLoc.sub (hf : MemLpLoc f p μ) (hg : MemLpLoc g p μ) : MemLpLoc (f - g) p μ := by
+  intro x
+  filter_upwards [hf x, hg x] with x hf hg
+  exact hf.sub hg
 
 @[to_fun (attr := fun_prop)]
-theorem MemLpLoc.neg (hu : MemLpLoc u p μ) : MemLpLoc (-u) p μ := by
-  intro s ⟨hs, hs'⟩
-  fun_prop
+theorem MemLpLoc.neg (hf : MemLpLoc f p μ) : MemLpLoc (-f) p μ := by
+  intro x
+  filter_upwards [hf x] with x hf
+  exact hf.neg
 
 @[to_fun (attr := fun_prop)]
-theorem memLpLoc_finsetSum {ι} (s₀ : Finset ι) {u : ι → α → E} (hu : ∀ i ∈ s₀, MemLpLoc (u i) p μ) :
-    MemLpLoc (∑ i ∈ s₀, u i) p μ := by
-  intro s hs
-  exact memLp_finsetSum' s₀ (hu · · s hs)
+theorem memLpLoc_finsetSum {ι} (s : Finset ι) {f : ι → α → E} (hf : ∀ i ∈ s, MemLpLoc (f i) p μ) :
+    MemLpLoc (∑ i ∈ s, f i) p μ := by
+  intro x
+  filter_upwards [(Filter.eventually_all_finset s).mpr (hf · · x)] with x hf'
+  exact memLp_finsetSum' s hf'
 
 variable {𝕜 : Type*} [NormedRing 𝕜] [MulActionWithZero 𝕜 E] [IsBoundedSMul 𝕜 E] {c : 𝕜}
 
 @[fun_prop]
-theorem MemLpLoc.const_smul (hu : MemLpLoc u p μ) : MemLpLoc (c • u) p μ := by
-  intro s hs
-  exact (hu s hs).const_smul c
-
-theorem memLpLoc_iff_memLp_indicator :
-    MemLpLoc u p μ ↔ ∀ s : Set α, MeasurableSet s ∧ IsBounded s → MemLp (s.indicator u) p μ := by
-  congrm (∀ s, (hs : _) → ?_)
-  rw [memLp_indicator_iff_restrict hs.1]
-
-theorem MemLpLoc.memLp_indicator {s₀ : Set α} (hs₀ : MeasurableSet s₀) (hs₀' : IsBounded s₀)
-    (hu : MemLpLoc u p μ) : MemLp (s₀.indicator u) p μ := by
-  rw [memLpLoc_iff_memLp_indicator] at hu
-  exact hu s₀ ⟨hs₀, hs₀'⟩
-
-@[fun_prop]
-theorem MemLpLoc.indicator {s₀ : Set α} (hs₀ : MeasurableSet s₀) (hu : MemLpLoc u p μ) :
-    MemLpLoc (s₀.indicator u) p μ := by
-  intro s hs
-  exact (hu s hs).indicator hs₀
-
-@[fun_prop]
-theorem MemLp.memLpLoc (hu : MemLp u p μ) : MemLpLoc u p μ := by
-  intro s _
-  exact hu.restrict s
-
-/-- In a bounded space, local `Lp` functions are in `Lp`. -/
-@[simp]
-theorem memLpLoc_iff_memLp [BoundedSpace α] : MemLpLoc u p μ ↔ MemLp u p μ := by
-  constructor
-  · intro h
-    rw [← MeasureTheory.Measure.restrict_univ (μ := μ)]
-    exact h Set.univ ⟨MeasurableSet.univ, BoundedSpace.bounded_univ⟩
-  · apply MemLp.memLpLoc
+theorem MemLpLoc.const_smul (hf : MemLpLoc f p μ) : MemLpLoc (c • f) p μ := by
+  intro x
+  filter_upwards [hf x] with x hf
+  exact hf.const_smul c
 
-end Bornology
 
 section MetricSpace
 
-variable [PseudoMetricSpace α] [ProperSpace α] [OpensMeasurableSpace α]
-  [IsFiniteMeasureOnCompacts μ]
+variable [OpensMeasurableSpace α]
+  [IsFiniteMeasureOnCompacts μ] [WeaklyLocallyCompactSpace α] [T2Space α]
+  [SecondCountableTopologyEither α E]
 
 variable {u : α → E}
 
 /-- Every continuous function is locally `Lp` -/
 @[fun_prop]
-theorem Continuous.memLpLoc (h : Continuous u) :
-    MemLpLoc u p μ := by
-  intro s ⟨hs₁, hs₂⟩
+theorem Continuous.memLpLoc (h : Continuous u) : MemLpLoc u p μ := by
+  rw [memLpLoc_iff_memLp_isCompact]
+  intro s hs
   rcases p.trichotomy with (rfl | rfl | hp)
   · simp [h.aestronglyMeasurable]
-  · obtain ⟨C, hC⟩ := hs₂.isCompact_closure.exists_bound_of_continuousOn (f := u) (by fun_prop)
-    apply memLp_top_of_bound (by fun_prop) C (ae_restrict_of_forall_mem hs₁ ?_)
-    intro x hx
-    exact hC _ (subset_closure hx)
+  · obtain ⟨C, hC⟩ := hs.exists_bound_of_continuousOn (f := u) (by fun_prop)
+    exact memLp_top_of_bound (by fun_prop) C (ae_restrict_of_forall_mem hs.measurableSet hC)
   · rw [ENNReal.toReal_pos_iff] at hp
     rw [← MeasureTheory.integrable_norm_rpow_iff (by fun_prop) hp.1.ne' hp.2.ne,
       ← MeasureTheory.IntegrableOn]
-    apply ContinuousOn.integrableOn_of_subset_isCompact (K := closure s)
-    · apply Continuous.continuousOn
-      apply Continuous.rpow_const (by fun_prop)
-      intro; right; positivity
-    · apply hs₂.isCompact_closure
-    · exact hs₁
-    · exact subset_closure
-    · rw [← lt_top_iff_ne_top]
-      exact IsBounded.measure_lt_top hs₂
+    apply ContinuousOn.integrableOn_compact hs
+    apply Continuous.continuousOn
+    apply Continuous.rpow_const (by fun_prop)
+    intro; right; positivity
 
 end MetricSpace
 
-end MemLpLoc
-
-variable [Bornology α]
-
-variable (E p) in
-/-- The space of locally Lp functions
-
-Not clear whether the condition should be `eLpNorm (s.indicator f) p μ < ∞` instead. They are
-equivalent. -/
-def LpLoc (μ : Measure α := by volume_tac) : AddSubgroup (α →ₘ[μ] E) where
-  carrier := { f | ∀ s : Set α, Measurable s ∧ IsBounded s → eLpNorm f p (μ.restrict s) < ∞ }
-  zero_mem' := by
-    intro s ⟨hs₁, hs₂⟩
-    have : eLpNorm (0 : α → E) p (μ.restrict s) < ∞ := by simp
-    convert this using 1
-    apply eLpNorm_congr_ae
-    apply Filter.EventuallyEq.restrict
-    apply AEEqFun.coeFn_zero
-  add_mem' {f g} hf hg := by
-    intro s hs
-    convert eLpNorm_add_lt_top
-      ⟨f.aestronglyMeasurable.restrict, hf s hs⟩ ⟨g.aestronglyMeasurable.restrict, hg s hs⟩ using 1
-    apply eLpNorm_congr_ae
-    apply Filter.EventuallyEq.restrict
-    filter_upwards [AEEqFun.coeFn_add f g] with x h
-    simp [h]
-  neg_mem' {f} hf := by
-    intro s hs
-    convert hf s hs using 1
-    rw [← eLpNorm_neg]
-    apply eLpNorm_congr_ae
-    apply Filter.EventuallyEq.restrict
-    filter_upwards [AEEqFun.coeFn_neg f] with x h
-    simp [h]
 
+end MemLpLoc
 
 end MeasureTheory
diff --git a/DynamicalSystems/InputOutput/Causal.lean b/DynamicalSystems/InputOutput/Causal.lean
index fc0471a..1e61504 100644
--- a/DynamicalSystems/InputOutput/Causal.lean
+++ b/DynamicalSystems/InputOutput/Causal.lean
@@ -15,7 +15,7 @@ open MeasureTheory Filter Bornology Set
 open scoped NNReal ENNReal
 
 variable {ι α E F : Type*}
-  [MeasurableSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] [Bornology α]
+  [MeasurableSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] [PseudoMetricSpace α]
   {f g : (α → E) → α → F} {s : ι → Set α} {p : ℝ≥0∞} {μ : Measure α}
 
 namespace SetRel
diff --git a/DynamicalSystems/InputOutput/ClosedLoop.lean b/DynamicalSystems/InputOutput/ClosedLoop.lean
index be5f617..9aaac6a 100644
--- a/DynamicalSystems/InputOutput/ClosedLoop.lean
+++ b/DynamicalSystems/InputOutput/ClosedLoop.lean
@@ -48,9 +48,9 @@ variable [NormedAddCommGroup E] [NormedAddCommGroup F]
 variable (α E F) in
 /-- A closed loop defined via relations. -/
 structure SetRel.closedLoop where
-  /-- foo -/
+  /-- The first relation of a closed feedback connection -/
   topRel : SetRel (α → E) (α → F)
-  /-- bar -/
+  /-- The second relation of a closed feedback connection -/
   botRel : SetRel (α → F) (α → E)
 
 namespace SetRel.closedLoop
@@ -234,7 +234,10 @@ theorem isLpStable_inputState (h_topRel : loop.topRel.IsGraph) (h_botRel : loop.
 
 /- Todo: closed loop is causal -/
 
-variable [Bornology α]
+section IsCausal
+
+variable [PseudoMetricSpace α]
+
 variable {s : ι → Set α} {p : ℝ≥0∞}
 
 /-- Proposition 1.2.9 in van der Schaft -/
@@ -283,6 +286,12 @@ theorem isCausal_inputOutput (h_topRel : loop.topRel.IsGraph) (h_botRel : loop.b
     have hbot := h_botRel'.causal t
     sorry
 
+end IsCausal
+
+section IsFiniteGainStable
+
+variable {s : ι → Set α} {p : ℝ≥0∞}
+
 variable {k₁ k₂ β₁ β₂ : ℝ≥0}
 
 /-- The input-state loop gain of a `Lp` feedback system. -/
@@ -297,6 +306,8 @@ noncomputable def inputOutputLoopGainLp (p : ℝ≥0∞) (k₁ k₂ : ℝ≥0∞
 noncomputable def loopBias (k₁ k₂ β₁ β₂ : ℝ≥0) : ℝ≥0 :=
   (β₁ + β₂ + k₁ * β₂ + k₂ * β₁) / (1 - k₁ * k₂)
 
+variable [TopologicalSpace α]
+
 theorem smallGainThm_part1₁
     {G₁ : (α → E) → α → F} (hG₁ : G₁.graph = loop.topRel)
     {G₂ : (α → F) → α → E} (hG₂ : G₂.graph = loop.botRel)
@@ -304,7 +315,7 @@ theorem smallGainThm_part1₁
     {u₁ : α → E} {u₂ : α → F} {e₁ : α → E} {e₂ : α → F} (hu₂ : MemLpLoc u₂ p μ)
     (he₁ : MemLpLoc e₁ p μ)
     (h : (fun x ↦ (e₁ x, e₂ x), fun x ↦ (u₁ x, u₂ x)) ∈ loop.inputState) {t : ι}
-    (ht : MeasurableSet (s t) ∧ IsBounded (s t)) :
+    (ht : IsCompact (s t)) :
     eLpNorm u₁ p (μ.restrict (s t)) ≤
       eLpNorm e₁ p (μ.restrict (s t)) + k₂ * eLpNorm u₂ p (μ.restrict (s t)) + β₂ := by
   calc
@@ -312,8 +323,8 @@ theorem smallGainThm_part1₁
       rw [blubb₁ hG₁ hG₂ h]
     _ ≤ eLpNorm e₁ p (μ.restrict (s t)) + eLpNorm (G₂ u₂) p (μ.restrict (s t)) := by
       apply MeasureTheory.eLpNorm_sub_le
-      · apply (he₁ (s t) ht).aestronglyMeasurable
-      · apply (hG₂'.memLpLoc hu₂ (s t) ht).aestronglyMeasurable
+      · apply he₁.aestronglyMeasurable ht
+      · apply (hG₂'.memLpLoc hu₂).aestronglyMeasurable ht
       · exact hp
     _ ≤ _ := by
       rw [add_assoc]
@@ -327,7 +338,7 @@ theorem smallGainThm_part1₂
     {u₁ : α → E} {u₂ : α → F} {e₁ : α → E} {e₂ : α → F}
     (hu₁ : MemLpLoc u₁ p μ) (he₂ : MemLpLoc e₂ p μ)
     (h : (fun x ↦ (e₁ x, e₂ x), fun x ↦ (u₁ x, u₂ x)) ∈ loop.inputState) {t : ι}
-    (ht : MeasurableSet (s t) ∧ IsBounded (s t)) :
+    (ht : IsCompact (s t)) :
     eLpNorm u₂ p (μ.restrict (s t)) ≤
       eLpNorm e₂ p (μ.restrict (s t)) + k₁ * eLpNorm u₁ p (μ.restrict (s t)) + β₁ := by
   calc
@@ -335,8 +346,8 @@ theorem smallGainThm_part1₂
       rw [blubb₂ hG₁ hG₂ h]
     _ ≤ eLpNorm e₂ p (μ.restrict (s t)) + eLpNorm (G₁ u₁) p (μ.restrict (s t)) := by
       apply MeasureTheory.eLpNorm_add_le
-      · apply (he₂ (s t) ht).aestronglyMeasurable
-      · apply (hG₁'.memLpLoc hu₁ (s t) ht).aestronglyMeasurable
+      · apply he₂.aestronglyMeasurable ht
+      · apply (hG₁'.memLpLoc hu₁).aestronglyMeasurable ht
       · exact hp
     _ ≤ _ := by
       rw [add_assoc]
@@ -351,7 +362,7 @@ theorem smallGainThm_part2₁
     {u₁ : α → E} {u₂ : α → F} {e₁ : α → E} {e₂ : α → F}
     (hu₁ : MemLpLoc u₁ p μ) (hu₂ : MemLpLoc u₂ p μ) (he₁ : MemLpLoc e₁ p μ) (he₂ : MemLpLoc e₂ p μ)
     (h : (fun x ↦ (e₁ x, e₂ x), fun x ↦ (u₁ x, u₂ x)) ∈ loop.inputState) {t : ι}
-    (ht : MeasurableSet (s t) ∧ IsBounded (s t)) :
+    (ht : IsCompact (s t)) :
     eLpNorm u₁ p (μ.restrict (s t)) ≤
       (eLpNorm e₁ p (μ.restrict (s t)) + k₂ * eLpNorm e₂ p (μ.restrict (s t)) + β₂ + k₂ * β₁) /
       (1 - k₁ * k₂) := by
@@ -362,7 +373,7 @@ theorem smallGainThm_part2₁
     rw [ENNReal.coe_ne_zero]
     apply hk'.ne'
   simp only [ENNReal.coe_sub, ENNReal.coe_one, ENNReal.coe_mul]
-  rw [ENNReal.mul_sub (fun _ _ ↦ (hu₁ (s t) ht).eLpNorm_ne_top)]
+  rw [ENNReal.mul_sub (fun _ _ ↦ (hu₁.memLp_restrict_isCompact ht).eLpNorm_ne_top)]
   simp only [mul_one, tsub_le_iff_right]
   calc
     _ ≤ eLpNorm e₁ p (μ.restrict (s t)) + k₂ * eLpNorm u₂ p (μ.restrict (s t)) + β₂ := by
@@ -380,7 +391,7 @@ theorem smallGainThm_part2₂
     {u₁ : α → E} {u₂ : α → F} {e₁ : α → E} {e₂ : α → F}
     (hu₁ : MemLpLoc u₁ p μ) (hu₂ : MemLpLoc u₂ p μ) (he₁ : MemLpLoc e₁ p μ) (he₂ : MemLpLoc e₂ p μ)
     (h : (fun x ↦ (e₁ x, e₂ x), fun x ↦ (u₁ x, u₂ x)) ∈ loop.inputState) {t : ι}
-    (ht : MeasurableSet (s t) ∧ IsBounded (s t)) :
+    (ht : IsCompact (s t)) :
     eLpNorm u₂ p (μ.restrict (s t)) ≤
       (eLpNorm e₂ p (μ.restrict (s t)) + k₁ * eLpNorm e₁ p (μ.restrict (s t)) + β₁ + k₁ * β₂) /
       (1 - k₁ * k₂) := by
@@ -391,7 +402,7 @@ theorem smallGainThm_part2₂
     rw [ENNReal.coe_ne_zero]
     apply hk'.ne'
   simp only [ENNReal.coe_sub, ENNReal.coe_one, ENNReal.coe_mul]
-  rw [ENNReal.mul_sub (fun _ _ ↦ (hu₂ (s t) ht).eLpNorm_ne_top)]
+  rw [ENNReal.mul_sub (fun _ _ ↦ (hu₂.memLp_restrict_isCompact ht).eLpNorm_ne_top)]
   simp only [mul_one, tsub_le_iff_right]
   calc
     _ ≤ eLpNorm e₂ p (μ.restrict (s t)) + k₁ * eLpNorm u₁ p (μ.restrict (s t)) + β₁ := by
@@ -411,7 +422,7 @@ theorem inputStateLp_isFiniteGainStableWith [hp : Fact (1 ≤ p)]
     (hG₁' : G₁.IsFiniteGainStableWith k₁ β₁ s p μ)
     {G₂ : (α → F) → α → E} (hG₂ : G₂.graph = loop.botRel)
     (hG₂' : G₂.IsFiniteGainStableWith k₂ β₂ s p μ) (hk : k₁ * k₂ < 1)
-    (ht : ∀ t, MeasurableSet (s t) ∧ IsBounded (s t)) :
+    (ht : ∀ t, IsCompact (s t)) :
     (loop.inputStateLp p).IsFiniteGainStableWith (inputStateLoopGainLp p k₁ k₂).toNNReal
       (loopBias k₁ k₂ β₁ β₂) s p μ := by
   intro t e u he hu heu
@@ -426,7 +437,7 @@ theorem inputStateLp_isFiniteGainStableWith [hp : Fact (1 ≤ p)]
   have he₂ : MemLpLoc e₂ p μ := he.2
   calc
     _ ≤ eLpNorm u₁ p (μ.restrict (s t)) + eLpNorm u₂ p (μ.restrict (s t)) :=
-      eLpNorm_withLp_prod_le_add (hu₁ (s t) (ht t)).aestronglyMeasurable
+      eLpNorm_withLp_prod_le_add (hu₁.aestronglyMeasurable (ht t))
     _ ≤ ((eLpNorm e₁ p (μ.restrict (s t)) + k₂ * eLpNorm e₂ p (μ.restrict (s t)) + β₂ + k₂ * β₁) /
         (1 - k₁ * k₂)) +
         ((eLpNorm e₂ p (μ.restrict (s t)) + k₁ * eLpNorm e₁ p (μ.restrict (s t)) + β₁ + k₁ * β₂) /
@@ -450,7 +461,7 @@ theorem inputStateLp_isFiniteGainStableWith [hp : Fact (1 ≤ p)]
         (addLEConst p * eLpNorm e p (μ.restrict (s t))) +
         (β₁ + β₂ + k₁ * β₂ + k₂ * β₁) / (1 - k₁ * k₂) := by
       gcongr
-      exact add_le_eLpNorm_withLp_prod (he₁ (s t) (ht t)).aestronglyMeasurable
+      exact add_le_eLpNorm_withLp_prod (he₁.aestronglyMeasurable (ht t))
     _ = _ := by
       have hk' : 0 < 1 - k₁ * k₂ := by simp [hk]
       rw [← mul_assoc]
@@ -473,7 +484,7 @@ theorem smallGainThm_part1₁'
     {y₁ : α → F} {y₂ : α → E} {e₁ : α → E} {e₂ : α → F} (hy₂ : MemLpLoc y₂ p μ)
     (he₁ : MemLpLoc e₁ p μ)
     (h : (fun x ↦ (e₁ x, e₂ x), fun x ↦ (y₁ x, y₂ x)) ∈ loop.inputOutput) {t : ι}
-    (ht : MeasurableSet (s t) ∧ IsBounded (s t)) :
+    (ht : IsCompact (s t)) :
     eLpNorm y₁ p (μ.restrict (s t)) ≤
       k₁ * eLpNorm e₁ p (μ.restrict (s t)) + k₁ * eLpNorm y₂ p (μ.restrict (s t)) + β₁ := by
   calc
@@ -483,8 +494,8 @@ theorem smallGainThm_part1₁'
     _ ≤ k₁ * (eLpNorm e₁ p (μ.restrict (s t)) + eLpNorm y₂ p (μ.restrict (s t))) + β₁ := by
       gcongr
       apply MeasureTheory.eLpNorm_sub_le
-      · apply (he₁ (s t) ht).aestronglyMeasurable
-      · apply (hy₂ (s t) ht).aestronglyMeasurable
+      · apply he₁.aestronglyMeasurable ht
+      · apply hy₂.aestronglyMeasurable ht
       · exact hp
     _ = _ := by ring
 
@@ -497,7 +508,7 @@ theorem smallGainThm_part1₂'
     {y₁ : α → F} {y₂ : α → E} {e₁ : α → E} {e₂ : α → F} (hy₁ : MemLpLoc y₁ p μ)
     (he₂ : MemLpLoc e₂ p μ)
     (h : (fun x ↦ (e₁ x, e₂ x), fun x ↦ (y₁ x, y₂ x)) ∈ loop.inputOutput) {t : ι}
-    (ht : MeasurableSet (s t)) (ht' : IsBounded (s t)) :
+    (ht : IsCompact (s t)) :
     eLpNorm y₂ p (μ.restrict (s t)) ≤
       k₂ * eLpNorm e₂ p (μ.restrict (s t)) + k₂ * eLpNorm y₁ p (μ.restrict (s t)) + β₂ := by
   calc
@@ -517,17 +528,18 @@ theorem smallGainThm_part2₁'
     {y₁ : α → F} {y₂ : α → E} {e₁ : α → E} {e₂ : α → F}
     (hy₁ : MemLpLoc y₁ p μ) (hy₂ : MemLpLoc y₂ p μ) (he₁ : MemLpLoc e₁ p μ) (he₂ : MemLpLoc e₂ p μ)
     (h : (fun x ↦ (e₁ x, e₂ x), fun x ↦ (y₁ x, y₂ x)) ∈ loop.inputOutput) {t : ι}
-    (ht : MeasurableSet (s t) ∧ IsBounded (s t)) :
+    (ht : IsCompact (s t)) :
     (1 - k₁ * k₂) * eLpNorm y₁ p (μ.restrict (s t)) ≤
       k₁ * eLpNorm e₁ p (μ.restrict (s t)) + (k₁ * k₂) * eLpNorm e₂ p (μ.restrict (s t)) +
       k₁ * β₂ + β₁ := by
-  rw [ENNReal.sub_mul (fun _ _ ↦ (hy₁ (s t) ht).eLpNorm_ne_top), one_mul, tsub_le_iff_right]
+  rw [ENNReal.sub_mul (fun _ _ ↦ (hy₁.memLp_restrict_isCompact ht).eLpNorm_ne_top), one_mul,
+    tsub_le_iff_right]
   calc
     _ ≤ k₁ * eLpNorm e₁ p _ + k₁ * eLpNorm y₂ p _ + β₁ :=
       smallGainThm_part1₁' hG₁ hG₂ hG₁' hp hy₂ he₁ h ht
     _ ≤ k₁ * eLpNorm e₁ p _ + k₁ * (k₂ * eLpNorm e₂ p _ + k₂ * eLpNorm y₁ p _ + β₂) + β₁ := by
       gcongr
-      apply smallGainThm_part1₂' hG₁ hG₂ hG₂' hp hy₁ he₂ h ht.1 ht.2
+      apply smallGainThm_part1₂' hG₁ hG₂ hG₂' hp hy₁ he₂ h ht
     _ = _ := by ring
 
 theorem smallGainThm_part2₂'
@@ -538,14 +550,15 @@ theorem smallGainThm_part2₂'
     {y₁ : α → F} {y₂ : α → E} {e₁ : α → E} {e₂ : α → F}
     (hy₁ : MemLpLoc y₁ p μ) (hy₂ : MemLpLoc y₂ p μ) (he₁ : MemLpLoc e₁ p μ) (he₂ : MemLpLoc e₂ p μ)
     (h : (fun x ↦ (e₁ x, e₂ x), fun x ↦ (y₁ x, y₂ x)) ∈ loop.inputOutput) {t : ι}
-    (ht : MeasurableSet (s t) ∧ IsBounded (s t)) :
+    (ht : IsCompact (s t)) :
     (1 - k₁ * k₂) * eLpNorm y₂ p (μ.restrict (s t)) ≤
       k₂ * eLpNorm e₂ p (μ.restrict (s t)) + (k₁ * k₂) * eLpNorm e₁ p (μ.restrict (s t)) +
       k₂ * β₁ + β₂ := by
-  rw [ENNReal.sub_mul (fun _ _ ↦ (hy₂ (s t) ht).eLpNorm_ne_top), one_mul, tsub_le_iff_right]
+  rw [ENNReal.sub_mul (fun _ _ ↦ (hy₂.memLp_restrict_isCompact ht).eLpNorm_ne_top), one_mul,
+    tsub_le_iff_right]
   calc
     _ ≤ k₂ * eLpNorm e₂ p _ + k₂ * eLpNorm y₁ p _ + β₂ :=
-      smallGainThm_part1₂' hG₁ hG₂ hG₂' hp hy₁ he₂ h ht.1 ht.2
+      smallGainThm_part1₂' hG₁ hG₂ hG₂' hp hy₁ he₂ h ht
     _ ≤ k₂ * eLpNorm e₂ p _ + k₂ * (k₁ * eLpNorm e₁ p _ + k₁ * eLpNorm y₂ p _ + β₁) + β₂ := by
       gcongr
       apply smallGainThm_part1₁' hG₁ hG₂ hG₁' hp hy₂ he₁ h ht
@@ -561,7 +574,7 @@ theorem inputOutputLp_isFiniteGainStableWith [hp : Fact (1 ≤ p)]
     (hG₁' : G₁.IsFiniteGainStableWith k₁ β₁ s p μ)
     {G₂ : (α → F) → α → E} (hG₂ : G₂.graph = loop.botRel)
     (hG₂' : G₂.IsFiniteGainStableWith k₂ β₂ s p μ) (hk : k₁ * k₂ < 1)
-    (ht : ∀ t, MeasurableSet (s t) ∧ IsBounded (s t)) :
+    (ht : ∀ t, IsCompact (s t)) :
     (loop.inputOutputLp p).IsFiniteGainStableWith (inputOutputLoopGainLp p k₁ k₂).toNNReal
       (loopBias k₁ k₂ β₁ β₂) s p μ := by
   intro t e y he hy hey
@@ -588,7 +601,7 @@ theorem inputOutputLp_isFiniteGainStableWith [hp : Fact (1 ≤ p)]
   calc
     _ ≤ (eLpNorm y₁ p (μ.restrict (s t)) + eLpNorm y₂ p (μ.restrict (s t))) * (1 - k₁ * k₂) := by
       gcongr
-      · apply eLpNorm_withLp_prod_le_add (hy₁ (s t) (ht t)).aestronglyMeasurable
+      · apply eLpNorm_withLp_prod_le_add (hy₁.aestronglyMeasurable (ht t))
       · norm_cast
     _ = (1 - k₁ * k₂) * eLpNorm y₁ p _ + (1 - k₁ * k₂) * eLpNorm y₂ p _ := by ring
     _ ≤ (k₁ * eLpNorm e₁ p (μ.restrict (s t)) + (k₁ * k₂) * eLpNorm e₂ p (μ.restrict (s t)) +
@@ -615,11 +628,13 @@ theorem inputOutputLp_isFiniteGainStableWith [hp : Fact (1 ≤ p)]
       rw [mul_rotate, mul_assoc]
       gcongr 2
       · rw [mul_comm]
-        grw [add_le_eLpNorm_withLp_prod (he₁ (s t) (ht t)).aestronglyMeasurable]
+        grw [add_le_eLpNorm_withLp_prod (he₁.aestronglyMeasurable (ht t))]
         rfl
       · apply le_of_eq
         ring
 
+end IsFiniteGainStable
+
 end SetRel.closedLoop
 
 variable (f : α → E × F)
diff --git a/DynamicalSystems/InputOutput/Example.lean b/DynamicalSystems/InputOutput/Example.lean
index 4aef4d6..1253699 100644
--- a/DynamicalSystems/InputOutput/Example.lean
+++ b/DynamicalSystems/InputOutput/Example.lean
@@ -17,24 +17,32 @@ open scoped NNReal ENNReal
 variable {ι α 𝕜 E F : Type*}
 
 variable [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [MeasurableSpace α]
-  [Bornology α] {s : ι → Set α} {μ : Measure α}
+  [TopologicalSpace α] {s : ι → Set α} {μ : Measure α} {f : α → 𝕜}
 
 /-- The multiplication operator with an almost everywhere bounded function is `Lp` finite gain
 stable. -/
-theorem smul_isFiniteGainStableWith {f : α → 𝕜} (p : ℝ≥0∞) (hf : AEStronglyMeasurable f μ) {k : ℝ}
-    (h_bound : ∀ᵐ x ∂μ, ‖f x‖ ≤ k) :
-    (fun (u : α → E) (x : α) ↦ (f x) • (u x)).IsFiniteGainStableWith k.toNNReal 0 s p μ := by
+theorem smul_isFiniteGainStableWith' {k : ℝ≥0} (p : ℝ≥0∞) (hf : AEStronglyMeasurable f μ)
+    (h_bound : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ k) :
+    (fun (u : α → E) (x : α) ↦ (f x) • (u x)).IsFiniteGainStableWith k 0 s p μ := by
   constructor
-  · intro u hu s hs
-    apply (hu s hs).smul (p := ∞)
-    apply memLp_top_of_bound hf.restrict k
-    exact h_bound.filter_mono ae_restrict_le
+  · intro u hu x
+    filter_upwards [hu x] with s hu
+    exact hu.smul (memLp_top_of_bound hf.restrict k <| h_bound.filter_mono ae_restrict_le)
   · intro t u hu
     calc
       _ ≤ ENNReal.ofReal k * eLpNorm u p (μ.restrict (s t)) := by
         apply MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul
         filter_upwards [h_bound.filter_mono ae_restrict_le] with x hbdd
+        rw [NNReal.toReal_le ‖f x‖₊ k] at hbdd
+        simp only [coe_nnnorm] at hbdd
         grw [norm_smul, hbdd]
-      _ = _ := by
-        simp only [ENNReal.coe_zero, add_zero]
-        rfl
+      _ = _ := by simp
+
+/-- The multiplication operator with an almost everywhere bounded function is `Lp` finite gain
+stable. -/
+theorem smul_isFiniteGainStableWith {k : ℝ} (p : ℝ≥0∞) (hf : AEStronglyMeasurable f μ)
+    (h_bound : ∀ᵐ x ∂μ, ‖f x‖ ≤ k) :
+    (fun (u : α → E) (x : α) ↦ (f x) • (u x)).IsFiniteGainStableWith k.toNNReal 0 s p μ := by
+  apply smul_isFiniteGainStableWith' p hf
+  filter_upwards [h_bound] with s h
+  simpa [Real.le_toNNReal_iff_coe_le ((norm_nonneg _).trans h)]
diff --git a/DynamicalSystems/InputOutput/Stability.lean b/DynamicalSystems/InputOutput/Stability.lean
index 34a831b..fc44e7f 100644
--- a/DynamicalSystems/InputOutput/Stability.lean
+++ b/DynamicalSystems/InputOutput/Stability.lean
@@ -64,10 +64,10 @@ section IsFiniteGainStable
 
 /-! ## Finite gain stability -/
 
-variable [Bornology α]
-
 namespace SetRel
 
+variable [TopologicalSpace α]
+
 variable (f : SetRel (α → E) (α → E))
 
 /-- A map is called finite gain stable with gain less than `k` if there exists `β` such that
@@ -101,8 +101,8 @@ variable {k k' β β' : ℝ≥0} {s : ι → Set α} {p : ℝ≥0∞} {μ : Meas
 
 /-- A map is called finite gain stable with gain less than `k` if there exists `β` such that
 for all local `Lp` functions `u`, we have the `Lp`-norm estimate `‖(f u)ₜ‖ ≤ k * ‖uₜ‖ + β`. -/
-structure IsFiniteGainStableWith (f : (α → E) → α → F) (k β : ℝ≥0) (s : ι → Set α) (p : ℝ≥0∞)
-    (μ : Measure α) where
+structure IsFiniteGainStableWith [TopologicalSpace α] (f : (α → E) → α → F) (k β : ℝ≥0)
+    (s : ι → Set α) (p : ℝ≥0∞) (μ : Measure α) where
   /-- Every `u` in `Lp` gets mapped to `Lp`. -/
   memLpLoc : ∀ ⦃u⦄, MemLpLoc u p μ → MemLpLoc (f u) p μ
   /-- For every `u` in `LpLoc`, we have `‖yₜ‖ ≤ k * ‖(f u)ₜ‖ + β`. -/
@@ -111,6 +111,8 @@ structure IsFiniteGainStableWith (f : (α → E) → α → F) (k β : ℝ≥0)
 
 namespace IsFiniteGainStableWith
 
+variable [TopologicalSpace α]
+
 theorem graph (h : f.IsFiniteGainStableWith k β s p μ) :
     f.graph.IsFiniteGainStableWith k β s p μ := by
   intro t u y hu hy huy
@@ -132,15 +134,15 @@ theorem comp (hg : g.IsFiniteGainStableWith k' β' s p μ) (hf : f.IsFiniteGainS
 
 /-- The addition of two finite gain stable maps is finite gain stable. -/
 theorem add {f : (α → E) → α → F} {g : (α → E) → (α → F)} (hp : 1 ≤ p)
-    (hs : ∀ t, MeasurableSet (s t) ∧ IsBounded (s t))
+    (hs : ∀ t, IsCompact (s t))
     (hf : f.IsFiniteGainStableWith k β s p μ) (hg : g.IsFiniteGainStableWith k' β' s p μ) :
     (f + g).IsFiniteGainStableWith (k + k') (β + β') s p μ where
   memLpLoc u hu := (hf.memLpLoc hu).add (hg.memLpLoc hu)
   stableWith t u hu := calc
     _ ≤ eLpNorm (f u) p _ + eLpNorm (g u) p _ := by
       apply eLpNorm_add_le _ _ hp
-      · exact (hf.memLpLoc hu (s t) (hs t)).aestronglyMeasurable
-      · exact (hg.memLpLoc hu (s t) (hs t)).aestronglyMeasurable
+      · exact (hf.memLpLoc hu).aestronglyMeasurable (hs t)
+      · exact (hg.memLpLoc hu).aestronglyMeasurable (hs t)
     _ ≤ (k * eLpNorm u p _ + β) + (k' * eLpNorm u p _ + β') := by
       gcongr
       · exact hf.stableWith t u hu
@@ -150,15 +152,15 @@ theorem add {f : (α → E) → α → F} {g : (α → E) → (α → F)} (hp :
 
 /-- The subtraction of two finite gain stable maps is finite gain stable. -/
 theorem sub {f : (α → E) → α → F} {g : (α → E) → (α → F)} (hp : 1 ≤ p)
-    (hs : ∀ t, MeasurableSet (s t) ∧ IsBounded (s t))
+    (hs : ∀ t, IsCompact (s t))
     (hf : f.IsFiniteGainStableWith k β s p μ) (hg : g.IsFiniteGainStableWith k' β' s p μ) :
     (f - g).IsFiniteGainStableWith (k + k') (β + β') s p μ where
   memLpLoc u hu := (hf.memLpLoc hu).sub (hg.memLpLoc hu)
   stableWith t u hu := calc
     _ ≤ eLpNorm (f u) p _ + eLpNorm (g u) p _ := by
       apply eLpNorm_sub_le _ _ hp
-      · exact (hf.memLpLoc hu (s t) (hs t)).aestronglyMeasurable
-      · exact (hg.memLpLoc hu (s t) (hs t)).aestronglyMeasurable
+      · exact (hf.memLpLoc hu).aestronglyMeasurable (hs t)
+      · exact (hg.memLpLoc hu).aestronglyMeasurable (hs t)
     _ ≤ (k * eLpNorm u p _ + β) + (k' * eLpNorm u p _ + β') := by
       gcongr
       · exact hf.stableWith t u hu
@@ -193,12 +195,13 @@ theorem isLpStable (hf : IsFiniteGainStableWith f k β s p μ)
 
 end IsFiniteGainStableWith
 
+variable [PseudoMetricSpace α] [OpensMeasurableSpace α] [T2Space α] {k β : ℝ≥0}
+
 /-- Every system that is causal and satisfies the finite gain estimate is for `Lp` functions is
 finite gain stable.
 
 Proposition 1.2.3 in van der Schaft. -/
-theorem IsCausal.isFiniteGainStableWith (hf : IsCausal f s p μ) (k β : ℝ≥0)
-    (hs : ∀ t, MeasurableSet (s t) ∧ IsBounded (s t))
+theorem IsCausal.isFiniteGainStableWith (hf : IsCausal f s p μ) (hs : ∀ t, IsCompact (s t))
     (h : ∀ u (_hu : MemLp u p μ), eLpNorm (f u) p μ ≤ k * eLpNorm u p μ + β) :
     IsFiniteGainStableWith f k β s p μ := by
   constructor
@@ -207,16 +210,16 @@ theorem IsCausal.isFiniteGainStableWith (hf : IsCausal f s p μ) (k β : ℝ≥0
   · intro t u hu
     calc
       _ = eLpNorm ((s t).indicator (f u)) p μ :=
-        (eLpNorm_indicator_eq_eLpNorm_restrict (hs t).1).symm
+        (eLpNorm_indicator_eq_eLpNorm_restrict (hs t).measurableSet).symm
       _ = eLpNorm ((s t).indicator (f <| (s t).indicator u)) p μ := by
         rw [← hf.causal t u hu]
       _ ≤ eLpNorm (f <| (s t).indicator u) p μ :=
         eLpNorm_indicator_le (f ((s t).indicator u))
       _ ≤ ↑k * eLpNorm ((s t).indicator u) p μ + β := by
         apply h
-        exact hu.memLp_indicator (hs t).1 (hs t).2
+        exact hu.memLp_indicator (hs t)
       _ = _ := by
-        rw [eLpNorm_indicator_eq_eLpNorm_restrict (hs t).1]
+        rw [eLpNorm_indicator_eq_eLpNorm_restrict (hs t).measurableSet]
 
 /- Todo: define the gain -/