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

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

Finite Volume Weights

For a finite-measure set W and measurable subsets U i ⊆ W, the relative volumes volume (U i) / volume W have finite partial sums at most one and form a summable family, and every finite disjoint subfamily splits volume W into the volumes of its pieces together with the volume of the uncovered remainder, normalized to total mass one. These are the volume weights that the countable subadditivity of the response quadratic is summed against, in the proofs of p.response.transfer and p.successful.short.bridge.

Volume weights for CG response sums

Self-contained CG/Mathlib support for the relative-volume weights appearing in the countable response summability statement.

theorem HCPolySupport.HighContrast.CG.volume_piece_ne_top_of_subset {d : ℕ} {W V : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn W)] (hsub : V ⊆ W) : MeasureTheory.volume V ≠ ⊤

theorem HCPolySupport.HighContrast.CG.sum_volumeRatio_le_one {d : ℕ} {ι : Type u_1} {s : Set ι} {W : Set (Vec d)} {U : ι → Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn W)] (hmeas : ∀ i ∈ s, MeasurableSet (U i)) (hsub : ∀ i ∈ s, U i ⊆ W) (hdisj : s.PairwiseDisjoint U) (F : Finset ↑s) : ∑ i ∈ F, (MeasureTheory.volume (U ↑i)).toReal / (MeasureTheory.volume W).toReal ≤ 1

theorem HCPolySupport.HighContrast.CG.summable_volumeRatio {d : ℕ} {ι : Type u_1} {s : Set ι} {W : Set (Vec d)} {U : ι → Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn W)] (hmeas : ∀ i ∈ s, MeasurableSet (U i)) (hsub : ∀ i ∈ s, U i ⊆ W) (hdisj : s.PairwiseDisjoint U) : Summable fun (i : ↑s) => (MeasureTheory.volume (U ↑i)).toReal / (MeasureTheory.volume W).toReal

Finite splitting for CG response defects

Self-contained CG/Mathlib support for finite volume and integral decompositions. The same finite-volume facts are proved again in the response-weight file; this module repeats the short measure-theory layer instead of importing any HCPoly.Entry.* module.

theorem HCPolySupport.HighContrast.CG.volume_eq_sum_add_remainder {d : ℕ} {ι : Type u_1} (F : Finset ι) {W : Set (Vec d)} {U : ι → Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn W)] (hmeas : ∀ i ∈ F, MeasurableSet (U i)) (hsub : ∀ i ∈ F, U i ⊆ W) (hdisj : (↑F).PairwiseDisjoint U) : (MeasureTheory.volume W).toReal = ∑ i ∈ F, (MeasureTheory.volume (U i)).toReal + (MeasureTheory.volume (W \ ⋃ i ∈ F, U i)).toReal

theorem HCPolySupport.HighContrast.CG.sum_volumeRatio_add_remainder_eq_one {d : ℕ} {ι : Type u_1} (F : Finset ι) {W : Set (Vec d)} {U : ι → Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn W)] (hWvol : (MeasureTheory.volume W).toReal ≠ 0) (hmeas : ∀ i ∈ F, MeasurableSet (U i)) (hsub : ∀ i ∈ F, U i ⊆ W) (hdisj : (↑F).PairwiseDisjoint U) : ∑ i ∈ F, (MeasureTheory.volume (U i)).toReal / (MeasureTheory.volume W).toReal + (MeasureTheory.volume (W \ ⋃ i ∈ F, U i)).toReal / (MeasureTheory.volume W).toReal = 1