SelectorMain.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The simultaneous multiscale selector

The actual minimum-move cover bounds the bad probability from below by its weighted cost. The profile reconstruction and counting theorem bounds that same cost from above. Both conclusions use the literal independent color law.

theorem OAI.TalagrandThreshold.Selector.half_bad_probability_le_selected_cost line 24
Source documentation
The actual selected changed sets give the cover-cost inequality.
```
theorem half_bad_probability_le_selected_cost {F : Family α}
    (mu : MassFamily F) (p : ℝ) (s : ℕ) (hp : 0 < p)
    (hs : p * scaleSum s ≤ 1 / 2) (hF : ¬ Small p F) :
    (1 / 2 : ℝ) * (coloringLaw (α := α) p s hp hs).prob (Bad mu) ≤
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.scaleSum, OAI.TalagrandThreshold.Small, OAI.TalagrandThreshold.coloringLaw, OAI.TalagrandThreshold.Selector.Bad
theorem OAI.TalagrandThreshold.Selector.bad_probability_le_one_tenth line 44
Source documentation
The actual bad event has probability at most one tenth.
```
theorem bad_probability_le_one_tenth {F : Family α}
    (mu : MassFamily F) (p : ℝ) (s : ℕ) (hp : 0 < p)
    (hs : p * scaleSum s ≤ 1 / 2) (hF : ¬ Small p F) :
    (coloringLaw (α := α) p s hp hs).prob (Bad mu) ≤ 1 / 10 := by
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.scaleSum, OAI.TalagrandThreshold.Small, OAI.TalagrandThreshold.coloringLaw, OAI.TalagrandThreshold.Selector.Bad
theorem OAI.TalagrandThreshold.Selector.simultaneous_capture line 53
Source documentation
One family member is simultaneously captured at every scale.
```
theorem simultaneous_capture (F : Family α) (_hF : F.Nonempty)
    (_hsets : ∀ H ∈ F, H.Nonempty) (mu : MassFamily F)
    (p : ℝ) (hp0 : 0 < p) (_hp1 : p ≤ 1) (hnotsmall : ¬ Small p F)
    (s : ℕ) (hs : p * scaleSum s ≤ 1 / 2) :
    (9 / 10 : ℝ) ≤
      (coloringLaw (α := α) p s hp0 hs).prob (Captured mu) := by
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Small, OAI.TalagrandThreshold.scaleSum, OAI.TalagrandThreshold.coloringLaw, OAI.TalagrandThreshold.Selector.Captured
theorem OAI.TalagrandThreshold.Selector.average_color line 66
Source documentation
With probability at least nine tenths, one member has mean color at most two.
```
theorem average_color (F : Family α) (hF : F.Nonempty)
    (hsets : ∀ H ∈ F, H.Nonempty) (mu : MassFamily F)
    (p : ℝ) (hp0 : 0 < p) (hp1 : p ≤ 1) (hnotsmall : ¬ Small p F)
    (s : ℕ) (hs : p * scaleSum s ≤ 1 / 2) :
    (9 / 10 : ℝ) ≤ (coloringLaw (α := α) p s hp0 hs).prob
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Small, OAI.TalagrandThreshold.scaleSum, OAI.TalagrandThreshold.coloringLaw