High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.BallTriangleCore

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

Minkowski for the volume-normalized weighted norm, on an arbitrary domain

weightedGradNorm b V F = ‖s(b)^{1/2} F‖_{L_underlined²(V)} is built on ∫⁻, Mathlib's lower Lebesgue integral, so the triangle inequality is false for arbitrary F, G: for a Bernstein set S the pair F = 1_S • v, G = -1_{Sᶜ} • v has both norms 0 while F - G = v. It is true, and is proved here, for square-integrable fields, where the norm is the genuine seminorm of the positive symmetric coefficient form on HilbertVectorL2 V.

Three steps.

• ofReal_sqrt_normalizedLocalSymmetricEnergy_eq_weightedGradNorm identifies ENNReal.ofReal (√ E(F)) with weightedGradNorm b V F on an L² witness. It is the square root of the ofReal_normalizedLocalSymmetricEnergy_eq_weightedGradNorm_sq, taken in ℝ≥0∞ through the injectivity of squaring.
• weightedGradNorm_sub_le_add_of_memVectorL2 is then Minkowski for the positive form (sqrt_normalizedLocalSymmetricEnergy_add_le, stated for an arbitrary U : Set (Vec d)), applied to F and -G and transported through the class identity for a difference.
• weightedGradNorm_sub_le_add_of_aeElliptic removes the pointwise IsEllipticFieldOn hypothesis: a field of the coefficient class is elliptic only almost everywhere on the bounded measurable set carrying the norm, with that set's constants, so the estimate is transported along weightedGradNorm_congr_coeff_ae_on from the pointwise-good representative that fills the exceptional set with lam • I — the construction of Internal.Ch02.BookCh02.pointwiseCoeffField, redone here for an arbitrary measurable set rather than for a Domain.

The degenerate case volume V = 0 needs no hypothesis at all: the lower integral over a null set vanishes and 0 / 0 = 0 in ℝ≥0∞, so every weighted norm is 0 there.

The degenerate domain

theorem HCPolySupport.HighContrast.CorrectorComposition.weightedGradNorm_of_volume_eq_zero {d : ℕ} {U : Set (Vec d)} (hU : MeasureTheory.volume U = 0) (b : CoeffField d) (F : Vec d → Vec d) : weightedGradNorm b U F = 0

On a null domain every weighted norm vanishes: the restricted measure is zero, so the lower integral is 0, and 0 / 0 = 0 in ℝ≥0∞.

The square-root bridge

theorem HCPolySupport.HighContrast.CorrectorComposition.ofReal_sqrt_normalizedLocalSymmetricEnergy_eq_weightedGradNorm {d : ℕ} {U : Set (Vec d)} {b : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U b) {f : Vec d → Vec d} (hf : MemVectorL2 U f) : ENNReal.ofReal √(normalizedLocalSymmetricEnergy hEll (toHilbertVectorL2OfVecField hf)) = weightedGradNorm b U f

The ℝ≥0∞ weighted norm of a square-integrable field is the square root of its normalized symmetric class energy.

The class identity for a difference

Minkowski, for a pointwise elliptic coefficient

theorem HCPolySupport.HighContrast.CorrectorComposition.weightedGradNorm_sub_le_add_of_memVectorL2 {d : ℕ} {U : Set (Vec d)} {b : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U b) (hvol : 0 < MeasureTheory.volume U) (hvoltop : MeasureTheory.volume U ≠ ⊤) {F G : Vec d → Vec d} (hF : MemVectorL2 U F) (hG : MemVectorL2 U G) : (weightedGradNorm b U fun (x : Vec d) => F x - G x) ≤ weightedGradNorm b U F + weightedGradNorm b U G

The triangle inequality for ‖s^{1/2} ·‖_{L_underlined²(U)}, on two square-integrable fields. The membership hypotheses are not removable (∫⁻ is the lower integral).

The pointwise-good representative on an arbitrary measurable set

theorem HCPolySupport.HighContrast.CorrectorComposition.exists_isEllipticFieldOn_ae_eq {d : ℕ} {b0 : CoeffField d} {lam Lam : ℝ} (hlam : 0 < lam) (hle : lam ≤ Lam) (hb0 : MeasureTheory.StronglyMeasurable b0) {U : Set (Vec d)} (hU : MeasurableSet U) (hell : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict U, IsEllipticMatrix lam Lam (b0 x)) : ∃ (b' : CoeffField d), IsEllipticFieldOn lam Lam U b' ∧ b' =ᵐ[MeasureTheory.volume.restrict U] b0

A strongly measurable field elliptic almost everywhere on a measurable set, with that set's constants, has a pointwise elliptic representative there, agreeing with it almost everywhere on the set: fill the exceptional set with lam • I.

Minkowski, for an almost-everywhere elliptic coefficient

theorem HCPolySupport.HighContrast.CorrectorComposition.weightedGradNorm_sub_le_add_of_aeElliptic {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (hvoltop : MeasureTheory.volume U ≠ ⊤) {b b0 : CoeffField d} {lam Lam : ℝ} (hlam : 0 < lam) (hle : lam ≤ Lam) (hb0 : MeasureTheory.StronglyMeasurable b0) (hb0ae : b0 =ᵐ[MeasureTheory.volume] b) (hell : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict U, IsEllipticMatrix lam Lam (b0 x)) {F G : Vec d → Vec d} (hF : MemVectorL2 U F) (hG : MemVectorL2 U G) : (weightedGradNorm b U fun (x : Vec d) => F x - G x) ≤ weightedGradNorm b U F + weightedGradNorm b U G

The triangle inequality on a measurable set of finite volume, for a coefficient field elliptic only almost everywhere on that set, with that set's constants — the situation of every field of the coefficient class.