SharpFramedActualPotential #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Framed potential-coordinate layer summation #
This file carries the observation-to-layer frame through the existing potential-coordinate decomposition. Every declaration here is an internal conditional proof obligation.
theorem
Algsuperdiff.Section3.Provider.Multiscale.probeFramedGoodLayerMeanRhs_nonneg
{d : ℕ}
(hd : 2 ≤ d)
(M : ABKModel d)
(m : ℤ)
(hn : ℕ → ℕ)
(n : ℕ)
(i L : ℤ)
(omega : Cutoff.CutoffSample d)
(p : HCPolySupport.Vec d)
:
theorem
Algsuperdiff.Section3.Provider.Multiscale.probeFramedCollarLayerMeanRhs_nonneg
{d : ℕ}
(hd : 2 ≤ d)
(M : ABKModel d)
(m : ℤ)
(hn : ℕ → ℕ)
(n : ℕ)
(i L : ℤ)
(omega : Cutoff.CutoffSample d)
(p : HCPolySupport.Vec d)
(Cgrad b : ℝ)
:
theorem
Algsuperdiff.Section3.Provider.Multiscale.probe_ofReal_abs_potentialCoordinate_le_tsum_framedMeanLayers_ae
{d : ℕ}
(hd : 2 ≤ d)
(M : ABKModel d)
{m0 : ℤ}
{E : { E : ℝ // 1 ≤ E }}
(hS : Frozen.Section3.inductionState M m0 E)
(m : ℤ)
{b : ℝ}
(hb0 : 0 < b)
(hb : b ≤ 1 / 8)
{k₀ : ℕ}
(hk₀ : 3 ≤ k₀)
{i : ℤ}
(hmi : m - 1 ≤ i)
(hi : i ≤ m0)
{L : ℤ}
(hmL : m ≤ L)
(p : HCPolySupport.Vec d)
:
∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), (Percolation.hsepSet M m (↑E) b omega).Nonempty →
ENNReal.ofReal
|HCPolySupport.blockVecDot ((√↑(Annealed.sigmaBar M i))⁻¹ • p, 0)
(HCPolySupport.blockMatVecMul
(HCPolySupport.Book.Ch02.coarseBlockMatrix
(HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d m))
((Cutoff.coefficientCutoffTriadicCoeffFamily M L omega).coeffOn (HCPolySupport.originCube d m)))
((√↑(Annealed.sigmaBar M i))⁻¹ • p, 0))| ≤ ∑' (n : ℕ), ENNReal.ofReal
(probeFramedGoodLayerMeanRhs M m (Whitney.whitneyScale M m (↑E) b k₀ omega) n i L omega p + probeFramedCollarLayerMeanRhs M m (Whitney.whitneyScale M m (↑E) b k₀ omega) n i L omega p
(Affine.superposedGradConst d) b)