RoundingLowerBound.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The deterministic lower bound for rounding

A weighted average at most two places at least half the mass on subsets with average at most four. On those subsets the quotient-of-powers product is at least one, yielding the lower bound one quarter for the full product score. This statement is pointwise in the coloring and needs no independence premise.

theorem OAI.TalagrandThreshold.half_mass_of_weighted_average_le line 23

Source documentation

Finite weighted Markov inequality in the form used by rounding.

theorem half_mass_of_weighted_average_le {β : Type*} (T : Finset β)
    (w v : β → ℝ) (hw : ∀ i ∈ T, 0 ≤ w i) (hv : ∀ i ∈ T, 0 ≤ v i)
    (hmean : (∑ i ∈ T, w i * v i) ≤ 2 * (∑ i ∈ T, w i)) :
    (∑ i ∈ T, w i) / 2 ≤ ∑ i ∈ T.filter (fun i => v i ≤ 4), w i := by
…

theorem OAI.TalagrandThreshold.subsetAverage_nat_nonneg line 53
theorem OAI.TalagrandThreshold.sum_le_four_card_of_subsetAverage_le line 60
theorem OAI.TalagrandThreshold.productScore_lower_of_mean line 70
Source documentation
The fractional member mass and its mean color force a product-score lower bound. Natural colors can include zero; the actual selector uses val + 1.
```
theorem productScore_lower_of_mean (g : Finset α → ℝ) (H : Finset α)
    (a : α → ℕ) (hg : ∀ S, 0 ≤ g S) (hMH : (1 / 2 : ℝ) ≤ memberMass g H)
    (hmean : (∑ x : α, (a x : ℝ) * roundingMass g H x) ≤ 2) :
    (1 / 4 : ℝ) ≤ productScore g (fun x => (512 : ℝ) ^ 4 / (512 : ℝ) ^ a x) := by
…
```
Mentions: OAI.TalagrandThreshold.memberMass, OAI.TalagrandThreshold.roundingMass, OAI.TalagrandThreshold.productScore