High-contrast homogenization: Provider.Window.CountableSubadditivity

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

Countable subadditivity over an almost-everywhere partition

The response functional is subadditive over a countable disjoint family of bounded convex cells when the weighted cell quadratic forms are summable.

theorem HCPolySupport.HighContrast.Window.ae_eq_iUnion_of_countable_aePartition {d : ℕ} {ι : Type u_1} {U : Set (Vec d)} {c : ι → Set (Vec d)} (hsub : ∀ (i : ι), c i ⊆ U) (hnull : MeasureTheory.volume (U \ ⋃ (i : ι), c i) = 0) : U =ᵐ[MeasureTheory.volume] ⋃ (i : ι), c i

The parent and a countable disjoint covering by subsets agree almost everywhere when the uncovered part is null.

theorem HCPolySupport.HighContrast.Window.tsum_weight_eq_one_of_countable_aePartition {d : ℕ} {ι : Type u_1} [Countable ι] {U : Set (Vec d)} {c : ι → Set (Vec d)} (hmeas : ∀ (i : ι), MeasurableSet (c i)) (hsub : ∀ (i : ι), c i ⊆ U) (hdisj : Pairwise fun (i j : ι) => Disjoint (c i) (c j)) (hnull : MeasureTheory.volume (U \ ⋃ (i : ι), c i) = 0) (hU0 : MeasureTheory.volume U ≠ 0) (hUtop : MeasureTheory.volume U ≠ ⊤) : ∑' (i : ι), (MeasureTheory.volume (c i)).toReal / (MeasureTheory.volume U).toReal = 1

The weights of a countable almost-everywhere partition sum to one.

theorem HCPolySupport.HighContrast.Window.volumeAverage_eq_tsum_weight_of_countable_aePartition {d : ℕ} {ι : Type u_1} [Countable ι] {U : Set (Vec d)} {c : ι → Set (Vec d)} {f : Vec d → ℝ} (hmeas : ∀ (i : ι), MeasurableSet (c i)) (hsub : ∀ (i : ι), c i ⊆ U) (hdisj : Pairwise fun (i j : ι) => Disjoint (c i) (c j)) (hnull : MeasureTheory.volume (U \ ⋃ (i : ι), c i) = 0) (hint : MeasureTheory.IntegrableOn f U MeasureTheory.volume) (hcell0 : ∀ (i : ι), MeasureTheory.volume (c i) ≠ 0) (hUtop : MeasureTheory.volume U ≠ ⊤) : volumeAverage U f = ∑' (i : ι), (MeasureTheory.volume (c i)).toReal / (MeasureTheory.volume U).toReal * volumeAverage (c i) f

The volume average over a countable almost-everywhere partition is the weighted sum of the cell averages.

theorem HCPolySupport.HighContrast.Window.summable_weight_mul_volumeAverage_of_countable_aePartition {d : ℕ} {ι : Type u_1} [Countable ι] {U : Set (Vec d)} {c : ι → Set (Vec d)} {f : Vec d → ℝ} (hmeas : ∀ (i : ι), MeasurableSet (c i)) (hsub : ∀ (i : ι), c i ⊆ U) (hdisj : Pairwise fun (i j : ι) => Disjoint (c i) (c j)) (hint : MeasureTheory.IntegrableOn f U MeasureTheory.volume) (hcell0 : ∀ (i : ι), MeasureTheory.volume (c i) ≠ 0) (hUtop : MeasureTheory.volume U ≠ ⊤) : Summable fun (i : ι) => (MeasureTheory.volume (c i)).toReal / (MeasureTheory.volume U).toReal * volumeAverage (c i) f

The weighted cell averages over a countable measurable partition form a summable family whenever the integrand is integrable on the parent.

theorem HCPolySupport.HighContrast.Window.blockQuadratic_le_tsum_weight_of_countable_aePartition {d : ℕ} [NeZero d] {ι : Type u_1} [Countable ι] {U : Set (Vec d)} {c : ι → Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hU0 : MeasureTheory.volume U ≠ 0) (a : CoeffSpace d) (hc : ∀ (i : ι), IsOpenBoundedConvexDomain (c i)) (hsub : ∀ (i : ι), c i ⊆ U) (hdisj : Pairwise fun (i j : ι) => Disjoint (c i) (c j)) (hnull : MeasureTheory.volume (U \ ⋃ (i : ι), c i) = 0) (hcell0 : ∀ (i : ι), MeasureTheory.volume (c i) ≠ 0) (X : BlockVec d) (hsum : Summable fun (i : ι) => (MeasureTheory.volume (c i)).toReal / (MeasureTheory.volume U).toReal * (1 / 2 * blockVecDot X (blockMatVecMul (coarseBlock (c i) a) X))) : 1 / 2 * blockVecDot X (blockMatVecMul (coarseBlock U a) X) ≤ ∑' (i : ι), (MeasureTheory.volume (c i)).toReal / (MeasureTheory.volume U).toReal * (1 / 2 * blockVecDot X (blockMatVecMul (coarseBlock (c i) a) X))

Countable subadditivity of the coarse response in quadratic-form order. The summability premise is a convergence condition, not an estimate: callers prove it from their quantitative row bound.