Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section4.Provider.MinimalScale.KickTails

KickTails #

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

The Step-1 kick tails:, unconditionally #

ABK26, Β§4.2, Step 1 of l.minimal.scale.sep. The manuscript's Step-1 claim is

X_j^{(1)} ≀ π’ͺ_{Ξ“β‚‚}(C c⋆^{βˆ’1}s^{βˆ’5/2}√γ) ,      X_j^{(2)} ≀ π’ͺ_{Ξ“_{1/2}}(C e^{βˆ’C^{βˆ’1}c⋆³/Ξ³}) ,

uniformly in j, on the regime and window. This module proves it, from the four citations the manuscript lists (e.induction.E.bounds, e.Gamma.sigma.triangle, e.maxy.bound and the good-event bound) and nothing else.

The chain, and where each citation enters #

per-cube display at the inner scale i   exists_isTwoTermBigOWith_…  (e.induction.E.bounds)
  β†’ lattice-annulus maximum             isTwoTermBigOWith_kickAnnMax  (e.maxy.bound)
  β†’ weighted inner-scale sum            isTwoTermBigOWith_annularKick (e.Gamma.sigma.triangle)
  β†’ closed forms in s                   kickAmpTwo_le, kickAmpHalf_le (the two closures)
  β†’ the two legs                        KickSplit                     (the clamp)
  β†’ the printed amplitudes              exists_kickFamily_tails       (the absorptions)

The Β§4.1 𝒒₂ chain (Proportion.isTwoTermBigOWith_errorAnnMax, isTwoTermBigOWith_Xcal) is the template and its two devices β€” the union bound Proportion.isBigOWith_fmax at the machine-computed annulusPenalty and the two-term countable triangle inequality Proportion.isTwoTermBigOWith_wsum β€” are consumed by name. The difference is that Β§4.2 does not square: the Orlicz indices stay (Ξ“β‚‚, Ξ“_{1/2}) rather than moving to (Γ₁, Ξ“_{1/4}), the weight is 3^{βˆ’Β½sΒ·} rather than 3^{βˆ’ΒΌsΒ·}, and the union-bound penalties are therefore √(jβˆ’i+1) and (jβˆ’i+1)Β² rather than (jβˆ’i+1) and (jβˆ’i+1)⁴.

The s-bookkeeping, sharply #

The Ξ“β‚‚ closure is the sharp one: βˆ‘_r √(r+1)3^{βˆ’Β½sr} = O(s^{βˆ’3/2}), which against the anchor's own s^{βˆ’1} gives exactly the printed s^{βˆ’5/2}. The crude √(r+1) ≀ r+1 would give s^{βˆ’2} and hence s^{βˆ’3}, and the printed exponent would be missed by half a power. On the Ξ“_{1/2} lane the (jβˆ’i+1)Β² penalty contributes s^{βˆ’3}, which the printed amplitude does not carry: it is absorbed into the exponential explicitly by KickArith.inv_cube_mul_exp_le on the window s β‰₯ 8Ξ³, at the cost of halving the exponent β€” i.e. of doubling the dimensional constant, which is what the manuscript's "for C chosen sufficiently large" buys.

The regime and the window are the lemma's own hypotheses #

states l.minimal.scale.sep under Ξ³ ≀ C^{βˆ’10}c⋆^{10} and s ∈ [8Ξ³, 1/2], and the endpoint below carries exactly those two premises. Both are used: the regime twice, in the two absorptions of KickArith (which need a lower bound on c⋆³γ^{βˆ’1}, without which the absorbed prefactor carries c⋆^{βˆ’9}), and the upper window endpoint s ≀ 1/2 in the two geometric closures (geomTailConst (Β½s) ≀ 4/s needs Β½s ≀ Β½). The upper endpoint 1/4 was not needed.

Inside the proof, prints the weaker regime Ξ³ ≀ C^{βˆ’1}c⋆⁡, which does not imply the lemma's own hypothesis and which nothing here uses. The proved producer of the per-cube display, Proportion.exists_isTwoTermBigOWith_annularErrorObservable, also carries Ξ³ ≀ C^{βˆ’10}c⋆^{10}.

References #

1. The dimensional base of the union-bound penalty #

source
noncomputable def Algsuperdiff.Section4.Provider.MinimalScale.penaltyBase (d : β„•) :
ℝ

1 + 2d log 3, the dimensional base of the lattice-annulus penalty.

