OAI/Geometry/CylinderCovering/Simplex/Projection.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CylinderCovering.orthogonalProjection_add line 15
  2. lemma OAI.CylinderCovering.orthogonalProjection_smul line 21
  3. lemma OAI.CylinderCovering.orthogonalProjection_sub line 25
  4. lemma OAI.CylinderCovering.orthogonalProjection_homothety line 31
  5. lemma OAI.CylinderCovering.projection_image_homothety line 37
  6. theorem OAI.CylinderCovering.projected_homothety_measure line 47
  7. lemma OAI.CylinderCovering.projected_homothety_area line 56
  8. theorem OAI.CylinderCovering.projected_intersection_area line 66
  9. lemma OAI.CylinderCovering.real_fiber_length_iff line 78
  10. def OAI.CylinderCovering.lineFiber line 95
  11. lemma OAI.CylinderCovering.lineFiber_isometry line 98
  12. lemma OAI.CylinderCovering.lineFiber_compact line 105
  13. lemma OAI.CylinderCovering.lineFiber_convex line 110
  14. lemma OAI.CylinderCovering.projection_mem_normal line 121
  15. lemma OAI.CylinderCovering.projection_line line 126
  16. lemma OAI.CylinderCovering.projection_reconstruct line 132
  17. theorem OAI.CylinderCovering.fiber_superlevel_iff line 136
  18. lemma OAI.CylinderCovering.simplex_normalPlane_rank line 155
  19. theorem OAI.CylinderCovering.fiber_superlevel_measure line 164
  20. theorem OAI.CylinderCovering.fiber_distribution_of_intersection line 193
  21. def OAI.CylinderCovering.simplexAffineBasis line 206
  22. theorem OAI.CylinderCovering.simplex_chord_data line 212
  23. lemma OAI.CylinderCovering.measurable_lineFiber_volume line 250
  24. lemma OAI.CylinderCovering.integrable_lineFiber_length line 260
  25. lemma OAI.CylinderCovering.real_volume_eq_integral_lineFiber line 271
  26. lemma OAI.CylinderCovering.lineFiber_length_le_of_chord_bound line 282
  27. theorem OAI.CylinderCovering.simplex_chord_projection_product line 294
  28. theorem OAI.CylinderCovering.simplex_chord_projection line 327
  29. theorem OAI.CylinderCovering.tetrahedron_edge_minimizer line 331