UpperCollarBandMeanConsumption

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

Literal consumption of the collar copy of the tuned band mean

This file sums the literal ninth named summand over Whitney layers at one translated strict descendant. The pointwise layer estimate is the cap/mass-interpolated estimate from UpperCollarBandMeanProfile; the only random factor left after summation is the actual collar power 3 ^ ((gamma + 2 b) hsep) read at the translated sample.

The frozen profile gates are used internally to price that power. No summability, domination, or probabilistic proposition is supplied by a caller. The finite coordinate trace is also formed here, before any cube maximum. These declarations are internal Provider results and make no source-node or development-status claim.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBandMeanPowerScale {d : ℕ} (M : ABKModel d) (sigma : ℝ) : ℝ

The exact hsep-power scale furnished by e.hsep.tails.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBandMeanPowerScale_nonneg {d : ℕ} (M : ABKModel d) (sigma : ℝ) : 0 ≤ probeSharpCollarBandMeanPowerScale M sigma

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.isBigOWith_upperProfileTarget_slstarPowerTerm {d : ℕ} (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M (m - 1) E) {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hmax : max (Real.exp (profileAuxiliaryConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E) (hEgamma : ↑E ≤ M.gamma ^ (-(1 / 5))) : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma (upperProfileTargetSigma sigma)) (Multiscale.slstarPowerTerm M R.scale (↑E) bfaProfileB M.gamma) (probeSharpCollarBandMeanPowerScale M sigma)

The frozen gates price the exact collar hsep power at the target upper profile exponent.