High-contrast homogenization: Analytic.DirichletDomain

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

The domain class of the Dirichlet estimate is inhabited

The Dirichlet estimate e.random.dirichlet is stated for a domain U ⊆ E_1 whose constant depends on U only through the shape of the adapted domain s_bar^{-1/2}U. In the formalization the shape datum is the concentric ball sandwich HasBallSandwich, so the hypothesis of the estimate is the conjunction

• U is a nonempty bounded open convex domain;
• the adapted domain s_bar^{-1/2}U admits a concentric ball sandwich;
• U ⊆ E_1.

This module produces such a U from the positivity of the symmetric part of ā alone, so the estimate is not read on an empty family of domains.

The witness is exact rather than approximate. For S = s_bar positive definite with square root B, the change of variables y = B z turns the ellipsoid quadratic form into the Euclidean one, (B z) · S⁻¹ (B z) = ‖z‖², so the B-image of the Euclidean ball of radius |s_bar⁻¹|^{1/2} is carried into E_1 by an identity. Its adapted image is that ball again, which sandwiches itself.

The degenerate dimension is treated separately: for d = 0 the space is a single point, every quadratic form vanishes and s_bar^{-1/2} acts as the identity, so the Euclidean unit ball serves directly.

theorem HCPolySupport.HighContrast.euclideanBallAt_zero_one_subset_ellipsoid {d : ℕ} (abar : Mat d) : euclideanBallAt 0 1 ⊆ ellipsoid abar 1

The unit Euclidean ball is contained in the unit ellipsoid, for every abar.

Invertibility of the adapted matrix

theorem HCPolySupport.HighContrast.isUnit_det_matSqrt {d : ℕ} {M : Mat d} (hM : Matrix.PosDef M) : IsUnit (matSqrt M).det

The positive semidefinite square root of a positive definite matrix is invertible.

theorem HCPolySupport.HighContrast.isUnit_det_matSqrt_inv {d : ℕ} {M : Mat d} (hM : Matrix.PosDef M) : IsUnit (matSqrt M)⁻¹.det

The inverse of the adapted matrix s_bar^{1/2} is invertible, so the adapted domain s_bar^{-1/2}U is a linear image under an invertible matrix and the shape lemmas for linear images apply.

The adapted image of a ball, computed exactly

For S positive definite with square root B = matSqrt S, the change of variables y = B z turns the ellipsoid quadratic form into the Euclidean one: y · S⁻¹ y = ‖z‖², exactly. So the B-image of a Euclidean ball is the sublevel set of the ellipsoid form, and the inclusion into ellipsoid abar 1 is an identity rather than an estimate.

theorem HCPolySupport.HighContrast.matVecMul_inv_matVecMul_matSqrt {d : ℕ} {S : Mat d} (hS : Matrix.PosDef S) (z : Vec d) : matVecMul S⁻¹ (matVecMul (matSqrt S) z) = matVecMul (matSqrt S)⁻¹ z

S⁻¹ B = B⁻¹ for B the square root of the positive definite S.

theorem HCPolySupport.HighContrast.vecDot_matVecMul_inv_matSqrt {d : ℕ} {S : Mat d} (hS : Matrix.PosDef S) (z : Vec d) : vecDot (matVecMul (matSqrt S) z) (matVecMul S⁻¹ (matVecMul (matSqrt S) z)) = vecNormSq z

The change of variables. (B z) · S⁻¹ (B z) = ‖z‖², exactly.

theorem HCPolySupport.HighContrast.matImage_matSqrt_euclideanBallAt_subset_ellipsoid {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {r : ℝ} (hr : r ^ 2 ≤ specBound (symmPart abar)⁻¹) : matImage (matSqrt (symmPart abar)) (euclideanBallAt 0 r) ⊆ ellipsoid abar 1

The adapted image of a small ball sits in the unit ellipsoid. The radius constraint r² ≤ |s_bar⁻¹| is the exact one: the inclusion is the identity (B z) · s_bar⁻¹ (B z) = ‖z‖² combined with ‖z‖² < r².

Positivity of |s_bar⁻¹|

theorem HCPolySupport.HighContrast.basisVec_ne_zero {d : ℕ} {i : Fin d} : basisVec i ≠ 0

A coordinate basis vector is nonzero.

theorem HCPolySupport.HighContrast.specBound_inv_symmPart_pos {d : ℕ} {abar : Mat d} (hd : 0 < d) (hS : Matrix.PosDef (symmPart abar)) : 0 < specBound (symmPart abar)⁻¹

|s_bar⁻¹| > 0 in positive dimension. The hypothesis 0 < d is necessary: in dimension 0 every quadratic form vanishes identically, so specBound M = 0 for every M and the conclusion is false. The three lemmas below record that failure explicitly.

0 < specBound ((symmPart abar)⁻¹) is false without 0 < d

In dimension 0 the space Vec 0 is a one-point space, every quadratic form is identically zero, hence every scalar Loewner inequality holds at t = 0 and specBound M = 0 for every M. The positivity hypothesis on the symmetric part is vacuously true there (there is no nonzero vector), so it cannot rescue the statement: the hypothesis 0 < d is necessary.

theorem HCPolySupport.HighContrast.specBound_eq_zero_of_dim_zero (M : Mat 0) : specBound M = 0

In dimension zero every scalar Loewner bound holds at 0.

theorem HCPolySupport.HighContrast.vecDot_pos_of_dim_zero (abar : Mat 0) (x : Vec 0) : x ≠ 0 → 0 < vecDot x (matVecMul (symmPart abar) x)

In dimension zero the positivity hypothesis on the symmetric part is vacuous.

theorem HCPolySupport.HighContrast.not_specBound_inv_symmPart_pos_of_dim_zero (abar : Mat 0) : (∀ (x : Vec 0), x ≠ 0 → 0 < vecDot x (matVecMul (symmPart abar) x)) ∧ ¬0 < specBound (symmPart abar)⁻¹

Counterexample. In dimension zero the positivity hypothesis holds and specBound ((symmPart abar)⁻¹) = 0, so the implication from that hypothesis to 0 < specBound ((symmPart abar)⁻¹) is false as stated; 0 < d is required.

The assembly

theorem HCPolySupport.HighContrast.matImage_inv_matImage {d : ℕ} {M : Mat d} (hM : IsUnit (Matrix.det M)) (S : Set (Vec d)) : matImage M⁻¹ (matImage M S) = S

Applying the inverse to the image undoes it.

theorem HCPolySupport.HighContrast.matImage_of_dim_zero (M : Mat 0) (U : Set (Vec 0)) : matImage M U = U

In dimension zero every linear image is the identity.

theorem HCPolySupport.HighContrast.exists_domain_of_dirichlet_clause {d : ℕ} {abar : Mat d} (hpd : ∀ (x : Vec d), x ≠ 0 → 0 < vecDot x (matVecMul (symmPart abar) x)) : ∃ (U : Set (Vec d)) (ρ : ℝ) (Rad : ℝ), IsOpenBoundedConvexDomain U ∧ U.Nonempty ∧ HasBallSandwich (matImage (matSqrt (symmPart abar))⁻¹ U) ρ Rad ∧ U ⊆ ellipsoid abar 1

The domain class of the Dirichlet estimate is inhabited. There is a nonempty bounded open convex domain U inside the unit ellipsoid whose adapted image s_bar^{-1/2}U carries a concentric ball sandwich.

All three domain conjuncts of e.random.dirichlet appear. The only hypothesis is the positivity of the symmetric part of ā, which the theorem statement already asserts.