UpperBandMeanConsumption

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

Exact consumption of the framed band-mean lane

This file connects the deterministic deep-band mean to its literal named good-cell summand in the framed strict-descendant envelope. The random separation factor is split pointwise into its deterministic 2 branch and the explicit hsep residual. The ordinary branch is exactly the previously proved band-mean shift profile; the rare branch is priced directly as a deterministic multiple of the hsep residual, without introducing a fictitious random input.

Almost-everywhere summability of the translated rare layers is derived from their layerwise stretched-exponential bounds. Only one good-cell band-mean coordinate lane is treated. Root, collar, the other named lanes, the complete envelope, the cutoff observable, and the source-facing upper theorem remain outside this file.

Common-depth terminal specialization

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpBandMeanTunedBaseTerm {d : ℕ} (M : ABKModel d) (E : ℝ) (k n : ℕ) : ℝ

The deterministic carrier of literal named summand 3 at the common source-compatible depth.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpBandMeanTunedCoordinateCoeff {d : ℕ} (M : ABKModel d) (E : ℝ) (k : ℕ) (j : Fin d) : ℝ

The deterministic coefficient remaining after summing the tuned Whitney layers for one basis coordinate.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedBandMeanTunedCoordinateWhitneySum {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (E : ℝ) (j : Fin d) (omega : Cutoff.CutoffSample d) : ℝ

The literal real-valued Whitney sum of named summand 3 at the common depth and translated strict descendant.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpBandMeanTunedBaseTerm_nonneg {d : ℕ} (M : ABKModel d) (E : ℝ) (k n : ℕ) : 0 ≤ probeSharpBandMeanTunedBaseTerm M E k n

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpBandMeanTunedCoordinateCoeff_nonneg {d : ℕ} (M : ABKModel d) (E : ℝ) (k : ℕ) (j : Fin d) : 0 ≤ probeSharpBandMeanTunedCoordinateCoeff M E k j

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.summable_probeSharpBandMeanTunedBaseTerm {d : ℕ} (M : ABKModel d) (E : ℝ) (k : ℕ) : Summable fun (n : ℕ) => probeSharpBandMeanTunedBaseTerm M E k n

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedGoodWavePart_bandMean_tuned_le_ordinary_add_rare {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 }} (hstate : 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))) (n : ℕ) (j : Fin d) (omega : Cutoff.CutoffSample d) : Multiscale.probeSharpFramedGoodWavePart M R.scale (↑E) bfaProfileB (collarBandMeanDepth M ↑E) n (m - 1) (HCPolySupport.basisVec j) (fun (_eta : Cutoff.CutoffSample d) => waveBandMean (probeDeepBandMeanAmplitude d) M.gamma (collarBandMeanDepth M ↑E) ^ 2) (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega) ≤ 2 * (Multiscale.probeMeanGoodWaveConst M * HCPolySupport.vecNormSq (HCPolySupport.basisVec j) * probeSharpBandMeanTunedBaseTerm M (↑E) k n) + Multiscale.probeSharpAfterBandHsepResidual M R.scale (↑E) (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega) * (Multiscale.probeMeanGoodWaveConst M * HCPolySupport.vecNormSq (HCPolySupport.basisVec j) * probeSharpBandMeanTunedBaseTerm M (↑E) k n)

The literal tuned band-mean layer is bounded by its deterministic branch and the explicit hsep-residual branch.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedBandMeanTunedCoordinateWhitneySum_le_split {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 }} (hstate : 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))) (j : Fin d) (omega : Cutoff.CutoffSample d) : probeSharpFramedBandMeanTunedCoordinateWhitneySum M m R (↑E) j omega ≤ 2 * probeSharpBandMeanTunedCoordinateCoeff M (↑E) k j + Multiscale.probeSharpAfterBandHsepResidual M R.scale (↑E) (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega) * probeSharpBandMeanTunedCoordinateCoeff M (↑E) k j

