RoundingMasses.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Concrete rounding masses

Each nonempty subset's fractional weight is split equally among its members. Normalizing by the total nonempty-subset weight gives the probability mass used by the common selector. Both normalization and the mean identity are finite double-sum calculations.

def OAI.TalagrandThreshold.nonemptySubsets line 25
def OAI.TalagrandThreshold.memberMass line 27
def OAI.TalagrandThreshold.subsetAverage line 30
def OAI.TalagrandThreshold.roundingMass line 33
theorem OAI.TalagrandThreshold.mem_nonemptySubsets line 38
theorem OAI.TalagrandThreshold.memberMass_add_empty line 43
theorem OAI.TalagrandThreshold.memberMass_nonneg line 48
theorem OAI.TalagrandThreshold.empty_weight_le_half line 53
theorem OAI.TalagrandThreshold.memberMass_ge_half line 58
theorem OAI.TalagrandThreshold.memberMass_pos_of_fractionalCover line 67
theorem OAI.TalagrandThreshold.subsetAverage_nonneg line 75
theorem OAI.TalagrandThreshold.roundingMass_nonneg line 80
theorem OAI.TalagrandThreshold.roundingMass_eq_zero_of_not_mem line 91

theorem OAI.TalagrandThreshold.sum_uniform_subset_weight line 103

Source documentation

A nonempty set distributes exactly its original weight.

theorem sum_uniform_subset_weight (g : Finset α → ℝ) (S : Finset α)
    (hS : S ≠ ∅) :
    (∑ x : α, if x ∈ S then g S / (S.card : ℝ) else 0) = g S := by
…

theorem OAI.TalagrandThreshold.sum_rounding_numerator line 113
Source documentation
Counting each set's members evaluates the full double sum.
```
theorem sum_rounding_numerator (g : Finset α → ℝ) (H : Finset α) :
    (∑ x : α, ∑ S ∈ nonemptySubsets H,
      if x ∈ S then g S / (S.card : ℝ) else 0) = memberMass g H := by
…
```
Mentions: OAI.TalagrandThreshold.nonemptySubsets, OAI.TalagrandThreshold.memberMass
theorem OAI.TalagrandThreshold.roundingMass_sum line 121

theorem OAI.TalagrandThreshold.sum_weighted_uniform_subset_weight line 127

Source documentation

Averaging one set's distributed weight gives its subset average.

theorem sum_weighted_uniform_subset_weight (g : Finset α → ℝ)
    (S : Finset α) (a : α → ℝ) :
    (∑ x : α, a x * (if x ∈ S then g S / (S.card : ℝ) else 0)) =
      g S * subsetAverage a S := by
…

Mentions: OAI.TalagrandThreshold.subsetAverage

theorem OAI.TalagrandThreshold.roundingMass_mean line 136