UpperCollarBandMeanProfile

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

Literal collar profile for the tuned band mean

This file prices the collar copy of the deterministic deep-band mean in one framed Whitney layer. The carrier is the literal ninth summand of probeSharpFramedLayerNamedSum: it retains the collar gradient factor, the square root of the actual assemblyBad minimum, and the descendant frame.

The load-bearing estimate uses both branches of assemblyBad. The bad mass is first bounded by the geometric mean of its density cap and its layer-mass cap; taking the square root already present in the wave lane therefore costs a fourth root. This leaves a summable 3^(-n/8) Whitney profile after the literal collar growth is paid. No domination proposition is supplied by a caller.

The deterministic cap scale is deliberately not absorbed here. In particular its factor at the tuned depth waveBandDepth 1 E gamma remains visible, so later code cannot silently assume that the percolation rate pays the fixed collar slope. These are internal Provider declarations and make no source-node or development-status claim.

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

The density cap with its decreasing hsep contribution enlarged at hsep = 0. It is deterministic and keeps both density mechanisms visible.

Equations

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

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

The fourth root of the deterministic collar cap.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBandMeanCapQuarter M E k₀ = √√(Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBandMeanCapEnvelope M E k₀)

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

The dimension-only fourth root of the Whitney mass prefactor.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBandMeanMassQuarterConst d = √√(6 * ↑d)

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

The exact collar/frame core multiplying the deterministic band square in one translated strict-descendant layer.

Equations

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

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

A dimension-only bound for the deterministic band coefficient.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBandMeanCapEnvelope_nonneg {d : ℕ} (M : ABKModel d) (E : ℝ) (k₀ : ℕ) : 0 ≤ probeSharpCollarBandMeanCapEnvelope M E k₀

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBandMeanCapQuarter_nonneg {d : ℕ} (M : ABKModel d) (E : ℝ) (k₀ : ℕ) : 0 ≤ probeSharpCollarBandMeanCapQuarter M E k₀

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBandMeanMassQuarterConst_nonneg (d : ℕ) : 0 ≤ probeSharpCollarBandMeanMassQuarterConst d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBandMeanLayerCore_nonneg {d : ℕ} (M : ABKModel d) (root : ℤ) (E : ℝ) (k₀ n : ℕ) (i : ℤ) (Cgrad : ℝ) (omega : Cutoff.CutoffSample d) : 0 ≤ probeSharpCollarBandMeanLayerCore M root E k₀ n i Cgrad omega

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.measurable_probeSharpCollarBandMeanLayerCore {d : ℕ} (M : ABKModel d) (root : ℤ) (E : ℝ) (k₀ n : ℕ) (i : ℤ) (Cgrad : ℝ) : Measurable (probeSharpCollarBandMeanLayerCore M root E k₀ n i Cgrad)

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.collarMassCap_le_probeSharpCollarBandMeanCapEnvelope {d : ℕ} (M : ABKModel d) (E : ℝ) (hs k₀ : ℕ) : Multiscale.collarMassCap M E hs k₀ ≤ probeSharpCollarBandMeanCapEnvelope M E k₀

The random collar mass cap is bounded by the deterministic hsep = 0 envelope.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.sqrt_assemblyBad_le_collarBandMean_fourthRoot {d : ℕ} (M : ABKModel d) (E : ℝ) (hs k₀ n : ℕ) : √(Multiscale.assemblyBad M E hs k₀ n) ≤ √√(probeSharpCollarBandMeanCapEnvelope M E k₀ * Multiscale.probeSharpLayerMassEnvelope d n)

at the square-root collar-wave carrier: using both branches of assemblyBad gives a fourth-root cap/mass interpolation.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.sqrt_sqrt_probeSharpLayerMassEnvelope_eq (d n : ℕ) : √√(Multiscale.probeSharpLayerMassEnvelope d n) = probeSharpCollarBandMeanMassQuarterConst d * 3 ^ (-↑n / 4)

Exact fourth-root form of the Whitney mass profile.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMean_fourthRoot_eq {d : ℕ} (M : ABKModel d) (E : ℝ) (k₀ n : ℕ) : √√(probeSharpCollarBandMeanCapEnvelope M E k₀ * Multiscale.probeSharpLayerMassEnvelope d n) = probeSharpCollarBandMeanCapQuarter M E k₀ * probeSharpCollarBandMeanMassQuarterConst d * 3 ^ (-↑n / 4)

The interpolated fourth root splits into the deterministic cap quarter and the exact geometric Whitney profile.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarWavePart_bandMean_eq {d : ℕ} (M : ABKModel d) (root : ℤ) (E : ℝ) (k₀ n : ℕ) (i : ℤ) (j : Fin d) (Cgrad : ℝ) (omega : Cutoff.CutoffSample d) : Multiscale.probeSharpFramedCollarWavePart M root E bfaProfileB k₀ n i (HCPolySupport.basisVec j) Cgrad (fun (_eta : Cutoff.CutoffSample d) => waveBandMean (probeDeepBandMeanAmplitude d) M.gamma k₀ ^ 2) omega = Multiscale.probeMeanGoodWaveConst M * HCPolySupport.vecNormSq (HCPolySupport.basisVec j) * (5 * ↑d ^ 2 * waveBandMean (probeDeepBandMeanAmplitude d) M.gamma k₀ ^ 2) * probeSharpCollarBandMeanLayerCore M root E k₀ n i Cgrad omega

The literal ninth named summand is exactly the deterministic band coefficient times the collar/frame core.