HomStepEnvelope

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Theorem B, §4.5: the defect random variable EthmB(m) and the

parameter web of the §4.5 parameter choices

The target

t.homogenization, the definition of E_thmB:

EthmB(m):= s^{-1} 3^{(1-α) X_m(α)}
              sup_{L ≥ m} 𝓔_{s₁,∞,2}(□_m, n; ã_{L,m}, σ_m)
              ( 1 + sup_{L ≥ m} 𝓔_{1/4,∞,2}(□_m; ã_{L,m}, σ_m) )
            + C γ⁵ ( 1 + sup_{L ≥ m} 𝓔²_{s₁/2,∞,2}(□_m, n; ã_{L,m}, σ_m) )

together with node the parameter selection:

s:= |log γ|⁻¹,  s₁:= s/2,  s₂:= 1/2,  α:= 1 - s/2,  k:= ⌈10|log γ|⌉,
n:= m - k.

Carrier

The three sup_{L ≥ m} 𝓔 factors are the OWN carrier: the two-argument observable Algsuperdiff.Section4.Support.fluxCorrectedTwoScaleErrorObservableSup of Support/FluxCorrectedTwoScale.lean, which is the carrier of the anchor Algsuperdiff.Frozen.Section4.bounds_mathcal_E_aL. It already carries the L-supremum and the flux correction ã_{L,m} = a_L - (k_L - k_m)_{□_m}, takes values in [0,∞], so that no convergence side condition enters the statement, and reduces at a matched index pair n = m to the one-argument observable by rfl. The one-argument 𝓔_{1/4,∞,2}(□_m; ·) of the middle factor is therefore rendered as the two-argument observable at n = m, exactly as the source's own convention prescribes.

Consequently ethmB takes values in ℝ≥0∞. The real-valued witness EB: Ω → ℝ demanded by the frozen block of generator_renormalization is obtained downstream, after the Step-1 moment bound has certified ethmB < ∞ a.e.; it is NOT formed here.

Exponent binders

