High-contrast homogenization: Analytic.WeightedEnergy

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

The weighted Dirichlet energy against the unweighted one

The energy sEnergyOn b V F = ∫_V F · s F of the coefficient-weighted spaces of s.introduction is the Lebesgue integral of the quadratic form of the symmetric part s of the coefficient field. Where the field is uniformly elliptic almost everywhere on the set the integral runs over, the quadratic form is pinched between lam ‖F‖² and Lam ‖F‖² pointwise a.e. on that set, so the weighted energy is two-sided comparable to the unweighted one and is finite exactly when F ∈ L²(V). The constants are those of V; each comparison is stated first for the pinching restricted to V, and the form with a pinching on all of ℝ^d follows by restriction. The identity that lets the skew part drop out of the quadratic form is vecDot_matVecMul_symmPart, already in CoarseGraining.

Neither half of the comparison uses any measurability, of b or of F: both are pointwise a.e. comparisons of Lebesgue integrals. Measurability enters only where the ℝ≥0∞ finiteness statement is turned into Bochner square integrability, which is the form the pairing estimates consume.

theorem HCPolySupport.HighContrast.lintegral_ofReal_vecNormSq_le_sEnergyOn_restrict {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hell : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict V, IsEllipticMatrix lam Lam (b x)) (F : Vec d → Vec d) : ENNReal.ofReal lam * ∫⁻ (x : Vec d) in V, ENNReal.ofReal (vecNormSq (F x)) ≤ sEnergyOn b V F

The lower half of the comparison, with the pinching read on V alone: lam ∫_V ‖F‖² ≤ ∫_V F · s F.

theorem HCPolySupport.HighContrast.lintegral_ofReal_vecNormSq_le_sEnergyOn {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x)) (F : Vec d → Vec d) : ENNReal.ofReal lam * ∫⁻ (x : Vec d) in V, ENNReal.ofReal (vecNormSq (F x)) ≤ sEnergyOn b V F

The lower half of the comparison: lam ∫_V ‖F‖² ≤ ∫_V F · s F.

theorem HCPolySupport.HighContrast.sEnergyOn_le_lintegral_ofReal_vecNormSq_restrict {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hell : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict V, IsEllipticMatrix lam Lam (b x)) (F : Vec d → Vec d) : sEnergyOn b V F ≤ ENNReal.ofReal Lam * ∫⁻ (x : Vec d) in V, ENNReal.ofReal (vecNormSq (F x))

The upper half of the comparison, with the pinching read on V alone: ∫_V F · s F ≤ Lam ∫_V ‖F‖².

theorem HCPolySupport.HighContrast.sEnergyOn_le_lintegral_ofReal_vecNormSq {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x)) (F : Vec d → Vec d) : sEnergyOn b V F ≤ ENNReal.ofReal Lam * ∫⁻ (x : Vec d) in V, ENNReal.ofReal (vecNormSq (F x))

The upper half of the comparison: ∫_V F · s F ≤ Lam ∫_V ‖F‖².

theorem HCPolySupport.HighContrast.sEnergyOn_ne_top_iff_restrict {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hlam : 0 < lam) (hell : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict V, IsEllipticMatrix lam Lam (b x)) (F : Vec d → Vec d) : sEnergyOn b V F ≠ ⊤ ↔ ∫⁻ (x : Vec d) in V, ENNReal.ofReal (vecNormSq (F x)) ≠ ⊤

The weighted energy is finite exactly when the field is in L², with the pinching read on V alone. No measurability of b or of F is used: both halves are pointwise a.e. comparisons of Lebesgue integrals.

theorem HCPolySupport.HighContrast.sEnergyOn_ne_top_iff {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hlam : 0 < lam) (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x)) (F : Vec d → Vec d) : sEnergyOn b V F ≠ ⊤ ↔ ∫⁻ (x : Vec d) in V, ENNReal.ofReal (vecNormSq (F x)) ≠ ⊤

The weighted energy is finite exactly when the field is in L². No measurability of b or of F is used: both halves are pointwise a.e. comparisons of Lebesgue integrals.

theorem HCPolySupport.HighContrast.aestronglyMeasurable_vecNormSq {d : ℕ} {μ : MeasureTheory.Measure (Vec d)} {F : Vec d → Vec d} (hF : ∀ (j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => F x j) μ) : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => vecNormSq (F x)) μ

Measurability of the squared Euclidean norm of a vector field, from measurability of its components.

theorem HCPolySupport.HighContrast.integrableOn_vecNormSq_iff_lintegral_ne_top {d : ℕ} {V : Set (Vec d)} {F : Vec d → Vec d} (hF : ∀ (j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => F x j) (MeasureTheory.volume.restrict V)) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecNormSq (F x)) V MeasureTheory.volume ↔ ∫⁻ (x : Vec d) in V, ENNReal.ofReal (vecNormSq (F x)) ≠ ⊤

The ℝ≥0∞ finiteness statement and Bochner square integrability agree.

theorem HCPolySupport.HighContrast.integrableOn_vecNormSq_of_sEnergyOn_ne_top_restrict {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hlam : 0 < lam) (hell : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict V, IsEllipticMatrix lam Lam (b x)) {F : Vec d → Vec d} (hF : ∀ (j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => F x j) (MeasureTheory.volume.restrict V)) (hfin : sEnergyOn b V F ≠ ⊤) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecNormSq (F x)) V MeasureTheory.volume

Finite weighted energy forces F ∈ L²(V), with the pinching read on V alone; this is the hypothesis the absolute convergence of the weak pairing needs.

theorem HCPolySupport.HighContrast.integrableOn_vecNormSq_of_sEnergyOn_ne_top {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hlam : 0 < lam) (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x)) {F : Vec d → Vec d} (hF : ∀ (j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => F x j) (MeasureTheory.volume.restrict V)) (hfin : sEnergyOn b V F ≠ ⊤) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecNormSq (F x)) V MeasureTheory.volume

Finite weighted energy forces F ∈ L²(V), which is the hypothesis the absolute convergence of the weak pairing needs.