Source-scale reduction for the remainder index. The corrected indexing fixes the remainder at Jcut β; the estimates below retain that exact exponent.

noncomputable def AVenhance.Infra.Section4.dmFrozenTailTerm {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (n : ℕ) (z : ℝ × Homogenization.Vec 2) : Homogenization.Vec 2

The actual tensor remainder at the corrected index Jcut.

Equations

• AVenhance.Infra.Section4.dmFrozenTailTerm I hΦ m κ T n z i = ∑ j : Fin 2, ∑ k : Fin 2, I.Amnr hΦ m κ n T (AVenhance.Jcut β) z.1 z.2 i j k * I.qMNR κ m n (AVenhance.Jcut β) z.1 j k

noncomputable def AVenhance.Infra.Section4.dmFrozenSource {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (first : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (z : ℝ × Homogenization.Vec 2) : Homogenization.Vec 2

d_m source split with its first vector term left explicit. The first term is (Jhat_m - J_m) Σ_l xihat_l (∇X_l∘X_l⁻¹)∇T; the second is the literal A_{m,n,Jcut} q_{m,n,Jcut} remainder.

Equations

• AVenhance.Infra.Section4.dmFrozenSource I hΦ m κ T first z = first z + ∑ n ∈ Finset.range (AVenhance.Nstar β), AVenhance.Infra.Section4.dmFrozenTailTerm I hΦ m κ T n z

noncomputable def AVenhance.Infra.Section4.dmFrozenFluxFirst {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (z : ℝ × Homogenization.Vec 2) : Homogenization.Vec 2

The Jhat_m - J_m first term of d_m: Σ_l ξ̂_l F_lᵀ (JHat - 𝒥) F_l ∇T, with the flow Jacobian F_l on both sides of the flux gap (§9.4).

Equations

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

theorem AVenhance.Infra.Section4.matrix_mulVec_norm_le_two {M : Matrix (Fin 2) (Fin 2) ℝ} {v : Homogenization.Vec 2} (F : ℝ) (hF : 0 ≤ F) (hM : ‖M‖ ≤ F) : ‖M.mulVec v‖ ≤ 2 * F * ‖v‖

In two dimensions, the elementwise matrix supremum norm controls its action on vectors equipped with the Vec 2 supremum norm.

theorem AVenhance.Infra.Section4.hatXiML_average_norm_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) (f : ℤ → Homogenization.Vec 2) {B : ℝ} (hb : ∀ (l : ℤ), I.hatXiML m l t ≠ 0 → ‖f l‖ ≤ B) : ‖∑' (l : ℤ), I.hatXiML m l t • f l‖ ≤ B

Convexity of the cutoff average for vector-valued summands.

theorem AVenhance.Infra.Section4.dmFrozenFluxFirst_norm_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) {L : ℝ} (hL : 0 ≤ L) (hflow : ∀ (z : ℝ × Homogenization.Vec 2) (l : ℤ), I.hatXiML m l z.1 ≠ 0 → ‖I.flowGrad hΦ m l z.1 z.2‖ ≤ L) {F : ℝ} (hF : 0 ≤ F) (hgap : ∀ (t : ℝ), ‖I.Jhat κ m t - I.flux κ m t‖ ≤ F) (z : ℝ × Homogenization.Vec 2) : ‖dmFrozenFluxFirst I hΦ m κ T z‖ ≤ 2 * F * (4 * L ^ 2) * ‖spaceGrad (T z.1) z.2‖

Pointwise bound on the first summand from an active-window flow bound and a uniform flux-gap bound.

theorem AVenhance.Infra.Section4.dm_frozenFluxFirst_eLpNorm_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (hfirstMeas : MeasureTheory.AEStronglyMeasurable (dmFrozenFluxFirst I hΦ m κ T) (MeasureTheory.volume.restrict timeCube)) {L : ℝ} (hL : 0 ≤ L) (hflow : ∀ (z : ℝ × Homogenization.Vec 2) (l : ℤ), I.hatXiML m l z.1 ≠ 0 → ‖I.flowGrad hΦ m l z.1 z.2‖ ≤ L) {G₀ : ℝ} (hTgrad : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (T z.1) z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal G₀) {F : ℝ} (hF : 0 ≤ F) (hgap : ∀ (t : ℝ), ‖I.Jhat κ m t - I.flux κ m t‖ ≤ F) (hm : 1 ≤ m) : MeasureTheory.eLpNorm (dmFrozenFluxFirst I hΦ m κ T) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (2 * F * (4 * L ^ 2 * G₀))

The first term has the Piola-conjugated flux gap as multiplier. Its analytic inputs are a pointwise bound L on the active flow Jacobians and the source L² bound for the temperature gradient; the flux gap is supplied by the corrected Section 3 Jhat estimate.

theorem AVenhance.Infra.Section4.dm_frozenFluxFirst_eLpNorm_le_of_section3 {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) {G : ℝ} (hfirstMeas : MeasureTheory.AEStronglyMeasurable (dmFrozenFluxFirst I hΦ m κ T) (MeasureTheory.volume.restrict timeCube)) {L : ℝ} (hL : 0 ≤ L) (hflow : ∀ (z : ℝ × Homogenization.Vec 2) (l : ℤ), I.hatXiML m l z.1 ≠ 0 → ‖I.flowGrad hΦ m l z.1 z.2‖ ≤ L) {G₀ : ℝ} (hTgrad : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (T z.1) z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal G₀) (hGL : 4 * L ^ 2 * G₀ ≤ G) (hm : 1 ≤ m) (hκ : 0 < κ) : MeasureTheory.eLpNorm (dmFrozenFluxFirst I hΦ m κ T) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (2 * (4 * Real.pi ^ 2 * I.Czeta * ↑(Nstar β) * 2 ^ Nstar β * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ) * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m)) ^ Nstar β) * G)

