UpperAfterBandOrdinaryProfile

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

Outer coefficient for the ordinary after-band profile

This file restores the exact outer mean coefficient and the squared norm of a coordinate vector to the normalized deterministic 2 branch of the framed after-band estimate. It shows that the resulting strict-descendant layer sum has the algebraic amplitude consumed by UpperSaturatedBlockProfile.

The complementary random hsep branch, the depth-zero/root row, and every other wave, collar, base, and deep-band lane are absent.

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

Dimension-only coefficient left after extracting the exact cstar M⁻¹ factor from probeMeanGoodWaveConst M. This definition does not assert an estimate for any omitted lane.

Equations

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

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

The unframed after-band carrier at the common collar-band depth.

Equations

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

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

The exact Gamma_1 scale of the common-depth carrier.

Equations

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

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

Dimension-only coefficient of the common-depth ordinary trace scale.

Equations

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

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

Dimension-only prefactor of the common-depth rare trace scale.

Equations

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

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

A single dimension-only gate for the common-depth good after-band split.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpAfterBandOrdinaryPerCubeConst_nonneg {d : ℕ} (hd : 2 ≤ d) : 0 ≤ probeSharpAfterBandOrdinaryPerCubeConst d

The literal good after-band lane at the common tuned depth

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cstarInv_mul_exp_neg_afterBandRate_le_halfRate {cstarInv rate E X : ℝ} (hrate : 0 < rate) (hE : 1 ≤ E) (hlarge : 2 * rate⁻¹ ≤ E) (hX : E ^ 3 ≤ X) (hcstarInvE : cstarInv ≤ E) : cstarInv * Real.exp (-(rate * X)) ≤ Real.exp (-(rate / 2 * X))

Absorb an inverse-prefactor bound using the cubic after-band depth margin.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.exists_tunedAfterBand_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 : probeSharpAfterBandTunedOutputConst 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) => probeSharpAfterBandTerm M R.scale (probeSharpLayerAnchor R.scale bfaProfileB (collarBandMeanDepth M ↑E) n) (collarBandMeanDepth M ↑E) m 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) => probeSharpAfterBandTerm M R.scale (probeSharpLayerAnchor R.scale bfaProfileB (collarBandMeanDepth M ↑E) n) (collarBandMeanDepth M ↑E) m 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) => probeSharpAfterBandTerm M R.scale (probeSharpLayerAnchor R.scale bfaProfileB (collarBandMeanDepth M ↑E) n) (collarBandMeanDepth M ↑E) m 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) => probeSharpAfterBandTerm M R.scale (probeSharpLayerAnchor R.scale bfaProfileB (collarBandMeanDepth M ↑E) n) (collarBandMeanDepth M ↑E) m 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 ≤ 3 ^ (M.gamma * ↑(k + 1)) * Real.exp (-(Cup⁻¹ * ((↑E)⁻¹ ^ 2 * M.gamma⁻¹))) ^ 8

The literal fifth named lane at the common tuned depth, in the same ordinary/rare form consumed by the other good-wave estimates.