SourceErrorDContract: scale bookkeeping

The cutoff exponent budget 2δ + qβ ≤ δ Jcut / 2, the 2δ first-term scale at the terminal step, the assembly of the d_m bound in paper-scale form, and the final conversion to ε_{m-1}^{2δ} √κ_m (e.monster.est.11.a.d, enhance.tex 7860-7880).

theorem AVenhance.Infra.Section5.Contracts.sed_budget_core {q δ N : ℝ} (hq : 1 < q) (hδ : δ = (q - 1) ^ 2 / (4 * (q + 1) * (4 * q - 1))) (hN : 500 / δ + 128 * q ^ 2 * (q - 1) ≤ N) : 10 * δ + 16 * q / 3 ≤ δ * N

Abstract-real core of the cutoff exponent budget: 10 δ + 16 q/3 ≤ δ N for the δ = (q-1)²/(4(q+1)(4q-1)) and N ≥ 500/δ + 128 q²(q-1).

theorem AVenhance.Infra.Section5.Contracts.sed_jcut_budget {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 2 * delta β + q β * β ≤ delta β * ↑(Jcut β) / 2

The cutoff absorbs the lower bound ε_m ≳ ε_{m-1}^q and the extra ε^{2δ}: 2δ + qβ ≤ δ J / 2.

theorem AVenhance.Infra.Section5.Contracts.sed_first_scale {N : ℕ} {E δ Czeta Cprod Cexprat Cg Theta κprev B R G Khalf x : ℝ} (hE : 0 < E) (hCzeta : 0 ≤ Czeta) (hCprod : 0 ≤ Cprod) (hCg : 0 ≤ Cg) (hTheta : 0 ≤ Theta) (hκprev : 0 < κprev) (hRnonneg : 0 ≤ R) (hGnonneg : 0 ≤ G) (hKhalf : Khalf = √κprev * Theta) (hx : x = E ^ (δ / 2)) (hProduct : B ≤ Cprod * κprev) (hExprat : R ≤ Cexprat * E ^ (2 * δ)) (hG : G ≤ Cg * Theta / √κprev) : 2 * (4 * Real.pi ^ 2 * Czeta * ↑N * 2 ^ N * B * R ^ N) * G ≤ 2 * (4 * Real.pi ^ 2 * Czeta * ↑N * 2 ^ N) * Cprod * Cg * Khalf * (Cexprat * x ^ 4) ^ N

The first d_m term at the 2δ exprat rate (the bound at the terminal step m = M, where the 4δ of the interior diffusivity display is not available).

theorem AVenhance.Infra.Section5.Contracts.sed_eLpNorm_le {β C₀ Csrc Cprod Cexpr Θ κprev A : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (hcutoff : I.Czeta ≤ C₀) (hκ : 0 < κ) (hκprev : 0 < κprev) (hC₀ : 0 ≤ C₀) (hCsrc : 0 ≤ Csrc) (hCprod : 0 ≤ Cprod) (hCexpr : 1 ≤ Cexpr) (hCzeta : 0 ≤ I.Czeta) (hΘ : 0 ≤ Θ) (hProduct : a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ ≤ Cprod * κprev) (hExprat : epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m) ≤ Cexpr * epsilon β I.Λ (m - 1) ^ (2 * delta β)) (hTimeRatio : tau β I.Λ m / tauP β I.Λ m ≤ 1 / 4 * epsilon β I.Λ (m - 1) ^ delta β) (hA : 0 ≤ A ∧ A ≤ Csrc * Θ * (epsilon β I.Λ m ^ 2 / κ) * (√κprev)⁻¹ * epsilon β I.Λ (m - 1) ^ (-(2 + gamma β)) * (tauP β I.Λ m)⁻¹ ^ Jcut β) (hflow : ∀ (z : ℝ × Homogenization.Vec 2) (l : ℤ), I.hatXiML m l z.1 ≠ 0 → ‖I.flowGrad hΦ m l z.1 z.2‖ ≤ 2) (hTgrad : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (T z.1) z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (Θ / √κprev)) (hfirstMeas : MeasureTheory.AEStronglyMeasurable (Section4.dmFrozenFluxFirst I hΦ m κ T) (MeasureTheory.volume.restrict timeCube)) (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 (Section4.dmFrozenTailCoordinateTerm I hΦ m κ T n i j k) (MeasureTheory.volume.restrict timeCube)) (hratio : epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m) ≤ 1) (hcut : 2 ≤ Jcut β) : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => sourceErrorD I hΦ m κ T z.1 z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal ((2 * (4 * Real.pi ^ 2 * I.Czeta * ↑(Nstar β) * 2 ^ Nstar β) * Cprod * 16 + ↑(Nstar β) * (8 * (4 * Real.pi ^ 2 * C₀) * Csrc * Cprod)) * (√κprev * Θ) * ((Cexpr ^ 3 + 2 + 1) * epsilon β I.Λ (m - 1) ^ (delta β / 2)) ^ Jcut β)

Assembly of the d_m bound from the pulled-gradient bound G, the tail tensor bound A, and the scale data (product rate, 2δ exprat rate, time ratio), in the paper-scale form C (√κ_{m-1} Θ) (C' ε_{m-1}^{δ/2})^{Jcut}.

theorem AVenhance.Infra.Section5.Contracts.sed_final_scale {x εm κm κp K Θ Cb δ q β : ℝ} {J : ℕ} (hx0 : 0 < x) (hx1 : x ≤ 1) (hεm : 0 < εm) (hκm : 0 < κm) (hκp : 0 < κp) (hK : 1 ≤ K) (hκpK : κp ≤ K) (hβ : 0 < β) (hpow : x ^ q ≤ 2 * εm) (hε : εm ^ (2 * β) ≤ K * κp * κm) (hE : 2 * δ + q * β ≤ δ * ↑J / 2) (hΘ : 0 ≤ Θ) (hCb : 0 ≤ Cb) : √κp * Θ * (Cb * x ^ (δ / 2)) ^ J ≤ Θ * Cb ^ J * 2 ^ β * K * √K * x ^ (2 * δ) * √κm

Abstract-real final scale: the Jcut-th power of C x^{δ/2} times √κ_{m-1} Θ is at most a constant times x^{2δ} √κ_m.