Specialization of the preceding first-term estimate to the actual Section 3 coefficients. The paper's J_m is the flux, so the corrected flux_sub_Jhat_norm_le estimate bounds the matrix multiplier directly.

noncomputable def AVenhance.Infra.Section4.dmFrozenTailCoordinateTerm {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (n : ℕ) (i j k : Fin 2) (z : ℝ × Homogenization.Vec 2) : Homogenization.Vec 2

One coordinate summand in the A_{m,n,Jcut} q_{m,n,Jcut} vector tail.

Equations

• AVenhance.Infra.Section4.dmFrozenTailCoordinateTerm I hΦ m κ T n i j k z p = if i = p then I.Amnr hΦ m κ n T (AVenhance.Jcut β) z.1 z.2 i j k * I.qMNR κ m n (AVenhance.Jcut β) z.1 j k else 0

theorem AVenhance.Infra.Section4.eLpNorm_mul_right_le_of_abs_bound {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ} {A Q : ℝ} (hQ : 0 ≤ Q) (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) (hbound : ∀ (x : α), |g x| ≤ Q) (hLp : MeasureTheory.eLpNorm f 2 μ ≤ ENNReal.ofReal A) : MeasureTheory.eLpNorm (fun (x : α) => f x * g x) 2 μ ≤ ENNReal.ofReal (Q * A)

L² multiplication by a scalar bounded in absolute value.

theorem AVenhance.Infra.Section4.dmFrozenTailTerm_eq_coordinate_sum {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (n : ℕ) (z : ℝ × Homogenization.Vec 2) : dmFrozenTailTerm I hΦ m κ T n z = ∑ i : Fin 2, ∑ j : Fin 2, ∑ k : Fin 2, dmFrozenTailCoordinateTerm I hΦ m κ T n i j k z

Decomposition of the vector tail into its eight single-coordinate products.

theorem AVenhance.Infra.Section4.dmFrozenTailTerm_eLpNorm_le_of_pAmnr_qMNR {β C₀ A : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (n : ℕ) {μ : MeasureTheory.Measure (ℝ × Homogenization.Vec 2)} (hcutoff : I.Czeta ≤ C₀) (hm : 1 ≤ m) (hκ : 0 < κ) (hAmnr : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => I.Amnr hΦ m κ n T (Jcut β) z.1 z.2) 2 μ ≤ ENNReal.ofReal A) (hAentryMeas : ∀ (i j k : Fin 2), MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => I.Amnr hΦ m κ n T (Jcut β) z.1 z.2 i j k) μ) (hCoordinateMeas : ∀ (i j k : Fin 2), MeasureTheory.AEStronglyMeasurable (dmFrozenTailCoordinateTerm I hΦ m κ T n i j k) μ) (hn : n ≤ Nstar β) : MeasureTheory.eLpNorm (dmFrozenTailTerm I hΦ m κ T n) 2 μ ≤ ENNReal.ofReal (8 * A * (4 * Real.pi ^ 2 * C₀ * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 2) * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m)) ^ n * (8 * tau β I.Λ m) ^ Jcut β))

