UpperCollarBaseProfile #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Literal collar-base profile #
This file estimates the seventh summand of
probeSharpFramedLayerNamedSum, namely the literal collar base term. It uses
both available bounds on assemblyBad: the density cap and the total Whitney
layer mass. Their geometric-mean interpolation supplies the decay needed to
sum the collar growth.
The profile first retains k₀ as an explicit deterministic parameter. Its
terminal section then specializes to the common small dimension-dependent
choice collarBandMeanDepth and absorbs the resulting square-root cap decay
into the local eighth-power rare scale.
noncomputable def
Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBaseCapHalf
{d : ℕ}
(M : ABKModel d)
(E : ℝ)
(k₀ : ℕ)
:
Square root of the deterministic collar density cap.
Equations
Instances For
noncomputable def
Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBaseMassHalfConst
(d : ℕ)
:
Square root of the dimension-only Whitney layer-mass prefactor.
Equations
Instances For
noncomputable def
Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBaseLayerScale
{d : ℕ}
(M : ABKModel d)
(E : ℝ)
(k₀ n : ℕ)
:
The deterministic coordinate scale in the literal collar-base layer bound. Its tuned-depth factor is deliberately retained.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBaseCapHalf_nonneg
{d : ℕ}
(M : ABKModel d)
(E : ℝ)
(k₀ : ℕ)
:
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.assemblyBad_le_collarBase_geometricMean
{d : ℕ}
(M : ABKModel d)
(E : ℝ)
(hs k₀ n : ℕ)
:
Multiscale.assemblyBad M E hs k₀ n ≤ √(probeSharpCollarBandMeanCapEnvelope M E k₀ * Multiscale.probeSharpLayerMassEnvelope d n)
Interpolation of the two literal assemblyBad bounds.
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.sqrt_probeSharpLayerMassEnvelope_eq_collarBase
(d n : ℕ)
:
Exact square-root Whitney mass profile.
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBase_geometricMean_eq
{d : ℕ}
(M : ABKModel d)
(E : ℝ)
(k₀ n : ℕ)
:
√(probeSharpCollarBandMeanCapEnvelope M E k₀ * Multiscale.probeSharpLayerMassEnvelope d n) = probeSharpCollarBaseCapHalf M E k₀ * probeSharpCollarBaseMassHalfConst d * 3 ^ (-↑n / 2)
Exact factorization of the interpolated bad mass.
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarBaseTerm_basisVec_le
{d : ℕ}
(hd : 2 ≤ d)
(M : ABKModel d)
(root : ℤ)
(E : ℝ)
(k₀ n : ℕ)
(j : Fin d)
(omega : Cutoff.CutoffSample d)
:
Multiscale.probeSharpFramedCollarBaseTerm M root E bfaProfileB k₀ n (HCPolySupport.basisVec j)
(Affine.superposedGradConst d) omega ≤ probeSharpCollarBaseLayerScale M E k₀ n * Multiscale.slstarPowerTerm M root E bfaProfileB M.gamma omega
The actual literal collar-base summand in one Whitney layer is bounded by the target hsep power times a summable deterministic layer profile.
Whitney sum, translation, and finite-coordinate trace #
noncomputable def
Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarBaseCoordinateLane
{d : ℕ}
(M : ABKModel d)
(R : HCPolySupport.TriadicCube d)
(E : ℝ)
(k₀ : ℕ)
(j : Fin d)
(omega : Cutoff.CutoffSample d)
:
The literal collar-base coordinate lane at one translated cube.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarBaseCoordinateENNRealLane
{d : ℕ}
(M : ABKModel d)
(R : HCPolySupport.TriadicCube d)
(E : ℝ)
(k₀ : ℕ)
(j : Fin d)
(omega : Cutoff.CutoffSample d)
:
The same literal coordinate lane in the envelope's shape.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBaseCoordinateMajorant
{d : ℕ}
(M : ABKModel d)
(R : HCPolySupport.TriadicCube d)
(E : ℝ)
(k₀ : ℕ)
(omega : Cutoff.CutoffSample d)
:
Pointwise majorant after summing the deterministic Whitney profile.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarBaseTraceLane
{d : ℕ}
(M : ABKModel d)
(R : HCPolySupport.TriadicCube d)
(E : ℝ)
(k₀ : ℕ)
(omega : Cutoff.CutoffSample d)
:
The literal finite-coordinate collar-base trace.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.summable_probeSharpCollarBaseLayerScale
{d : ℕ}
(M : ABKModel d)
(E : ℝ)
(k₀ : ℕ)
:
Summable fun (n : ℕ) => probeSharpCollarBaseLayerScale M E k₀ n
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.summable_probeSharpFramedCollarBaseCoordinateLayer
{d : ℕ}
(hd : 2 ≤ d)
(M : ABKModel d)
(R : HCPolySupport.TriadicCube d)
(E : ℝ)
(k₀ : ℕ)
(j : Fin d)
(omega : Cutoff.CutoffSample d)
:
Summable fun (n : ℕ) =>
Multiscale.probeSharpFramedCollarBaseTerm M R.scale E bfaProfileB k₀ n (HCPolySupport.basisVec j)
(Affine.superposedGradConst d) (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega)
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarBaseCoordinateLane_nonneg
{d : ℕ}
(hd : 2 ≤ d)
(M : ABKModel d)
(R : HCPolySupport.TriadicCube d)
(E : ℝ)
(k₀ : ℕ)
(j : Fin d)
(omega : Cutoff.CutoffSample d)
:
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.measurable_probeSharpFramedCollarBaseCoordinateLane
{d : ℕ}
(M : ABKModel d)
(R : HCPolySupport.TriadicCube d)
(E : ℝ)
(k₀ : ℕ)
(j : Fin d)
:
Measurable (probeSharpFramedCollarBaseCoordinateLane M R E k₀ j)
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarBaseCoordinateLane_le_majorant
{d : ℕ}
(hd : 2 ≤ d)
(M : ABKModel d)
(R : HCPolySupport.TriadicCube d)
(E : ℝ)
(k₀ : ℕ)
(j : Fin d)
(omega : Cutoff.CutoffSample d)
:
probeSharpFramedCollarBaseCoordinateLane M R E k₀ j omega ≤ probeSharpCollarBaseCoordinateMajorant M R E k₀ omega
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarBaseCoordinateENNRealLane_eq
{d : ℕ}
(hd : 2 ≤ d)
(M : ABKModel d)
(R : HCPolySupport.TriadicCube d)
(E : ℝ)
(k₀ : ℕ)
(j : Fin d)
(omega : Cutoff.CutoffSample d)
:
probeSharpFramedCollarBaseCoordinateENNRealLane M R E k₀ j omega = ENNReal.ofReal (probeSharpFramedCollarBaseCoordinateLane M R E k₀ j omega)
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.isBigOWith_upperProfileTarget_probeSharpCollarBaseCoordinateMajorant
{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)))
(k₀ : ℕ)
:
HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M))
(HCPolySupport.IndependentSums.gammaSigma (upperProfileTargetSigma sigma))
(probeSharpCollarBaseCoordinateMajorant M R (↑E) k₀) (probeSharpCollarBaseCoordinateScale M (↑E) sigma k₀)
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.isBigOWith_upperProfileTarget_probeSharpFramedCollarBaseCoordinateLane
{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)))
(k₀ : ℕ)
(j : Fin d)
:
HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M))
(HCPolySupport.IndependentSums.gammaSigma (upperProfileTargetSigma sigma))
(probeSharpFramedCollarBaseCoordinateLane M R (↑E) k₀ j) (probeSharpCollarBaseCoordinateScale M (↑E) sigma k₀)
The actual translated literal collar-base coordinate has the target rare exponent, with no supplied estimate premise.
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarBaseCoordinateLane_eq
{d : ℕ}
(M : ABKModel d)
(R : HCPolySupport.TriadicCube d)
(E : ℝ)
(k₀ : ℕ)
(j j' : Fin d)
:
probeSharpFramedCollarBaseCoordinateLane M R E k₀ j = probeSharpFramedCollarBaseCoordinateLane M R E k₀ j'
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarBaseTraceLane_eq_dimension_mul
{d : ℕ}
(M : ABKModel d)
(R : HCPolySupport.TriadicCube d)
(E : ℝ)
(k₀ : ℕ)
(j : Fin d)
(omega : Cutoff.CutoffSample d)
:
probeSharpFramedCollarBaseTraceLane M R E k₀ omega = ↑d * probeSharpFramedCollarBaseCoordinateLane M R E k₀ j omega
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarBaseTraceLane_nonneg
{d : ℕ}
(hd : 2 ≤ d)
(M : ABKModel d)
(R : HCPolySupport.TriadicCube d)
(E : ℝ)
(k₀ : ℕ)
(omega : Cutoff.CutoffSample d)
:
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.measurable_probeSharpFramedCollarBaseTraceLane
{d : ℕ}
(M : ABKModel d)
(R : HCPolySupport.TriadicCube d)
(E : ℝ)
(k₀ : ℕ)
:
Measurable (probeSharpFramedCollarBaseTraceLane M R E k₀)
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.isBigOWith_upperProfileTarget_probeSharpFramedCollarBaseTraceLane
{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)))
(k₀ : ℕ)
:
HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M))
(HCPolySupport.IndependentSums.gammaSigma (upperProfileTargetSigma sigma))
(probeSharpFramedCollarBaseTraceLane M R (↑E) k₀) (probeSharpCollarBaseTraceScale d M (↑E) sigma k₀)
Tuned-depth terminal estimate #
noncomputable def
Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBaseTunedTracePrefactor
(d : ℕ)
:
Dimension-only prefactor remaining after the tuned collar density collapse, Whitney summation, finite-coordinate trace, and hsep-power estimate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBaseTunedOutputConst
(d : ℕ)
:
Dimension-only threshold which pays the profile gate, tuned-depth rounding, the collar-base trace prefactor, and eight copies of the frozen rare scale.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.isBigOWith_upperProfileTarget_probeSharpFramedCollarBaseTraceLane_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 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 : probeSharpCollarBaseTunedOutputConst d ≤ Cup)
:
HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M))
(HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 3))
(probeSharpFramedCollarBaseTraceLane M R (↑E) (collarBandMeanDepth M ↑E))
(3 ^ (M.gamma * (↑k + 1)) * Real.exp (-(Cup⁻¹ * ((↑E)⁻¹ ^ 2 * M.gamma⁻¹))) ^ 8)
The literal finite-coordinate collar-base trace at the common tuned depth has the exact local per-descendant rare scale required by the upper assembly.