Documentation

LeanPool.Superdiffusion.Algsuperdiff.Probability.WindowAmplitudes

WindowAmplitudes #

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

The √-growing window amplitudes of the Step-3 layer variables #

ABK26, l.minimal.scale.sep Step 3. Step 3 applies the Γ_σ triangle inequality to two finite layer sums, and the resulting scales are geometrically weighted sums of the √-growing per-cube amplitude Cv √(k + 1 − i) supplied by e.maxy.bound. This module closes both of those deterministic amplitude sums, and the weighted tsum that recombines the below-window channel.

The two closures are exactly the tex's Cs^{−3/2} and Cs^{−5/2}, i.e. geomSqrtConst α and geomTailConst α · geomSqrtConst α. They are the point of the sharp Cauchy--Schwarz closure Algsuperdiff.Probability.sum_threePow_neg_sqrt_le: the crude √(r+1) ≤ r+1 would give geomTailConst α ^ 2 and geomTailConst α ^ 3, half a power of the parameter worse in each channel, and the printed envelope would not close.

Everything here is deterministic real arithmetic in the amplitudes Cv, α and the scale indices; no sample space, no measure and no coefficient field appears. The corresponding O_{Γ₂} statements about the layer variables themselves are left to the consumer, which owns the carrier.

Main results #

References #

The explicit amplitudes #

source
noncomputable def Algsuperdiff.Probability.step3WindowAmp (Cv α : ℝ) :
ℝ

The uniform Γ₂ amplitude of the in-window layer variable: gammaTriangleConst 2 · Cv · (1−3^{−α})^{−3/2} — the tex's Cs^{−3/2}.

Equations
Instances For
    source
    noncomputable def Algsuperdiff.Probability.step3HeadAmp (Cv α : ℝ) (j : ℕ) :
    ℝ

    The per-j Γ₂ amplitude of the below-window layer variable: gammaTriangleConst 2 · Cv · ((1−3^{−α})^{−3/2} + √(j+1)(1−3^{−α})⁻¹). It grows like √j, which is exactly why the below-window channel needs a per-layer tail closure and not a uniform one.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def Algsuperdiff.Probability.step3TailAmp (Cv α : ℝ) :
      ℝ

      The Γ₂ amplitude of the below-window weighted sum ∑'_j 3^{−αj} H_j: (gammaTriangleConst 2)² · 2 Cv (1−3^{−α})^{−5/2} — the tex's Cs^{−5/2}.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Algsuperdiff.Probability.step3WindowAmp_pos {Cv α : ℝ} (hα : 0 < α) (hCv : 0 < Cv) :
        0 < step3WindowAmp Cv α
        source
        theorem Algsuperdiff.Probability.step3HeadAmp_nonneg {Cv α : ℝ} (hα : 0 < α) (hCv : 0 ≤ Cv) (j : ℕ) :
        0 ≤ step3HeadAmp Cv α j
        source
        theorem Algsuperdiff.Probability.step3HeadAmp_pos {Cv α : ℝ} (hα : 0 < α) (hCv : 0 < Cv) (j : ℕ) :
        0 < step3HeadAmp Cv α j
        source
        theorem Algsuperdiff.Probability.step3TailAmp_nonneg {Cv α : ℝ} (hα : 0 < α) (hCv : 0 ≤ Cv) :
        0 ≤ step3TailAmp Cv α

        The two deterministic amplitude sums #

        source
        theorem Algsuperdiff.Probability.sum_windowAmp_le {Cv α : ℝ} (hα : 0 < α) (hCv : 0 ≤ Cv) (i m : ℤ) :
        ∑ k ∈ Finset.Icc i m, 3 ^ (-(α * ↑(k - i))) * (Cv * √↑(k + 1 - i)) ≤ Cv * geomSqrtConst α

        The in-window amplitude sum, uniformly in i and m. The Γ_σ triangle applied to ∑_{k=i}^m 3^{−α(k−i)} V i k produces the scale ∑_{k=i}^m 3^{−α(k−i)} Cv √(k+1−i); that sum is ≤ Cv(1−3^{−α})^{−3/2} for every i and every m.

        source
        theorem Algsuperdiff.Probability.sum_headAmp_le {Cv α : ℝ} (hα : 0 < α) (hCv : 0 ≤ Cv) (n m : ℤ) (j : ℕ) :
        ∑ k ∈ Finset.Icc n m, 3 ^ (-(α * ↑(k - n))) * (Cv * √↑(k + 1 - (n - 1 - ↑j))) ≤ Cv * (geomSqrtConst α + √(↑j + 1) * geomTailConst α)

        The below-window amplitude sum, at layer depth j. For i = n−1−j and k ∈ [n, m] we have k+1−i = (k−n+1) + (j+1), so √(k+1−i) ≤ √(k−n+1) + √(j+1), and the geometric closures give the per-j amplitude Cv((1−3^{−α})^{−3/2} + √(j+1)(1−3^{−α})⁻¹).

        The weighted amplitude tsum of the below-window channel #

        source
        theorem Algsuperdiff.Probability.weight_step3HeadAmp_eq (Cv α : ℝ) (j : ℕ) :
        3 ^ (-(α * ↑j)) * step3HeadAmp Cv α j = HCPolySupport.IndependentSums.gammaTriangleConst 2 * (Cv * geomSqrtConst α) * 3 ^ (-(α * ↑j)) + HCPolySupport.IndependentSums.gammaTriangleConst 2 * (Cv * geomTailConst α) * (3 ^ (-(α * ↑j)) * √(↑j + 1))

        The below-window weighted amplitude splits into a pure geometric channel and a √-weighted geometric channel.

        source
        theorem Algsuperdiff.Probability.summable_weight_step3HeadAmp {Cv α : ℝ} (hα : 0 < α) :
        Summable fun (j : ℕ) => 3 ^ (-(α * ↑j)) * step3HeadAmp Cv α j

        The below-window amplitudes are geometrically summable (they grow like √j).

        source
        theorem Algsuperdiff.Probability.tsum_weight_step3HeadAmp_le {Cv α : ℝ} (hα : 0 < α) (hCv : 0 ≤ Cv) :
        ∑' (j : ℕ), 3 ^ (-(α * ↑j)) * step3HeadAmp Cv α j ≤ HCPolySupport.IndependentSums.gammaTriangleConst 2 * (2 * Cv * (geomTailConst α * geomSqrtConst α))

        The below-window weighted amplitude tsum, closed. ∑'_j 3^{−αj}·step3HeadAmp ≤ gammaTriangleConst 2 · 2Cv(1−3^{−α})^{−5/2} — the tex's Cs^{−5/2}.