HomMomentTail

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

Theorem B, §4.5, Step 1: the missing glue hY

The target

Step 1's display carries EXACTLY ONE conditional edge, hY:

  ∫⁻ ω, Y ω ^ (2p) dμ ≤ (ENNReal.ofReal 2) ^ (2p),
      Y = 3^{(1-α) X_m(α)},

the exponential moment of the Theorem-C minimal-scale factor. The missing glue is exactly this: tail ⟹ exponential moment for an ℕ∞-valued scale, absent repo-wide and in CoarseGraining. This module supplies it.

The carrier

X_m(α) is ℕ∞-valued (the Provider.Regularity.minimalScaleX), so 3^{(1-α)X} must be ℝ≥0∞-valued with the value ⊤ on {X = ⊤}. enatThreeRpow is that function, defined by the WithTop recursor — NOT by a truncation, a junk value, or a comparable surrogate: on {X = k} it is exactly 3^{ck} and on {X = ⊤} it is exactly ⊤.

The engine

lintegral_homMinimalScaleFactor_rpow_le_two. Three elementary steps, no layer-cake identity and no series inversion:

1. The one-sided truncated layer bound (homMinimalScaleFactor_le_trunc_add_tsum): for any cut N₀,

     3^{cX} ≤ 3^{cN₀} + Σ_{N ≥ N₀+1} 3^{cN} 1{X ≥ N},
   

   an inequality, valid pointwise including at X = ⊤ (both sides ⊤, because the tail series of terms ≥ 1 diverges). This is where the naive layer-cake bound E[b^X] ≤ Σ_N b^N P(X ≥ N) — which overcounts by the cut length and is USELESS at p = 1 — is avoided.
