SharpPotentialNorm

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

theorem Algsuperdiff.Section3.Provider.Multiscale.probe_purePotentialCoordinateQuadratic_eq {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) {sigma : ℝ} (hsigma : 0 < sigma) (j : Fin d) : HCPolySupport.blockVecDot ((√sigma)⁻¹ • HCPolySupport.basisVec j, 0) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.coarseBlockMatrix U a) ((√sigma)⁻¹ • HCPolySupport.basisVec j, 0)) = sigma⁻¹ * HCPolySupport.Book.Ch02.bCoarse U a j j

theorem Algsuperdiff.Section3.Provider.Multiscale.probe_inv_mul_bCoarse_matrixNorm_le_sum_abs_purePotential {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) {sigma : ℝ} (hsigma : 0 < sigma) : sigma⁻¹ * HCPolySupport.Book.Ch02.matrixNorm (HCPolySupport.Book.Ch02.bCoarse U a) ≤ ∑ j : Fin d, |HCPolySupport.blockVecDot ((√sigma)⁻¹ • HCPolySupport.basisVec j, 0) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.coarseBlockMatrix U a) ((√sigma)⁻¹ • HCPolySupport.basisVec j, 0))|

The pure-potential half of the finite-coordinate trace reduction.

theorem Algsuperdiff.Section3.Provider.Multiscale.probe_cutoffBBlockFamily_inv_le_sum_abs_purePotential {d : ℕ} (M : ABKModel d) (L : ℤ) {sigma : ℝ} (hsigma : 0 < sigma) (R : HCPolySupport.TriadicCube d) (omega : Cutoff.CutoffSample d) : CoarseEllipticity.cutoffBBlockFamily M L sigma⁻¹ R omega ≤ ∑ j : Fin d, |HCPolySupport.blockVecDot ((√sigma)⁻¹ • HCPolySupport.basisVec j, 0) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.coarseBlockMatrix (HCPolySupport.Book.Ch02.cubeDomain R) ((Cutoff.coefficientCutoffTriadicCoeffFamily M L omega).coeffOn R)) ((√sigma)⁻¹ • HCPolySupport.basisVec j, 0))|

The pure-potential reduction at the literal upper per-cube cutoff family.