Actual tail estimate from the (k,ell)=(0,0) instance of the source p.Amnr.bounds and the corrected geometric qMNR bound. The AMNR input is the tensor-valued source estimate; only its finite coordinate projections are used here.

theorem AVenhance.Infra.Section4.dm_frozenSource_eLpNorm_le_of_term_bounds {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (first : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) {Bfirst Btail : ℝ} (hBfirst : 0 ≤ Bfirst) (hBtail : 0 ≤ Btail) (hfirst : MeasureTheory.eLpNorm first 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal Bfirst) (htail : ∀ n ∈ Finset.range (Nstar β), MeasureTheory.eLpNorm (dmFrozenTailTerm I hΦ m κ T n) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal Btail) : MeasureTheory.eLpNorm (dmFrozenSource I hΦ m κ T first) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (Bfirst + ↑(Nstar β) * Btail)

L² triangle estimate for the d_m split.

theorem AVenhance.Infra.Section4.dm_frozenSource_eLpNorm_le_of_section3_pAmnr {β C₀ A G : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (hcutoff : I.Czeta ≤ C₀) (hm : 1 ≤ m) (hκ : 0 < κ) (hA : 0 ≤ A) (hG : 0 ≤ G) (hratio : epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m) ≤ 1) (hfirstMeas : MeasureTheory.AEStronglyMeasurable (dmFrozenFluxFirst I hΦ m κ T) (MeasureTheory.volume.restrict timeCube)) {L : ℝ} (hL : 0 ≤ L) (hflow : ∀ (z : ℝ × Homogenization.Vec 2) (l : ℤ), I.hatXiML m l z.1 ≠ 0 → ‖I.flowGrad hΦ m l z.1 z.2‖ ≤ L) {G₀ : ℝ} (hTgrad : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (T z.1) z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal G₀) (hGL : 4 * L ^ 2 * G₀ ≤ G) (hAmnr : ∀ n ∈ Finset.range (Nstar β), MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => I.Amnr hΦ m κ n T (Jcut β) z.1 z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal A) (hAentryMeas : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k : Fin 2), MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => I.Amnr hΦ m κ n T (Jcut β) z.1 z.2 i j k) (MeasureTheory.volume.restrict timeCube)) (hCoordinateMeas : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k : Fin 2), MeasureTheory.AEStronglyMeasurable (dmFrozenTailCoordinateTerm I hΦ m κ T n i j k) (MeasureTheory.volume.restrict timeCube)) : MeasureTheory.eLpNorm (dmFrozenSource I hΦ m κ T (dmFrozenFluxFirst I hΦ m κ T)) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (2 * (4 * Real.pi ^ 2 * I.Czeta * ↑(Nstar β) * 2 ^ Nstar β * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ) * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m)) ^ Nstar β) * G + ↑(Nstar β) * (8 * A * (4 * Real.pi ^ 2 * C₀ * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 2) * (8 * tau β I.Λ m) ^ Jcut β)))

Complete d_m source estimate after inserting the actual J_m flux first term, the corrected Section 3 flux gap, and the (0,0) p.Amnr source bound for every tail mode. The ratio hypothesis is the Section 3 smallness input used to discard the remaining mode factor R^n ≤ 1.

theorem AVenhance.Infra.Section4.jcut_source_budget {β : ℝ} (hJ : 2 ≤ Jcut β) : 1 ≤ Jcut β ∧ Jcut β ≤ Nstar β ∧ Nstar β ≤ 3 * Jcut β ∧ Jcut β ≤ 4 * Nstar β

Arithmetic consequences of for the cutoff.

theorem AVenhance.Infra.Section4.dm_first_term_four_delta_to_Jcut {N J : ℕ} {Cexpr Couter x Khalf F : ℝ} (hCexpr : 1 ≤ Cexpr) (hCouter : 0 ≤ Couter) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) (hK : 0 ≤ Khalf) (hN : N ≤ 3 * J) (hJ : J ≤ 4 * N) (hfirst : F ≤ Couter * Khalf * (Cexpr * x ^ 4) ^ N) : F ≤ Couter * Khalf * (Cexpr ^ 3 * x) ^ J