2. Integration (lintegral_homMinimalScaleFactor_le): lintegral_tsum plus lintegral_indicator_const turn the right-hand side into 3^{cN₀} + Σ_N 3^{cN} μ{X ≥ N}.
3. The geometric tail: the tail μ{X ≥ N} ≤ B e^{-θN} makes the N-th term B ρ^N with ρ = 3^c e^{-θ}, and the three DISPLAYED gates
   • hratio: ρ ≤ 1/2 (the p-range: 2p(1-α)log 3 ≤ θ/2),
   • htrunc: 3^{c·2p·N₀} ≤ 2^p (the γ-smallness N₀ s log 3 ≤ log 2),
   • hsmall: 2 B ρ^{N₀+1} ≤ 1 (the cut is past the tail's turn-on), give ≤ 2^p + 1 ≤ 2^{2p}.

The three gates are stated, not absorbed: they are exactly the γ-smallness and p-range the §4.5 web must supply, and homTailNormalForm converts the own tail (step_two_minimalScaleX's fourth clause) into the (B, θ) shape they speak about.

Why p = 1 is the binding case

At the bottom of the range the moment must be below 2^2 = 4 while the crude layer-cake bound gives ≈ N₀. Step 1 above is exactly what avoids that: the cut contributes 3^{cN₀} ≤ 2^p, not N₀, and the tail contributes ≤ 1.

1. 3^{c n} for an ℕ∞-valued scale

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.enatThreeRpow (c : ℝ) : ℕ∞ → ENNReal

3^{c n} for n: ℕ∞, with the value ⊤ at n = ⊤. Faithful: no truncation and no junk value.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.enatThreeRpow c n = WithTop.recTopCoe ⊤ (fun (k : ℕ) => ENNReal.ofReal (3 ^ (c * ↑k))) n

theorem Algsuperdiff.Section4.Provider.Homogenization.enatThreeRpow_top (c : ℝ) : enatThreeRpow c ⊤ = ⊤

theorem Algsuperdiff.Section4.Provider.Homogenization.enatThreeRpow_coe (c : ℝ) (k : ℕ) : enatThreeRpow c ↑k = ENNReal.ofReal (3 ^ (c * ↑k))

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.homMinimalScaleFactor {Omega : Type u_1} (c : ℝ) (X : Omega → ℕ∞) : Omega → ENNReal

The Theorem-C minimal-scale factor 3^{(1-α) X_m(α)} as an ℝ≥0∞-valued observable — the Y slot of EthmB(m).

Equations

• Algsuperdiff.Section4.Provider.Homogenization.homMinimalScaleFactor c X omega = Algsuperdiff.Section4.Provider.Homogenization.enatThreeRpow c (X omega)

theorem Algsuperdiff.Section4.Provider.Homogenization.measurable_homMinimalScaleFactor {Omega : Type u_1} [MeasurableSpace Omega] (c : ℝ) {X : Omega → ℕ∞} (hX : Measurable X) : Measurable (homMinimalScaleFactor c X)

theorem Algsuperdiff.Section4.Provider.Homogenization.enatThreeRpow_rpow {c r : ℝ} (hr : 0 < r) (n : ℕ∞) : enatThreeRpow c n ^ r = enatThreeRpow (c * r) n

Raising the factor to a positive power multiplies the exponent: this is what turns Y^{2p} into the same object at c ↦ 2pc.

theorem Algsuperdiff.Section4.Provider.Homogenization.homMinimalScaleFactor_rpow {Omega : Type u_1} {c r : ℝ} (hr : 0 < r) (X : Omega → ℕ∞) (omega : Omega) : homMinimalScaleFactor c X omega ^ r = homMinimalScaleFactor (c * r) X omega

2. The one-sided truncated layer bound

theorem Algsuperdiff.Section4.Provider.Homogenization.homMinimalScaleFactor_le_trunc_add_tsum {Omega : Type u_1} {c : ℝ} (hc : 0 ≤ c) (N0 : ℕ) (X : Omega → ℕ∞) (omega : Omega) : homMinimalScaleFactor c X omega ≤ ENNReal.ofReal (3 ^ (c * ↑N0)) + ∑' (N : ℕ), {w : Omega | ↑(N0 + 1 + N) ≤ X w}.indicator (fun (x : Omega) => ENNReal.ofReal (3 ^ (c * ↑(N0 + 1 + N)))) omega

The truncated layer bound, pointwise and valid at X = ⊤:

  3^{cX} ≤ 3^{cN₀} + Σ_{N ≥ N₀+1} 3^{cN} 1{X ≥ N}.

Below the cut the first summand dominates; above it the matching term of the series does. Unlike the untruncated layer-cake bound this does not accumulate N₀ copies of 1, which is what makes the p = 1 endpoint reachable.

3. Integration

theorem Algsuperdiff.Section4.Provider.Homogenization.lintegral_homMinimalScaleFactor_le {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {c : ℝ} (hc : 0 ≤ c) (N0 : ℕ) {X : Omega → ℕ∞} (hX : Measurable X) : ∫⁻ (omega : Omega), homMinimalScaleFactor c X omega ∂mu ≤ ENNReal.ofReal (3 ^ (c * ↑N0)) + ∑' (N : ℕ), ENNReal.ofReal (3 ^ (c * ↑(N0 + 1 + N))) * mu {w : Omega | ↑(N0 + 1 + N) ≤ X w}

The truncated layer bound, integrated.

4. The geometric tail

theorem Algsuperdiff.Section4.Provider.Homogenization.tsum_ofReal_pow_le_two {rho : ℝ} (h : rho ≤ 1 / 2) : ∑' (_N : ℕ), ENNReal.ofReal rho ^ _N ≤ 2

The extended-nonnegative geometric series is at most two for ratio at most one half.

5. hY: the exponential moment

theorem Algsuperdiff.Section4.Provider.Homogenization.lintegral_homMinimalScaleFactor_rpow_le_two {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {X : Omega → ℕ∞} (hX : Measurable X) {c B theta p : ℝ} {N0 : ℕ} (hc : 0 ≤ c) (hp : 1 ≤ p) (hB : 0 ≤ B) (htail : ∀ (N : ℕ), mu {w : Omega | ↑N ≤ X w} ≤ ENNReal.ofReal (B * Real.exp (-(theta * ↑N)))) (hratio : 3 ^ (c * (2 * p)) * Real.exp (-theta) ≤ 1 / 2) (htrunc : 3 ^ (c * (2 * p) * ↑N0) ≤ 2 ^ p) (hsmall : 2 * (B * (3 ^ (c * (2 * p)) * Real.exp (-theta)) ^ (N0 + 1)) ≤ 1) : ∫⁻ (omega : Omega), homMinimalScaleFactor c X omega ^ (2 * p) ∂mu ≤ ENNReal.ofReal 2 ^ (2 * p)

The hY discharge.

For an ℕ∞-valued scale X with the geometric tail μ{X ≥ N} ≤ B e^{-θN}, the Theorem-C factor Y = 3^{cX} obeys the moment normal form

  ∫⁻ Y^{2p} dμ ≤ (ENNReal.ofReal 2)^{2p}

under the three DISPLAYED gates hratio, htrunc, hsmall. This is exactly the shape of the conditional edge hY, so Step 1's display becomes unconditional once the §4.5 web supplies the gates.

6. The tail in the (B, θ) normal form

theorem Algsuperdiff.Section4.Provider.Homogenization.homTailNormalForm {Cst gam alpha : ℝ} (hCst : Cst ≠ 0) (hgam : gam ≠ 0) (N : ℕ) : Cst * Real.exp (-((1 - alpha) ^ 2 * (↑N - Cst)) / (Cst * gam)) = Cst * Real.exp ((1 - alpha) ^ 2 / gam) * Real.exp (-((1 - alpha) ^ 2 / (Cst * gam) * ↑N))

the Step-2 tail, rewritten. step_two_minimalScaleX's fourth clause gives μ{X ≥ N} ≤ C exp(-((1-α)²(N - C))/(Cγ)); that is the (B, θ) shape the engine consumes, at

  B = C e^{(1-α)²/γ},      θ = (1-α)²/(Cγ).

An identity, not an estimate.

7. hY at this development carrier

theorem Algsuperdiff.Section4.Provider.Homogenization.homY_moment_bound {d : ℕ} (M : Section3.ABKModel d) {X : Section3.Cutoff.CutoffSample d → ℕ∞} (hX : Measurable X) {Cst alpha p : ℝ} {N0 : ℕ} (hCst : 0 < Cst) (halpha : alpha ≤ 1) (hp : 1 ≤ p) (htail : ∀ (N : ℕ), ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | ↑N ≤ X omega} ≤ ENNReal.ofReal (Cst * Real.exp (-((1 - alpha) ^ 2 * (↑N - Cst)) / (Cst * M.gamma)))) (hratio : 3 ^ ((1 - alpha) * (2 * p)) * Real.exp (-((1 - alpha) ^ 2 / (Cst * M.gamma))) ≤ 1 / 2) (htrunc : 3 ^ ((1 - alpha) * (2 * p) * ↑N0) ≤ 2 ^ p) (hsmall : 2 * (Cst * Real.exp ((1 - alpha) ^ 2 / M.gamma) * (3 ^ ((1 - alpha) * (2 * p)) * Real.exp (-((1 - alpha) ^ 2 / (Cst * M.gamma)))) ^ (N0 + 1)) ≤ 1) : ∫⁻ (omega : Section3.Cutoff.CutoffSample d), homMinimalScaleFactor (1 - alpha) X omega ^ (2 * p) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal 2 ^ (2 * p)

The hY discharge at the §4.5 carrier.

The step_two_minimalScaleX supplies, for the own law, the tail

  P{ X_m(α) ≥ N } ≤ C exp( -((1-α)²(N - C)) / (Cγ) ),

and this theorem turns it into the conditional edge hY verbatim:

  ∫⁻ ω, (3^{(1-α)X_m(α)})^{2p} dP ≤ (ENNReal.ofReal 2)^{2p}.

The three gates are the (B,θ) instances of the engine's, at B = C e^{(1-α)²/γ} and θ = (1-α)²/(Cγ). They are the §4.5 web's γ- and p-side conditions, stated rather than absorbed.