High-contrast homogenization: Analytic.NormComparison

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

The ambient norm against the Euclidean quantities

Vec d = Fin d → ℝ carries the supremum norm, while every Euclidean quantity in the volume-normalized spaces of s.introduction is written through vecNormSq. The two are comparable, with the dimensional loss appearing only in one direction:

‖z‖ ≤ |z| and |z|² ≤ d ‖z‖².

Both are needed by the finiteness statements for the normalized norms: the first turns a Euclidean distance in a Gagliardo denominator into an ambient one, and the second turns an ambient bound on a test field into a Euclidean one.

The module also collects the elementary consequences of smoothness and compact support that those statements consume — a uniform bound on the field, a uniform bound on its derivative, the resulting global Lipschitz bound for the ambient norm — and the volume of an ambient ball, which is a product of intervals and therefore has an explicit value independent of the centre.

Comparison of the ambient (sup) norm with the Euclidean quantities

theorem HCPolySupport.HighContrast.norm_le_sqrt_vecNormSq {d : ℕ} (z : Vec d) : ‖z‖ ≤ √(vecNormSq z)

theorem HCPolySupport.HighContrast.vecNormSq_le_dim_mul_norm_sq {d : ℕ} (z : Vec d) : vecNormSq z ≤ ↑d * ‖z‖ ^ 2

theorem HCPolySupport.HighContrast.norm_basisVec_le_one {d : ℕ} (i : Fin d) : ‖basisVec i‖ ≤ 1

Smooth compactly supported maps are bounded and Lipschitz

theorem HCPolySupport.HighContrast.exists_norm_bound_of_hasCompactSupport {d : ℕ} {ψ : Vec d → Vec d} (hcont : Continuous ψ) (hcs : HasCompactSupport ψ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (x : Vec d), ‖ψ x‖ ≤ M

theorem HCPolySupport.HighContrast.exists_fderiv_bound_of_hasCompactSupport {d : ℕ} {ψ : Vec d → Vec d} (hsm : ContDiff ℝ (↑⊤) ψ) (hcs : HasCompactSupport ψ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : Vec d), ‖fderiv ℝ ψ x‖ ≤ C

theorem HCPolySupport.HighContrast.exists_lipschitz_of_hasCompactSupport {d : ℕ} {ψ : Vec d → Vec d} (hsm : ContDiff ℝ (↑⊤) ψ) (hcs : HasCompactSupport ψ) : ∃ (L : ℝ), 0 ≤ L ∧ ∀ (x y : Vec d), ‖ψ x - ψ y‖ ≤ L * ‖x - y‖

A smooth compactly supported field is globally Lipschitz for the ambient (sup) norm.

The volume of an ambient ball

theorem HCPolySupport.HighContrast.volume_ball_eq {d : ℕ} (x : Vec d) {r : ℝ} (hr : 0 < r) : MeasureTheory.volume (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ d)