Transfer of the first d_m term from the corrected 4δ exprat scale to the Jcut exponent. The proof uses N ≤ 3J and J ≤ 4N, which hold for the large cutoff once Jcut ≥ 2.

theorem AVenhance.Infra.Section4.dm_source_split_scale {N J : ℕ} {Cexpr Couter Afac CA x Khalf F Tail : ℝ} (hCexpr : 1 ≤ Cexpr) (hCouter : 0 ≤ Couter) (hAfac : 0 ≤ Afac) (hCA : 0 ≤ CA) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) (hK : 0 ≤ Khalf) (hN : N ≤ 3 * J) (hJ : J ≤ 4 * N) (hfirst : F ≤ Couter * Khalf * (Cexpr * x ^ 4) ^ N) (htail : Tail ≤ ↑N * CA * Khalf * (Afac * x) ^ J) : F + Tail ≤ (Couter + ↑N * CA) * Khalf * ((Cexpr ^ 3 + Afac + 1) * x) ^ J

Assembly of the corrected first-term transfer and the Jcut remainder sum. This is the scalar source split used before the spacetime L² triangle inequality for the vector-valued d_m.

theorem AVenhance.Infra.Section4.dm_frozenSource_paper_scale {β C₀ A G Cexpr Couter Afac CA x Khalf : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (hcutoff : I.Czeta ≤ C₀) (hm : 1 ≤ m) (hκ : 0 < κ) (hA : 0 ≤ A) (hG : 0 ≤ G) (hratio : epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m) ≤ 1) (hfirstMeas : MeasureTheory.AEStronglyMeasurable (dmFrozenFluxFirst I hΦ m κ T) (MeasureTheory.volume.restrict timeCube)) {L : ℝ} (hL : 0 ≤ L) (hflow : ∀ (z : ℝ × Homogenization.Vec 2) (l : ℤ), I.hatXiML m l z.1 ≠ 0 → ‖I.flowGrad hΦ m l z.1 z.2‖ ≤ L) {G₀ : ℝ} (hTgrad : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (T z.1) z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal G₀) (hGL : 4 * L ^ 2 * G₀ ≤ G) (hAmnr : ∀ n ∈ Finset.range (Nstar β), MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => I.Amnr hΦ m κ n T (Jcut β) z.1 z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal A) (hAentryMeas : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k : Fin 2), MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => I.Amnr hΦ m κ n T (Jcut β) z.1 z.2 i j k) (MeasureTheory.volume.restrict timeCube)) (hCoordinateMeas : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k : Fin 2), MeasureTheory.AEStronglyMeasurable (dmFrozenTailCoordinateTerm I hΦ m κ T n i j k) (MeasureTheory.volume.restrict timeCube)) (hCexpr : 1 ≤ Cexpr) (hCouter : 0 ≤ Couter) (hAfac : 0 ≤ Afac) (hCA : 0 ≤ CA) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) (hK : 0 ≤ Khalf) (hcut : 2 ≤ Jcut β) (hfirstScale : 2 * (4 * Real.pi ^ 2 * I.Czeta * ↑(Nstar β) * 2 ^ Nstar β * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ) * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m)) ^ Nstar β) * G ≤ Couter * Khalf * (Cexpr * x ^ 4) ^ Nstar β) (htailScale : ↑(Nstar β) * (8 * A * (4 * Real.pi ^ 2 * C₀ * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 2) * (8 * tau β I.Λ m) ^ Jcut β)) ≤ ↑(Nstar β) * CA * Khalf * (Afac * x) ^ Jcut β) : MeasureTheory.eLpNorm (dmFrozenSource I hΦ m κ T (dmFrozenFluxFirst I hΦ m κ T)) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal ((Couter + ↑(Nstar β) * CA) * Khalf * ((Cexpr ^ 3 + Afac + 1) * x) ^ Jcut β)

p.dm.bounds after the source parameter inequalities are supplied. The first scalar premise is the four-delta flux transfer; the second is the p.Amnr/qMNR scale for the Jcut tail. The actual L² estimate and its J_m = flux identification are proved by dm_frozenSource_eLpNorm_le_of_section3_pAmnr above.