Amplitude-generic leading-energy estimates on the actual datum and T iterates. The quadratic error has amplitude S squared; the base consumes only integrated gradients.

Abstract-real lemmas

theorem AVenhance.Infra.Section5.RelativeError.mul_le_sq_of_sqrt_mul_le {κ G L A : ℝ} (hκ : 0 ≤ κ) (hG : 0 ≤ G) (h : √κ * √G ≤ A * √L) (hL : 0 ≤ L) : κ * G ≤ A ^ 2 * L

Squaring √κ √G ≤ A √L.

theorem AVenhance.Infra.Section5.RelativeError.second_final {Lc X R κp e G L A K : ℝ} (hX0 : 0 ≤ X) (hR0 : 0 ≤ R) (hK : 0 ≤ K) (hκp : 0 ≤ κp) (hG : 0 ≤ G) (he : 0 ≤ e) (hXK : X ≤ K * κp) (hRK : R ≤ K * e) (hκG : κp * G ≤ A ^ 2 * L) : 2 * (Lc * X * R) * G ≤ 2 * |Lc| * K ^ 2 * e * (A ^ 2 * L)

Final arithmetic of the second estimate.

theorem AVenhance.Infra.Section5.RelativeError.spaceTimeGradNormSq_nonneg' (V : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : 0 ≤ spaceTimeGradNormSq V

theorem AVenhance.Infra.Section5.RelativeError.tIterates_classicalSol {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hΦ : IsStreamSeq I Φ} {m : ℕ} {κm κp : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m κm κp θ₀ θprev T) : IsClassicalSol (streamVel (Φ (m - 1))) κp (I.TForcing hΦ m κm κp (T (Nstar β - 1))) θ₀ (T (Nstar β))

Regularity of T (Nstar β) and periodicity of its slices.

e.ergodic.break.up.second

theorem AVenhance.Infra.Section5.RelativeError.relative_ergodic_break_up_second_scaled (β C₀ A P : ℝ) (hA : 0 < A) (hP : 0 ≤ P) : ∃ (C : ℝ), ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → C ≤ ↑I.Λ → ∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ), ∀ κ ∈ permissibleSet β I.Λ, ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → ∀ (m : ℕ), 2 ≤ m → m ≤ M → ∀ (S : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ), I.IsTIterates hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) θ₀ θprev T → √(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (T (Nstar β) t) x) ≤ A * √(S ^ 2) → |∫ (t : ℝ) in 0..1, LeftToShow.gradQuad (T (Nstar β)) (I.kappaSeq κ M m • LeftToShow.leadingGramAvg I hΦ m (I.kappaSeq κ M m) t - I.flux (I.kappaSeq κ M m) m t) t| ≤ C * epsilon β I.Λ (m - 1) ^ (2 * delta β) * S ^ 2

e.ergodic.break.up.second (8466–8509).

e.ergodic.break.up.last

theorem AVenhance.Infra.Section5.RelativeError.ibp_final {τpp τp KJ X K κp S Q A sL e3 x e2 : ℝ} (hτpp : 0 ≤ τpp) (hτp : 0 < τp) (hKJ : 0 ≤ KJ) (hXK : X ≤ K * κp) (hκ : 0 < κp) (hK : 0 ≤ K) (hS : 0 ≤ S) (hQ : 0 ≤ Q) (hA : 0 < A) (hsL : 0 ≤ sL) (he3 : 0 ≤ e3) (hSb : √κp * S ≤ A * sL) (hQb : Q ≤ A * e3 * (√κp)⁻¹ * sL * τp⁻¹) (hrat : τpp / τp ≤ 9 * x) (hx : e3 * x = e2) : 8 * (4 * τpp) * (2 * (KJ * X)) * S * Q ≤ 576 * KJ * K * A ^ 2 * e2 * sL ^ 2

Arithmetic of the integration-by-parts bound (source 8800–8830).

theorem AVenhance.Infra.Section5.RelativeError.remainder_final {c0 c0' X K κp r e G L A : ℝ} {N : ℕ} (hc0 : 0 ≤ c0) (hcc : c0 ≤ c0') (hX0 : 0 ≤ X) (hXK : X ≤ K * κp) (hK : 0 ≤ K) (hκp : 0 ≤ κp) (hr0 : 0 ≤ r) (hrK : r ≤ K * e) (he0 : 0 ≤ e) (he1 : e ≤ 1) (hN : 1 ≤ N) (hG : 0 ≤ G) (hκG : κp * G ≤ A ^ 2 * L) : 4 * (c0 * X * r ^ N) * G ≤ 4 * c0' * K ^ (N + 1) * e * (A ^ 2 * L)

Arithmetic of the J → JHat remainder (source 8700–8780).

theorem AVenhance.Infra.Section5.RelativeError.four_ceil_add_one_le_nine {x : ℝ} (hx : 1 ≤ x) : 4 * ↑⌈x⌉₊ + 1 ≤ 9 * x

4⌈x⌉ + 1 ≤ 9x for x ≥ 1.

theorem AVenhance.Infra.Section5.RelativeError.rpow_three_mul_neg_eq {ε δ : ℝ} (hε : 0 < ε) : ε ^ (3 * δ) * ε ^ (-δ) = ε ^ (2 * δ)

ε^{3δ} ε^{-δ} = ε^{2δ}.

theorem AVenhance.Infra.Section5.RelativeError.relative_ergodic_break_up_last (β C₀ A P : ℝ) (hA : 0 < A) (hP : 0 ≤ P) : ∃ (C : ℝ), ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → C ≤ ↑I.Λ → ∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ), ∀ κ ∈ permissibleSet β I.Λ, ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → ∀ (m : ℕ), 2 ≤ m → m ≤ M → ∀ (S : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ), I.IsTIterates hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) θ₀ θprev T → √(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (T (Nstar β) t) x) ≤ A * √(S ^ 2) → √(spaceTimeGradNormSq (LeftToShow.materialGrad (streamVel (Φ (m - 1))) (T (Nstar β)))) ≤ A * epsilon β I.Λ (m - 1) ^ (3 * delta β) * (√(I.kappaSeq κ M (m - 1)))⁻¹ * √(S ^ 2) * (tauP β I.Λ m)⁻¹ → |(∫ (t : ℝ) in 0..1, LeftToShow.gradQuad (T (Nstar β)) (I.flux (I.kappaSeq κ M m) m t) t) - ∫ (t : ℝ) in 0..1, LeftToShow.gradQuad (T (Nstar β)) (timeAvgMat fun (s : ℝ) => I.flux (I.kappaSeq κ M m) m s) t| ≤ C * epsilon β I.Λ (m - 1) ^ (2 * delta β) * S ^ 2

e.ergodic.break.up.last (8640–8860).