UpperDeepBandTailConsumption #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Exact consumption of the translated framed deep-band-tail lane #
This file treats the good-cell and collar deep-tail summands of the framed descendant envelope, preserving the descendant scale and translation. It does not assert root aggregation, the complete envelope, or source-node status.
noncomputable def
Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarDeepTailLayer
{d : ℕ}
(M : ABKModel d)
(m : ℤ)
(R : HCPolySupport.TriadicCube d)
(E : ℝ)
(j : Fin d)
(n : ℕ)
(omega : Cutoff.CutoffSample d)
:
One exact translated layer of the literal collar deep-tail summand.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarDeepTailTraceLane
{d : ℕ}
(M : ABKModel d)
(m : ℤ)
(R : HCPolySupport.TriadicCube d)
(E : ℝ)
(omega : Cutoff.CutoffSample d)
:
The finite-coordinate real trace of the literal collar deep-tail summand.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarDeepTailLayer_nonneg
{d : ℕ}
(M : ABKModel d)
(m : ℤ)
(R : HCPolySupport.TriadicCube d)
(E : ℝ)
(j : Fin d)
(n : ℕ)
(omega : Cutoff.CutoffSample d)
:
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.measurable_probeSharpFramedCollarDeepTailLayer
{d : ℕ}
(M : ABKModel d)
(m : ℤ)
(R : HCPolySupport.TriadicCube d)
(E : ℝ)
(j : Fin d)
(n : ℕ)
:
Measurable (probeSharpFramedCollarDeepTailLayer M m R E j n)
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.collarDeepTail_coordinate_isBigOWith_and_ae_summable
{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)))
(hCup : max (profileAuxiliaryConst d) (collarBandMeanDepthThreshold d) ≤ Cup)
(j : Fin d)
:
have k₀ := collarBandMeanDepth M ↑E;
have tailA := HCPolySupport.IndependentSums.gammaTriangleConst 2 * (probeDeepBandGainRootConst d * 3 * √2);
have D₀ :=
Multiscale.probeMeanGoodWaveConst M * (5 * ↑d ^ 2) * (4 * Affine.superposedGradConst d ^ 2 * probeSharpCollarBandMeanCapQuarter M (↑E) k₀ * probeSharpCollarBandMeanMassQuarterConst d * 3 ^ (2 * bfaProfileB * ↑k₀) * 3 ^ (1 / 16));
have B₀ := D₀ * (64 * superposedFluxHsepConst ^ 3 * (tailA ^ 2 * 81) * M.gamma);
HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M))
(HCPolySupport.IndependentSums.gammaSigma (upperProfileTargetSigma sigma))
(fun (omega : Cutoff.CutoffSample d) => ∑' (n : ℕ), probeSharpFramedCollarDeepTailLayer M m R (↑E) j n omega)
(HCPolySupport.IndependentSums.gammaTriangleConst (upperProfileTargetSigma sigma) * (B₀ * (1 - whitneyDecayRatio)⁻¹)) ∧ ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), Summable fun (n : ℕ) => probeSharpFramedCollarDeepTailLayer M m R (↑E) j n omega
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarDeepTailTraceLane_nonneg
{d : ℕ}
(M : ABKModel d)
(m : ℤ)
(R : HCPolySupport.TriadicCube d)
(E : ℝ)
(omega : Cutoff.CutoffSample d)
:
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.measurable_probeSharpFramedCollarDeepTailTraceLane
{d : ℕ}
(M : ABKModel d)
(m : ℤ)
(R : HCPolySupport.TriadicCube d)
(E : ℝ)
:
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.ae_ofReal_probeSharpFramedCollarDeepTailTraceLane_eq_sum_tsum
{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)))
(hCup : max (profileAuxiliaryConst d) (collarBandMeanDepthThreshold d) ≤ Cup)
:
∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ENNReal.ofReal (probeSharpFramedCollarDeepTailTraceLane M m R (↑E) omega) = ∑ j : Fin d, ∑' (n : ℕ), ENNReal.ofReal (probeSharpFramedCollarDeepTailLayer M m R (↑E) j n omega)
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.collarDeepTail_trace_isBigOWith
{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)))
(hCup : max (profileAuxiliaryConst d) (collarBandMeanDepthThreshold d) ≤ Cup)
:
have k₀ := collarBandMeanDepth M ↑E;
have tailA := HCPolySupport.IndependentSums.gammaTriangleConst 2 * (probeDeepBandGainRootConst d * 3 * √2);
have D₀ :=
Multiscale.probeMeanGoodWaveConst M * (5 * ↑d ^ 2) * (4 * Affine.superposedGradConst d ^ 2 * probeSharpCollarBandMeanCapQuarter M (↑E) k₀ * probeSharpCollarBandMeanMassQuarterConst d * 3 ^ (2 * bfaProfileB * ↑k₀) * 3 ^ (1 / 16));
have B₀ := D₀ * (64 * superposedFluxHsepConst ^ 3 * (tailA ^ 2 * 81) * M.gamma);
HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M))
(HCPolySupport.IndependentSums.gammaSigma (upperProfileTargetSigma sigma))
(probeSharpFramedCollarDeepTailTraceLane M m R ↑E)
(↑d * (HCPolySupport.IndependentSums.gammaTriangleConst (upperProfileTargetSigma sigma) * (B₀ * (1 - whitneyDecayRatio)⁻¹)))
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.collarDeepTail_traceScale_le_exp
{d : ℕ}
(hd : 2 ≤ d)
(M : ABKModel d)
{E : { E : ℝ // 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)))
(hCup : max (profileAuxiliaryConst d) (collarBandMeanDepthThreshold d) ≤ Cup)
:
have k₀ := collarBandMeanDepth M ↑E;
have tailA := HCPolySupport.IndependentSums.gammaTriangleConst 2 * (probeDeepBandGainRootConst d * 3 * √2);
have D₀ :=
Multiscale.probeMeanGoodWaveConst M * (5 * ↑d ^ 2) * (4 * Affine.superposedGradConst d ^ 2 * probeSharpCollarBandMeanCapQuarter M (↑E) k₀ * probeSharpCollarBandMeanMassQuarterConst d * 3 ^ (2 * bfaProfileB * ↑k₀) * 3 ^ (1 / 16));
have B₀ := D₀ * (64 * superposedFluxHsepConst ^ 3 * (tailA ^ 2 * 81) * M.gamma);
have K :=
↑d * upperAfterBandRareTriangleConst * (probeMeanGoodWaveDimensionConst d * (5 * ↑d ^ 2) * (4 * Affine.superposedGradConst d ^ 2 * probeSharpCollarBandMeanMassQuarterConst d * 3 ^ (1 / 16)) * collarBandMeanTunedCapPrefactor d * (64 * superposedFluxHsepConst ^ 3 * (tailA ^ 2 * 81)) * (1 - whitneyDecayRatio)⁻¹);
↑d * (HCPolySupport.IndependentSums.gammaTriangleConst (upperProfileTargetSigma sigma) * (B₀ * (1 - whitneyDecayRatio)⁻¹)) ≤ K * Real.exp (-(collarBandMeanTunedDecayRate d * ((↑E)⁻¹ ^ 2 * M.gamma⁻¹)))
noncomputable def
Algsuperdiff.Section3.Provider.CoarseEllipticity.collarDeepTailTunedOutputConst
(d : ℕ)
:
Dimension-only threshold for the direct tuned collar deep-tail trace.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.collarDeepTail_trace_isBigOWith_frozenReserve
{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 : collarDeepTailTunedOutputConst d ≤ Cup)
:
Literal named summand 10 at one strict descendant, with the exact local eighth-power rare reserve used by the upper assembly.