UpperCollarBandMeanTunedConsumption

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 UpperCollarBandMeanTunedProfile; 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.probeSharpFramedCollarBandMeanTunedCoordinateLane {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (E : ℝ) (j : Fin d) (omega : Cutoff.CutoffSample d) : ℝ

The real-valued literal collar band-mean coordinate lane at one translated strict descendant.

Equations

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

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

The same literal lane in the shape used by the framed envelope.

Equations

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

@[reducible, inline]

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

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

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBandMeanTunedPowerScale M sigma = Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBandMeanPowerScale M sigma

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

The deterministic Whitney sum times the exact collar-power scale.

Equations

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

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

The pointwise majorant left after Whitney summation.

Equations

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

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

The literal finite-coordinate collar band-mean trace at one strict descendant.

Equations

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

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

The literal finite-coordinate trace in the envelope's shape.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBandMeanTunedTraceScale (d : ℕ) (M : ABKModel d) (E sigma : ℝ) : ℝ

The exact finite-coordinate trace scale.

Equations

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

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.summable_probeSharpFramedCollarBandMeanTunedCoordinateLayer {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) {E : ℝ} (hE : 1 ≤ E) (hcstarE : (Disorder.cstar M)⁻¹ ≤ E) (hEgamma : E ≤ M.gamma ^ (-(1 / 5))) (j : Fin d) (omega : Cutoff.CutoffSample d) : Summable fun (n : ℕ) => Multiscale.probeSharpFramedCollarWavePart M R.scale E bfaProfileB (collarBandMeanDepth M E) n (m - 1) (HCPolySupport.basisVec j) (Affine.superposedGradConst d) (fun (_eta : Cutoff.CutoffSample d) => waveBandMean (probeDeepBandMeanAmplitude d) M.gamma (collarBandMeanDepth M E) ^ 2) (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega)

The literal real Whitney family is summable at every sample point.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarBandMeanTunedCoordinateLane_nonneg {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (E : ℝ) (j : Fin d) (omega : Cutoff.CutoffSample d) : 0 ≤ probeSharpFramedCollarBandMeanTunedCoordinateLane M m R E j omega

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.measurable_probeSharpFramedCollarBandMeanTunedCoordinateLane {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (E : ℝ) (j : Fin d) : Measurable (probeSharpFramedCollarBandMeanTunedCoordinateLane M m R E j)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarBandMeanTunedCoordinateLane_le_majorant {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) {E : ℝ} (hE : 1 ≤ E) (hcstarE : (Disorder.cstar M)⁻¹ ≤ E) (hEgamma : E ≤ M.gamma ^ (-(1 / 5))) (j : Fin d) (omega : Cutoff.CutoffSample d) : probeSharpFramedCollarBandMeanTunedCoordinateLane M m R E j omega ≤ probeSharpCollarBandMeanTunedCoordinateMajorant M R E omega

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarBandMeanTunedCoordinateENNRealLane_eq {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) {E : ℝ} (hE : 1 ≤ E) (hcstarE : (Disorder.cstar M)⁻¹ ≤ E) (hEgamma : E ≤ M.gamma ^ (-(1 / 5))) (j : Fin d) (omega : Cutoff.CutoffSample d) : probeSharpFramedCollarBandMeanTunedCoordinateENNRealLane M m R E j omega = ENNReal.ofReal (probeSharpFramedCollarBandMeanTunedCoordinateLane M m R E j omega)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.isBigOWith_upperProfileTarget_slstarPowerTerm_tuned {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) (probeSharpCollarBandMeanTunedPowerScale M sigma)

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.isBigOWith_upperProfileTarget_probeSharpCollarBandMeanTunedCoordinateMajorant {d : ℕ} (hd : 2 ≤ 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)) (probeSharpCollarBandMeanTunedCoordinateMajorant M R ↑E) (probeSharpCollarBandMeanTunedCoordinateScale M (↑E) sigma)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.isBigOWith_upperProfileTarget_probeSharpFramedCollarBandMeanTunedCoordinateLane {d : ℕ} (hd : 2 ≤ 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))) (j : Fin d) : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma (upperProfileTargetSigma sigma)) (probeSharpFramedCollarBandMeanTunedCoordinateLane M m R (↑E) j) (probeSharpCollarBandMeanTunedCoordinateScale M (↑E) sigma)

The actual translated coordinate lane inherits the target exponent from its proved pointwise majorant.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarBandMeanTunedCoordinateLane_eq {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (E : ℝ) (j j' : Fin d) : probeSharpFramedCollarBandMeanTunedCoordinateLane M m R E j = probeSharpFramedCollarBandMeanTunedCoordinateLane M m R E j'

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarBandMeanTunedTraceLane_eq_dimension_mul {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (E : ℝ) (j : Fin d) (omega : Cutoff.CutoffSample d) : probeSharpFramedCollarBandMeanTunedTraceLane M m R E omega = ↑d * probeSharpFramedCollarBandMeanTunedCoordinateLane M m R E j omega

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarBandMeanTunedTraceLane_nonneg {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (E : ℝ) (omega : Cutoff.CutoffSample d) : 0 ≤ probeSharpFramedCollarBandMeanTunedTraceLane M m R E omega

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.measurable_probeSharpFramedCollarBandMeanTunedTraceLane {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (E : ℝ) : Measurable (probeSharpFramedCollarBandMeanTunedTraceLane M m R E)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.isBigOWith_upperProfileTarget_probeSharpFramedCollarBandMeanTunedTraceLane {d : ℕ} (hd : 2 ≤ 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)) (probeSharpFramedCollarBandMeanTunedTraceLane M m R ↑E) (probeSharpCollarBandMeanTunedTraceScale d M (↑E) sigma)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarBandMeanTunedTraceENNRealLane_eq {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) {E : ℝ} (hE : 1 ≤ E) (hcstarE : (Disorder.cstar M)⁻¹ ≤ E) (hEgamma : E ≤ M.gamma ^ (-(1 / 5))) (omega : Cutoff.CutoffSample d) : probeSharpFramedCollarBandMeanTunedTraceENNRealLane M m R E omega = ENNReal.ofReal (probeSharpFramedCollarBandMeanTunedTraceLane M m R E omega)