High-contrast homogenization: Consistency.AdmissibleTests

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

The admissible-test family of the dual norms is not empty

This module checks the definition IsLocalVecTest of an admissible test field: the class of smooth compactly supported vector fields on a domain over which the two dual norms negSobolevNorm and negOneNorm of e.physical.negative.norm take their suprema. Were that check to fail — were the admissible tests of hsNormSq (respectively h1NormSq) at most 1 to contain only the zero field, or to be empty — then each of those two suprema would be 0 for a reason that has nothing to do with the field F it measures, and every estimate written with them, among them the Dirichlet estimate e.random.dirichlet and the corrector estimate e.random.corrector of t.random.homogenization, would be vacuous: satisfied by the absence of anything to estimate. This module is a consistency check of that definition and is not a result of the paper.

The dual norms ‖F‖_{H^{-s}(V)} and ‖F‖_{H_underlined^{-1}(V)} of e.physical.negative.norm are suprema over the smooth compactly supported fields on V whose normalized norm is at most 1. This module shows that this failure does not occur: over any domain containing a ball, each of the two families contains a nonzero field.

The witness is a Mathlib smooth bump supported in a ball inside the domain, pointed along a fixed coordinate direction. It is nonzero because the bump equals 1 at its centre. Its normalized norm is finite by the finiteness statements for the normalized norms, so if it is nonzero it can be rescaled to norm exactly 1 by the quadratic homogeneity, and if it is zero it already satisfies the constraint.

The hypothesis 0 < d is necessary and is not a convenience: for d = 0 the only field Vec 0 → Vec 0 is the zero field, so the family really does contain nothing else and every such supremum vanishes.

A nonzero local test on any nonempty open set

theorem HCPolySupport.HighContrast.exists_nonzero_isLocalVecTest {d : ℕ} (hd : 0 < d) {U : Set (Vec d)} (hUball : ∃ (c : Vec d) (ε : ℝ), 0 < ε ∧ Metric.ball c ε ⊆ U) : ∃ (ψ : Vec d → Vec d), IsLocalVecTest U ψ ∧ ψ ≠ 0

The headline statements

theorem HCPolySupport.HighContrast.ofReal_one_div_toReal_mul_self {M : ENNReal} (h0 : M ≠ 0) (hT : M ≠ ⊤) : ENNReal.ofReal (1 / M.toReal) * M = 1

The rescaling identity used to normalize a finite nonzero norm to 1.

theorem HCPolySupport.HighContrast.exists_nonzero_admissible_test_of_ball {d : ℕ} (hd : 0 < d) {U : Set (Vec d)} (hUm : MeasurableSet U) (hUb : IsBoundedDomain U) (hUball : ∃ (c : Vec d) (ε : ℝ), 0 < ε ∧ Metric.ball c ε ⊆ U) {s : ℝ} (hs0 : 0 ≤ ↑d + 2 * s) (hs1 : s < 1) : ∃ (ψ : Vec d → Vec d), IsLocalVecTest U ψ ∧ ψ ≠ 0 ∧ hsNormSq U s ψ ≤ 1

The admissible-test family of the H^{-s} dual norm contains a nonzero field. Only openness, boundedness and nonemptiness of U are used; 0 < d is necessary, since Vec 0 → Vec 0 has 0 as its only element.

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

The same statement on a bounded open convex domain.

theorem HCPolySupport.HighContrast.exists_nonzero_admissible_test_h1_of_ball {d : ℕ} (hd : 0 < d) {U : Set (Vec d)} (hUb : IsBoundedDomain U) (hUball : ∃ (c : Vec d) (ε : ℝ), 0 < ε ∧ Metric.ball c ε ⊆ U) : ∃ (ψ : Vec d → Vec d), IsLocalVecTest U ψ ∧ ψ ≠ 0 ∧ h1NormSq U ψ ≤ 1

The admissible-test family of the H_underlined^{-1} dual norm contains a nonzero field. Only openness, boundedness and nonemptiness of U are used, together with 0 < d.

theorem HCPolySupport.HighContrast.exists_nonzero_admissible_test_h1 {d : ℕ} (hd : 0 < d) {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) : ∃ (ψ : Vec d → Vec d), IsLocalVecTest U ψ ∧ ψ ≠ 0 ∧ h1NormSq U ψ ≤ 1

The same statement on a bounded open convex domain.