OAI/Algebra/DepthFive/DegreeDistances.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem335.nearestIntegerDistance line 10

    Source documentation

    Distance to the nearest integer, with rounding used only to select a minimizer.

    def nearestIntegerDistance (x : ℝ) : ℝ := |x - (round x : ℝ)|
  2. lemma OAI.Problem335.nearestIntegerDistance_nonneg line 12
  3. lemma OAI.Problem335.nearestIntegerDistance_le_half line 15
  4. lemma OAI.Problem335.nearestIntegerDistance_le line 18
  5. lemma OAI.Problem335.nearestIntegerDistance_even line 22
  6. lemma OAI.Problem335.nearestIntegerDistance_odd line 34
  7. lemma OAI.Problem335.nearestIntegerDistance_half_sub_ge line 46
  8. def OAI.Problem335.degreeDistance line 55

    Source documentation

    The degree-saving distance at slope (n-s)/(2*n).

    def degreeDistance (n s : ℝ) (e : ℕ) : ℝ :=
…
  9. lemma OAI.Problem335.degreeDistance_eq_half_sub line 58
  10. lemma OAI.Problem335.low_degree_offset line 64
  11. lemma OAI.Problem335.degreeDistance_even line 74
  12. lemma OAI.Problem335.degreeDistance_odd line 81
  13. lemma OAI.Problem335.degreeDistance_ge line 88
  14. lemma OAI.Problem335.degreeDistance_odd_ge line 95
  15. lemma OAI.Problem335.sum_degreeDistance_ge line 104
  16. lemma OAI.Problem335.sum_degreeDistance_ge_half line 115
  17. lemma OAI.Problem335.prod_degreeDistance_rpow_le line 125