Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section4.Provider.Proportion.LargeWaves

LargeWaves #

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

Step 1 of l.ratio.of.good.scales.for.k: the large-waves lane #

This module realizes the 𝒢₁a half of l.ratio.of.good.scales.for.k: the scale-counting variable X_k and its cube-comparison link to the first condition of 𝒢₁.

The manuscript's ‖·‖_{W^{1,∞}(□_m)} ≤^{k-m}‖·‖_{W^{1,∞}(□_k)} for m ≤ k is the proved GaugeBridge.shellW1InfGradNorm_le_zpow_mul_of_le, with constant 1 at the exact p = ∞ gauge. Combined with the exponent identity 3^{(2-γ)m} 3^{k-m} = 3^{-(1-γ)(k-m)} 3^{(2-γ)k} this gives, for m ≤ k,

3^{(2-γ)m} ‖∇j_k‖_{W^{1,∞}(□_m)} ≤ 3^{-(1-γ)(k-m)} X_k ,

which is the manuscript's display with C = 1. The Appendix-D weight rate s' is taken anywhere in (0, 1-γ]; the standing assumption γ ≤ 1/4 of ShellLawPrefix makes s' = 1/2 always admissible, and 2s' ≤ 1 is what the row-summability of the engine needs.

The concentration application (e.counting.scales.G1.step1.pre) #

The graph's correction records that the application is at level θ/2 and that the printed rate denominator 32 over-claims by a bounded factor. Here nothing is rounded: the lane is run at the honest rate produced by the proved p.concentration.for.scales, and the θ/2 level is supplied by the caller.

References #

1. The first condition of 𝒢₁, as a named event #

source
def Algsuperdiff.Section4.Provider.Proportion.eventG1a {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (T : ℝ) :
Set (Section3.Cutoff.CutoffSample d)

The first condition of 𝒢₁(m; s, T): Σ_{k ≥ m} 3^{(2-γ)m}‖∇j_k‖_{W^{1,∞}(□_m)} ≤ T, the ℝ≥0∞ sum of the frozen definition.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Algsuperdiff.Section4.Provider.Proportion.eventG1b {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (s T : ℝ) :
    Set (Section3.Cutoff.CutoffSample d)

    The second condition of 𝒢₁(m; s, T), named for the ½θ split; it is the lane of SmallWaves.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algsuperdiff.Section4.Provider.Proportion.eventG1_eq_inter {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (s T : ℝ) :
      Support.eventG1 M m s T = eventG1a M m T ∩ eventG1b M m s T

      The frozen 𝒢₁ is the intersection of the two named conditions.

      source
      theorem Algsuperdiff.Section4.Provider.Proportion.score_le_wt_mul_atomG1a {d : ℕ} (M : Section3.ABKModel d) {sprime : ℝ} (hsle : sprime ≤ 1 - M.gamma) {m k : ℤ} (hmk : m ≤ k) (omega : Section3.Cutoff.CutoffSample d) :
      Real.rpow 3 ((2 - M.gamma) * ↑m) * Support.shellW1InfGradNorm m (↑omega k) ≤ Probability.ScalesConcentration.wt sprime m k * atomG1a M k omega

      e.counting.scales.G1.Xk.link, at constant 1. For m ≤ k the m-cube term of 𝒢₁'s first condition is below the Appendix-D weighted atom, at any weight rate s' ≤ 1 - γ.

      3. The Appendix-D array of the large-waves lane #

      source
      noncomputable def Algsuperdiff.Section4.Provider.Proportion.arrayG1a {d : ℕ} (M : Section3.ABKModel d) :
      ℤ → ℤ → Section3.Cutoff.CutoffSample d → ℝ

      The large-waves Appendix-D array: the two-index array whose every row is the atom family X_k.

      Equations
      Instances For
        source
        theorem Algsuperdiff.Section4.Provider.Proportion.arrayG1a_nonneg {d : ℕ} (M : Section3.ABKModel d) (m k : ℤ) (omega : Section3.Cutoff.CutoffSample d) :
        0 ≤ arrayG1a M m k omega
        source
        theorem Algsuperdiff.Section4.Provider.Proportion.measurable_arrayG1a {d : ℕ} (M : Section3.ABKModel d) (m k : ℤ) :
        Measurable (arrayG1a M m k)
        source
        theorem Algsuperdiff.Section4.Provider.Proportion.shellLocal_arrayG1a {d : ℕ} (M : Section3.ABKModel d) (m k : ℤ) :
        Measurable (arrayG1a M m k)

        Each column of the array reads exactly one shell — the (J1) input of the independence hypothesis.

        source
        theorem Algsuperdiff.Section4.Provider.Proportion.isBigOWith_arrayG1a {d : ℕ} (M : Section3.ABKModel d) (m k : ℤ) :
        HCPolySupport.IndependentSums.IsBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (arrayG1a M m k) 1

        4. The deterministic reduction of the lane's bad event #

        source
        theorem Algsuperdiff.Section4.Provider.Proportion.eventG1a_lhs_le_rowGE {d : ℕ} (M : Section3.ABKModel d) {sprime : ℝ} (hsle : sprime ≤ 1 - M.gamma) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) :
        ∑' (k : { k : ℤ // m ≤ k }), ENNReal.ofReal (Real.rpow 3 ((2 - M.gamma) * ↑m) * Support.shellW1InfGradNorm m (↑omega ↑k)) ≤ rowGE (arrayG1a M) sprime m omega

        The first 𝒢₁ condition is dominated by the Appendix-D row. Pointwise in ω, unconditional, in ℝ≥0∞: the one-sided sum of the frozen definition is below the two-sided Appendix-D row of the array.

        source
        theorem Algsuperdiff.Section4.Provider.Proportion.lt_rowGE_of_notMem_eventG1a {d : ℕ} (M : Section3.ABKModel d) {sprime T : ℝ} (hsle : sprime ≤ 1 - M.gamma) (m : ℤ) {omega : Section3.Cutoff.CutoffSample d} (hnot : omega ∉ eventG1a M m T) :
        ENNReal.ofReal T < rowGE (arrayG1a M) sprime m omega

        Off the lane's good event the ℝ≥0∞ row exceeds the threshold.