SharpFramedPotentialDescendant #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Framed sharp potential estimate at descendant cubes #
This file transports the framed origin-cube estimate to a fixed descendant. Its main theorem is an internal conditional proof obligation; the displayed bad-event inequalities remain caller-supplied A inputs.
theorem
Algsuperdiff.Section3.Provider.Multiscale.cutoffBBlockFamily_translateCutoffSample_sharp_framed_probe
{d : ℕ}
[NeZero d]
(M : ABKModel d)
(L : ℤ)
(scaling : ℝ)
(R : HCPolySupport.TriadicCube d)
(omega : Cutoff.CutoffSample d)
:
CoarseEllipticity.cutoffBBlockFamily M L scaling R omega = CoarseEllipticity.cutoffBBlockFamily M L scaling (HCPolySupport.originCube d R.scale)
(Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega)
theorem
Algsuperdiff.Section3.Provider.Multiscale.probe_ofReal_cutoffBBlockFamily_descendant_le_sharpFramedMeanEnvelope_ae
{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 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₀)
{L : ℤ}
(hL : m - 1 ≤ L)
:
∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ENNReal.ofReal (CoarseEllipticity.cutoffBBlockFamily M L (↑(Annealed.sigmaBar M (m - 1)))⁻¹ R omega) ≤ ∑ j : Fin d,
∑' (n : ℕ), ENNReal.ofReal
(probeSharpFramedMeanLayerEnvelope M R.scale (↑E) b k₀ n (m - 1) L
(Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega) (HCPolySupport.basisVec j)
(Affine.superposedGradConst d))
The normalized cutoff upper block at a fixed descendant cube, bounded almost surely by the translated sharp layer envelope with the global observation frame retained.