High-contrast homogenization: Entry.CG.Proofs.ResponseFiniteDefect

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

Finite CG response defect

For a finite pairwise disjoint family of open pieces U i of an open set W of finite volume, the response of a locally elliptic coefficient field over W is at most the volume-weighted sum of the responses over the pieces, plus the relative volume of the uncovered remainder W \ ⋃ i, U i times the plain pointwise upper bound lam⁻¹ * (Lam ^ 2 * vecNormSq p + vecNormSq q) on the response integrand. This finite subadditivity of the response over a partition, with its uncovered-volume defect, is the partition input to the coarse block comparisons of p.successful.short.bridge and to the parent--child recurrence p.fixed.geometry.parent.child.recurrence.

theorem HCPolySupport.HighContrast.CG.responseCompetitor_piece_le {d : ℕ} {W V : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn W)] (hWopen : IsOpen W) (hVopen : IsOpen V) (hsub : V ⊆ W) {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam W a) (p q : Vec d) (u : AHarmonicFunction a W) : ∫ (x : Vec d) in V, scalarResponseIntegrand W a p q u x ≤ (MeasureTheory.volume V).toReal * ResponseJ V p q a

theorem HCPolySupport.HighContrast.CG.responseCompetitor_remainder_le {d : ℕ} {W R : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn W)] (hR : MeasurableSet R) (hsub : R ⊆ W) {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam W a) (p q : Vec d) (u : AHarmonicFunction a W) : ∫ (x : Vec d) in R, scalarResponseIntegrand W a p q u x ≤ (MeasureTheory.volume R).toReal * (lam⁻¹ * (Lam ^ 2 * vecNormSq p + vecNormSq q))

theorem HCPolySupport.HighContrast.CG.responseCompetitor_finite_defect {d : ℕ} {ι : Type u_1} (F : Finset ι) {W : Set (Vec d)} {U : ι → Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn W)] (hWopen : IsOpen W) (hWvol : (MeasureTheory.volume W).toReal ≠ 0) (hopen : ∀ i ∈ F, IsOpen (U i)) (hsub : ∀ i ∈ F, U i ⊆ W) (hdisj : (↑F).PairwiseDisjoint U) {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam W a) (p q : Vec d) (u : AHarmonicFunction a W) : volumeAverage W (scalarResponseIntegrand W a p q u) ≤ ∑ i ∈ F, (MeasureTheory.volume (U i)).toReal / (MeasureTheory.volume W).toReal * ResponseJ (U i) p q a + (MeasureTheory.volume (W \ ⋃ i ∈ F, U i)).toReal / (MeasureTheory.volume W).toReal * (lam⁻¹ * (Lam ^ 2 * vecNormSq p + vecNormSq q))

theorem HCPolySupport.HighContrast.CG.responseJ_le_weightedSum_add_remainder {d : ℕ} {ι : Type u_1} (F : Finset ι) {W : Set (Vec d)} {U : ι → Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn W)] (hWopen : IsOpen W) (hWvol : (MeasureTheory.volume W).toReal ≠ 0) (hopen : ∀ i ∈ F, IsOpen (U i)) (hsub : ∀ i ∈ F, U i ⊆ W) (hdisj : (↑F).PairwiseDisjoint U) {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam W a) (p q : Vec d) : ResponseJ W p q a ≤ ∑ i ∈ F, (MeasureTheory.volume (U i)).toReal / (MeasureTheory.volume W).toReal * ResponseJ (U i) p q a + (MeasureTheory.volume (W \ ⋃ i ∈ F, U i)).toReal / (MeasureTheory.volume W).toReal * (lam⁻¹ * (Lam ^ 2 * vecNormSq p + vecNormSq q))