High-contrast homogenization: Provider.PolynomialHomogenization.CountableDisjointDiagonal

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

Diagonal integrals over a countable disjoint family

The diagonal products of pairwise disjoint measurable sets are again pairwise disjoint. Their nonnegative integrals therefore sum to at most the integral over any common containing set.

theorem HCPolySupport.HighContrast.tsum_setLIntegral_prod_self_le {ι : Type u_1} {α : Type u_2} [Countable ι] [MeasurableSpace α] (μ : MeasureTheory.Measure α) {A : ι → Set α} {U : Set α} (hAmeas : ∀ (i : ι), MeasurableSet (A i)) (hAdisj : Pairwise (Function.onFun Disjoint A)) (hAsub : ∀ (i : ι), A i ⊆ U) (f : α × α → ENNReal) : ∑' (i : ι), ∫⁻ (z : α × α) in A i ×ˢ A i, f z ∂μ.prod μ ≤ ∫⁻ (z : α × α) in U ×ˢ U, f z ∂μ.prod μ

The sum of diagonal product integrals over a countable disjoint family is bounded by the product integral over a containing set.