RoundingMain.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual rounding of an unrestricted fractional cover

The concrete member masses feed the proved multiscale selector. The same independent color law supplies the lower and upper bounds on the subset-product score. No selector hypothesis or bound on support sizes appears in the result.

theorem OAI.TalagrandThreshold.fractionalCover_empty_not_mem line 26
def OAI.TalagrandThreshold.fractionalMassFamily line 37
Source documentation
The actual normalized probability masses attached to family members.
```
def fractionalMassFamily (F : Family α) (g : Finset α → ℝ) {r : ℝ}
    (hr : 0 ≤ r) (hcover : FractionalCover F g) (hcost : fracCost r g ≤ 1 / 2) :
    Selector.MassFamily F where
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.FractionalCover, OAI.TalagrandThreshold.fracCost, OAI.TalagrandThreshold.Selector.MassFamily
theorem OAI.TalagrandThreshold.fractionalCover_rounding line 49
Source documentation
Every fractional cover of cost at most one half rounds at the exact parameter r / (25 * 512^4). Its support may contain subsets of any size.
```
theorem fractionalCover_rounding (F : Family α) (g : Finset α → ℝ) {r : ℝ}
    (hr0 : 0 < r) (hr1 : r ≤ 1) (hcover : FractionalCover F g)
    (hcost : fracCost r g ≤ 1 / 2) :
    Small (r / ((25 : ℝ) * (512 : ℝ) ^ 4)) F := by
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.FractionalCover, OAI.TalagrandThreshold.fracCost, OAI.TalagrandThreshold.Small
theorem OAI.TalagrandThreshold.fractionalSmall_rounding line 96
Source documentation
Parameterwise rounding also includes density zero, with an actual cover.
```
theorem fractionalSmall_rounding (F : Family α) {r : ℝ}
    (hr0 : 0 ≤ r) (hr1 : r ≤ 1) (hF : FractionalSmall r F) :
    Small (r / ((25 : ℝ) * (512 : ℝ) ^ 4)) F := by
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.FractionalSmall, OAI.TalagrandThreshold.Small