From 2b9775890d759e1ae98e9bf0f0043b7ab6027725 Mon Sep 17 00:00:00 2001 From: Moritz Doll Date: Tue, 15 Sep 2026 14:48:44 +1000 Subject: [PATCH] fix build --- DynamicalSystems/Basic/LpLoc.lean | 24 ++++----- DynamicalSystems/Basic/WithLp.lean | 33 ++++++++---- DynamicalSystems/InputOutput/ClosedLoop.lean | 56 +++++++++----------- DynamicalSystems/InputOutput/Example.lean | 9 ++-- DynamicalSystems/InputOutput/ProdLp.lean | 13 +++-- DynamicalSystems/InputOutput/Stability.lean | 25 +++------ DynamicalSystems/Stability/Basic.lean | 3 +- DynamicalSystems/Stability/Hamiltonian.lean | 13 +++-- lake-manifest.json | 8 +-- lakefile.toml | 2 +- 10 files changed, 96 insertions(+), 90 deletions(-) diff --git a/DynamicalSystems/Basic/LpLoc.lean b/DynamicalSystems/Basic/LpLoc.lean index 5cdba46..b477870 100644 --- a/DynamicalSystems/Basic/LpLoc.lean +++ b/DynamicalSystems/Basic/LpLoc.lean @@ -31,14 +31,15 @@ section eLpNorm @[simp] theorem lpAddConst_top : ∞.LpAddConst = 1 := rfl -variable [ENorm ε] +variable [ENorm ε] [TopologicalSpace ε] [TopologicalSpace.PseudoMetrizableSpace ε] /-- Addition of measures -/ -theorem eLpNorm_add_measure {f : α → ε} : +theorem eLpNorm_add_measure {f : α → ε} (hμ : AEStronglyMeasurable f μ) + (hν : AEStronglyMeasurable 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] + · simp [hμ, hν] + · simp only [eLpNorm_exponent_top, hμ, hν, hμ.add_measure hν] refine eLpNormEssSup_le_of_ae_enorm_bound ?_ simp only [ae_add_measure_iff] constructor @@ -53,8 +54,9 @@ theorem eLpNorm_add_measure {f : α → ε} : 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] + simp_rw [eLpNorm_eq_eLpNorm' hp.1.ne' hp.2.ne hμ, eLpNorm_eq_eLpNorm' hp.1.ne' hp.2.ne hν, + eLpNorm_eq_eLpNorm' hp.1.ne' hp.2.ne (hμ.add_measure hν), + eLpNorm'_eq_lintegral_enorm, one_div, lintegral_add_measure] apply ENNReal.rpow_add_le_mul_rpow_add_rpow'' end eLpNorm @@ -66,12 +68,10 @@ attribute [fun_prop] MemLp MemLp.add MemLp.sub MemLp.neg MemLp.aestronglyMeasura variable [TopologicalSpace ε] [TopologicalSpace.PseudoMetrizableSpace ε] [ENorm ε] theorem add_measure {f : α → ε} (hμ : MemLp f p μ) (hν : MemLp f p ν) : MemLp f p (μ + ν) := by - constructor - · rw [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⟩⟩ + rw [memLp_iff] + grw [eLpNorm_add_measure hμ.aestronglyMeasurable hν.aestronglyMeasurable] + rw [ENNReal.mul_lt_top_iff, ENNReal.add_lt_top] + exact Or.inl ⟨p.LpAddConst_lt_top, ⟨hμ, hν⟩⟩ end MemLp diff --git a/DynamicalSystems/Basic/WithLp.lean b/DynamicalSystems/Basic/WithLp.lean index 75d8b25..39a54f7 100644 --- a/DynamicalSystems/Basic/WithLp.lean +++ b/DynamicalSystems/Basic/WithLp.lean @@ -63,12 +63,16 @@ namespace MeasureTheory variable {f : α → E} {g : α → F} -theorem eLpNorm_withLp_prod [hp : Fact (1 ≤ p)] (hp' : p ≠ ∞) (hf : AEStronglyMeasurable f μ) : +theorem eLpNorm_withLp_prod [hp : Fact (1 ≤ p)] (hp' : p ≠ ∞) (hf : AEStronglyMeasurable f μ) + (hg : AEStronglyMeasurable g μ) : (eLpNorm (fun x ↦ WithLp.toLp p (f x, g x)) p μ) ^ p.toReal = (eLpNorm f p μ) ^ p.toReal + (eLpNorm g p μ) ^ p.toReal := by + have hfg : AEStronglyMeasurable (fun x ↦ WithLp.toLp p (f x, g x)) μ := by fun_prop have hp'' : 0 < p.toReal := (ENNReal.toReal_pos_iff_ne_top p).mpr hp' have hp''' : p ≠ 0 := (lt_of_lt_of_le zero_lt_one hp.out).ne' - simp_rw [MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal hp''' hp'] + simp_rw [MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal hp''' hp' hf] + simp_rw [MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal hp''' hp' hg] + simp_rw [MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal hp''' hp' hfg] simp_rw [← ENNReal.rpow_mul] simp_rw [one_div_mul_cancel hp''.ne'] simp only [ENNReal.rpow_one] @@ -83,12 +87,16 @@ theorem eLpNorm_withLp_prod [hp : Fact (1 ≤ p)] (hp' : p ≠ ∞) (hf : AEStro rw [← Real.rpow_mul (by positivity), one_div_mul_cancel hp''.ne'] simp -theorem eLpNorm_withLp_prod' [hp : Fact (1 ≤ p)] (hp' : p ≠ ∞) (hf : AEStronglyMeasurable f μ) : +theorem eLpNorm_withLp_prod' [hp : Fact (1 ≤ p)] (hp' : p ≠ ∞) (hf : AEStronglyMeasurable f μ) + (hg : AEStronglyMeasurable g μ) : eLpNorm (fun x ↦ WithLp.toLp p (f x, g x)) p μ = ((eLpNorm f p μ) ^ p.toReal + (eLpNorm g p μ) ^ p.toReal) ^ (1 / p.toReal) := by + have hfg : AEStronglyMeasurable (fun x ↦ WithLp.toLp p (f x, g x)) μ := by fun_prop have hp'' : 0 < p.toReal := (ENNReal.toReal_pos_iff_ne_top p).mpr hp' have hp''' : p ≠ 0 := (lt_of_lt_of_le zero_lt_one hp.out).ne' - simp_rw [MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal hp''' hp'] + simp_rw [MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal hp''' hp' hf] + simp_rw [MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal hp''' hp' hg] + simp_rw [MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal hp''' hp' hfg] simp_rw [← ENNReal.rpow_mul] simp_rw [one_div_mul_cancel hp''.ne'] simp only [ENNReal.rpow_one] @@ -104,17 +112,19 @@ theorem eLpNorm_withLp_prod' [hp : Fact (1 ≤ p)] (hp' : p ≠ ∞) (hf : AEStr rw [← Real.rpow_mul (by positivity), one_div_mul_cancel hp''.ne'] simp -theorem eLpNorm_withLp_prod_le_add [hp : Fact (1 ≤ p)] (hf : AEStronglyMeasurable f μ) : +theorem eLpNorm_withLp_prod_le_add [hp : Fact (1 ≤ p)] (hf : AEStronglyMeasurable f μ) + (hg : AEStronglyMeasurable g μ) : eLpNorm (fun x ↦ WithLp.toLp p (f x, g x)) p μ ≤ eLpNorm f p μ + eLpNorm g p μ := by by_cases! hp' : p ≠ ∞ · calc _ = ((eLpNorm f p μ) ^ p.toReal + (eLpNorm g p μ) ^ p.toReal) ^ (1 / p.toReal) := - eLpNorm_withLp_prod' hp' hf + eLpNorm_withLp_prod' hp' hf hg _ ≤ _ := by apply ENNReal.rpow_add_rpow_le_add simp [← ENNReal.ofReal_le_iff_le_toReal hp', hp.out] · unfold eLpNorm - simp only [hp', ENNReal.top_ne_zero, ↓reduceIte] + have hfg : AEStronglyMeasurable (fun x ↦ WithLp.toLp p (f x, g x)) μ := by fun_prop + simp only [hp', ENNReal.top_ne_zero, ↓reduceIte, hf, hg, hfg] apply MeasureTheory.eLpNormEssSup_le_of_ae_enorm_bound simp only [← WithLp.ennnorm_copy hp', WithLp.copy_toLp, WithLp.prod_enorm_eq_sup, WithLp.toLp_fst, WithLp.toLp_snd, sup_le_iff, eventually_and] @@ -147,7 +157,8 @@ theorem addLEConst_ne_top {p : ℝ≥0∞} : addLEConst p ≠ ∞ := by · simp [addLEConst_of_ne hp] · simp [hp] -theorem add_le_eLpNorm_withLp_prod [hp : Fact (1 ≤ p)] (hf : AEStronglyMeasurable f μ) : +theorem add_le_eLpNorm_withLp_prod [hp : Fact (1 ≤ p)] (hf : AEStronglyMeasurable f μ) + (hg : AEStronglyMeasurable g μ) : eLpNorm f p μ + eLpNorm g p μ ≤ addLEConst p * eLpNorm (fun x ↦ WithLp.toLp p (f x, g x)) p μ := by by_cases! hp' : p ≠ ∞ @@ -164,13 +175,15 @@ theorem add_le_eLpNorm_withLp_prod [hp : Fact (1 ≤ p)] (hf : AEStronglyMeasura simp [← ENNReal.ofReal_le_iff_le_toReal hp', hp.out] _ = ((2 : ℝ≥0∞) ^ (p.toReal - 1) * (eLpNorm (fun x ↦ WithLp.toLp p (f x, g x)) p μ) ^ p.toReal) ^ (1 / p.toReal) := by - rw [← eLpNorm_withLp_prod hp' hf] + rw [← eLpNorm_withLp_prod hp' hf hg] _ = _ := by have hp'' : 0 < p.toReal := (ENNReal.toReal_pos_iff_ne_top p).mpr hp' rw [ENNReal.mul_rpow_of_nonneg _ _ (by simp), ← ENNReal.rpow_mul, ← ENNReal.rpow_mul, mul_one_div_cancel hp''.ne', mul_one_div] simp [addLEConst_of_ne hp'] - · simp only [hp', eLpNorm_exponent_top, addLEConst_infty, two_mul] + · have hfg : AEStronglyMeasurable (fun x ↦ WithLp.toLp p (f x, g x)) μ := by fun_prop + simp only [hp', eLpNorm_exponent_top hf, eLpNorm_exponent_top hg, eLpNorm_exponent_top hfg, + addLEConst_infty, two_mul] gcongr · apply eLpNormEssSup_mono_enorm_ae' filter_upwards with x diff --git a/DynamicalSystems/InputOutput/ClosedLoop.lean b/DynamicalSystems/InputOutput/ClosedLoop.lean index 8333c5b..b0852b5 100644 --- a/DynamicalSystems/InputOutput/ClosedLoop.lean +++ b/DynamicalSystems/InputOutput/ClosedLoop.lean @@ -406,9 +406,7 @@ theorem smallGainThm_part1₁ {G₂ : (α → F) → α → E} (hG₂ : G₂.graph = loop.botRel) (hG₂' : G₂.IsFiniteGainStableWith k₂ β₂ s p μ) (hp : 1 ≤ p) {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 : IsCompact (s t)) : + (h : (fun x ↦ (e₁ x, e₂ x), fun x ↦ (u₁ x, u₂ x)) ∈ loop.inputState) {t : ι} : eLpNorm u₁ p (μ.restrict (s t)) ≤ eLpNorm e₁ p (μ.restrict (s t)) + k₂ * eLpNorm u₂ p (μ.restrict (s t)) + β₂ := by calc @@ -416,7 +414,7 @@ theorem smallGainThm_part1₁ rw [eq_fst_of_mem_inputState hG₁ hG₂ h] _ ≤ eLpNorm e₁ p (μ.restrict (s t)) + eLpNorm (G₂ u₂) p (μ.restrict (s t)) := by have : MemLpLoc (G₂ u₂) p μ := hG₂'.memLpLoc hu₂ - exact MeasureTheory.eLpNorm_sub_le (by fun_prop) (by fun_prop) hp + exact MeasureTheory.eLpNorm_sub_le hp _ ≤ _ := by rw [add_assoc] gcongr @@ -427,9 +425,8 @@ theorem smallGainThm_part1₂ (hG₁' : G₁.IsFiniteGainStableWith k₁ β₁ s p μ) {G₂ : (α → F) → α → E} (hG₂ : G₂.graph = loop.botRel) (hp : 1 ≤ p) {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 : IsCompact (s t)) : + (hu₁ : MemLpLoc u₁ p μ) + (h : (fun x ↦ (e₁ x, e₂ x), fun x ↦ (u₁ x, u₂ x)) ∈ loop.inputState) {t : ι} : eLpNorm u₂ p (μ.restrict (s t)) ≤ eLpNorm e₂ p (μ.restrict (s t)) + k₁ * eLpNorm u₁ p (μ.restrict (s t)) + β₁ := by calc @@ -437,7 +434,7 @@ theorem smallGainThm_part1₂ rw [eq_snd_of_mem_inputState hG₁ hG₂ h] _ ≤ eLpNorm e₂ p (μ.restrict (s t)) + eLpNorm (G₁ u₁) p (μ.restrict (s t)) := by have : MemLpLoc (G₁ u₁) p μ := hG₁'.memLpLoc hu₁ - exact MeasureTheory.eLpNorm_add_le (by fun_prop) (by fun_prop) hp + exact MeasureTheory.eLpNorm_add_le hp _ ≤ _ := by rw [add_assoc] gcongr @@ -449,7 +446,7 @@ theorem smallGainThm_part2₁ {G₂ : (α → F) → α → E} (hG₂ : G₂.graph = loop.botRel) (hG₂' : G₂.IsFiniteGainStableWith k₂ β₂ s p μ) (hp : 1 ≤ p) (hk : k₁ * k₂ < 1) {u₁ : α → E} {u₂ : α → F} {e₁ : α → E} {e₂ : α → F} - (hu₁ : MemLpLoc u₁ p μ) (hu₂ : MemLpLoc u₂ p μ) (he₁ : MemLpLoc e₁ p μ) (he₂ : MemLpLoc e₂ p μ) + (hu₁ : MemLpLoc u₁ p μ) (hu₂ : MemLpLoc u₂ p μ) (h : (fun x ↦ (e₁ x, e₂ x), fun x ↦ (u₁ x, u₂ x)) ∈ loop.inputState) {t : ι} (ht : IsCompact (s t)) : eLpNorm u₁ p (μ.restrict (s t)) ≤ @@ -466,9 +463,9 @@ theorem smallGainThm_part2₁ simp only [mul_one, tsub_le_iff_right] calc _ ≤ eLpNorm e₁ p (μ.restrict (s t)) + k₂ * eLpNorm u₂ p (μ.restrict (s t)) + β₂ := by - exact smallGainThm_part1₁ hG₁ hG₂ hG₂' hp hu₂ he₁ h ht + exact smallGainThm_part1₁ hG₁ hG₂ hG₂' hp hu₂ h _ ≤ _ := by - grw [smallGainThm_part1₂ hG₁ hG₁' hG₂ hp hu₁ he₂ h ht] + grw [smallGainThm_part1₂ hG₁ hG₁' hG₂ hp hu₁ h] ring_nf gcongr @@ -478,7 +475,7 @@ theorem smallGainThm_part2₂ {G₂ : (α → F) → α → E} (hG₂ : G₂.graph = loop.botRel) (hG₂' : G₂.IsFiniteGainStableWith k₂ β₂ s p μ) (hp : 1 ≤ p) (hk : k₁ * k₂ < 1) {u₁ : α → E} {u₂ : α → F} {e₁ : α → E} {e₂ : α → F} - (hu₁ : MemLpLoc u₁ p μ) (hu₂ : MemLpLoc u₂ p μ) (he₁ : MemLpLoc e₁ p μ) (he₂ : MemLpLoc e₂ p μ) + (hu₁ : MemLpLoc u₁ p μ) (hu₂ : MemLpLoc u₂ p μ) (h : (fun x ↦ (e₁ x, e₂ x), fun x ↦ (u₁ x, u₂ x)) ∈ loop.inputState) {t : ι} (ht : IsCompact (s t)) : eLpNorm u₂ p (μ.restrict (s t)) ≤ @@ -495,9 +492,9 @@ theorem smallGainThm_part2₂ simp only [mul_one, tsub_le_iff_right] calc _ ≤ eLpNorm e₂ p (μ.restrict (s t)) + k₁ * eLpNorm u₁ p (μ.restrict (s t)) + β₁ := by - exact smallGainThm_part1₂ hG₁ hG₁' hG₂ hp hu₁ he₂ h ht + exact smallGainThm_part1₂ hG₁ hG₁' hG₂ hp hu₁ h _ ≤ _ := by - grw [smallGainThm_part1₁ hG₁ hG₂ hG₂' hp hu₂ he₁ h ht] + grw [smallGainThm_part1₁ hG₁ hG₂ hG₂' hp hu₂ h] ring_nf gcongr @@ -526,14 +523,14 @@ 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₁.aestronglyMeasurable (ht t)) + eLpNorm_withLp_prod_le_add (hu₁.aestronglyMeasurable (ht t)) (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₁ * β₂) / (1 - k₁ * k₂)) := by gcongr - · apply smallGainThm_part2₁ hG₁ hG₁' hG₂ hG₂' hp.out hk hu₁ hu₂ he₁ he₂ heu (ht t) - · apply smallGainThm_part2₂ hG₁ hG₁' hG₂ hG₂' hp.out hk hu₁ hu₂ he₁ he₂ heu (ht t) + · apply smallGainThm_part2₁ hG₁ hG₁' hG₂ hG₂' hp.out hk hu₁ hu₂ heu (ht t) + · apply smallGainThm_part2₂ hG₁ hG₁' hG₂ hG₂' hp.out hk hu₁ hu₂ heu (ht t) _ = ((1 + k₁) * eLpNorm e₁ p (μ.restrict (s t)) + (1 + k₂) * eLpNorm e₂ p (μ.restrict (s t)) + (β₁ + β₂ + k₁ * β₂ + k₂ * β₁)) / (1 - k₁ * k₂) := by @@ -551,6 +548,7 @@ theorem inputStateLp_isFiniteGainStableWith [hp : Fact (1 ≤ p)] (β₁ + β₂ + k₁ * β₂ + k₂ * β₁) / (1 - k₁ * k₂) := by gcongr exact add_le_eLpNorm_withLp_prod (he₁.aestronglyMeasurable (ht t)) + (he₂.aestronglyMeasurable (ht t)) _ = _ := by have hk' : 0 < 1 - k₁ * k₂ := by simp [hk] rw [← mul_assoc] @@ -572,8 +570,7 @@ theorem smallGainThm_part1₁' (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 : IsCompact (s t)) : + (h : (fun x ↦ (e₁ x, e₂ x), fun x ↦ (y₁ x, y₂ x)) ∈ loop.inputOutput) {t : ι} : eLpNorm y₁ p (μ.restrict (s t)) ≤ k₁ * eLpNorm e₁ p (μ.restrict (s t)) + k₁ * eLpNorm y₂ p (μ.restrict (s t)) + β₁ := by calc @@ -583,9 +580,7 @@ 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₁.aestronglyMeasurable ht - · apply hy₂.aestronglyMeasurable ht - · exact hp + exact hp _ = _ := by ring attribute [fun_prop] MeasureTheory.MemLp.aestronglyMeasurable @@ -596,8 +591,7 @@ theorem smallGainThm_part1₂' (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 : IsCompact (s t)) : + (h : (fun x ↦ (e₁ x, e₂ x), fun x ↦ (y₁ x, y₂ x)) ∈ loop.inputOutput) {t : ι} : eLpNorm y₂ p (μ.restrict (s t)) ≤ k₂ * eLpNorm e₂ p (μ.restrict (s t)) + k₂ * eLpNorm y₁ p (μ.restrict (s t)) + β₂ := by calc @@ -606,7 +600,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 - exact eLpNorm_add_le (by fun_prop) (by fun_prop) hp + exact eLpNorm_add_le hp _ = _ := by ring theorem smallGainThm_part2₁' @@ -625,10 +619,10 @@ theorem smallGainThm_part2₁' 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 _ ≤ 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 _ = _ := by ring theorem smallGainThm_part2₂' @@ -647,10 +641,10 @@ theorem smallGainThm_part2₂' 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 _ ≤ 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 _ = _ := by ring /-- The *small-gain theorem* states that if two maps `G₁` and `G₂` are finite gain stable with @@ -691,6 +685,7 @@ theorem inputOutputLp_isFiniteGainStableWith [hp : Fact (1 ≤ p)] _ ≤ (eLpNorm y₁ p (μ.restrict (s t)) + eLpNorm y₂ p (μ.restrict (s t))) * (1 - k₁ * k₂) := by gcongr · apply eLpNorm_withLp_prod_le_add (hy₁.aestronglyMeasurable (ht t)) + (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)) + @@ -717,7 +712,8 @@ theorem inputOutputLp_isFiniteGainStableWith [hp : Fact (1 ≤ p)] rw [mul_rotate, mul_assoc] gcongr 2 · rw [mul_comm] - grw [add_le_eLpNorm_withLp_prod (he₁.aestronglyMeasurable (ht t))] + grw [add_le_eLpNorm_withLp_prod (he₁.aestronglyMeasurable (ht t)) + (he₂.aestronglyMeasurable (ht t))] rfl · apply le_of_eq ring diff --git a/DynamicalSystems/InputOutput/Example.lean b/DynamicalSystems/InputOutput/Example.lean index 1253699..8a00337 100644 --- a/DynamicalSystems/InputOutput/Example.lean +++ b/DynamicalSystems/InputOutput/Example.lean @@ -22,16 +22,17 @@ variable [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [Measura /-- The multiplication operator with an almost everywhere bounded function is `Lp` finite gain stable. -/ theorem smul_isFiniteGainStableWith' {k : ℝ≥0} (p : ℝ≥0∞) (hf : AEStronglyMeasurable f μ) - (h_bound : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ k) : + (hs : ∀ t, IsCompact (s t)) (h_bound : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ k) : (fun (u : α → E) (x : α) ↦ (f x) • (u x)).IsFiniteGainStableWith k 0 s p μ := by constructor · 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) + exact (memLp_top_of_bound hf.restrict k <| h_bound.filter_mono ae_restrict_le).smul hu · 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 + · exact hf.restrict.smul (hu.aestronglyMeasurable <| hs t) 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 @@ -41,8 +42,8 @@ theorem smul_isFiniteGainStableWith' {k : ℝ≥0} (p : ℝ≥0∞) (hf : AEStro /-- 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) : + (hs : ∀ t, IsCompact (s t)) (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 + apply smul_isFiniteGainStableWith' p hf hs filter_upwards [h_bound] with s h simpa [Real.le_toNNReal_iff_coe_le ((norm_nonneg _).trans h)] diff --git a/DynamicalSystems/InputOutput/ProdLp.lean b/DynamicalSystems/InputOutput/ProdLp.lean index 3f5fe88..1642b5a 100644 --- a/DynamicalSystems/InputOutput/ProdLp.lean +++ b/DynamicalSystems/InputOutput/ProdLp.lean @@ -77,8 +77,12 @@ theorem isFiniteGainStableWith_mapProdLp [Fact (1 ≤ p)] calc _ ≤ eLpNorm (f₁ (WithLp.fst ∘ u)) p _ + eLpNorm (f₂ (WithLp.snd ∘ u)) p _ := by apply eLpNorm_withLp_prod_le_add - rw [memLpLoc_withLp_prod_iff] at hu - exact (hf₁.memLpLoc hu.1).aestronglyMeasurable (hs t) + · rw [memLpLoc_withLp_prod_iff] at hu + exact (hf₁.memLpLoc hu.1).aestronglyMeasurable (hs t) + · apply MemLpLoc.aestronglyMeasurable (p := p) (hs t) + apply hf₂.memLpLoc + rw [memLpLoc_withLp_prod_iff] at hu + exact hu.2 _ ≤ (k₁ * eLpNorm (WithLp.fst ∘ u) p _ + β₁) + (k₂ * eLpNorm (WithLp.snd ∘ u) p _ + β₂) := by rw [memLpLoc_withLp_prod_iff] at hu gcongr @@ -102,5 +106,8 @@ theorem isFiniteGainStableWith_mapProdLp [Fact (1 ≤ p)] nth_rw 3 [this] gcongr apply add_le_eLpNorm_withLp_prod + · rw [memLpLoc_withLp_prod_iff] at hu + exact hu.1.aestronglyMeasurable (hs t) + apply MemLpLoc.aestronglyMeasurable (p := p) (hs t) rw [memLpLoc_withLp_prod_iff] at hu - exact hu.1.aestronglyMeasurable (hs t) + exact hu.2 diff --git a/DynamicalSystems/InputOutput/Stability.lean b/DynamicalSystems/InputOutput/Stability.lean index 0eff6be..fd2cb14 100644 --- a/DynamicalSystems/InputOutput/Stability.lean +++ b/DynamicalSystems/InputOutput/Stability.lean @@ -166,15 +166,11 @@ theorem comp_setRel_graph {f : SetRel (α → E) (α → F)} (hg : g.IsFiniteGai /-- 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, 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).aestronglyMeasurable (hs t) - · exact (hg.memLpLoc hu).aestronglyMeasurable (hs t) + _ ≤ eLpNorm (f u) p _ + eLpNorm (g u) p _ := eLpNorm_add_le hp _ ≤ (k * eLpNorm u p _ + β) + (k' * eLpNorm u p _ + β') := by gcongr · exact hf.stableWith t u hu @@ -184,15 +180,11 @@ 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, 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).aestronglyMeasurable (hs t) - · exact (hg.memLpLoc hu).aestronglyMeasurable (hs t) + _ ≤ eLpNorm (f u) p _ + eLpNorm (g u) p _ := eLpNorm_sub_le hp _ ≤ (k * eLpNorm u p _ + β) + (k' * eLpNorm u p _ + β') := by gcongr · exact hf.stableWith t u hu @@ -207,7 +199,8 @@ 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, ?_⟩⟩ + constructor + intro 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 @@ -221,6 +214,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) + · apply hfu _ hu · apply hs.ae_tendsto_indicator _ < _ := by simp [MemLp.eLpNorm_lt_top hu, ENNReal.mul_lt_top_iff] @@ -245,18 +239,15 @@ theorem IsCausal.isFiniteGainStableWith (hf : IsCausal f s p μ) (hs : ∀ t, Is (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)) + _ ≤ eLpNorm (f <| (s t).indicator u) p μ := by + apply eLpNorm_indicator_le + exact (hs t).measurableSet _ ≤ ↑k * eLpNorm ((s t).indicator u) p μ + β := by apply h exact hu.memLp_indicator (hs t) _ = _ := by rw [eLpNorm_indicator_eq_eLpNorm_restrict (hs t).measurableSet] -/- Todo: define the gain -/ - --- def eLpGain (f : (α → E) → α → F) (p : ℝ≥0∞) : ℝ≥0∞ := ⨅ i, sorry - end Function end IsFiniteGainStable diff --git a/DynamicalSystems/Stability/Basic.lean b/DynamicalSystems/Stability/Basic.lean index 2d9034d..638233f 100644 --- a/DynamicalSystems/Stability/Basic.lean +++ b/DynamicalSystems/Stability/Basic.lean @@ -57,8 +57,7 @@ theorem HasBasis.isStableOn_iff {ι' : Sort*} {p : ι' → Prop} {s : ι' → Se theorem IsStableOn.mono {I I'} (hl : l.IsStableOn Φ I) (h : I' ⊆ I) : l.IsStableOn Φ I' := by unfold IsStableOn at hl ⊢ - peel hl with s hs s' hs' hl - exact (hl · <| h ·) + gconvert hl variable {l' : Filter ι} diff --git a/DynamicalSystems/Stability/Hamiltonian.lean b/DynamicalSystems/Stability/Hamiltonian.lean index f34ceed..922ac1d 100644 --- a/DynamicalSystems/Stability/Hamiltonian.lean +++ b/DynamicalSystems/Stability/Hamiltonian.lean @@ -105,7 +105,7 @@ theorem gradient_sq_norm (ζ : E) : variable (E) in /-- The vector field of the harmonic oscillator -/ abbrev harmonicOscillatorVf (ζ : WithLp 2 (E × E)) : WithLp 2 (E × E) := - hamiltonvf (fun x : WithLp 2 (E × E) ↦ ‖x‖ ^ 2) ζ + hamiltonvf (‖·‖ ^ 2) ζ theorem fst_harmonicOscillatorVf (ζ : WithLp 2 (E × E)) : (harmonicOscillatorVf E ζ).fst = -2 • ζ.snd := by @@ -117,8 +117,9 @@ theorem snd_harmonicOscillatorVf (ζ : WithLp 2 (E × E)) : simp [gradient_sq_norm] private -theorem lipschitzWith_two_grad_norm_sq : - LipschitzWith 2 (gradient fun x : E ↦ ‖x‖ ^ 2) := by +theorem exists_lipschitzWith_grad_norm_sq : + ∃ C, LipschitzWith C (gradient fun x : E ↦ ‖x‖ ^ 2) := by + use 2 have h : (gradient fun x : E ↦ ‖x‖ ^ 2) = fun x : E ↦ (2 : ℝ) • x := by funext x simp [gradient_sq_norm, two_smul] @@ -130,15 +131,13 @@ variable (E) in /-- The flow of the harmonic oscillator -/ @[no_expose] def harmonicOscillatorFlow : AutonomousFlow ℝ (WithLp 2 (E × E)) := - (exists_hamiltonvf_autonomousFlow (H := (fun x : WithLp 2 (E × E) ↦ ‖x‖ ^ 2)) - ⟨2, lipschitzWith_two_grad_norm_sq⟩).choose + (exists_hamiltonvf_autonomousFlow exists_lipschitzWith_grad_norm_sq).choose /-- The harmonic oscillator flow is the fundamental solution of the harmonic oscillator vector field. -/ theorem isFundamentalSolution_harmonicOscillatorFlow : (harmonicOscillatorFlow E).IsFundamentalSolution (harmonicOscillatorVf E) := - (exists_hamiltonvf_autonomousFlow (H := (fun x : WithLp 2 (E × E) ↦ ‖x‖ ^ 2)) - ⟨2, lipschitzWith_two_grad_norm_sq⟩).choose_spec + (exists_hamiltonvf_autonomousFlow exists_lipschitzWith_grad_norm_sq).choose_spec /-- The origin of the harmonic oscillator is stable. -/ theorem isStableOn_harmonicOscillatorFlow [FiniteDimensional ℝ E] : diff --git a/lake-manifest.json b/lake-manifest.json index 697fead..3688e37 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,10 +15,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "85e3a25e006c35636f0e53b0e9296caca2685bc0", + "rev": "8319c83af32e262ad477c8a896a0859cdd061b16", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.34.0-rc2", + "inputRev": "8319c83af32e262ad477c8a896a0859cdd061b16", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/verso", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d8823026ac7ef130c253089d95685f9877b95323", + "rev": "1681d78dd6e65e38b143f9740d829c826673807c", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,7 +95,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d54dddc581e08be364c278052863524bff7a99a9", + "rev": "3b4ce082a2051785ac99f899a50c55d43b6d9c28", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.toml b/lakefile.toml index 863b4e6..9a6390e 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -19,7 +19,7 @@ rev = "v4.34.0-rc2" [[require]] name = "mathlib" scope = "leanprover-community" -rev = "v4.34.0-rc2" +rev = "8319c83af32e262ad477c8a896a0859cdd061b16" [[require]] name = "axiom-audit"