Lemma U: the abstract mode system

A finite family of scalar paths c a with c a' = -(κ λₐ c a + G a), together with an integrable energy density e dominating Σ λₐ (c a)² and (after the factor B²) Σ (G a)². The two consequences used by Lemma U are proved here, with no reference to PDEs or Fourier series: the low-mode increment bound and the high-mode amplitude bound.

structure AVenhance.Infra.FullTheorem.LemmaU.ModeSystem {ι : Type u_1} [Fintype ι] (κ B : ℝ) (lam : ι → ℝ) (c G : ι → ℝ → ℝ) (e : ℝ → ℝ) (Etot : ℝ) : Prop

Hypotheses on a finite family of mode paths.

• kappa_pos : 0 < κ
• B_nonneg : 0 ≤ B
• lam_nonneg (a : ι) : 0 ≤ lam a
• c_cont (a : ι) : ContinuousOn (c a) (Set.Icc 0 1)
• G_int (a : ι) : IntervalIntegrable (G a) MeasureTheory.volume 0 1
• path (a : ι) (t : ℝ) : t ∈ Set.Icc 0 1 → c a t = c a 0 - ∫ (r : ℝ) in 0..t, κ * lam a * c a r + G a r
• e_nonneg (r : ℝ) : 0 ≤ e r
• e_int : IntervalIntegrable e MeasureTheory.volume 0 1
• e_total : ∫ (r : ℝ) in 0..1, e r ≤ Etot
• bessel_c : ∀ᵐ (r : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 1), ∑ a : ι, lam a * c a r ^ 2 ≤ e r
• bessel_G : ∀ᵐ (r : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 1), ∑ a : ι, G a r ^ 2 ≤ B ^ 2 * e r

theorem AVenhance.Infra.FullTheorem.LemmaU.ModeSystem.ModeEnergy.uIcc_sub {s t : ℝ} (hs : s ∈ Set.Icc 0 1) (ht : t ∈ Set.Icc 0 1) : Set.uIcc s t ⊆ Set.uIcc 0 1

theorem AVenhance.Infra.FullTheorem.LemmaU.ModeSystem.etot_nonneg {ι : Type u_1} [Fintype ι] {κ B : ℝ} {lam : ι → ℝ} {c G : ι → ℝ → ℝ} {e : ℝ → ℝ} {Etot : ℝ} (hM : ModeSystem κ B lam c G e Etot) : 0 ≤ Etot

theorem AVenhance.Infra.FullTheorem.LemmaU.ModeSystem.c_intervalIntegrable {ι : Type u_1} [Fintype ι] {κ B : ℝ} {lam : ι → ℝ} {c G : ι → ℝ → ℝ} {e : ℝ → ℝ} {Etot : ℝ} (hM : ModeSystem κ B lam c G e Etot) (a : ι) : IntervalIntegrable (c a) MeasureTheory.volume 0 1

theorem AVenhance.Infra.FullTheorem.LemmaU.ModeSystem.G_sq_intervalIntegrable {ι : Type u_1} [Fintype ι] {κ B : ℝ} {lam : ι → ℝ} {c G : ι → ℝ → ℝ} {e : ℝ → ℝ} {Etot : ℝ} (hM : ModeSystem κ B lam c G e Etot) (a : ι) : IntervalIntegrable (fun (r : ℝ) => G a r ^ 2) MeasureTheory.volume 0 1

theorem AVenhance.Infra.FullTheorem.LemmaU.ModeSystem.q_intervalIntegrable {ι : Type u_1} [Fintype ι] {κ B : ℝ} {lam : ι → ℝ} {c G : ι → ℝ → ℝ} {e : ℝ → ℝ} {Etot : ℝ} (hM : ModeSystem κ B lam c G e Etot) (a : ι) : IntervalIntegrable (fun (r : ℝ) => κ * lam a * c a r + G a r) MeasureTheory.volume 0 1

theorem AVenhance.Infra.FullTheorem.LemmaU.ModeSystem.q_sq_intervalIntegrable {ι : Type u_1} [Fintype ι] {κ B : ℝ} {lam : ι → ℝ} {c G : ι → ℝ → ℝ} {e : ℝ → ℝ} {Etot : ℝ} (hM : ModeSystem κ B lam c G e Etot) (a : ι) : IntervalIntegrable (fun (r : ℝ) => (κ * lam a * c a r + G a r) ^ 2) MeasureTheory.volume 0 1

theorem AVenhance.Infra.FullTheorem.LemmaU.ModeSystem.increment_eq {ι : Type u_1} [Fintype ι] {κ B : ℝ} {lam : ι → ℝ} {c G : ι → ℝ → ℝ} {e : ℝ → ℝ} {Etot : ℝ} (hM : ModeSystem κ B lam c G e Etot) (a : ι) {s t : ℝ} (hs : s ∈ Set.Icc 0 1) (ht : t ∈ Set.Icc 0 1) : c a t - c a s = -∫ (r : ℝ) in s..t, κ * lam a * c a r + G a r

The increment of one mode over [s,t].