OAI/Geometry/TriangularCovering/Shadows.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TriangularCovering.faceNormal_sum line 11
  2. lemma OAI.TriangularCovering.positive_face_exists line 16
  3. def OAI.TriangularCovering.front line 29
  4. lemma OAI.TriangularCovering.mem_front line 31
  5. lemma OAI.TriangularCovering.projection_add_axis line 34
  6. lemma OAI.TriangularCovering.forward_face line 39
  7. lemma OAI.TriangularCovering.shadow_front line 68
  8. lemma OAI.TriangularCovering.projected_faces_inter_subset line 79
  9. lemma OAI.TriangularCovering.vertical_edge_mem line 114
  10. lemma OAI.TriangularCovering.upper_edge_mem line 121
  11. lemma OAI.TriangularCovering.lower_edge_mem line 129
  12. lemma OAI.TriangularCovering.face_coord line 137
  13. lemma OAI.TriangularCovering.face_pair_edge line 143
  14. lemma OAI.TriangularCovering.cross3_self line 192
  15. lemma OAI.TriangularCovering.face_pair_projection_null line 197
  16. lemma OAI.TriangularCovering.front_pairwise_aeDisjoint line 203
  17. lemma OAI.TriangularCovering.shadow_measure line 210
  18. lemma OAI.TriangularCovering.max_pos_abs line 224
  19. lemma OAI.TriangularCovering.shadowArea_positive_sum line 229
  20. lemma OAI.TriangularCovering.shadowArea_abs_sum line 240
  21. lemma OAI.TriangularCovering.abs_pair line 246
  22. lemma OAI.TriangularCovering.shadowArea_formula line 250
  23. lemma OAI.TriangularCovering.shadowArea_ge_H line 272
  24. lemma OAI.TriangularCovering.xAxis_unit line 292
  25. lemma OAI.TriangularCovering.xAxis_shadow line 294
  26. theorem OAI.TriangularCovering.projection_minimum line 300

    Source documentation

    The minimum Euclidean shadow area equals the height H.

    theorem projection_minimum : A_min = H := by
…

    Mentions: OAI.TriangularCovering.A_min, OAI.TriangularCovering.H

  27. def OAI.TriangularCovering.normalPlane line 316

    Source documentation

    The actual two-dimensional linear plane of a unit normal.

    def normalPlane (u : Space) : Submodule ℝ Space := (ℝ ∙ u)ᗮ

    Mentions: OAI.TriangularCovering.Space

  28. lemma OAI.TriangularCovering.normalPlane_rank line 318
  29. lemma OAI.TriangularCovering.normalPlane_projection line 328
  30. lemma OAI.TriangularCovering.twoPlane_normal line 336
  31. def OAI.TriangularCovering.intrinsicShadow line 357

    Source documentation

    Planar Lebesgue measure of the orthogonal shadow, intrinsically in the plane.

    def intrinsicShadow (P : Submodule ℝ Space) : ℝ :=
…

    Mentions: OAI.TriangularCovering.Space

  32. lemma OAI.TriangularCovering.intrinsicShadow_eq_area line 360
  33. lemma OAI.TriangularCovering.intrinsicShadow_normal line 371
  34. lemma OAI.TriangularCovering.shadow_values_eq_planes line 379
  35. lemma OAI.TriangularCovering.A_min_eq_plane_inf line 391

    Source documentation

    The unit-normal parametrization preserves the minimum-area definition.

    lemma A_min_eq_plane_inf : A_min = sInf
    {a : ℝ | ∃ P : Submodule ℝ Space, Module.finrank ℝ P = 2 ∧ a = intrinsicShadow P} := by
…

    Mentions: OAI.TriangularCovering.A_min, OAI.TriangularCovering.Space, OAI.TriangularCovering.intrinsicShadow

  36. theorem OAI.TriangularCovering.minimum_over_planes line 397

    Source documentation

    The minimum is attained over all two-dimensional subspaces.

    theorem minimum_over_planes :
    IsLeast {a : ℝ | ∃ P : Submodule ℝ Space,
      Module.finrank ℝ P = 2 ∧ a = intrinsicShadow P} H := by
…

    Mentions: OAI.TriangularCovering.Space, OAI.TriangularCovering.intrinsicShadow, OAI.TriangularCovering.H