OAI/Combinatorics/Sensitivity/LabelingEstimate.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

An explicit numerical union-bound estimate.

  1. theorem OAI.Paper320.labeling_union_bound_numerator line 9
  2. theorem OAI.Paper320.labeling_union_bound_constant line 22
  3. theorem OAI.Paper320.labeling_power_bound line 28
  4. theorem OAI.Paper320.labeling_union_bound_real line 39
  5. theorem OAI.Paper320.labeling_sqrt_expression line 53
  6. theorem OAI.Paper320.labeling_source_estimate line 61