High-contrast homogenization: Entry.CG.Proofs.ResponseSummable #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Summability of weighted CG responses #
For a countable family of pairwise disjoint open pieces inside a locally elliptic container,
the relative-volume-weighted scalar coarse responses ResponseJ are summable. Each response
is nonnegative and bounded by the container's plain ellipticity bound λ⁻¹ (Λ² |p|² + |q|²),
so the weighted series is dominated by the relative volumes of the pieces, which sum to at
most one. This is the summability input to the countable response subadditivity used by
p.successful.short.bridge.
theorem
HCPolySupport.HighContrast.CG.responseJ_piece_bounds
{d : ℕ}
{ι : Type u_1}
{s : Set ι}
{W : Set (Vec d)}
{U : ι → Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn W)]
(hopen : ∀ i ∈ s, IsOpen (U i))
(hsub : ∀ i ∈ s, U i ⊆ W)
{a : CoeffField d}
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam W a)
(p q : Vec d)
{i : ι}
(hi : i ∈ s)
(hvol : (MeasureTheory.volume (U i)).toReal ≠ 0)
:
theorem
HCPolySupport.HighContrast.CG.summable_volumeWeightedResponseJ
{d : ℕ}
{ι : Type u_1}
{s : Set ι}
(_hs : s.Countable)
{W : Set (Vec d)}
{U : ι → Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn W)]
(hopen : ∀ i ∈ s, IsOpen (U i))
(hsub : ∀ i ∈ s, U i ⊆ W)
(hdisj : s.PairwiseDisjoint U)
{a : CoeffField d}
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam W a)
(p q : Vec d)
:
Summable fun (i : ↑s) => (MeasureTheory.volume (U ↑i)).toReal / (MeasureTheory.volume W).toReal * ResponseJ (U ↑i) p q a