OAI/Analysis/Mahler/Faces.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SymmetricMahler.IsFace line 13
  2. lemma OAI.SymmetricMahler.IsFace.subset line 17
  3. lemma OAI.SymmetricMahler.IsFace.trans line 18
  4. lemma OAI.SymmetricMahler.IsFace.inter line 20
  5. lemma OAI.SymmetricMahler.IsFace.mono line 22
  6. lemma OAI.SymmetricMahler.IsFace.refl line 24
  7. lemma OAI.SymmetricMahler.IsFace.empty line 25
  8. lemma OAI.SymmetricMahler.IsFace.eq_convexHull_inter line 28
  9. lemma OAI.SymmetricMahler.IsFace.isCompact_of_finite_hull line 47
  10. lemma OAI.SymmetricMahler.IsFace.eq_of_inter_eq line 52
  11. def OAI.SymmetricMahler.faceHull line 57
  12. lemma OAI.SymmetricMahler.subset_faceHull line 59
  13. lemma OAI.SymmetricMahler.faceHull_min line 62
  14. lemma OAI.SymmetricMahler.isFace_faceHull line 65
  15. lemma OAI.SymmetricMahler.faceHull_mono line 70
  16. lemma OAI.SymmetricMahler.faceHull_eq line 75
  17. lemma OAI.SymmetricMahler.finite_faces_of_finite_hull line 78
  18. lemma OAI.SymmetricMahler.finite_unit_faces_of_medians line 88
  19. lemma OAI.SymmetricMahler.extreme_set_eq_ball_of_zero line 102
  20. lemma OAI.SymmetricMahler.norm_eq_one_of_mem_proper_face line 111
  21. lemma OAI.SymmetricMahler.normalized_summand_mem_face line 128
  22. theorem OAI.SymmetricMahler.disjoint_faces_distance_two line 144
  23. theorem OAI.SymmetricMahler.disjoint_faces_opposite_support line 169
  24. lemma OAI.SymmetricMahler.bidual_functional_representation line 236
  25. theorem OAI.SymmetricMahler.dual_ball_eq_convexHull_opposite_faces line 246
  26. theorem OAI.SymmetricMahler.extreme_dual_eval_eq_one_or_neg_one line 276
  27. lemma OAI.SymmetricMahler.dual_eval_bounds line 284
  28. lemma OAI.SymmetricMahler.norm_le_of_dual_extreme_le line 292
  29. lemma OAI.SymmetricMahler.eq_of_dual_extreme_eq line 313
  30. lemma OAI.SymmetricMahler.extreme_of_dual_levels line 322
  31. lemma OAI.SymmetricMahler.isFace_support line 349
  32. def OAI.SymmetricMahler.exchangeFace line 365
  33. lemma OAI.SymmetricMahler.isFace_exchangeFace line 368
  34. lemma OAI.SymmetricMahler.exchange_vertex line 398
  35. theorem OAI.SymmetricMahler.face_vertex_exchange line 414
  36. lemma OAI.SymmetricMahler.IsFace.singleton line 448
  37. lemma OAI.SymmetricMahler.IsFace.extremePoints_eq line 451
  38. lemma OAI.SymmetricMahler.unitBall_eq_convexHull_extreme line 460
  39. lemma OAI.SymmetricMahler.IsFace.isCompact_unit line 467
  40. lemma OAI.SymmetricMahler.IsFace.eq_convexHull_vertices line 472
  41. lemma OAI.SymmetricMahler.IsFace.exists_vertex line 478
  42. lemma OAI.SymmetricMahler.IsFace.subset_of_vertices line 484
  43. lemma OAI.SymmetricMahler.IsFace.exists_vertex_outside line 490
  44. lemma OAI.SymmetricMahler.isFace_dual_common line 499
  45. lemma OAI.SymmetricMahler.isCompact_dual_common line 519
  46. lemma OAI.SymmetricMahler.face_vertex_dual_separation line 528
  47. def OAI.SymmetricMahler.IsParallelPair line 553
  48. def OAI.SymmetricMahler.IsParallelFace line 556
  49. lemma OAI.SymmetricMahler.IsParallelPair.symm line 561
  50. lemma OAI.SymmetricMahler.IsParallelPair.vertex_mem line 564
  51. lemma OAI.SymmetricMahler.IsParallelPair.not_mem_iff line 568
  52. lemma OAI.SymmetricMahler.parallelPair_of_dual_vertex line 576
  53. theorem OAI.SymmetricMahler.maximal_avoiding_vertex_parallel line 609
  54. lemma OAI.SymmetricMahler.face_mem_of_parallelogram line 629
  55. lemma OAI.SymmetricMahler.proper_face_support line 640
  56. lemma OAI.SymmetricMahler.vertex_not_mem_span_face line 649
  57. def OAI.SymmetricMahler.faceRank line 674
  58. lemma OAI.SymmetricMahler.faceRank_lt line 676
  59. lemma OAI.SymmetricMahler.faceHull_subset_face line 690
  60. lemma OAI.SymmetricMahler.parallel_face_vertex_exchange line 693
  61. theorem OAI.SymmetricMahler.parallel_faceHull_rank line 713
  62. def OAI.SymmetricMahler.IsMaximalProperFace line 745
  63. lemma OAI.SymmetricMahler.parallelogram_not_parallel line 754
  64. theorem OAI.SymmetricMahler.nonparallel_vertex_parallelogram line 765
  65. lemma OAI.SymmetricMahler.faceRank_mono line 823
  66. lemma OAI.SymmetricMahler.faceRank_le_dim line 827
  67. lemma OAI.SymmetricMahler.rank_succ_maximal line 830
  68. lemma OAI.SymmetricMahler.parallel_faceHull_maximal line 845
  69. theorem OAI.SymmetricMahler.maximal_avoiding_vertex_rank line 864
  70. lemma OAI.SymmetricMahler.extend_face_avoiding_vertex line 906
  71. lemma OAI.SymmetricMahler.maximal_proper_parallel line 921
  72. lemma OAI.SymmetricMahler.maximal_proper_rank line 931
  73. lemma OAI.SymmetricMahler.span_support_dual_vertex line 942
  74. lemma OAI.SymmetricMahler.full_rank_maximal_proper line 963
  75. lemma OAI.SymmetricMahler.maximal_unit_face_rank line 974
  76. def OAI.SymmetricMahler.HasMFaceStructure line 988
  77. lemma OAI.SymmetricMahler.IsFace.extreme_mem line 999
  78. lemma OAI.SymmetricMahler.IsParallelPair.restrict line 1003
  79. lemma OAI.SymmetricMahler.IsParallelPair.complement_anti line 1019
  80. lemma OAI.SymmetricMahler.IsParallelPair.complement_unique line 1027
  81. lemma OAI.SymmetricMahler.IsParallelPair.subset_of_disjoint line 1033
  82. lemma OAI.SymmetricMahler.IsParallelPair.nonempty_right line 1042
  83. lemma OAI.SymmetricMahler.IsParallelPair.left_ne line 1050
  84. lemma OAI.SymmetricMahler.IsMaximalProperFace.faceHull_vertex line 1057
  85. lemma OAI.SymmetricMahler.IsMaximalProperFace.exchange line 1070
  86. lemma OAI.SymmetricMahler.maximal_pair_of_disjoint line 1081
  87. lemma OAI.SymmetricMahler.proper_unit_face_subface_ne line 1093
  88. lemma OAI.SymmetricMahler.IsFace.rank_pos line 1099
  89. lemma OAI.SymmetricMahler.IsFace.of_support_le line 1113
  90. lemma OAI.SymmetricMahler.disjoint_faces_dual_vertex line 1139
  91. lemma OAI.SymmetricMahler.IsParallelPair.support_dual_vertex line 1168
  92. lemma OAI.SymmetricMahler.parallel_disjoint_union_face line 1181