SelectorFeasibility.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Feasible minima and the actual containment cover

Resetting an original family member to the first color proves existence of a bounded feasible move. Minimization itself retains the unrestricted feasibility witness from Feasible; the witness need not be that member. All retained minima contribute their actual changed sets to a cover.

def OAI.TalagrandThreshold.Selector.reset line 27
Source documentation
Reset only the specified member to zero, the first color index.
```
def reset (a : Coloring α s) (H₀ : ↥F) : Coloring α s :=
…
```
Mentions: OAI.TalagrandThreshold.Coloring
theorem OAI.TalagrandThreshold.Selector.reset_earlier line 31
theorem OAI.TalagrandThreshold.Selector.changes_reset_subset line 38
theorem OAI.TalagrandThreshold.Selector.reset_feasibleFor line 46
Source documentation
The reset uses this one member as a witness, with every cutoff zero.
```
theorem reset_feasibleFor (mu : MassFamily F) (a : Coloring α s) (H₀ : ↥F) :
    FeasibleFor mu a (reset a H₀) H₀ := by
…
```
Mentions: OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.FeasibleFor, OAI.TalagrandThreshold.Selector.reset
theorem OAI.TalagrandThreshold.Selector.reset_boundedFeasible line 65
theorem OAI.TalagrandThreshold.Selector.exists_isMinimalMove line 70
Source documentation
A minimum exists for every member, without restricting its witness.
```
theorem exists_isMinimalMove (mu : MassFamily F) (a : Coloring α s) (H₀ : ↥F) :
    ∃ z, IsMinimalMove mu a H₀ z := by
…
```
Mentions: OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.IsMinimalMove
theorem OAI.TalagrandThreshold.Selector.Selected.feasible line 83
theorem OAI.TalagrandThreshold.Selector.Selected.earlier line 88
theorem OAI.TalagrandThreshold.Selector.mem_selectedMoves line 91
def OAI.TalagrandThreshold.Selector.selectedChanges line 97
Source documentation
Remove duplicate changed sets only when forming the containment cover.
```
def selectedChanges (mu : MassFamily F) (a : Coloring α s) : Family α := by
…
```
Mentions: OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Family
theorem OAI.TalagrandThreshold.Selector.selectedChanges_covers line 101
theorem OAI.TalagrandThreshold.Selector.half_lt_selectedMoves_cost line 111
Source documentation
The sum over selected colorings dominates the cost with duplicates removed.
```
theorem half_lt_selectedMoves_cost (mu : MassFamily F) (a : Coloring α s)
    {p : ℝ} (hp : 0 ≤ p) (hF : ¬ Small p F) :
    (1 / 2 : ℝ) < ∑ z ∈ selectedMoves mu a, p ^ (changes a z).card := by
…
```
Mentions: OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Small, OAI.TalagrandThreshold.Selector.selectedMoves, OAI.TalagrandThreshold.Selector.changes
theorem OAI.TalagrandThreshold.Selector.eq_of_changes_eq_empty line 120
Source documentation
An earlier move with no changed vertex is the unchanged coloring.
```
theorem eq_of_changes_eq_empty {a z : Coloring α s} (hz : Earlier a z)
    (hempty : changes a z = ∅) : z = a := by
…
```
Mentions: OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.Earlier, OAI.TalagrandThreshold.Selector.changes
theorem OAI.TalagrandThreshold.Selector.truncatedExcess_le_original line 132
Source documentation
Restoring weights increases the excess: only heavy points change, and their coefficient is the nonnegative value d.
```
theorem truncatedExcess_le_original (w : α → ℝ) (A : Finset α) (d u : ℝ)
    (hd : 0 ≤ d) (hheavy : ∀ x, u < w x → x ∈ A) :
    truncatedExcess w A d u ≤
      ∑ x, w x * ((if x ∈ A then 1 else 0) - (1 - d)) := by
…
```
Mentions: OAI.TalagrandThreshold.Selector.truncatedExcess
theorem OAI.TalagrandThreshold.Selector.originalExcess_eq_mass_sub line 149
theorem OAI.TalagrandThreshold.Selector.captured_of_feasible_self line 165
Source documentation
The actual feasibility witness is chosen once, before the scale index.
```
theorem captured_of_feasible_self {mu : MassFamily F} {a : Coloring α s}
    (h : Feasible mu a a) : Captured mu a := by
…
```
Mentions: OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.Feasible, OAI.TalagrandThreshold.Selector.Captured
theorem OAI.TalagrandThreshold.Selector.Selected.changes_nonempty line 185