Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section4.Provider.Regularity.RootPayloadCest

RootPayloadCest #

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

1. The sample-free cap on the Caccioppoli constant #

source
noncomputable def Algsuperdiff.Section4.Provider.Regularity.rootClauseBCaccUniform (C CB : ℝ) :
ℝ

The ω-free Caccioppoli constant of the §4.4 clause-(B) chain: √((2·max{1,C})⁴ · 4 · ((16384/441)·C_B²)²).

This is StepSevenCaccMatching.stepSevenCaccPrefactor_le evaluated at the Θ cap StepSevenLambdaSlots.stepSevenThetaRatio_le_of_caps produces from the A6 clause-(B) record, then square-rooted. It mentions neither the sample, nor the model, nor the scale.

Equations
Instances For
    source
    theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseBCaccUniform_nonneg (C CB : ℝ) :
    0 ≤ rootClauseBCaccUniform C CB
    source
    theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenCaccConst_le_uniform {d : ℕ} [NeZero d] {k : ℤ} {a : HCPolySupport.Book.Ch03.CoeffFamily d} {C sigma CB : ℝ} (hC : 0 < C) (hsigma : 0 < sigma) (hcaps : StepSevenLambdaCaps (HCPolySupport.originCube d (k + 1)) a sigma CB) :
    stepSevenCaccConst C (HCPolySupport.originCube d k) a ≤ rootClauseBCaccUniform C CB

    The C_est uniformization, at the level of the Caccioppoli constant.

    For every coefficient family satisfying the A6 clause-(B) caps on □_{k+1} against ANY positive comparator, the Caccioppoli constant on the child □_k is bounded by the sample-free rootClauseBCaccUniform. The comparator sigma cancels inside stepSevenThetaRatio_le_of_caps — this is why the bound is σ-free as well.

    2. Monotonicity of the composite prefactor in its C_cacc slot #

    source
    theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseBCg_mono_ccacc (d : ℕ) {Ccacc Ccacc' Cosc CBc : ℝ} (hCosc : 0 ≤ Cosc) (h : Ccacc ≤ Ccacc') :
    rootClauseBCg d Ccacc Cosc CBc ≤ rootClauseBCg d Ccacc' Cosc CBc

    rootClauseBCg is monotone in C_cacc: it is 3^{3d+1/4}·C_cacc·(…) with both cofactors nonnegative.

    source
    theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseBPrefactor_mono_ccacc (d : ℕ) {Cch Ccacc Ccacc' Cosc CBc CB Ctr CWG CdM : ℝ} (hCch : 0 ≤ Cch) (hCosc : 0 ≤ Cosc) (hCB : 0 ≤ CB) (hCtr : 0 ≤ Ctr) (hCWG : 0 ≤ CWG) (hCdM : 0 ≤ CdM) (h : Ccacc ≤ Ccacc') :
    rootClauseBPrefactor d Cch Ccacc Cosc CBc CB Ctr CWG CdM ≤ rootClauseBPrefactor d Cch Ccacc' Cosc CBc CB Ctr CWG CdM

    The composite clause-(B) prefactor is monotone in C_cacc. The two sign conditions on the brackets are exactly the endpoint's own nonnegativity binders.