Skip to content

chore: update mathlib #70

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
mcdoll merged 1 commit into from
Sep 15, 2026
Merged

chore: update mathlib #70

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 12 additions & 12 deletions DynamicalSystems/Basic/LpLoc.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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

Expand Down
33 changes: 23 additions & 10 deletions DynamicalSystems/Basic/WithLp.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand All @@ -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]
Expand All @@ -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]
Expand Down Expand Up @@ -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 ≠ ∞
Expand All @@ -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
Expand Down
56 changes: 26 additions & 30 deletions DynamicalSystems/InputOutput/ClosedLoop.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -406,17 +406,15 @@ 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
_ = eLpNorm (e₁ - G₂ u₂) p (μ.restrict (s t)) := by
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
Expand All @@ -427,17 +425,16 @@ 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
_ = eLpNorm (e₂ + G₁ u₁) p (μ.restrict (s t)) := by
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
Expand All @@ -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)) ≤
Expand All @@ -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

Expand All @@ -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)) ≤
Expand All @@ -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

Expand Down Expand Up @@ -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
Expand All @@ -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]
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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₁'
Expand All @@ -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₂'
Expand All @@ -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
Expand Down Expand Up @@ -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)) +
Expand All @@ -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
Expand Down
9 changes: 5 additions & 4 deletions DynamicalSystems/InputOutput/Example.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)]
Loading