High-contrast homogenization: Analytic.EllipsoidGeometry

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Non-degeneracy of the ellipsoids E_r

The ellipsoids E_r = {x : x · s_bar⁻¹ x ≤ λ_bar⁻¹ r²} of e.homogenized.ellipsoids are the domains on which the corrector estimate e.random.corrector, the Lipschitz estimate e.random.energy and the C^{1,ϑ} estimate e.random.regularity are read. Each of those is written through a volume-normalized average over E_r, and such an average carries the intended meaning only when E_r is a measurable set of positive finite volume. This module proves exactly that, together with the Loewner and positive-definiteness facts that the proof consumes.

The two halves are separately elementary.

• Positive volume is unconditional. The scalar Loewner bound x · M x ≤ |M| ‖x‖² holds for every matrix, so E_r contains the concentric Euclidean ball of radius r, which is open and nonempty for r > 0. No positivity, symmetry or invertibility hypothesis on ā is used.
• Finite volume needs the positive definiteness of the symmetric part s_bar, and follows from the reverse bound ‖x‖² ≤ (x · s_bar⁻¹ x) |s_bar|. That bound is Cauchy–Schwarz for the positive semidefinite form of s_bar⁻¹ applied to the pair (x, s_bar x); no eigenvalue theory enters.

The scalar Loewner bound in quadratic-form shape

matLoewnerLE_specBound_smul_one is unconditional: every matrix satisfies M ≤ |M| · I in the Loewner order. Written on the quadratic form this is the pointwise bound x · M x ≤ |M| ‖x‖², which is the only ingredient the ellipsoid inclusion needs.

theorem HCPolySupport.HighContrast.matVecMul_smul_one' {d : ℕ} (t : ℝ) (x : Vec d) : matVecMul (t • 1) x = t • x

Multiplication by a scalar multiple of the identity.

theorem HCPolySupport.HighContrast.vecDot_matVecMul_le_specBound_mul_vecNormSq {d : ℕ} (M : Mat d) (x : Vec d) : vecDot x (matVecMul M x) ≤ specBound M * vecNormSq x

The unconditional scalar Loewner bound, on the quadratic form. No hypothesis on M whatsoever.

The Euclidean ball sits inside the ellipsoid

This holds for every abar, with no positivity, symmetry or invertibility hypothesis: on euclideanBallAt 0 r one has ‖x‖² < r², the Loewner bound gives x · s_bar⁻¹ x ≤ |s_bar⁻¹| ‖x‖², and |s_bar⁻¹| ≥ 0 (specBound_nonneg, also unconditional) lets the two be multiplied.

theorem HCPolySupport.HighContrast.euclideanBallAt_zero_subset_ellipsoid {d : ℕ} (abar : Mat d) (r : ℝ) : euclideanBallAt 0 r ⊆ ellipsoid abar r

The ellipsoid contains the concentric Euclidean ball of the same radius, unconditionally.

The bridge to Matrix.PosDef

theorem HCPolySupport.HighContrast.isHermitian_symmPart {d : ℕ} (A : Mat d) : Matrix.IsHermitian (symmPart A)

symmPart is Hermitian by construction.

theorem HCPolySupport.HighContrast.posDef_symmPart_of_vecDot_pos {d : ℕ} {abar : Mat d} (hpd : ∀ (x : Vec d), x ≠ 0 → 0 < vecDot x (matVecMul (symmPart abar) x)) : Matrix.PosDef (symmPart abar)

The bridge. The elementwise positivity statement of the Dirichlet clause is Mathlib's Matrix.PosDef for the symmetric part. star x ⬝ᵥ M *ᵥ x and vecDot x (matVecMul M x) are definitionally equal on Vec d.

theorem HCPolySupport.HighContrast.vecDot_matVecMul_pos_of_posDef {d : ℕ} {M : Mat d} (hM : Matrix.PosDef M) {x : Vec d} (hx : x ≠ 0) : 0 < vecDot x (matVecMul M x)

The converse reading of Matrix.PosDef on Vec d.

Measurability, the centre, and positive volume

