SourceErrorDContract: the terminal A_{m,n,Jcut} tensor in L²

The tail of d_m is Σ_n A_{m,n,Jcut} q_{m,n,Jcut}. Its L² norm needs the AMNR tensor itself at level Jcut (no derivatives), which is the case α = [], ℓ = 0, ρ = Jcut of the amplitude-generic recursion relative_Amnr_mixed_bounds_of_spatial_profiles. The constants are I-uniform (the same primitive bounds as RelativeError.relative_Amnr_tensor_of_jets), the amplitude S is abstract, and the temperature input is the positive-order spatial jets of ∇T_i (RelativeError.relative_iterate_gradient_jets).

noncomputable def AVenhance.Infra.Section5.Contracts.sedTailConstant (β C₀ Cg Cl C : ℝ) : ℝ

The I-uniform constant of the terminal AMNR tensor.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section5.Contracts.sed_tail_core {β Creg C₀ c C Cg Cl : ℝ} (hCg : 0 ≤ Cg) (hCl : 1 ≤ Cl) (I : Ingredients β) (hz : I.Czeta ≤ C₀) (hh : I.Chat ≤ C₀) (hc : 0 < c) (hcC : c < C) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds Creg I Φ) {κ : ℝ} (hκ : 0 < κ) {M : ℕ} (hperm : κ ∈ permittedInterval β I.Λ M) (hA5 : (∀ (m : ℕ), 1 ≤ m → m < M → c * (AVenhance.a β I.Λ m * epsilon β I.Λ m ^ (2 + gamma β)) ≤ I.kappaAt κ m (M - m) ∧ I.kappaAt κ m (M - m) ≤ C * (AVenhance.a β I.Λ m * epsilon β I.Λ m ^ (2 + gamma β))) ∧ ∀ (m : ℕ), 2 ≤ m → m < M → c * epsilon β I.Λ (m - 1) ^ (4 * delta β) ≤ epsilon β I.Λ m ^ 2 / (I.kappaAt κ m (M - m) * tau β I.Λ m) ∧ epsilon β I.Λ m ^ 2 / (I.kappaAt κ m (M - m) * tau β I.Λ m) ≤ C * epsilon β I.Λ (m - 1) ^ (4 * delta β)) {m : ℕ} (hm : 2 ≤ m) (hmM : m ≤ M) (hsm1 : Section4.amnrSourceRatioConstant β C * epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ 1 / 2) (hsm2 : Section3.lAmtOneStepConstant β C₀ * (Section4.amnrSourceRatioConstant β C * epsilon β I.Λ (m - 1) ^ (2 * delta β) + epsilon β I.Λ (m - 1) ^ delta β) ≤ 9 / 160) {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaSeq κ M (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) θ₀ θprev T) {S : ℝ} (hS : 0 ≤ S) (hjets : ∀ i ≤ Nstar β, ∀ (p : Fin 2) (α : List (Fin 2)), α.length ≤ Nstar β → MeasureTheory.eLpNorm (Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (List.map some α) (Section4.amnrTGradient (T i) p)) 2 ((MeasureTheory.volume.restrict (Set.uIoc 0 1)).prod (MeasureTheory.volume.restrict unitCube)) ≤ ENNReal.ofReal (Cg * S / √(I.kappaSeq κ M (m - 1)) * (Cl * epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2))) ^ α.length)) {n : ℕ} (hn : n ∈ Finset.range (Nstar β)) : MeasureTheory.eLpNorm (fun (z : Section4.AmnrSpace) => I.Amnr hΦ m (I.kappaSeq κ M m) n (T (Nstar β)) (Jcut β) z.1 z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (sedTailConstant β C₀ Cg Cl C * S * (epsilon β I.Λ m ^ 2 / I.kappaSeq κ M m) / √(I.kappaSeq κ M (m - 1)) * (tauP β I.Λ m)⁻¹ ^ Jcut β)

Fixed-I core of the terminal AMNR tensor estimate.

theorem AVenhance.Infra.Section5.Contracts.sed_tail_amnr_of_jets (β C₀ Cg Cl : ℝ) (hCg : 0 ≤ Cg) (hCl : 1 ≤ Cl) : ∃ (CA : ℝ), 0 ≤ CA ∧ ∃ (Λ₀ : ℝ), ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → Λ₀ ≤ ↑I.Λ → ∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ), ∀ κ ∈ permissibleSet β I.Λ, ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → ∀ (m : ℕ), 2 ≤ m → m ≤ M → ∀ (θ₀ : Homogenization.Vec 2 → ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaSeq κ M (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev → I.IsTIterates hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) θ₀ θprev T → ∀ (S : ℝ), 0 ≤ S → (∀ i ≤ Nstar β, ∀ (p : Fin 2) (α : List (Fin 2)), α.length ≤ Nstar β → MeasureTheory.eLpNorm (Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (List.map some α) (Section4.amnrTGradient (T i) p)) 2 ((MeasureTheory.volume.restrict (Set.uIoc 0 1)).prod (MeasureTheory.volume.restrict unitCube)) ≤ ENNReal.ofReal (Cg * S / √(I.kappaSeq κ M (m - 1)) * (Cl * epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2))) ^ α.length)) → ∀ n ∈ Finset.range (Nstar β), MeasureTheory.eLpNorm (fun (z : Section4.AmnrSpace) => I.Amnr hΦ m (I.kappaSeq κ M m) n (T (Nstar β)) (Jcut β) z.1 z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (CA * S * (epsilon β I.Λ m ^ 2 / I.kappaSeq κ M m) / √(I.kappaSeq κ M (m - 1)) * (tauP β I.Λ m)⁻¹ ^ Jcut β)

Terminal AMNR tensor at amplitude S from the per-iterate temperature-gradient jets, with I-uniform constants.