OAI/Combinatorics/ExpectationThreshold/SelectorDefinitionsLemmas.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Elementary bounds on the literal truncation scales.

  1. theorem OAI.TalagrandThreshold.Selector.dscale_pos line 9
  2. theorem OAI.TalagrandThreshold.Selector.dscale_nonneg line 12
  3. theorem OAI.TalagrandThreshold.Selector.dscale_lt_one line 15