SelectorAverageColor.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Average color from simultaneous capture

An integer color is one plus the number of preceding prefixes it misses. Summing this finite identity against the actual probability mass gives the mean-color identity. A captured coloring has the same family member at every scale, so the geometric sum of its missed masses is at most one.

theorem OAI.TalagrandThreshold.Selector.sum_color_tail_indicators line 22
Source documentation
Count the prefixes strictly below a color, including the final color.
```
theorem sum_color_tail_indicators {s : ℕ} (c : Color s) :
    (∑ i : Fin s, if i.val < c.val then (1 : ℝ) else 0) = (c.val : ℝ) := by
…
```
Mentions: OAI.TalagrandThreshold.Color
theorem OAI.TalagrandThreshold.Selector.color_level_eq_one_add_tail line 38
Source documentation
The finite integer layer-cake identity for the zero-based color index.
```
theorem color_level_eq_one_add_tail {s : ℕ} (c : Color s) :
    (c.val + 1 : ℝ) = 1 + ∑ i : Fin s, if i.val < c.val then (1 : ℝ) else 0 := by
…
```
Mentions: OAI.TalagrandThreshold.Color
theorem OAI.TalagrandThreshold.Selector.sum_tail_eq_one_sub_prefix line 47
Source documentation
The mass of colors above a prefixSet is its complementary mass.
```
theorem sum_tail_eq_one_sub_prefix {F : Family α} (mu : MassFamily F) {s : ℕ}
    (H : ↥F) (a : Coloring α s) (i : Fin s) :
    (∑ x, if i.val < (a x).val then mu.weight H x else 0) =
      1 - ∑ x ∈ prefixSet a i, mu.weight H x := by
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.prefixSet
theorem OAI.TalagrandThreshold.Selector.meanColor_eq_one_add_sum_tail line 62
Source documentation
The actual mean color is one plus the sum of all missed prefixSet masses.
```
theorem meanColor_eq_one_add_sum_tail {F : Family α} (mu : MassFamily F) {s : ℕ}
    (H : ↥F) (a : Coloring α s) :
    meanColor mu H a = 1 +
      ∑ i : Fin s, (1 - ∑ x ∈ prefixSet a i, mu.weight H x) := by
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.meanColor, OAI.TalagrandThreshold.Selector.prefixSet
theorem OAI.TalagrandThreshold.Selector.sum_dscale_le_one line 74
Source documentation
The truncation scales have total mass at most one, also when there are no scales.
```
theorem sum_dscale_le_one (s : ℕ) : (∑ i : Fin s, dscale i) ≤ 1 := by
…
```
Mentions: OAI.TalagrandThreshold.Selector.dscale
theorem OAI.TalagrandThreshold.Selector.meanColor_le_two_of_capture line 79
Source documentation
A single member capturing every prefixSet has mean color at most two.
```
theorem meanColor_le_two_of_capture {F : Family α} (mu : MassFamily F) {s : ℕ}
    (H : ↥F) (a : Coloring α s)
    (hcapture : ∀ i : Fin s,
      1 - dscale i ≤ ∑ x ∈ prefixSet a i, mu.weight H x) :
    meanColor mu H a ≤ 2 := by
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.dscale, OAI.TalagrandThreshold.Selector.prefixSet, OAI.TalagrandThreshold.Selector.meanColor
theorem OAI.TalagrandThreshold.Selector.Captured.exists_meanColor_le_two line 97
Source documentation
The same captured member supplies the average-color witness.
```
theorem Captured.exists_meanColor_le_two {F : Family α} {mu : MassFamily F} {s : ℕ}
    {a : Coloring α s} (h : Captured mu a) : ∃ H : ↥F, meanColor mu H a ≤ 2 := by
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.Captured, OAI.TalagrandThreshold.Selector.meanColor