Equations
Instances For
    source
    theorem Algsuperdiff.Section4.Provider.MinimalScale.one_le_penaltyBase (d : β„•) :
    1 ≀ penaltyBase d
    source
    theorem Algsuperdiff.Section4.Provider.MinimalScale.penaltyBase_pos (d : β„•) :
    0 < penaltyBase d
    source
    theorem Algsuperdiff.Section4.Provider.MinimalScale.annulusPenalty_two_le (d p : β„•) :
    Proportion.annulusPenalty d 2 (p + 1) ≀ √(penaltyBase d) * √(↑p + 1)

    The Ξ“β‚‚ penalty comparison √(1+d(p+2)log 3) ≀ √(penaltyBase d)·√(p+1).

    source
    theorem Algsuperdiff.Section4.Provider.MinimalScale.annulusPenalty_half_le (d p : β„•) :
    Proportion.annulusPenalty d (1 / 2) (p + 1) ≀ penaltyBase d ^ 2 * (↑p + 1) ^ 2

    The Ξ“_{1/2} penalty comparison (1+d(p+2)log 3)Β² ≀ penaltyBase dΒ²(p+1)Β².

    source
    theorem Algsuperdiff.Section4.Provider.MinimalScale.annulusPenalty_two_le_one (d p : β„•) :
    Proportion.annulusPenalty d 2 p ≀ Proportion.annulusPenalty d 1 p

    The Ξ“β‚‚ penalty is below the Γ₁ penalty: 1/Οƒ decreases in Οƒ and the base is at least 1. This is what makes the proved summability instance at N = 1 applicable on the Ξ“β‚‚ lane.

    2. e.maxy.bound: the lattice-annulus maximum #

    source
    theorem Algsuperdiff.Section4.Provider.MinimalScale.isTwoTermBigOWith_kickAnnMax {d : β„•} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) {A1 A2 : ℝ} (j i : β„€) (hcube : Section3.Probability.IsTwoTermBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Support.annularErrorObservable M i s) A1 A2) :
    Section3.Probability.IsTwoTermBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (kickAnnMax M s j i) (Proportion.annulusPenalty d 2 (j - i).toNat * A1) (Proportion.annulusPenalty d (1 / 2) (j - i).toNat * A2)

    The lattice translation is stationarity (GoodEvents.measurePreserving_translateCutoffSample), not a new estimate.

    3. e.Gamma.sigma.triangle: the weighted inner-scale sum #

    source
    noncomputable def Algsuperdiff.Section4.Provider.MinimalScale.kickAmpTwo (d : β„•) (s A1 : ℝ) :
    ℝ

    The Ξ“β‚‚ amplitude of the Step-1 sum, as the weighted penalty series.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def Algsuperdiff.Section4.Provider.MinimalScale.kickAmpHalf (d : β„•) (s A2 : ℝ) :
      ℝ

      The Ξ“_{1/2} amplitude of the Step-1 sum, as the weighted penalty series.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Algsuperdiff.Section4.Provider.MinimalScale.summable_kickAmpTwo (d : β„•) {s A1 : ℝ} (hs : 0 < s) (hA1 : 0 ≀ A1) :
        Summable fun (p : β„•) => Proportion.weightThird (s / 2) (p + 1) * (Proportion.annulusPenalty d 2 (p + 1) * A1)
        source
        theorem Algsuperdiff.Section4.Provider.MinimalScale.summable_kickAmpHalf (d : β„•) {s A2 : ℝ} (hs : 0 < s) (hA2 : 0 ≀ A2) :
        Summable fun (p : β„•) => Proportion.weightThird (s / 2) (p + 1) * (Proportion.annulusPenalty d (1 / 2) (p + 1) * A2)
        source
        theorem Algsuperdiff.Section4.Provider.MinimalScale.isTwoTermBigOWith_annularKick {d : β„•} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (j : β„€) {A1 A2 : ℝ} (hA1 : 0 < A1) (hA2 : 0 < A2) (hcube : βˆ€ i ≀ j - 1, Section3.Probability.IsTwoTermBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Support.annularErrorObservable M i s) A1 A2) :
        Section3.Probability.IsTwoTermBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (annularKick M s j) (kickAmpTwo d (↑s) A1) (kickAmpHalf d (↑s) A2)

        The Step-1 inner-scale sum inherits the two-term display through the two-term countable generalized triangle inequality, applied at Οƒ = 2 and Οƒ = 1/2 simultaneously. hcube is the per-inner-scale display, uniform in i.

        4. The closed forms in the window parameter #

        source
        noncomputable def Algsuperdiff.Section4.Provider.MinimalScale.kickTwoConst (d : β„•) :
        ℝ

        The dimensional constant of the Ξ“β‚‚ closed form.

        Equations
        Instances For
          source
          noncomputable def Algsuperdiff.Section4.Provider.MinimalScale.kickHalfConst (d : β„•) :
          ℝ

          The dimensional constant of the Ξ“_{1/2} closed form.

          Equations
          Instances For
            source
            theorem Algsuperdiff.Section4.Provider.MinimalScale.kickHalfConst_pos (d : β„•) :
            0 < kickHalfConst d
            source
            theorem Algsuperdiff.Section4.Provider.MinimalScale.kickAmpTwo_le (d : β„•) {s A1 : ℝ} (hs0 : 0 < s) (hs1 : s ≀ 1) (hA1 : 0 ≀ A1) :
            kickAmpTwo d s A1 ≀ kickTwoConst d * (A1 * (√s ^ 3)⁻¹)

            The Ξ“β‚‚ closed form, sharp: s^{βˆ’3/2}. The √(jβˆ’i+1) penalty summed against 3^{βˆ’Β½s(jβˆ’i)} closes by Cauchy--Schwarz at (1βˆ’3^{βˆ’Β½s})^{βˆ’3/2}, i.e. 8s^{βˆ’3/2}; the crude comparison √(r+1) ≀ r+1 would give s^{βˆ’2}.

            source
            theorem Algsuperdiff.Section4.Provider.MinimalScale.kickAmpHalf_le (d : β„•) {s A2 : ℝ} (hs0 : 0 < s) (hs1 : s ≀ 1) (hA2 : 0 ≀ A2) :
            kickAmpHalf d s A2 ≀ kickHalfConst d * (A2 * s⁻¹ ^ 3)

            The Ξ“_{1/2} closed form: s^{βˆ’3}. The (jβˆ’i+1)Β² penalty summed against 3^{βˆ’Β½s(jβˆ’i)} closes at 2(1βˆ’3^{βˆ’Β½s})^{βˆ’3}, i.e. 128s^{βˆ’3}. This s^{βˆ’3} is exactly what inv_cube_mul_exp_le absorbs into the exponential.

            5. The endpoint #

            source
            theorem Algsuperdiff.Section4.Provider.MinimalScale.exists_kickFamily_tails (d : β„•) :
            βˆƒ (C : ℝ), 0 < C ∧ βˆ€ (M : Section3.ABKModel d), M.gamma ≀ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 β†’ βˆ€ (s : { s : ℝ // 0 < s }), 8 * M.gamma ≀ ↑s β†’ ↑s ≀ 1 / 2 β†’ βˆƒ (lam : ℝ), 0 ≀ lam ∧ (βˆ€ (j : β„€), HCPolySupport.IndependentSums.IsBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (kickLegLow M s lam j) (C * (Section3.Disorder.cstar M)⁻¹ * (βˆšβ†‘s ^ 5)⁻¹ * √M.gamma)) ∧ βˆ€ (j : β„€), HCPolySupport.IndependentSums.IsBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (kickLegHigh M s lam j) (C * Real.exp (-(C⁻¹ * Section3.Disorder.cstar M ^ 3 * M.gamma⁻¹)))

            The Step-1 kick family and its two tails, unconditionally.

            There is a dimensional constant C such that for every model in the regime Ξ³ ≀ C^{βˆ’10}c⋆^{10} and every window parameter s ∈ [8Ξ³, 1/2] there is a threshold lam for which, uniformly in the annulus index j,

            X_j^{(1)} = min(annularKick_j, lam)             ≀ π’ͺ_{Ξ“β‚‚}(C c⋆^{βˆ’1}s^{βˆ’5/2}√γ) ,
X_j^{(2)} = annularKick_j βˆ’ min(annularKick_j, lam) ≀ π’ͺ_{Ξ“_{1/2}}(C exp(βˆ’C^{βˆ’1}c⋆³γ^{βˆ’1})) ,

            and X_j^{(1)} + X_j^{(2)} = annularKick_j exactly. The r-dependence of the pair is settled in KickFamily, which needs nothing from here.

            s^{βˆ’5/2} is written ((√s)⁡)⁻¹, so that no rpow appears in the statement.

            Hypotheses. Exactly the premises of l.minimal.scale.sep as printed: Ξ³ ≀ C^{βˆ’10}c⋆^{10} and s ∈ [8Ξ³, 1/2]. The positivity of s is the typing datum of the observable's index and is implied by the window.