Coarse-graining support: Support.CoarseGraining.ThetaEllipticity #

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Ellipticity class and shared matrix infrastructure #

Formalization of the sharp-constant pointwise ellipticity vocabulary of Proposition 2.1 of the high-moment paper (Armstrong–Kuusi–Loher, in preparation), against the coarse-graining surface of this development. Items A1–A3, together with a handful of shared MatLoewnerLE helpers and the key nonsymmetric flux inequality (★) reused by the sharp block bounds.

All matrix work is on Vec d = Fin d → ℝ / Mat d; no EuclideanSpace.

Scalar-multiple-of-identity quadratic forms and `MatLoewnerLE` helpers #

source

theorem HCPolySupport.matVecMul_one {d : ℕ} (x : Vec d) :

matVecMul 1 x = x

The identity matrix acts as the identity on vectors.

source

theorem HCPolySupport.matVecMul_smul_one {d : ℕ} (c : ℝ) (x : Vec d) :

matVecMul (c • 1) x = c • x

A scalar multiple of the identity acts by scaling.

source

theorem HCPolySupport.vecDot_matVecMul_smul_one {d : ℕ} (c : ℝ) (x : Vec d) :

vecDot x (matVecMul (c • 1) x) = c * vecNormSq x

Quadratic form of a scalar multiple of the identity.

source

theorem HCPolySupport.vecDot_matVecMul_one {d : ℕ} (x : Vec d) :

vecDot x (matVecMul 1 x) = vecNormSq x

Quadratic form of the identity matrix.

source

theorem HCPolySupport.matLoewnerLE_iff {d : ℕ} (A B : Mat d) :

MatLoewnerLE A B ↔ ∀ (x : Vec d), vecDot x (matVecMul A x) ≤ vecDot x (matVecMul B x)

MatLoewnerLE unwound to a plain quadratic-form comparison (the ½ factors cancel).

source

theorem HCPolySupport.matLoewnerLE_of_forall {d : ℕ} {A B : Mat d} (h : ∀ (x : Vec d), vecDot x (matVecMul A x) ≤ vecDot x (matVecMul B x)) :

MatLoewnerLE A B

Build MatLoewnerLE from a plain quadratic-form comparison.

A1 — the `(1, Θ)` ellipticity class #

source

@[reducible, inline]

abbrev HCPolySupport.IsThetaElliptic {d : ℕ} (Θ : ℝ) (A : Mat d) :

Prop

A1. Membership in the uniform ellipticity class with constants (1, Θ): ξ · A ξ ≥ |ξ|² and ξ · A⁻¹ ξ ≥ Θ⁻¹ |ξ|².

Equations

HCPolySupport.IsThetaElliptic Θ A = HCPolySupport.IsEllipticMatrix 1 Θ A

Instances For

A2 — the law-level ellipticity predicate #

source

def HCPolySupport.ThetaEllipticLaw {d : ℕ} (Θ : ℝ) (P : Book.Ch04.RestrictionCoeffLaw d) :

Prop

A2. A carrier coefficient law is Θ-elliptic when almost every realization lies, almost everywhere in space, in the (1, Θ) ellipticity class. Following the carrier redesign (Packet P3, decision E-2), the entrywise measurability conjunct of the paper's class Ω_Θ is now free by type: every element of the honest-fields carrier RegCoeffField d carries a proof that each of its scalar entries is Borel measurable (RegCoeffField.entry_measurable), so the a.e.-modification bridge (CoarseBounds/AeBridge.lean) recovers the pointwise-elliptic representative from a.entry_measurable rather than a bundled conjunct. The statement is therefore the paper's clean Ω_Θ membership.

Equations

HCPolySupport.ThetaEllipticLaw Θ P = ∀ᵐ (a : HCPolySupport.RegCoeffField d) ∂P, ∀ᵐ (x : HCPolySupport.Vec d), HCPolySupport.IsEllipticMatrix 1 Θ (a.toFun x)

Instances For

The key nonsymmetric flux inequality `(★)` #

For an elliptic matrix B, |B η|² ≤ Lam · (η · sᴮ η) where sᴮ = symmPart B. This is the second ellipticity inequality read backwards, and is the workhorse behind the sharp flux bounds A5 and the nonsymmetric coercivity A4.

source