SelectorReconstruction.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Minimal moves reconstruct inside the heavy sets

The family member in this theorem is any member witnessing feasibility of the selected endpoint. It need not be the member restricting the changed set in the minimization. This permits one witness to be used for an entire profile.

theorem OAI.TalagrandThreshold.Selector.selected_movedRow_subset_heavySet line 22
Source documentation
Every point moved into row i is heavy for every admissible cutoff of any common feasibility witness. Otherwise its actual color can be delayed by one, preserving that witness and contradicting minimal total movement.
```
theorem selected_movedRow_subset_heavySet {F : Family α} (mu : MassFamily F)
    {s : ℕ} (a z : Coloring α s) (hselected : Selected mu a z)
    (H : ↥F) (hfeasible : FeasibleFor mu a z H) (i : Fin s) (ε : ℝ)
    (hε : Admissible (mu.weight H) (prefixSet z i)
      (crossings a z i : ℝ) (dscale i) ε) :
    movedRow a z i ⊆ heavySet (mu.weight H) ε := by
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.Selected, OAI.TalagrandThreshold.Selector.FeasibleFor, OAI.TalagrandThreshold.Selector.Admissible, OAI.TalagrandThreshold.Selector.prefixSet, OAI.TalagrandThreshold.Selector.crossings, OAI.TalagrandThreshold.Selector.dscale, OAI.TalagrandThreshold.Selector.movedRow, OAI.TalagrandThreshold.Selector.heavySet
theorem OAI.TalagrandThreshold.Selector.selected_movedRow_subset_filter line 47
Source documentation
The same reconstruction statement with the heavy set written explicitly.
```
theorem selected_movedRow_subset_filter {F : Family α} (mu : MassFamily F)
    {s : ℕ} (a z : Coloring α s) (hselected : Selected mu a z)
    (H : ↥F) (hfeasible : FeasibleFor mu a z H) (i : Fin s) (ε : ℝ)
    (hε : Admissible (mu.weight H) (prefixSet z i)
      (crossings a z i : ℝ) (dscale i) ε) :
    movedRow a z i ⊆ Finset.univ.filter (fun x => ε < mu.weight H x) := by
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.Selected, OAI.TalagrandThreshold.Selector.FeasibleFor, OAI.TalagrandThreshold.Selector.Admissible, OAI.TalagrandThreshold.Selector.prefixSet, OAI.TalagrandThreshold.Selector.crossings, OAI.TalagrandThreshold.Selector.dscale, OAI.TalagrandThreshold.Selector.movedRow