High-contrast homogenization: Analytic.ClassHonesty

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

The coefficient-Sobolev classes have finite weighted energy

MemH1a, MemH1a0 and MemH1sLoc — the spaces H¹_a(V), H¹_{a,0}(V) and H¹_{s,loc}(ℝ^d) of s.introduction — are approximability conditions: each carries a sequence of smooth functions whose H¹_s distance to the pair tends to 0. Eventual finiteness of that distance together with finiteness of the energy of one smooth approximant gives finiteness of the weighted energy of the weak gradient itself.

The module first collects the finiteness facts for the unweighted energy of a continuous field — on a bounded set, on an arbitrary set when the field has compact support, and across the triangle inequality in both directions — and then feeds them through the two-sided energy comparison to the three classes.

The domain hypotheses differ between the classes, and the difference is real. H¹_{a,0}(V) needs no hypothesis on V, its approximants being compactly supported inside V. H¹_a(V) needs V bounded: its approximants are globally smooth but not compactly supported, so nothing bounds their gradients on an unbounded V, and without a hypothesis on V the conclusion is false.

theorem HCPolySupport.HighContrast.lintegral_ofReal_vecNormSq_ne_top_of_isBounded {d : ℕ} {V : Set (Vec d)} (hV : Bornology.IsBounded V) {G : Vec d → Vec d} (hG : Continuous G) : ∫⁻ (x : Vec d) in V, ENNReal.ofReal (vecNormSq (G x)) ≠ ⊤

A continuous field has finite unweighted energy on a bounded set.

theorem HCPolySupport.HighContrast.lintegral_ofReal_vecNormSq_ne_top_of_hasCompactSupport {d : ℕ} {V : Set (Vec d)} {G : Vec d → Vec d} (hG : Continuous G) (hGs : HasCompactSupport G) : ∫⁻ (x : Vec d) in V, ENNReal.ofReal (vecNormSq (G x)) ≠ ⊤

A continuous field with compact support has finite unweighted energy on every set.

theorem HCPolySupport.HighContrast.lintegral_ofReal_vecNormSq_ne_top_of_sub {d : ℕ} {V : Set (Vec d)} {G H : Vec d → Vec d} (hGmeas : AEMeasurable (fun (x : Vec d) => ENNReal.ofReal (vecNormSq (G x))) (MeasureTheory.volume.restrict V)) (hG : ∫⁻ (x : Vec d) in V, ENNReal.ofReal (vecNormSq (G x)) ≠ ⊤) (hD : ∫⁻ (x : Vec d) in V, ENNReal.ofReal (vecNormSq (G x - H x)) ≠ ⊤) : ∫⁻ (x : Vec d) in V, ENNReal.ofReal (vecNormSq (H x)) ≠ ⊤

The triangle step: if G has finite unweighted energy and G - H has finite unweighted energy, then so does H.

theorem HCPolySupport.HighContrast.lintegral_ofReal_vecNormSq_ne_top_of_add {d : ℕ} {V : Set (Vec d)} {G H : Vec d → Vec d} (hHmeas : AEMeasurable (fun (x : Vec d) => ENNReal.ofReal (vecNormSq (H x))) (MeasureTheory.volume.restrict V)) (hH : ∫⁻ (x : Vec d) in V, ENNReal.ofReal (vecNormSq (H x)) ≠ ⊤) (hD : ∫⁻ (x : Vec d) in V, ENNReal.ofReal (vecNormSq (G x - H x)) ≠ ⊤) : ∫⁻ (x : Vec d) in V, ENNReal.ofReal (vecNormSq (G x)) ≠ ⊤

The mirror triangle step: if H has finite unweighted energy and G - H has finite unweighted energy, then so does G.

theorem HCPolySupport.HighContrast.lintegral_ofReal_vecNormSq_ne_top_of_ae_bounded {d : ℕ} {V : Set (Vec d)} (hVb : Bornology.IsBounded V) {G : Vec d → Vec d} {L : ℝ} (hG : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict V, vecNormSq (G x) ≤ L) : ∫⁻ (x : Vec d) in V, ENNReal.ofReal (vecNormSq (G x)) ≠ ⊤

An essentially bounded field has finite unweighted energy on a bounded set.

theorem HCPolySupport.HighContrast.vecNormSq_le_sq_of_sqrt_le {d : ℕ} {x : Vec d} {L : ℝ} (h : √(vecNormSq x) ≤ L) : vecNormSq x ≤ L ^ 2

The essential bound of the Dirichlet clause is stated through the Euclidean norm; this is its squared form.

theorem HCPolySupport.HighContrast.exists_sEnergyOn_sub_ne_top {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {u : Vec d → ℝ} {Du : Vec d → Vec d} {v : ℕ → Vec d → ℝ} (htend : Filter.Tendsto (fun (n : ℕ) => h1sNormSqOn b V (fun (x : Vec d) => v n x - u x) fun (x : Vec d) => smoothGrad (v n) x - Du x) Filter.atTop (nhds 0)) : ∃ (n : ℕ), (sEnergyOn b V fun (x : Vec d) => smoothGrad (v n) x - Du x) ≠ ⊤

Along a sequence whose H¹_s distance to the pair tends to 0, some approximant has finite H¹_s distance.

theorem HCPolySupport.HighContrast.sEnergyOn_ne_top_of_memH1a {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hlam : 0 < lam) (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x)) (hVb : Bornology.IsBounded V) {u : Vec d → ℝ} {Du : Vec d → Vec d} (hu : MemH1a b V u Du) : sEnergyOn b V Du ≠ ⊤

The H¹_a(V) class is honest on a bounded V: its weak gradient has finite weighted energy.

Hypotheses used, in full: the coefficient class hypothesis 0 < lam, hell; and V bounded. Boundedness of V is genuinely needed: the approximants of MemH1a are globally smooth but not compactly supported, so nothing bounds their gradients on an unbounded V.

theorem HCPolySupport.HighContrast.memH1a_of_memH1a0 {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {u : Vec d → ℝ} {Du : Vec d → Vec d} (hu : MemH1a0 b V u Du) : MemH1a b V u Du

A compactly supported smooth approximant is in particular a globally smooth one: H¹_{a,0}(V) ⊆ H¹_a(V).

theorem HCPolySupport.HighContrast.sEnergyOn_ne_top_of_memH1a0 {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hlam : 0 < lam) (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x)) {u : Vec d → ℝ} {Du : Vec d → Vec d} (hu : MemH1a0 b V u Du) : sEnergyOn b V Du ≠ ⊤

The H¹_{a,0}(V) class is honest on an arbitrary V: the approximants are compactly supported inside V, so no boundedness of V is needed.

theorem HCPolySupport.HighContrast.isBounded_euclideanBall (d : ℕ) {R : ℝ} (hR : 0 < R) : Bornology.IsBounded (euclideanBall d R)

Centered Euclidean balls are bounded.

theorem HCPolySupport.HighContrast.sEnergyOn_ne_top_of_memH1sLoc {d : ℕ} {b : CoeffField d} (hb : IsAELocallyUniformlyElliptic b) {v : Vec d → ℝ} {Dv : Vec d → Vec d} (hv : MemH1sLoc b v Dv) {R : ℝ} (hR : 0 < R) : sEnergyOn b (euclideanBall d R) Dv ≠ ⊤

The H¹_{s,loc}(ℝ^d) class is honest: on every centered Euclidean ball, the weak gradient has finite weighted energy, with the ball's own ellipticity constants.