High-contrast homogenization: Provider.Quenched.SmallContrastRowWeightSummable

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

Row weights: summability and the partition bound together

The relative-volume bound bounds the value of the row series but says nothing about summability — in Mathlib ∑' f ≤ 1 holds of every unsummable f, since an unsummable tsum is 0. Its consumer needs both: the burn split replaces a dominating geometric series with a partition bound, and a partition bound is not a domination, so summability has to come from somewhere else.

It comes from the same place the bound does — nonnegativity together with uniformly bounded partial sums — and the partial sums are bounded because a finite subfamily of a disjoint filling has total volume at most the parent's. Both facts are recorded here, the first at the generality the bridge uses and the second purely arithmetically.

theorem HCPolySupport.HighContrast.Quenched.finset_relative_volume_le_one {d : ℕ} {ι : Type u_1} (s : Finset ι) {c : ι → Set (Vec d)} {T : Set (Vec d)} (hmeas : ∀ i ∈ s, MeasurableSet (c i)) (hdisj : (↑s).Pairwise (Function.onFun Disjoint c)) (hsub : ∀ i ∈ s, c i ⊆ T) (hT : MeasureTheory.volume T ≠ ⊤) (hT0 : MeasureTheory.volume T ≠ 0) : ∑ i ∈ s, (MeasureTheory.volume (c i)).toReal / (MeasureTheory.volume T).toReal ≤ 1

A finite disjoint subfamily has total relative volume at most one. This is what bounds the partial sums of the row series.

theorem HCPolySupport.HighContrast.Quenched.summable_and_tsum_le_one_of_sum_range_le {w : ℕ → ℝ} (hw0 : ∀ (u : ℕ), 0 ≤ w u) (hpartial : ∀ (N : ℕ), ∑ u ∈ Finset.range N, w u ≤ 1) : Summable w ∧ ∑' (u : ℕ), w u ≤ 1

Summability and the bound, from nonnegativity and bounded partial sums. This is the conjunction the burn split's consumer needs; the bound alone is not enough, because an unsummable family satisfies it vacuously.