SharpLayerEnvelope #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.seamSimplexObject_le_five_sharp_terms_probe
{d : ℕ}
(M : ABKModel d)
{m : ℤ}
{E b : ℝ}
{hn : ℕ → ℕ}
{n : ℕ}
(hstep : hn n ≤ hn (n + 1) + 1)
{ell L : ℤ}
{k₀ N g₀ : ℕ}
(hk₀ : 2 ≤ k₀)
(hN : k₀ < 3 ^ N)
(hm : m = ell + ↑k₀ + ↑g₀)
(htopL : ell + ↑k₀ ≤ L)
(omega : Cutoff.CutoffSample d)
:
Multiscale.seamSimplexObject M m hn n ell (Percolation.hsep M m E b omega) L omega ≤ 5 * ↑d ^ 2 * (Multiscale.waveHeadTerm M m E b ell omega ^ 2 + waveBandMean (probeDeepBandMeanAmplitude d) M.gamma k₀ ^ 2 + probeDeepBandGaugedTail M (HCPolySupport.originCube d m) ell k₀ N omega ^ 2 + probeSharpAfterBandTerm M m ell k₀ L omega ^ 2 + Multiscale.waveTailTerm M m E b m ell omega ^ 2)
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.probeLayerWaveFactor_actual_le_five_sharp_terms_probe
{d : ℕ}
(M : ABKModel d)
{m : ℤ}
{E b : ℝ}
(hb0 : 0 < b)
(hb1 : b ≤ 1 / 8)
{k₀ : ℕ}
(hk₀ : 2 ≤ k₀)
{L : ℤ}
(hmL : m ≤ L)
(n : ℕ)
(omega : Cutoff.CutoffSample d)
:
Multiscale.probeLayerWaveFactor M m (Whitney.whitneyScale M m E b k₀ omega) n L omega ≤ 3 ^ (2 * M.gamma * ↑(Percolation.hsep M m E b omega)) * (5 * ↑d ^ 2 * (Multiscale.waveHeadTerm M m E b (probeSharpLayerAnchor m b k₀ n) omega ^ 2 + waveBandMean (probeDeepBandMeanAmplitude d) M.gamma k₀ ^ 2 + probeDeepBandGaugedTail M (HCPolySupport.originCube d m) (probeSharpLayerAnchor m b k₀ n) k₀ k₀ omega ^ 2 + probeSharpAfterBandTerm M m (probeSharpLayerAnchor m b k₀ n) k₀ L omega ^ 2 + Multiscale.waveTailTerm M m E b m (probeSharpLayerAnchor m b k₀ n) omega ^ 2))
The layer wave factor occurring in the mean decomposition, bounded by the five-term split at the wave gauge used in the paper. The factor `3^(2 * gamma
- hsep)
is retained explicitly: the layer's fourth-moment index isell - hsep, whereas this wave gauge is based atell`.