From f6ed34b02a20f6d490e278bbffd7d2d620632ed7 Mon Sep 17 00:00:00 2001 From: Moritz Doll Date: Thu, 25 Jun 2026 15:17:49 +1000 Subject: [PATCH] minor chores --- DynamicalSystems/Basic/LpLoc.lean | 42 ++++++++++++-------- DynamicalSystems/InputOutput/ClosedLoop.lean | 13 +++--- DynamicalSystems/InputOutput/Stability.lean | 36 +++++++++++++++++ 3 files changed, 67 insertions(+), 24 deletions(-) diff --git a/DynamicalSystems/Basic/LpLoc.lean b/DynamicalSystems/Basic/LpLoc.lean index f4941da..54e34f2 100644 --- a/DynamicalSystems/Basic/LpLoc.lean +++ b/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 diff --git a/DynamicalSystems/InputOutput/ClosedLoop.lean b/DynamicalSystems/InputOutput/ClosedLoop.lean index e808002..be5f617 100644 --- a/DynamicalSystems/InputOutput/ClosedLoop.lean +++ b/DynamicalSystems/InputOutput/ClosedLoop.lean @@ -488,6 +488,8 @@ 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) @@ -495,7 +497,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 : 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 diff --git a/DynamicalSystems/InputOutput/Stability.lean b/DynamicalSystems/InputOutput/Stability.lean index 0f3bee3..34a831b 100644 --- a/DynamicalSystems/InputOutput/Stability.lean +++ b/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. -/