ethmB is parametrized by the base exponent s: {s: ℝ // 0 < s}; the subordinate exponents s₁ = s/2 and s₁/2 = s/4 are formed inside the definition from s.2, so no extra positivity binder is carried. The §4.5 value s = |log γ|⁻¹ is supplied by homS below and is NOT baked into the definition: homS M is positive only under a γ ≠ 1 gate, and the convention is that gates live in theorems, not in definitions.

1. The exponent slots

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.homQuarter : { s : ℝ // 0 < s }

The fixed exponent 1/4 of the middle factor of EthmB(m).

Equations

• Algsuperdiff.Section4.Provider.Homogenization.homQuarter = ⟨1 / 4, Algsuperdiff.Section4.Provider.Homogenization.homQuarter._proof_1⟩

@[simp]

theorem Algsuperdiff.Section4.Provider.Homogenization.homQuarter_val : ↑homQuarter = 1 / 4

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.homHalf (s : { s : ℝ // 0 < s }) : { s : ℝ // 0 < s }

s₁:= s/2 (the §4.5 parameter choices).

Equations

• Algsuperdiff.Section4.Provider.Homogenization.homHalf s = ⟨↑s / 2, ⋯⟩

@[simp]

theorem Algsuperdiff.Section4.Provider.Homogenization.homHalf_val (s : { s : ℝ // 0 < s }) : ↑(homHalf s) = ↑s / 2

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.homQuarterOf (s : { s : ℝ // 0 < s }) : { s : ℝ // 0 < s }

s₁/2 = s/4, the exponent of the second summand of EthmB(m).

Equations

• Algsuperdiff.Section4.Provider.Homogenization.homQuarterOf s = ⟨↑s / 4, ⋯⟩

@[simp]

theorem Algsuperdiff.Section4.Provider.Homogenization.homQuarterOf_val (s : { s : ℝ // 0 < s }) : ↑(homQuarterOf s) = ↑s / 4

2. The parameter web the §4.5 parameter choices + the mesoscale energy definition

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.homS {d : ℕ} (M : Section3.ABKModel d) : ℝ

s:= |log γ|⁻¹.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.homS M = |Real.log M.gamma|⁻¹

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.homAlpha {d : ℕ} (M : Section3.ABKModel d) : ℝ

α:= 1 - s/2.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.homAlpha M = 1 - Algsuperdiff.Section4.Provider.Homogenization.homS M / 2

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.homK {d : ℕ} (M : Section3.ABKModel d) : ℕ

k:= ⌈10 |log γ|⌉.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.homK M = ⌈10 * |Real.log M.gamma|⌉₊

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.homN {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) : ℤ

n:= m - k (the mesoscale energy definition).

Equations

• Algsuperdiff.Section4.Provider.Homogenization.homN M m = m - ↑(Algsuperdiff.Section4.Provider.Homogenization.homK M)

theorem Algsuperdiff.Section4.Provider.Homogenization.homS_pos {d : ℕ} {M : Section3.ABKModel d} (hlog : 0 < |Real.log M.gamma|) : 0 < homS M

theorem Algsuperdiff.Section4.Provider.Homogenization.homS_le_quarter {d : ℕ} {M : Section3.ABKModel d} (hlog : 4 ≤ |Real.log M.gamma|) : homS M ≤ 1 / 4

The gate: s ≤ 1/4 is exactly |log γ| ≥ 4.

theorem Algsuperdiff.Section4.Provider.Homogenization.one_sub_homAlpha {d : ℕ} (M : Section3.ABKModel d) : 1 - homAlpha M = homS M / 2

1 - α = s/2: the exponent that Step 1's Markov step consumes.

theorem Algsuperdiff.Section4.Provider.Homogenization.homAlpha_pos {d : ℕ} {M : Section3.ABKModel d} (hlog : 4 ≤ |Real.log M.gamma|) : 0 < homAlpha M

theorem Algsuperdiff.Section4.Provider.Homogenization.homK_ge {d : ℕ} (M : Section3.ABKModel d) : 10 * |Real.log M.gamma| ≤ ↑(homK M)

Ceiling honesty, lower half: 10|log γ| ≤ k.

theorem Algsuperdiff.Section4.Provider.Homogenization.homK_le {d : ℕ} (M : Section3.ABKModel d) : ↑(homK M) ≤ 10 * |Real.log M.gamma| + 1

Ceiling honesty, upper half: k ≤ 10|log γ| + 1 (: the printed 3^{(1-α)(m-n)} ≤ 3^5 middle inequality is FALSE; the honest envelope keeps the +1 visible).

theorem Algsuperdiff.Section4.Provider.Homogenization.homN_le {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) : homN M m ≤ m

theorem Algsuperdiff.Section4.Provider.Homogenization.homN_gap {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) : ↑m - ↑(homN M m) = ↑(homK M)

The mesoscale gap in the real gauge the anchor's binders use.

3. The defect random variable EthmB(m)

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.ethmB {d : ℕ} (M : Section3.ABKModel d) (Cgap : ℝ) (Y : Section3.Cutoff.CutoffSample d → ENNReal) (m n : ℤ) (s : { s : ℝ // 0 < s }) : Section3.Cutoff.CutoffSample d → ENNReal

EthmB(m).

The three 𝓔 factors are the anchor's own carrier; the middle one is the one-argument functional, i.e. the two-argument observable at n = m. Y is the minimal-scale factor 3^{(1-α) X_m(α)} of Theorem C (an abstract [0,∞]-valued observable here: its construction and its Step-1 exponential moment are the business of the Step-1 module), and Cgap is the Step-3 gap-absorption constant C = C(d, c⋆) of the second summand.

Equations

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

theorem Algsuperdiff.Section4.Provider.Homogenization.measurable_ethmB {d : ℕ} (M : Section3.ABKModel d) (Cgap : ℝ) {Y : Section3.Cutoff.CutoffSample d → ENNReal} (hY : Measurable Y) {m n : ℤ} (hnm : n ≤ m) (s : { s : ℝ // 0 < s }) : Measurable (ethmB M Cgap Y m n s)

4.: the moment bound must survive the Step-3 rescaling

theorem Algsuperdiff.Section4.Provider.Homogenization.lintegral_rpow_const_mul_le {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {F : Omega → ENNReal} {R lam p : ℝ} (hp : 0 ≤ p) (hlam : 0 ≤ lam) (h : ∫⁻ (omega : Omega), F omega ^ p ∂mu ≤ ENNReal.ofReal R ^ p) : ∫⁻ (omega : Omega), (ENNReal.ofReal lam * F omega) ^ p ∂mu ≤ ENNReal.ofReal (lam * R) ^ p

The rescaling stability of the moment normal form.

If F obeys ∫⁻ F^p ≤ (ofReal R)^p and lam ≥ 0, then the rescaled observable ofReal lam * F obeys the SAME normal form with the majorant enlarged by exactly lam. This is the honest disposition of: the source's Step-3 sentence "absorbing the constant C into EthmB(m)" rescales a witness whose moment bound was already proved, so the moment bound's constant must absorb the same factor.

theorem Algsuperdiff.Section4.Provider.Homogenization.ethmB_const_smul_moment {d : ℕ} (M : Section3.ABKModel d) (Cgap : ℝ) {Y : Section3.Cutoff.CutoffSample d → ENNReal} {m n : ℤ} {s : { s : ℝ // 0 < s }} {R lam p : ℝ} (hp : 0 ≤ p) (hlam : 0 ≤ lam) (h : ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ethmB M Cgap Y m n s omega ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal R ^ p) : ∫⁻ (omega : Section3.Cutoff.CutoffSample d), (ENNReal.ofReal lam * ethmB M Cgap Y m n s omega) ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (lam * R) ^ p

The EthmB instance of the previous lemma: the Step-1 moment bound of EthmB(m) transports to the Step-3 rescaled witness C · EthmB(m) with the moment constant multiplied by the same C.