OAI/Combinatorics/FiniteCircle/Main.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteCircle.upperRates_sup_nonneg line 12
  2. theorem OAI.FiniteCircle.lowerRates_sup_nonneg line 18
  3. theorem OAI.FiniteCircle.distortion_isometry_restrict line 24
  4. theorem OAI.FiniteCircle.optimalDistortion_isometry_mono line 40
  5. instance OAI.FiniteCircle.wordsFinite line 49
  6. theorem OAI.FiniteCircle.words_nontrivial line 52
  7. theorem OAI.FiniteCircle.binary_alphabet_embedding line 60
  8. theorem OAI.FiniteCircle.setDistortion_le_E line 69
  9. theorem OAI.FiniteCircle.maskWitness_lower_E line 82
  10. theorem OAI.FiniteCircle.uniformUpper_E line 89
  11. theorem OAI.FiniteCircle.alphabetSupremum_bounds line 103
  12. theorem OAI.FiniteCircle.full_main line 116
  13. theorem OAI.finiteCircle_fullMain line 139

    Distinct definitions of this name: ComparatorChallenges/FiniteCircle.lean:225 (same statement text; different proof or body). Qualify references as OAI.finiteCircle_fullMain@path.