UpperDeepBandTailOrdinaryLane

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

The ordinary centered deep-band tail on the actual descendant carrier

This file constructs the random ordinary branch of the centered deep-band tail, rather than only its deterministic profile. The Whitney layers are summed at a strictly positive geometric majorant, so their Gamma_1 estimates give both the countable weak-Orlicz bound and almost-everywhere summability. The centered sum is then evaluated at the translated cutoff sample belonging to each descendant cube.

The resulting per-cube estimate has the exact cstar⁻¹ * gamma dependence and the source depth growth expected by the joint grid/depth maximum. The final part of the file also treats the literal good-cell centered-tail named summand at the tuned collar-band depth, including its ordinary/rare finite-coordinate split. Other named lanes and the complete cutoff observable remain separate.

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

A strictly positive enlargement of the deterministic ordinary layer constant. The added one is used only to make every summability scale positive; it is absorbed into a dimension-only constant.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpDeepBandTailOrdinaryAnalyticLayerConst d = 1 + Algsuperdiff.Section3.Provider.Multiscale.probeSharpDeepBandTailOrdinaryLayerConst d

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

The geometric positive scale used for one ordinary Whitney layer.

Equations

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

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

The exact geometric-series constant for the enlarged ordinary scales.

Equations

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

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

The dimension-only per-cube constant after the Whitney Gamma_1 triangle inequality and the literal outer mean coefficient are restored.

Equations

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

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

The dimension-only per-cube constant after the finite coordinate trace.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpDeepBandTailTunedBaseTerm {d : ℕ} (M : ABKModel d) (root : ℤ) (k₀ k n : ℕ) (omega : Cutoff.CutoffSample d) : ℝ

The unframed centered-tail square with an explicit band depth. This is the common carrier used by both sides of the separation split.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpDeepBandTailTunedBaseScale {d : ℕ} (M : ABKModel d) (root : ℤ) (k₀ k n : ℕ) : ℝ

The exact Gamma-one scale of the explicit-depth centered-tail carrier.

Equations

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

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

Dimension-only trace prefactor for the tuned rare good centered-tail lane.

Equations

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

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

Dimension-only threshold paying the tuned depth, ordinary trace constant, and the eighth-power exceptional reserve.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpDeepBandTailOrdinaryAnalyticLayerConst_pos (d : ℕ) : 0 < probeSharpDeepBandTailOrdinaryAnalyticLayerConst d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpDeepBandTailOrdinaryAnalyticLayerScale_pos {d : ℕ} (M : ABKModel d) (n : ℕ) : 0 < probeSharpDeepBandTailOrdinaryAnalyticLayerScale M n

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpDeepBandTailOrdinaryAnalyticSumConst_pos (d : ℕ) : 0 < probeSharpDeepBandTailOrdinaryAnalyticSumConst d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.summable_probeSharpDeepBandTailOrdinaryAnalyticLayerScale {d : ℕ} (M : ABKModel d) : Summable fun (n : ℕ) => probeSharpDeepBandTailOrdinaryAnalyticLayerScale M n

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.tsum_probeSharpDeepBandTailOrdinaryAnalyticLayerScale_eq {d : ℕ} (M : ABKModel d) : ∑' (n : ℕ), probeSharpDeepBandTailOrdinaryAnalyticLayerScale M n = probeSharpDeepBandTailOrdinaryAnalyticSumConst d * M.gamma

Literal good centered-tail lane at the tuned collar depth

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpDeepBandTailTunedOutputConst_pos (d : ℕ) : 0 < probeSharpDeepBandTailTunedOutputConst d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.exists_tunedDeepBandTail_good_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 }} (hS : 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 : max (profileAuxiliaryConst d) (probeSharpDeepBandTailTunedOutputConst d) ≤ Cup) : ∃ (ordinary : Cutoff.CutoffSample d → ℝ) (rare : Cutoff.CutoffSample d → ℝ) (ordinaryScale : ℝ) (rareScale : ℝ), (∀ (omega : Cutoff.CutoffSample d), 0 ≤ ordinary omega) ∧ Measurable ordinary ∧ (∀ (omega : Cutoff.CutoffSample d), 0 ≤ rare omega) ∧ Measurable rare ∧ (∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∑ j : Fin d, ∑' (n : ℕ), Multiscale.probeSharpFramedGoodWavePart M R.scale (↑E) bfaProfileB (collarBandMeanDepth M ↑E) n (m - 1) (HCPolySupport.basisVec j) (fun (eta : Cutoff.CutoffSample d) => probeDeepBandGaugedTail M (HCPolySupport.originCube d R.scale) (probeSharpLayerAnchor R.scale bfaProfileB (collarBandMeanDepth M ↑E) n) (collarBandMeanDepth M ↑E) (collarBandMeanDepth M ↑E) eta ^ 2) (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega) ≤ ordinary omega + rare omega) ∧ (∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∑ 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) => probeDeepBandGaugedTail M (HCPolySupport.originCube d R.scale) (probeSharpLayerAnchor R.scale bfaProfileB (collarBandMeanDepth M ↑E) n) (collarBandMeanDepth M ↑E) (collarBandMeanDepth M ↑E) eta ^ 2) (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega)) = ENNReal.ofReal (∑ j : Fin d, ∑' (n : ℕ), Multiscale.probeSharpFramedGoodWavePart M R.scale (↑E) bfaProfileB (collarBandMeanDepth M ↑E) n (m - 1) (HCPolySupport.basisVec j) (fun (eta : Cutoff.CutoffSample d) => probeDeepBandGaugedTail M (HCPolySupport.originCube d R.scale) (probeSharpLayerAnchor R.scale bfaProfileB (collarBandMeanDepth M ↑E) n) (collarBandMeanDepth M ↑E) (collarBandMeanDepth M ↑E) eta ^ 2) (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega))) ∧ (∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∑ 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) => probeDeepBandGaugedTail M (HCPolySupport.originCube d R.scale) (probeSharpLayerAnchor R.scale bfaProfileB (collarBandMeanDepth M ↑E) n) (collarBandMeanDepth M ↑E) (collarBandMeanDepth M ↑E) eta ^ 2) (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega)) ≤ ENNReal.ofReal (ordinary omega) + ENNReal.ofReal (rare omega)) ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) ordinary ordinaryScale ∧ 0 ≤ ordinaryScale ∧ ordinaryScale ≤ upperSaturatedPerCubeAmplitude Cup (Disorder.cstar M) M.gamma k ∧ 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

Finite-coordinate split for literal summand four of the named sharp envelope at the tuned collar-band depth. The pointwise comparison is stated on the full-measure set where the nonnegative deep-tail Whitney series are summable.