High-contrast homogenization: Analytic.LocalEllipticity

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

Reading the local ellipticity constants on one set

The coefficient class fixed in s.introduction is local: a field of the class carries a pair of ellipticity constants on each bounded set, and the pair belongs to the set. Every estimate of the coefficient-Sobolev classes is an estimate on one ball, one cube or one compact set, and each of them wants its hypothesis in the shape ∀ᵐ x ∂volume.restrict V, IsEllipticMatrix lam Lam (b x).

This module converts the class into that shape: on a bounded measurable set, on a centered Euclidean ball, and on a compact set. The three statements are the same extraction read at the three carriers the classes use.

theorem HCPolySupport.HighContrast.IsAELocallyUniformlyElliptic.exists_ae_isEllipticMatrix_restrict {d : ℕ} {b : CoeffField d} (hb : IsAELocallyUniformlyElliptic b) {S : Set (Vec d)} (hSm : MeasurableSet S) (hS : Bornology.IsBounded S) : ∃ (lam : ℝ) (Lam : ℝ), 0 < lam ∧ lam ≤ Lam ∧ ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict S, IsEllipticMatrix lam Lam (b x)

The constants of a bounded measurable set, in restricted-measure form: the shape the weighted-energy comparisons consume.

theorem HCPolySupport.HighContrast.IsAELocallyUniformlyElliptic.exists_ae_isEllipticMatrix_euclideanBall {d : ℕ} {b : CoeffField d} (hb : IsAELocallyUniformlyElliptic b) {R : ℝ} (hR : 0 < R) : ∃ (lam : ℝ) (Lam : ℝ), 0 < lam ∧ lam ≤ Lam ∧ ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict (euclideanBall d R), IsEllipticMatrix lam Lam (b x)

The constants of a centered Euclidean ball. The Euclidean ball of radius R lies in the ambient ball of the same radius, so the constants of the latter serve.

theorem HCPolySupport.HighContrast.IsAELocallyUniformlyElliptic.exists_ae_isEllipticMatrix_isCompact {d : ℕ} {b : CoeffField d} (hb : IsAELocallyUniformlyElliptic b) {K : Set (Vec d)} (hK : IsCompact K) : ∃ (lam : ℝ) (Lam : ℝ), 0 < lam ∧ lam ≤ Lam ∧ ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict K, IsEllipticMatrix lam Lam (b x)

The constants of a compact set. A compact subset of ℝ^d is bounded and measurable.