diff --git a/DynamicalSystems/Basic/LpLoc.lean b/DynamicalSystems/Basic/LpLoc.lean
index f4941da..c1e1dbd 100644
--- a/DynamicalSystems/Basic/LpLoc.lean
+++ b/DynamicalSystems/Basic/LpLoc.lean
@@ -94,7 +94,7 @@ theorem MemLpLoc.const_smul (hu : MemLpLoc u p μ) : MemLpLoc (c • u) p μ :=
 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]
+  rw [memLp_indicator_iff_restrict hs.1.nullMeasurableSet]
 
 theorem MemLpLoc.memLp_indicator {s₀ : Set α} (hs₀ : MeasurableSet s₀) (hs₀' : IsBounded s₀)
     (hu : MemLpLoc u p μ) : MemLp (s₀.indicator u) p μ := by
@@ -105,7 +105,7 @@ theorem MemLpLoc.memLp_indicator {s₀ : Set α} (hs₀ : MeasurableSet s₀) (h
 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₀
+  exact (hu s hs).indicator hs₀.nullMeasurableSet
 
 @[fun_prop]
 theorem MemLp.memLpLoc (hu : MemLp u p μ) : MemLpLoc u p μ := by
@@ -174,8 +174,9 @@ def LpLoc (μ : Measure α := by volume_tac) : AddSubgroup (α →ₘ[μ] E) whe
     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
+    have hf' : MemLp f p (μ.restrict s) := hf s hs
+    have hg' : MemLp g p (μ.restrict s) := hg s hs
+    convert eLpNorm_add_lt_top hf' hg' using 1
     apply eLpNorm_congr_ae
     apply Filter.EventuallyEq.restrict
     filter_upwards [AEEqFun.coeFn_add f g] with x h
diff --git a/DynamicalSystems/Engineering/RLCCircuit.lean b/DynamicalSystems/Engineering/RLCCircuit.lean
index f9bf99f..f738b94 100644
--- a/DynamicalSystems/Engineering/RLCCircuit.lean
+++ b/DynamicalSystems/Engineering/RLCCircuit.lean
@@ -40,7 +40,7 @@ theorem integral_differentiableAt (hf : Continuous f) (a) :
 variable {μ : MeasureTheory.Measure ℝ} {a b : ℝ}
 
 -- should be in mathlib
-theorem integral_nonneg_of_Ioo [MeasureTheory.NoAtoms μ] (hab : a ≤ b)
+theorem integral_nonneg_of_Ioo [MeasureTheory.NullSingletonClass μ] (hab : a ≤ b)
     (hf : IntervalIntegrable f μ a b) (h : ∀ x ∈ Set.Ioo a b, 0 ≤ f x) :
     0 ≤ ∫ u in a..b, f u ∂μ := by
   convert intervalIntegral.integral_mono_on_of_le_Ioo hab _ hf h
diff --git a/DynamicalSystems/InputOutput/Stability.lean b/DynamicalSystems/InputOutput/Stability.lean
index 0f3bee3..76ba108 100644
--- a/DynamicalSystems/InputOutput/Stability.lean
+++ b/DynamicalSystems/InputOutput/Stability.lean
@@ -137,13 +137,13 @@ theorem isLpStable (hf : IsFiniteGainStableWith f k β s p μ)
     (hfu : ∀ u (_hu : MemLp u p μ), AEStronglyMeasurable (f u) μ)
     (hs : AECover μ atTop s) :
     IsLpStable f p μ := by
-  refine ⟨fun u hu ↦ ⟨hfu u hu, ?_⟩⟩
+  refine ⟨fun u hu ↦ ?_⟩
   /- For every `t ∈ I`, we have that `‖(f u)ₜ‖ ≤ k * ‖uₜ‖ + β ≤ k * ‖u‖ + β`-/
   have : ∀ᶠ t in atTop, eLpNorm ((s t).indicator (f u)) p μ ≤ k * eLpNorm u p μ + β := by
     filter_upwards with t
     calc
       _ = eLpNorm (f u)  p (μ.restrict (s t)) :=
-        eLpNorm_indicator_eq_eLpNorm_restrict (hs.measurableSet t)
+        eLpNorm_indicator_eq_eLpNorm_restrict (hs.measurableSet t).nullMeasurableSet
       _ ≤ k * eLpNorm u p (μ.restrict <| s t) + β := hf.stableWith t u hu.memLpLoc
       _ ≤ _ := by gcongr; exact Measure.restrict_le_self
   calc
@@ -151,6 +151,7 @@ theorem isLpStable (hf : IsFiniteGainStableWith f k β s p μ)
       apply MeasureTheory.Lp.eLpNorm_le_of_ae_tendsto this
       · intro t
         exact (hfu u hu).indicator (hs.measurableSet t)
+      · exact hfu u hu
       · apply hs.ae_tendsto_indicator
     _ < _ := by
       simp [MemLp.eLpNorm_lt_top hu, ENNReal.mul_lt_top_iff]
@@ -171,16 +172,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).1.nullMeasurableSet).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))
+        eLpNorm_indicator_le (f ((s t).indicator u)) (hs t).1.nullMeasurableSet
       _ ≤ ↑k * eLpNorm ((s t).indicator u) p μ + β := by
         apply h
         exact hu.memLp_indicator (hs t).1 (hs t).2
       _ = _ := by
-        rw [eLpNorm_indicator_eq_eLpNorm_restrict (hs t).1]
+        rw [eLpNorm_indicator_eq_eLpNorm_restrict (hs t).1.nullMeasurableSet]
 
 /- Todo: define the gain -/
 
diff --git a/DynamicalSystems/Mathlib/Dynamics/Basic.lean b/DynamicalSystems/Mathlib/Dynamics/Basic.lean
index e248840..63420e9 100644
--- a/DynamicalSystems/Mathlib/Dynamics/Basic.lean
+++ b/DynamicalSystems/Mathlib/Dynamics/Basic.lean
@@ -50,23 +50,6 @@ example : f ^ 0 = Equiv.refl _ := by
   simp only [pow_zero]
   exact Equiv.Perm.one_def
 
-namespace Homeomorph
-
-variable [TopologicalSpace α] (f : Homeomorph α α)
-
-/-- The discrete flow `ℤ → α → α` induced by a homeomorphism `f : α → α`. -/
-def flow (f : Homeomorph α α) : Flow ℤ α where
-  toFun n x := (f ^ n) x
-  cont' := by
-    rw [continuous_prod_of_discrete_left]
-    intro n
-    simp only [Function.uncurry_apply_pair]
-    fun_prop
-  map_add' n₁ n₂ := by
-    simp_rw [← mul_apply, ← Homeomorph.ext_iff, zpow_add]
-  map_zero' x := by simp
-
-end Homeomorph
 
 end Discrete