OAI/Combinatorics/Progressions/Geometry/CoordinateFiberPatch.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.integerIntervalCenter line 13
  2. def OAI.Erdos3.integerIntervalWidth line 16
  3. theorem OAI.Erdos3.integerIntervalWidth_pos line 19
  4. theorem OAI.Erdos3.integer_interval_box_inner line 24
  5. theorem OAI.Erdos3.integer_interval_box_card line 34
  6. theorem OAI.Erdos3.smooth_interval_box_change line 45
  7. def OAI.Erdos3.finiteBoxPointsEquiv line 77
  8. theorem OAI.Erdos3.finiteBoxPoints_expect line 84
  9. def OAI.Erdos3.coordinateFiberParameters line 103
  10. theorem OAI.Erdos3.coordinateFiberParameters_degree line 108
  11. def OAI.Erdos3.PolynomialPatch.coordinateFiber line 116
  12. theorem OAI.Erdos3.PolynomialPatch.coordinateFiber_value line 120
  13. theorem OAI.Erdos3.finiteBoxPoints_expect_finset line 131
  14. theorem OAI.Erdos3.exists_integerBox_coordinate_fiber line 136
  15. theorem OAI.Erdos3.PolynomialPatch.exists_coordinate_fiber_score line 171