OAI/Combinatorics/FiniteCircle/Lower.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteCircle.lowerCap line 12
  2. theorem OAI.FiniteCircle.lowerCap_ge line 14
  3. theorem OAI.FiniteCircle.lower_parameter line 21
  4. theorem OAI.FiniteCircle.log_lowerCap line 38
  5. theorem OAI.FiniteCircle.cap_log_bound line 42
  6. theorem OAI.FiniteCircle.cap_loglog_bound line 66
  7. theorem OAI.FiniteCircle.scale_bound_of_logs line 79
  8. theorem OAI.FiniteCircle.all_length_inversion line 95
  9. theorem OAI.FiniteCircle.mask_witness_parameter line 114
  10. theorem OAI.FiniteCircle.excluded_witness_parameter line 136
  11. theorem OAI.FiniteCircle.both_witnesses line 159