High-contrast homogenization: Analytic.AntiVacuityInstances

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

The admissible-test families at the domains the estimates read

The two dual-norm estimates of t.random.homogenization are read on two concrete families of domains: the bounded convex domains carrying the Dirichlet estimate e.random.dirichlet, and the ellipsoids E_r of e.homogenized.ellipsoids carrying the corrector estimate e.random.corrector. This module instantiates the general nonemptiness of the admissible-test family at exactly those two domain classes, so neither estimate is satisfied by the absence of anything to estimate.

The one geometric ingredient is a bridge between the ambient supremum metric, in which the smooth bump of the witness is built, and the Euclidean radii in which the domains are described: a supremum-norm ball of radius r / √d sits inside the Euclidean ball of radius r, since a Euclidean square norm is at most d times the square of the supremum norm.

theorem HCPolySupport.HighContrast.metricBall_subset_euclideanBallAt {d : ℕ} (hd : 0 < d) (c : Vec d) {r : ℝ} (hr : 0 < r) : Metric.ball c (r / √↑d) ⊆ euclideanBallAt c r

A sup-norm ball of radius r / √d sits inside the Euclidean ball of radius r; this is the bridge between the ambient metric and the Euclidean radii.

theorem HCPolySupport.HighContrast.exists_metricBall_subset_ellipsoid {d : ℕ} (hd : 0 < d) (abar : Mat d) {r : ℝ} (hr : 0 < r) : ∃ (c : Vec d) (ε : ℝ), 0 < ε ∧ Metric.ball c ε ⊆ ellipsoid abar r

The ellipsoid contains a sup-norm ball about the origin.

theorem HCPolySupport.HighContrast.exists_nonzero_admissible_test_h1_ellipsoid {d : ℕ} (hd : 0 < d) {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {r : ℝ} (hr : 0 < r) : ∃ (ψ : Vec d → Vec d), IsLocalVecTest (ellipsoid abar r) ψ ∧ ψ ≠ 0 ∧ h1NormSq (ellipsoid abar r) ψ ≤ 1

The admissible-test family of the corrector estimate is not empty. The family of the H_underlined^{-1} dual norm on an ellipsoid contains a nonzero field, so the estimate e.random.corrector is not satisfied by the absence of anything to estimate.

theorem HCPolySupport.HighContrast.exists_nonzero_admissible_test_convex {d : ℕ} (hd : 0 < d) {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {ρ Rad : ℝ} (hsw : HasBallSandwich U ρ Rad) {s : ℝ} (hs : s ∈ Set.Ioo 0 (1 / 2)) : ∃ (ψ : Vec d → Vec d), IsLocalVecTest U ψ ∧ ψ ≠ 0 ∧ hsNormSq U s ψ ≤ 1

The admissible-test family of the Dirichlet estimate is not empty, at the domains that estimate binds: a bounded open convex domain whose shape datum is a concentric ball sandwich.