Coarse-graining support: Support.Probability.RegCoeffField.EllipticSet

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

The elliptic-matrix locus is closed, convex and measurable

This file ports the finite-dimensional closed/convex description of the elliptic matrix locus {A : Mat d | IsEllipticMatrix lam Lam A} from the coarse-graining salvage (HCPolySupport.Book.Ch04.Internal.SliceNullMeasurability), adapted to the shipped tree's imports. It is the ingredient that makes the carrier truncation ellipticTruncateReg a genuine carrier element: the pointwise predicate IsEllipticMatrix 1 Θ (a x) cuts out a Borel set of matrices, so the pullback {x | IsEllipticMatrix 1 Θ (a x)} is measurable.

The fourth ellipticity inequality Lam⁻¹ |ξ|² ≤ ξ · A⁻¹ ξ is replaced by an inverse-free image bound |A η|² ≤ Lam (η · A η) (IsEllipticEntryLU), whose sublevel description is a countable-free intersection of closed half-spaces, hence closed and convex.

The Mat d = Fin d → Fin d → ℝ matrix-entry space carries the product Borel structure; we record the corresponding BorelSpace instance transferred from the genuine pi type so that closed matrix sets are measurable for the carrier's instMatMeasurableSpace.

Reference: the paper (Armstrong–Kuusi–Loher, to appear).

Local copy of the identity action

The inverse-free ellipticity predicate

def HCPolySupport.IsEllipticEntryLU {d : ℕ} (lam Lam : ℝ) (v : Mat d) : Prop

The two inverse-free ellipticity inequalities for general constants (lam, Lam), as a predicate on the matrix-entry space Mat d. Coercivity is a linear inequality in the matrix; the image bound is a convex-quadratic ≤ affine inequality. Both loci are closed and convex.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.isEllipticMatrix_iff_isEllipticEntryLU {d : ℕ} {lam Lam : ℝ} (A : Mat d) : IsEllipticMatrix lam Lam A ↔ 0 < lam ∧ lam ≤ Lam ∧ IsEllipticEntryLU lam Lam A

Inverse-free characterization for general (lam, Lam). Given coercivity, the fourth ellipticity inequality is equivalent to the inverse-free image bound.

Closedness

theorem HCPolySupport.isClosed_isEllipticEntryLU {d : ℕ} {lam Lam : ℝ} : IsClosed {v : Mat d | IsEllipticEntryLU lam Lam v}

The inverse-free (lam, Lam)-ellipticity locus is closed in Mat d.

Convexity

theorem HCPolySupport.vecNormSq_convex_le {d : ℕ} {V W : Vec d} {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : vecNormSq (a • V + b • W) ≤ a * vecNormSq V + b * vecNormSq W

Convexity of the squared vector energy along convex combinations.

theorem HCPolySupport.convex_isEllipticEntryLU {d : ℕ} {lam Lam : ℝ} : Convex ℝ {v : Mat d | IsEllipticEntryLU lam Lam v}

The inverse-free (lam, Lam)-ellipticity locus is convex in Mat d.

The elliptic matrix locus is closed and convex

theorem HCPolySupport.isClosed_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} : IsClosed {A : Mat d | IsEllipticMatrix lam Lam A}

The (lam, Lam)-elliptic matrix locus is closed in Mat d.

theorem HCPolySupport.convex_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} : Convex ℝ {A : Mat d | IsEllipticMatrix lam Lam A}

The (lam, Lam)-elliptic matrix locus is convex in Mat d.

Measurability of the matrix locus

instance HCPolySupport.instBorelSpaceMatEntry {d : ℕ} : BorelSpace (Mat d)

The matrix-entry space Mat d = Fin d → Fin d → ℝ carries the product Borel structure: its carrier σ-algebra instMatMeasurableSpace agrees with the Borel σ-algebra of the product topology. Transferred from the genuine pi type.

Named distinctly from the raw-CoeffField layer's instBorelSpaceMat (Ch04.Internal.CoarseObservableMeasurability.Basic) so that the carrier and raw layers coexist in a single import closure; both witness the same (defeq) product Borel structure and are found by instance resolution, never by name.

theorem HCPolySupport.measurableSet_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} : MeasurableSet {A : Mat d | IsEllipticMatrix lam Lam A}

The elliptic matrix locus is measurable. Being closed in the product topology, it is Borel, hence measurable for the carrier's matrix σ-algebra.