SelectorDelayFeasibility.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Feasibility after delaying one color

Removing a point from a tested prefixSet subtracts exactly its truncated weight from the excess. If that point is not heavy, the heavy-set condition survives; the crossing count decreases by one, so the same cutoff remains admissible. The other tests and their cutoffs are unchanged.

theorem OAI.TalagrandThreshold.Selector.truncatedExcess_erase line 23
theorem OAI.TalagrandThreshold.Selector.Admissible.erase_one line 47
Source documentation
The same cutoff works after deleting a non-heavy point and reducing the crossing parameter by one. No maximality assumption on the cutoff is used.
```
theorem Admissible.erase_one {mu : α → ℝ} {A : Finset α} {m m' d u : ℝ}
    (hu : Admissible mu A m d u) {x : α} (hx : x ∈ A)
    (hxu : mu x ≤ u) (hm : m' + 1 = m) :
    Admissible mu (A.erase x) m' d u := by
…
```
Mentions: OAI.TalagrandThreshold.Selector.Admissible
theorem OAI.TalagrandThreshold.Selector.feasibleFor_delayColor line 67
Source documentation
An actual one-step delay preserves all tests for the same family member. At the affected scale it uses the supplied cutoff; all other cutoffs are the ones already supplied by hfeasible.
```
theorem feasibleFor_delayColor {F : Family α} (mu : MassFamily F) {s : ℕ}
    (a z : Coloring α s) (H : ↥F) (hfeasible : FeasibleFor mu a z H)
    (x : α) (i : Fin s) (hx : (z x).val = i.val)
    (hmove : (z x).val < (a x).val) (ε : ℝ)
    (hε : Admissible (mu.weight H) (prefixSet z i)
      (crossings a z i : ℝ) (dscale i) ε)
    (hweight : mu.weight H x ≤ ε) :
    FeasibleFor mu a (delayColor z x i) H := by
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.FeasibleFor, OAI.TalagrandThreshold.Selector.Admissible, OAI.TalagrandThreshold.Selector.prefixSet, OAI.TalagrandThreshold.Selector.crossings, OAI.TalagrandThreshold.Selector.dscale, OAI.TalagrandThreshold.Selector.delayColor