chore: use fun_prop, add missing lemmas

DynamicalSystems/Basic/LpLoc.lean

@@ -30,10 +30,7 @@ open Bornology
 
 section MemLpLoc
 
-/-! ## Local `Lp` functions
-In this section we define local `Lp` functions and prove elementary properties
-
--/
+attribute [fun_prop] MemLp MemLp.add MemLp.sub MemLp.neg
 
 /-- 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`. -/
@@ -45,6 +42,17 @@ section Bornology
 
 variable [Bornology α]
 
+variable {u v : α → E}
+
+@[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'⟩
+
+@[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_prod_iff {u : α → E × F} :
     MemLpLoc u p μ ↔ MemLpLoc (fun x ↦ (u x).1) p μ ∧ MemLpLoc (fun x ↦ (u x).2) p μ := by
   constructor
@@ -61,22 +69,20 @@ theorem memLpLoc_withLp_prod_iff {p : ℝ≥0∞} [Fact (1 ≤ p)] {u : α → W
   · intro ⟨h₁, h₂⟩ s hs
     exact MemLp.of_fst_of_snd_prodLp ⟨h₁ s hs, h₂ s hs⟩
 
-variable {u v : α → 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
-  exact (hu s hs).add (hv s hs)
+  intro s ⟨hs, hs'⟩
+  fun_prop
 
 @[to_fun (attr := fun_prop)]
 theorem MemLpLoc.sub (hu : MemLpLoc u p μ) (hv : MemLpLoc v p μ) : MemLpLoc (u - v) p μ := by
-  intro s hs
-  exact (hu s hs).sub (hv s hs)
+  intro s ⟨hs, hs'⟩
+  fun_prop
 
 @[to_fun (attr := fun_prop)]
 theorem MemLpLoc.neg (hu : MemLpLoc u p μ) : MemLpLoc (-u) p μ := by
-  intro s hs
-  exact (hu s hs).neg
+  intro s ⟨hs, hs'⟩
+  fun_prop
 
 @[to_fun (attr := fun_prop)]
 theorem memLpLoc_finsetSum {ι} (s₀ : Finset ι) {u : ι → α → E} (hu : ∀ i ∈ s₀, MemLpLoc (u i) p μ) :
@@ -131,16 +137,18 @@ variable [PseudoMetricSpace α] [ProperSpace α] [OpensMeasurableSpace α]
 variable {u : α → E}
 
 /-- Every continuous function is locally `Lp` -/
-theorem Continuous.memLpLoc (hp : p ≠ 0) (h : Continuous u) :
+@[fun_prop]
+theorem Continuous.memLpLoc (h : Continuous u) :
     MemLpLoc u p μ := by
   intro s ⟨hs₁, hs₂⟩
-  by_cases hp₂ : p = ∞
-  · rw [hp₂]
-    obtain ⟨C, hC⟩ := hs₂.isCompact_closure.exists_bound_of_continuousOn (f := u) (by fun_prop)
+  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)
-  · rw [← MeasureTheory.integrable_norm_rpow_iff (by fun_prop) hp hp₂,
+  · 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

DynamicalSystems/InputOutput/ClosedLoop.lean

@@ -488,14 +488,16 @@ theorem smallGainThm_part1₁'
       · exact hp
     _ = _ := by ring
 
+attribute [fun_prop] MeasureTheory.MemLp.aestronglyMeasurable
+
 theorem smallGainThm_part1₂'
     {G₁ : (α → E) → α → F} (hG₁ : G₁.graph = loop.topRel)
     {G₂ : (α → F) → α → E} (hG₂ : G₂.graph = loop.botRel)
     (hG₂' : G₂.IsFiniteGainStableWith k₂ β₂ s p μ) (hp : 1 ≤ p)
     {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 : MeasurableSet (s t)) (ht' : IsBounded (s t)) :
     eLpNorm y₂ p (μ.restrict (s t)) ≤
       k₂ * eLpNorm e₂ p (μ.restrict (s t)) + k₂ * eLpNorm y₁ p (μ.restrict (s t)) + β₂ := by
   calc
@@ -504,10 +506,7 @@ theorem smallGainThm_part1₂'
       apply hG₂'.stableWith _ _ (by fun_prop)
     _ ≤ k₂ * (eLpNorm e₂ p (μ.restrict (s t)) + eLpNorm y₁ p (μ.restrict (s t))) + β₂ := by
       gcongr
-      apply MeasureTheory.eLpNorm_add_le
-      · apply (he₂ (s t) ht).aestronglyMeasurable
-      · apply (hy₁ (s t) ht).aestronglyMeasurable
-      · exact hp
+      exact eLpNorm_add_le (by fun_prop) (by fun_prop) hp
     _ = _ := by ring
 
 theorem smallGainThm_part2₁'
@@ -528,7 +527,7 @@ theorem smallGainThm_part2₁'
       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
+      apply smallGainThm_part1₂' hG₁ hG₂ hG₂' hp hy₁ he₂ h ht.1 ht.2
     _ = _ := by ring
 
 theorem smallGainThm_part2₂'
@@ -546,7 +545,7 @@ theorem smallGainThm_part2₂'
   rw [ENNReal.sub_mul (fun _ _ ↦ (hy₂ (s t) 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
+      smallGainThm_part1₂' hG₁ hG₂ hG₂' hp hy₁ he₂ h ht.1 ht.2
     _ ≤ 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

DynamicalSystems/InputOutput/Stability.lean

@@ -130,6 +130,42 @@ theorem comp (hg : g.IsFiniteGainStableWith k' β' s p μ) (hf : f.IsFiniteGainS
     _ = _ := by
       push_cast; ring
 
+/-- 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))
+    (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
+    _ ≤ (k * eLpNorm u p _ + β) + (k' * eLpNorm u p _ + β') := by
+      gcongr
+      · exact hf.stableWith t u hu
+      · exact hg.stableWith t u hu
+    _ = _ := by
+      push_cast; ring
+
+/-- 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))
+    (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
+    _ ≤ (k * eLpNorm u p _ + β) + (k' * eLpNorm u p _ + β') := by
+      gcongr
+      · exact hf.stableWith t u hu
+      · exact hg.stableWith t u hu
+    _ = _ := by
+      push_cast; ring
+
 variable [Preorder ι] [Countable ι] [Nonempty ι] [IsDirectedOrder ι]
 
 /-- Every finite gain stable system is `Lp` stable. -/