theorem HCPolySupport.HighContrast.continuous_vecDot_matVecMul {d : ℕ} (M : Mat d) : Continuous fun (x : Vec d) => vecDot x (matVecMul M x)

The ellipsoid quadratic form is continuous.

theorem HCPolySupport.HighContrast.isClosed_ellipsoid {d : ℕ} (abar : Mat d) (r : ℝ) : IsClosed (ellipsoid abar r)

The ellipsoid is closed.

theorem HCPolySupport.HighContrast.measurableSet_ellipsoid {d : ℕ} (abar : Mat d) (r : ℝ) : MeasurableSet (ellipsoid abar r)

The ellipsoid is measurable.

theorem HCPolySupport.HighContrast.zero_mem_ellipsoid {d : ℕ} (abar : Mat d) (r : ℝ) : 0 ∈ ellipsoid abar r

The centre lies in every ellipsoid; no sign condition on r and no hypothesis on abar is needed.

theorem HCPolySupport.HighContrast.volume_ellipsoid_pos {d : ℕ} (abar : Mat d) {r : ℝ} (hr : 0 < r) : 0 < MeasureTheory.volume (ellipsoid abar r)

The ellipsoid has positive volume for positive radius; no hypothesis on abar is needed, because the ellipsoid contains the concentric Euclidean ball of the same radius.

The reverse Loewner bound, and finite volume

theorem HCPolySupport.HighContrast.vecDot_matVecMul_inv_nonneg {d : ℕ} {S : Mat d} (hS : Matrix.PosDef S) (x : Vec d) : 0 ≤ vecDot x (matVecMul S⁻¹ x)

The inverse quadratic form of a positive definite matrix is nonnegative.

theorem HCPolySupport.HighContrast.vecNormSq_le_vecDot_matVecMul_inv_mul_specBound {d : ℕ} {S : Mat d} (hS : Matrix.PosDef S) (x : Vec d) : vecNormSq x ≤ vecDot x (matVecMul S⁻¹ x) * specBound S

The reverse Loewner bound of a positive definite matrix, obtained from Cauchy–Schwarz for the positive semidefinite form of S⁻¹ — no eigenvalue theory is used: ‖x‖⁴ = (x · S⁻¹ (S x))² ≤ (x · S⁻¹ x)(S x · S⁻¹ S x) = (x · S⁻¹ x)(x · S x).

theorem HCPolySupport.HighContrast.vecNormSq_le_of_mem_ellipsoid {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {r : ℝ} {x : Vec d} (hx : x ∈ ellipsoid abar r) : vecNormSq x ≤ specBound (symmPart abar)⁻¹ * r ^ 2 * specBound (symmPart abar)

Every point of the ellipsoid obeys an explicit Euclidean bound.

theorem HCPolySupport.HighContrast.isBoundedDomain_ellipsoid {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (r : ℝ) : IsBoundedDomain (ellipsoid abar r)

The ellipsoid is a bounded domain.

theorem HCPolySupport.HighContrast.isBounded_ellipsoid {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (r : ℝ) : Bornology.IsBounded (ellipsoid abar r)

The ellipsoid is bornologically bounded.

theorem HCPolySupport.HighContrast.volume_ellipsoid_lt_top {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (r : ℝ) : MeasureTheory.volume (ellipsoid abar r) < ⊤

The ellipsoid has finite volume.

theorem HCPolySupport.HighContrast.ellipsoid_nondegenerate {d : ℕ} {abar : Mat d} (hpd : ∀ (x : Vec d), x ≠ 0 → 0 < vecDot x (matVecMul (symmPart abar) x)) {r : ℝ} (hr : 0 < r) : 0 ∈ ellipsoid abar r ∧ MeasurableSet (ellipsoid abar r) ∧ IsBoundedDomain (ellipsoid abar r) ∧ 0 < MeasureTheory.volume (ellipsoid abar r) ∧ MeasureTheory.volume (ellipsoid abar r) < ⊤

The non-degeneracy statement. Under the positivity of the symmetric part of ā, every ellipsoid of positive radius is a measurable set of positive finite volume containing the origin, so the volume-normalized averages read on E_r are neither 0/0 nor ∞/∞.