Lemma U: low-mode increments and high-mode amplitudes

For an abstract mode system, the low modes have a Hölder-1/2-in-time increment bound, and each high mode is controlled by its initial amplitude plus the forcing G. Combining the two gives the total squared increment bound Σ (c a t - c a s)² used by Lemma U.

theorem AVenhance.Infra.FullTheorem.LemmaU.interval_integral_mono_ae_Ioc {f g : ℝ → ℝ} {a b : ℝ} (hab : a ≤ b) (hf : IntervalIntegrable f MeasureTheory.volume a b) (hg : IntervalIntegrable g MeasureTheory.volume a b) (h : ∀ᵐ (r : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc a b), f r ≤ g r) : ∫ (r : ℝ) in a..b, f r ≤ ∫ (r : ℝ) in a..b, g r

theorem AVenhance.Infra.FullTheorem.LemmaU.intervalIntegrable_finset_sum' {ι : Type u_1} (s : Finset ι) {f : ι → ℝ → ℝ} {a b : ℝ} (h : ∀ i ∈ s, IntervalIntegrable (f i) MeasureTheory.volume a b) : IntervalIntegrable (fun (r : ℝ) => ∑ i ∈ s, f i r) MeasureTheory.volume a b

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

theorem AVenhance.Infra.FullTheorem.LemmaU.ModeSystem.LowHigh.ae_Ioc_of_sub {s t : ℝ} (hs : s ∈ Set.Icc 0 1) (ht : t ∈ Set.Icc 0 1) {P : ℝ → Prop} (h : ∀ᵐ (r : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 1), P r) : ∀ᵐ (r : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc s t), P r

theorem AVenhance.Infra.FullTheorem.LemmaU.ModeSystem.low_sum_le {ι : Type u_1} [Fintype ι] {κ B : ℝ} {lam : ι → ℝ} {c G : ι → ℝ → ℝ} {e : ℝ → ℝ} {Etot : ℝ} (hM : ModeSystem κ B lam c G e Etot) (low : Finset ι) {Λ : ℝ} (hΛ : 0 ≤ Λ) (hlow : ∀ a ∈ low, lam a ≤ Λ) {s t : ℝ} (hs : s ∈ Set.Icc 0 1) (ht : t ∈ Set.Icc 0 1) (hst : s ≤ t) : ∑ a ∈ low, (c a t - c a s) ^ 2 ≤ 2 * (t - s) * ((κ ^ 2 * Λ + B ^ 2) * Etot)

The low-mode increment bound.

theorem AVenhance.Infra.FullTheorem.LemmaU.ModeSystem.high_mode_le {ι : Type u_1} [Fintype ι] {κ B : ℝ} {lam : ι → ℝ} {c G : ι → ℝ → ℝ} {e : ℝ → ℝ} {Etot : ℝ} (hM : ModeSystem κ B lam c G e Etot) (a : ι) (hlam : 0 < lam a) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : c a t ^ 2 ≤ c a 0 ^ 2 + 1 / (2 * κ * lam a) * ∫ (r : ℝ) in 0..t, G a r ^ 2

One high mode: its amplitude is controlled by its initial value and the forcing.

theorem AVenhance.Infra.FullTheorem.LemmaU.ModeSystem.high_sum_le {ι : Type u_1} [Fintype ι] {κ B : ℝ} {lam : ι → ℝ} {c G : ι → ℝ → ℝ} {e : ℝ → ℝ} {Etot : ℝ} (hM : ModeSystem κ B lam c G e Etot) (high : Finset ι) {L D2 : ℝ} (hL : 0 < L) (hhigh : ∀ a ∈ high, L ≤ lam a) (hinit : ∑ a : ι, lam a * c a 0 ^ 2 ≤ D2) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : ∑ a ∈ high, c a t ^ 2 ≤ D2 / L + B ^ 2 * Etot / (2 * κ * L)

The high-mode amplitude bound, summed over modes with λ ≥ L.

theorem AVenhance.Infra.FullTheorem.LemmaU.ModeSystem.increment_sum_le {ι : Type u_1} [Fintype ι] {κ B : ℝ} {lam : ι → ℝ} {c G : ι → ℝ → ℝ} {e : ℝ → ℝ} {Etot : ℝ} (hM : ModeSystem κ B lam c G e Etot) (P : ι → Prop) {Λ L D2 : ℝ} (hΛ : 0 ≤ Λ) (hL : 0 < L) (hlow : ∀ (a : ι), P a → lam a ≤ Λ) (hhigh : ∀ (a : ι), ¬P a → L ≤ lam a) (hinit : ∑ a : ι, lam a * c a 0 ^ 2 ≤ D2) {s t : ℝ} (hs : s ∈ Set.Icc 0 1) (ht : t ∈ Set.Icc 0 1) (hst : s ≤ t) : ∑ a : ι, (c a t - c a s) ^ 2 ≤ 2 * (t - s) * ((κ ^ 2 * Λ + B ^ 2) * Etot) + 4 * (D2 / L + B ^ 2 * Etot / (2 * κ * L))

Total squared increment, split at the threshold predicate P (low modes).