The literal tuned Whitney sum for one coordinate has an exact deterministic-plus-residual majorant.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.two_mul_probeSharpBandMeanTunedCoordinateCoeff_le_shiftConst {d : ℕ} (M : ABKModel d) {E : ℝ} (hE : 1 ≤ E) (hcstarE : (Disorder.cstar M)⁻¹ ≤ E) (hEgamma : E ≤ M.gamma ^ (-(1 / 5))) (k : ℕ) (j : Fin d) : 2 * probeSharpBandMeanTunedCoordinateCoeff M E k j ≤ probeSharpBandMeanCoordinateShiftConst d

Twice the tuned deterministic coordinate coefficient fits the existing dimension-only band-mean shift budget.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpBandMeanTunedOutputConst (d : ℕ) : ℝ

One dimension-only choice pays the tuned deterministic trace, the profile gate, and the rare prefactor absorption.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpBandMeanTunedOutputConst_pos {d : ℕ} (hd : 2 ≤ d) : 0 < probeSharpBandMeanTunedOutputConst d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.exists_good_band_mean_tuned_finite_trace_split {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 }} (hstate : Frozen.Section3.inductionState M (m - 1) E) {sigma Cup : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hmax : max (Real.exp (Cup / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E) (hEgamma : ↑E ≤ M.gamma ^ (-(1 / 5))) (houtput : probeSharpBandMeanTunedOutputConst d ≤ Cup) : ∃ (ordinary : Cutoff.CutoffSample d → ℝ) (rare : Cutoff.CutoffSample d → ℝ) (rareScale : ℝ), (∀ (omega : Cutoff.CutoffSample d), 0 ≤ ordinary omega) ∧ Measurable ordinary ∧ (∀ (omega : Cutoff.CutoffSample d), 0 ≤ rare omega) ∧ Measurable rare ∧ (∀ (omega : Cutoff.CutoffSample d), ∑ j : Fin d, probeSharpFramedBandMeanTunedCoordinateWhitneySum M m R (↑E) j omega ≤ ordinary omega + rare omega) ∧ (∀ (omega : Cutoff.CutoffSample d), ∑ j : Fin d, ∑' (n : ℕ), ENNReal.ofReal (Multiscale.probeSharpFramedGoodWavePart M R.scale (↑E) bfaProfileB (collarBandMeanDepth M ↑E) n (m - 1) (HCPolySupport.basisVec j) (fun (_eta : Cutoff.CutoffSample d) => waveBandMean (probeDeepBandMeanAmplitude d) M.gamma (collarBandMeanDepth M ↑E) ^ 2) (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega)) = ENNReal.ofReal (∑ j : Fin d, probeSharpFramedBandMeanTunedCoordinateWhitneySum M m R (↑E) j omega)) ∧ (∀ (omega : Cutoff.CutoffSample d), ∑ j : Fin d, ∑' (n : ℕ), ENNReal.ofReal (Multiscale.probeSharpFramedGoodWavePart M R.scale (↑E) bfaProfileB (collarBandMeanDepth M ↑E) n (m - 1) (HCPolySupport.basisVec j) (fun (_eta : Cutoff.CutoffSample d) => waveBandMean (probeDeepBandMeanAmplitude d) M.gamma (collarBandMeanDepth M ↑E) ^ 2) (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega)) ≤ ENNReal.ofReal (ordinary omega) + ENNReal.ofReal (rare omega)) ∧ (∀ (omega : Cutoff.CutoffSample d), ordinary omega ≤ Cup) ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 3)) rare rareScale ∧ 0 ≤ rareScale ∧ rareScale ≤ Real.exp (-(Cup⁻¹ * ((↑E)⁻¹ ^ 2 * M.gamma⁻¹))) ^ 8

Terminal finite-coordinate split for literal named summand 3 at the common tuned depth. Its ordinary witness is a bounded deterministic shift; only the explicit hsep residual occupies the target Orlicz lane.