OAI/Geometry/Cannon/Beltrami/RectCrossing.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonRealPlane.integral_sq_cauchy line 34
  2. lemma OAI.CannonRealPlane.line_energy_bound line 65
  3. lemma OAI.CannonRealPlane.continuous_line_integral line 83
  4. lemma OAI.CannonRealPlane.exists_line_below_average line 87
  5. lemma OAI.CannonRealPlane.rectangle_fubini line 99
  6. lemma OAI.CannonRealPlane.rectangle_fubini_swap line 106
  7. lemma OAI.CannonRealPlane.vertical_slice_energy line 116
  8. lemma OAI.CannonRealPlane.horizontal_slice_energy line 133
  9. def OAI.CannonRealPlane.RectCrossing line 150
  10. lemma OAI.CannonRealPlane.norm_sq_triangle line 155
  11. theorem OAI.CannonRealPlane.rectangle_capacity_bound line 160
  12. lemma OAI.CannonRealPlane.preconnected_rectCrossing line 231
  13. theorem OAI.CannonRealPlane.continuum_capacity_bound line 271