SelectorEntropy.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The selector's finite entropy estimate

After scaling row i by 4^(i+1), its binomial coefficient is bounded by one term of the exponential series at T * 2^(-(i+1)). The sum of these arguments is at most T, so their product is at most exp T ≤ 3^T. This proves the row-count estimate directly, including rows of count zero.

theorem OAI.TalagrandThreshold.selector_exp_one_le_three line 23
Source documentation
A finite series and its explicit remainder already give the needed slack.
```
private theorem selector_exp_one_le_three : Real.exp 1 ≤ 3 := by
…
```

theorem OAI.TalagrandThreshold.selector_choose_le_scaled_exp line 29

Source documentation

A scaled binomial coefficient is bounded by an exponential-series term.

theorem selector_choose_le_scaled_exp (m t : ℕ) (d y : ℝ)
    (hd : 0 ≤ d) (hy : 0 ≤ y) (hm : (m : ℝ) ≤ d * y) :
    (m.choose t : ℝ) ≤ d ^ t * Real.exp y := by
…

theorem OAI.TalagrandThreshold.selector_entropy_bound line 45

Source documentation

The actual finite entropy bound for the selector's row sizes and counts. The statement also permits total count zero.

theorem selector_entropy_bound (s : ℕ) (m t : Fin s → ℕ)
    (hm : ∀ i, m i ≤ 2 ^ (i.val + 1) * (∑ j, t j)) :
    (∏ i, ((m i).choose (t i) : ℝ)) ≤
      ∏ i, (3 * 4 ^ (i.val + 1) : ℝ) ^ (t i) := by
…