OAI/Combinatorics/ExpectationThreshold/SelectorEntropyDyadic.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite dyadic mass for the selector entropy estimate

The positive dyadic levels have total mass at most one, including when there are no levels.

  1. lemma OAI.TalagrandThreshold.selector_dyadic_range_sum line 19
  2. theorem OAI.TalagrandThreshold.selector_dyadic_sum_le_one line 29

    Source documentation

    The dyadic weights of all positive selector levels sum to at most one.

    theorem selector_dyadic_sum_le_one (s : ℕ) :
    (∑ i : Fin s, (1 / 2 : ℝ) ^ (i.val + 1)) ≤ 1 := by
…