SharpFramedPotentialRoot #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Framed sharp potential estimate at an origin cube #
This file combines the framed coordinatewise potential estimate with the finite-coordinate pure-potential reduction. Its theorem is an internal conditional proof obligation; the displayed bad-event inequalities remain caller-supplied A inputs.
theorem
Algsuperdiff.Section3.Provider.Multiscale.probe_ofReal_cutoffBBlockFamily_inv_le_sum_tsum_sharpFramedMeanLayerEnvelope_ae
{d : ℕ}
(M : ABKModel d)
{m₀ : ℤ}
{E : { E : ℝ // 1 ≤ E }}
(hS : Frozen.Section3.inductionState M m₀ E)
(m : ℤ)
{sigma b : ℝ}
(hd : 2 ≤ d)
(hsigma0 : 0 < sigma)
(hsigma : sigma ≤ 1 / 2)
(hb0 : 0 < b)
(hb : b ≤ 1 / 8)
(hEexp : Real.exp (Percolation.badClustersConst d / sigma) ≤ ↑E)
(hE4 : 4 ≤ ↑E)
(hunit : BadEvents.unitGate M)
(hgamma20 : M.gamma ≤ 1 / 20)
(hinvSq : (↑E)⁻¹ ^ 2 ≤ Disorder.cstar M)
(hEb : Percolation.badClustersConst d / b ≤ ↑E)
(hgamma : M.gamma ≤ ↑E ^ (-5))
{k₀ : ℕ}
(hk₀ : 3 ≤ k₀)
{i : ℤ}
(hmi : m - 1 ≤ i)
(hi : i ≤ m₀)
{L : ℤ}
(hmL : m ≤ L)
:
∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ENNReal.ofReal
(CoarseEllipticity.cutoffBBlockFamily M L (↑(Annealed.sigmaBar M i))⁻¹ (HCPolySupport.originCube d m) omega) ≤ ∑ j : Fin d,
∑' (n : ℕ), ENNReal.ofReal
(probeSharpFramedMeanLayerEnvelope M m (↑E) b k₀ n i L omega (HCPolySupport.basisVec j)
(Affine.superposedGradConst d))
The normalized cutoff upper block at an origin cube, bounded almost surely by the sharp layer envelope with its observation-to-cube frame retained.