SelectorGlobalCost.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The global cost of actual selected moves

Partition selected pairs first by their final coloring and then by their full profile. The profile estimate removes the profile-dependent heavy sets before summation. Word-count normalization and the finite geometric bound then give the strict budget under the actual coloring law.

def OAI.TalagrandThreshold.Selector.selectedOriginals line 27
Source documentation
Actual bad original colorings that select one fixed endpoint.
```
def selectedOriginals (mu : MassFamily F) (z : Coloring α s) :
    Finset (Coloring α s) := by
…
```
Mentions: OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Coloring
def OAI.TalagrandThreshold.Selector.selectedProfiles line 33
Source documentation
Only the full profiles that occur for this endpoint.
```
def selectedProfiles (mu : MassFamily F) (z : Coloring α s) :
    Finset (Profile s) := by
…
```
Mentions: OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.Profile
theorem OAI.TalagrandThreshold.Selector.mem_selectedOriginals line 38
theorem OAI.TalagrandThreshold.Selector.selectedProfiles_rowCount_ne_zero line 45
Source documentation
A selected move from a bad coloring has a nonzero tuple of row sizes.
```
theorem selectedProfiles_rowCount_ne_zero (mu : MassFamily F)
    (z : Coloring α s) (n : Profile s) (hn : n ∈ selectedProfiles mu z) :
    rowCount n ≠ 0 := by
…
```
Mentions: OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.Profile, OAI.TalagrandThreshold.Selector.selectedProfiles, OAI.TalagrandThreshold.Selector.rowCount
theorem OAI.TalagrandThreshold.Selector.selected_endpoint_cost_grouped line 58
Source documentation
Grouping by the actual full profile loses no original coloring.
```
theorem selected_endpoint_cost_grouped (mu : MassFamily F)
    (z : Coloring α s) (f : Coloring α s → ℝ) :
    (∑ a ∈ selectedOriginals mu z, f a) =
      ∑ n ∈ selectedProfiles mu z, ∑ a ∈ groupOriginals mu z n, f a := by
…
```
Mentions: OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.selectedOriginals, OAI.TalagrandThreshold.Selector.selectedProfiles, OAI.TalagrandThreshold.Selector.groupOriginals
theorem OAI.TalagrandThreshold.Selector.selected_cost_group_by_endpoint line 79
Source documentation
Swapping the two finite sums groups all actual selected pairs by endpoint.
```
theorem selected_cost_group_by_endpoint (mu : MassFamily F)
    (f : Coloring α s → Coloring α s → ℝ) :
    (∑ a ∈ (Finset.univ : Finset (Coloring α s)).filter (Bad mu),
      ∑ z ∈ selectedMoves mu a, f a z) =
      ∑ z : Coloring α s, ∑ a ∈ selectedOriginals mu z, f a z := by
…
```
Mentions: OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.Bad, OAI.TalagrandThreshold.Selector.selectedMoves, OAI.TalagrandThreshold.Selector.selectedOriginals
theorem OAI.TalagrandThreshold.Selector.selected_endpoint_cost_lt line 99
Source documentation
All actual original colorings for one endpoint fit its probability-weighted budget.
```
theorem selected_endpoint_cost_lt (mu : MassFamily F)
    (p : ℝ) (s : ℕ) (hp : 0 < p) (hs : p * scaleSum s ≤ 1 / 2)
    (z : Coloring α s) :
    (∑ a ∈ selectedOriginals mu z, colorMass p s a * p ^ (changes a z).card) <
      colorMass p s z * (1 / 20) := by
…
```
Mentions: OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.scaleSum, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.selectedOriginals, OAI.TalagrandThreshold.colorMass, OAI.TalagrandThreshold.Selector.changes
theorem OAI.TalagrandThreshold.Selector.selected_total_cost_lt_one_twentieth line 133
Source documentation
The complete selected cost is strictly below one twentieth. All grouping, counting, reconstruction, entropy, and probability facts are proved above.
```
theorem selected_total_cost_lt_one_twentieth (mu : MassFamily F)
    (p : ℝ) (s : ℕ) (hp : 0 < p) (hs : p * scaleSum s ≤ 1 / 2) :
    (∑ a ∈ (Finset.univ : Finset (Coloring α s)).filter (Bad mu),
      ∑ z ∈ selectedMoves mu a, colorMass p s a * p ^ (changes a z).card) < 1 / 20 := by
…
```
Mentions: OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.scaleSum, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.Bad, OAI.TalagrandThreshold.Selector.selectedMoves, OAI.TalagrandThreshold.colorMass, OAI.TalagrandThreshold.Selector.changes
theorem OAI.TalagrandThreshold.Selector.weighted_bad_selected_cost_le line 151
Source documentation
The same bound in expectation notation, ready for the bad-event argument.
```
theorem weighted_bad_selected_cost_le (mu : MassFamily F)
    (p : ℝ) (s : ℕ) (hp : 0 < p) (hs : p * scaleSum s ≤ 1 / 2) :
    (∑ a : Coloring α s, if Bad mu a then
      colorMass p s a * ∑ z ∈ selectedMoves mu a, p ^ (changes a z).card else 0) ≤ 1 / 20 := by
…
```
Mentions: OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.scaleSum, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.Bad, OAI.TalagrandThreshold.colorMass, OAI.TalagrandThreshold.Selector.selectedMoves, OAI.TalagrandThreshold.Selector.changes