Pointwise

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Local block energy: pointwise algebra

Pointwise (single-matrix) inequalities feeding the local-energy estimate of p.local.block.energy (the high-moment paper (Armstrong–Kuusi–Loher, in preparation), §3.4). Everything here is elementary linear algebra on Vec d = Fin d → ℝ; no EuclideanSpace.

The central tool is the Young inequality in the s-metric (symmForm_young): for the symmetric part s = symmPart A of an elliptic matrix and t > 0,

ξ · V ≤ (2t)⁻¹ (ξ · s⁻¹ ξ) + (t/2) (V · s V),

with no square roots. Combined with the coefficient bounds q · s⁻¹ q ≤ |q|², (a p) · s⁻¹ (a p) ≤ Θ |p|², and the flux corollary ‖a e‖² ≤ 2Θ (e · s e) this drives the bulk and cutoff estimates.

The symmetric form is nonnegative and equals the full quadratic form

theorem HCPolySupport.vecDot_matVecMul_eq_symmPart {d : ℕ} (A : Mat d) (V : Vec d) : vecDot V (matVecMul A V) = vecDot V (matVecMul (symmPart A) V)

V · a V = V · s V: the skew part drops out of the diagonal quadratic form.

theorem HCPolySupport.vecDot_matVecMul_symmPart_nonneg {d : ℕ} {Θ : ℝ} {A : Mat d} (hA : IsThetaElliptic Θ A) (V : Vec d) : 0 ≤ vecDot V (matVecMul (symmPart A) V)

Nonnegativity of the s-form for an elliptic matrix.

The Young inequality in the s-metric

theorem HCPolySupport.symmForm_young {d : ℕ} {Θ : ℝ} {A : Mat d} (hA : IsThetaElliptic Θ A) {t : ℝ} (ht : 0 < t) (ξ V : Vec d) : vecDot ξ V ≤ (2 * t)⁻¹ * vecDot ξ (matVecMul (symmPart A)⁻¹ ξ) + t / 2 * vecDot V (matVecMul (symmPart A) V)

s-metric Young. For the symmetric part s = symmPart A of a (1, Θ)-elliptic matrix and any t > 0, ξ · V ≤ (2t)⁻¹ (ξ · s⁻¹ ξ) + (t/2) (V · s V).

Coefficient bounds in the s⁻¹-metric

theorem HCPolySupport.symmPartInv_quadratic_le_normSq {d : ℕ} {Θ : ℝ} {A : Mat d} (hA : IsThetaElliptic Θ A) (q : Vec d) : vecDot q (matVecMul (symmPart A)⁻¹ q) ≤ vecNormSq q

q · s⁻¹ q ≤ |q|².

theorem HCPolySupport.symmPartInv_image_le {d : ℕ} {Θ : ℝ} {A : Mat d} (hA : IsThetaElliptic Θ A) (p : Vec d) : vecDot (matVecMul A p) (matVecMul (symmPart A)⁻¹ (matVecMul A p)) ≤ Θ * vecNormSq p

(a p) · s⁻¹ (a p) ≤ Θ |p|².

theorem HCPolySupport.symmPartInv_imageTranspose_le {d : ℕ} {Θ : ℝ} {A : Mat d} (hA : IsThetaElliptic Θ A) (p : Vec d) : vecDot (matVecMul (matTranspose A) p) (matVecMul (symmPart A)⁻¹ (matVecMul (matTranspose A) p)) ≤ Θ * vecNormSq p

(aᵀ p) · s⁻¹ (aᵀ p) ≤ Θ |p|², using symmPart Aᵀ = symmPart A.

The bulk coefficient vectors

theorem HCPolySupport.symmPartInv_bulkV_le {d : ℕ} {Θ : ℝ} {A : Mat d} (hA : IsThetaElliptic Θ A) (p q : Vec d) : vecDot (q - (1 / 2) • matVecMul A p) (matVecMul (symmPart A)⁻¹ (q - (1 / 2) • matVecMul A p)) ≤ 2 * (Θ * vecNormSq p + vecNormSq q)

(q − ½ a p) · s⁻¹ (q − ½ a p) ≤ 2 (Θ|p|² + |q|²).

theorem HCPolySupport.symmPartInv_bulkVstar_le {d : ℕ} {Θ : ℝ} {A : Mat d} (hA : IsThetaElliptic Θ A) (p q : Vec d) : vecDot ((1 / 2) • matVecMul (matTranspose A) p) (matVecMul (symmPart A)⁻¹ ((1 / 2) • matVecMul (matTranspose A) p)) ≤ Θ * vecNormSq p + vecNormSq q

(½ aᵀ p) · s⁻¹ (½ aᵀ p) ≤ Θ|p|² + |q|².

The flux corollary ‖a e‖² ≤ 2Θ (e · s e)

theorem HCPolySupport.vecNormSq_image_le {d : ℕ} {Θ : ℝ} {A : Mat d} (hA : IsThetaElliptic Θ A) (e : Vec d) : vecNormSq (matVecMul A e) ≤ 2 * Θ * vecDot e (matVecMul (symmPart A) e)

‖a e‖² ≤ 2Θ (e · s e).

theorem HCPolySupport.vecNormSq_imageTranspose_le {d : ℕ} {Θ : ℝ} {A : Mat d} (hA : IsThetaElliptic Θ A) (e : Vec d) : vecNormSq (matVecMul (matTranspose A) e) ≤ 2 * Θ * vecDot e (matVecMul (symmPart A) e)

‖aᵀ e‖² ≤ 2Θ (e · s e).

An AM-GM helper with square roots

theorem HCPolySupport.two_mul_sqrt_mul_sqrt_le {A B t : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (ht : 0 < t) : 2 * √A * √B ≤ t * A + t⁻¹ * B

2 √A √B ≤ t A + t⁻¹ B for A, B ≥ 0 and t > 0.