High-contrast homogenization: Analytic.TestNorms

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

Homogeneity and finiteness of the normalized norms on a test field

The dual norms ‖·‖_{H^{-s}(V)} and ‖·‖_{H_underlined^{-1}(V)} of e.physical.negative.norm are suprema over the admissible tests, that is over the smooth compactly supported fields of unit normalized norm. For that index family to be nontrivial one needs two things about the normalized norms themselves: they are homogeneous of degree two under scalar multiplication, so a nonzero test of finite nonzero norm can be rescaled to unit norm; and they are finite on every test field over a bounded domain.

This module supplies both. Homogeneity is a direct computation, once the ℝ≥0∞-valued volume average is seen to commute with multiplication by a finite constant. Finiteness has three pieces:

• the L² term is bounded because a smooth compactly supported field is uniformly bounded and the domain has finite volume;
• the gradient term is bounded because the derivative is uniformly bounded, each coordinate of the derivative being controlled by the operator norm;
• the fractional term is bounded by the uniform kernel bound, the field being globally Lipschitz and every point of a bounded domain seeing the whole domain inside one ball of a fixed radius.

The fractional term is where the constraint s < 1 enters, through the requirement 2 - (d + 2s) > -d on the kernel exponent.

Averages and their scaling

theorem HCPolySupport.HighContrast.eVolumeAverage_const_mul {d : ℕ} (V : Set (Vec d)) (a : ENNReal) (ha : a ≠ ⊤) (f : Vec d → ENNReal) : (eVolumeAverage V fun (x : Vec d) => a * f x) = a * eVolumeAverage V f

theorem HCPolySupport.HighContrast.eVolumeAverage_lt_top {d : ℕ} {V : Set (Vec d)} (hV0 : MeasureTheory.volume V ≠ 0) {f : Vec d → ENNReal} (hf : ∫⁻ (x : Vec d) in V, f x ≠ ⊤) : eVolumeAverage V f < ⊤

theorem HCPolySupport.HighContrast.fracSeminormSq_smul {d : ℕ} (V : Set (Vec d)) (s c : ℝ) (ψ : Vec d → Vec d) : (fracSeminormSq V s fun (x : Vec d) => c • ψ x) = ENNReal.ofReal (c ^ 2) * fracSeminormSq V s ψ

theorem HCPolySupport.HighContrast.hsNormSq_smul {d : ℕ} (V : Set (Vec d)) (s c : ℝ) (ψ : Vec d → Vec d) : (hsNormSq V s fun (x : Vec d) => c • ψ x) = ENNReal.ofReal (c ^ 2) * hsNormSq V s ψ

theorem HCPolySupport.HighContrast.smoothGrad_const_mul {d : ℕ} {f : Vec d → ℝ} (hf : Differentiable ℝ f) (c : ℝ) (x : Vec d) : smoothGrad (fun (y : Vec d) => c * f y) x = c • smoothGrad f x

theorem HCPolySupport.HighContrast.h1NormSq_smul {d : ℕ} (V : Set (Vec d)) (c : ℝ) {ψ : Vec d → Vec d} (hψ : Differentiable ℝ ψ) : (h1NormSq V fun (x : Vec d) => c • ψ x) = ENNReal.ofReal (c ^ 2) * h1NormSq V ψ

Finiteness of the normalized norms on a local test

theorem HCPolySupport.HighContrast.exists_uniform_ball {d : ℕ} {U : Set (Vec d)} (hUb : IsBoundedDomain U) : ∃ (D : ℝ), 0 < D ∧ ∀ x ∈ U, U ⊆ Metric.ball x D

Every point of a bounded domain sees the whole domain inside a fixed ball.

theorem HCPolySupport.HighContrast.lintegral_vecNormSq_ne_top {d : ℕ} {U : Set (Vec d)} (hUb : IsBoundedDomain U) {ψ : Vec d → Vec d} (hcont : Continuous ψ) (hcs : HasCompactSupport ψ) : ∫⁻ (x : Vec d) in U, ENNReal.ofReal (vecNormSq (ψ x)) ≠ ⊤

theorem HCPolySupport.HighContrast.lintegral_fracSeminorm_ne_top {d : ℕ} {U : Set (Vec d)} (hUm : MeasurableSet U) (hUb : IsBoundedDomain U) {s : ℝ} (hs0 : 0 ≤ ↑d + 2 * s) (hs1 : s < 1) {ψ : Vec d → Vec d} (hsm : ContDiff ℝ (↑⊤) ψ) (hcs : HasCompactSupport ψ) : ∫⁻ (x : Vec d) (y : Vec d) in U, ENNReal.ofReal (vecNormSq (ψ x - ψ y) / √(vecNormSq (x - y)) ^ (↑d + 2 * s)) ≠ ⊤

theorem HCPolySupport.HighContrast.hsNormSq_ne_top {d : ℕ} {U : Set (Vec d)} (hUm : MeasurableSet U) (hUb : IsBoundedDomain U) (hV0 : MeasureTheory.volume U ≠ 0) {s : ℝ} (hs0 : 0 ≤ ↑d + 2 * s) (hs1 : s < 1) {ψ : Vec d → Vec d} (hψ : IsLocalVecTest U ψ) : hsNormSq U s ψ ≠ ⊤

theorem HCPolySupport.HighContrast.h1NormSq_ne_top {d : ℕ} {U : Set (Vec d)} (hUb : IsBoundedDomain U) (hV0 : MeasureTheory.volume U ≠ 0) {ψ : Vec d → Vec d} (hψ : IsLocalVecTest U ψ) : h1NormSq U ψ ≠ ⊤