OAI/Geometry/Cannon/Conformal/Center.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonConformal.determinant_continuous line 18
  2. lemma OAI.CannonConformal.evaluate_continuous line 22
  3. lemma OAI.CannonConformal.evaluate_add line 26
  4. lemma OAI.CannonConformal.evaluate_smul line 31
  5. lemma OAI.CannonConformal.lowerBound_positive line 36
  6. lemma OAI.CannonConformal.lowerBound_closed line 50
  7. lemma OAI.CannonConformal.lowerBound_convex line 55
  8. lemma OAI.CannonConformal.determinant_midpoint_identity line 65
  9. lemma OAI.CannonConformal.determinant_midpoint_strict line 72
  10. lemma OAI.CannonConformal.determinant_max_unique line 101
  11. theorem OAI.CannonConformal.exists_unique_maxdet line 110
  12. def OAI.CannonConformal.center line 126
  13. lemma OAI.CannonConformal.center_spec line 130
  14. lemma OAI.CannonConformal.center_eq line 136
  15. lemma OAI.CannonConformal.image_closedConvexHull line 144
  16. theorem OAI.CannonConformal.center_equivariant line 152
  17. abbrev OAI.CannonConformal.PlaneLinear line 174
  18. def OAI.CannonConformal.planeDet line 176
  19. def OAI.CannonConformal.adjugate line 178
  20. def OAI.CannonConformal.pullForm line 180
  21. lemma OAI.CannonConformal.determinant_pullForm line 191
  22. lemma OAI.CannonConformal.determinant_smul line 196
  23. lemma OAI.CannonConformal.evaluate_pullForm line 201
  24. lemma OAI.CannonConformal.planeDet_adjugate line 206
  25. lemma OAI.CannonConformal.adjugate_adjugate line 210
  26. lemma OAI.CannonConformal.pullForm_adjugate line 214
  27. def OAI.CannonConformal.normalizedPull line 219
  28. lemma OAI.CannonConformal.normalizedPull_apply line 222
  29. lemma OAI.CannonConformal.normalizedPull_det line 225
  30. lemma OAI.CannonConformal.normalizedPull_adjugate line 234
  31. def OAI.CannonConformal.pullbackEquiv line 244
  32. lemma OAI.CannonConformal.pullbackEquiv_det line 255
  33. def OAI.CannonConformal.planeMul line 258
  34. lemma OAI.CannonConformal.planeDet_mul line 261
  35. lemma OAI.CannonConformal.pullForm_mul line 265
  36. lemma OAI.CannonConformal.normalizedPull_mul line 270
  37. def OAI.CannonConformal.roundForm line 283
  38. lemma OAI.CannonConformal.derivativeMatrix_comp line 285
  39. lemma OAI.CannonConformal.derivativeDet_comp line 293
  40. lemma OAI.CannonConformal.pull_round_derivative line 299
  41. lemma OAI.CannonConformal.evaluate_normalized_round line 305
  42. theorem OAI.CannonConformal.normalized_derivative_bounds line 311
  43. theorem OAI.CannonConformal.continuous_unique_max_image line 363
  44. def OAI.CannonConformal.combination line 396
  45. lemma OAI.CannonConformal.combination_apply line 400
  46. lemma OAI.CannonConformal.combination_image line 404
  47. lemma OAI.CannonConformal.closedConvexHull_finite_range line 432
  48. abbrev OAI.CannonConformal.FiniteForms line 437
  49. lemma OAI.CannonConformal.continuous_finite_center line 439
  50. def OAI.CannonConformal.orbitPrefix line 482
  51. lemma OAI.CannonConformal.prefix_nonempty line 484
  52. lemma OAI.CannonConformal.prefix_subset_range line 487
  53. lemma OAI.CannonConformal.prefix_monotone line 491
  54. lemma OAI.CannonConformal.prefix_closure_union line 496
  55. theorem OAI.CannonConformal.prefix_center_tendsto line 509
  56. lemma OAI.CannonConformal.measurable_finite_center line 546
  57. theorem OAI.CannonConformal.measurable_countable_center line 558
  58. lemma OAI.CannonConformal.upperBound_closed line 572
  59. lemma OAI.CannonConformal.upperBound_convex line 577
  60. lemma OAI.CannonConformal.norm_le_of_bounds line 587
  61. lemma OAI.CannonConformal.bounded_of_bounds line 612
  62. lemma OAI.CannonConformal.center_bounds line 620
  63. lemma OAI.CannonConformal.measurable_indexed_center line 628
  64. theorem OAI.CannonConformal.invariant_measurable_form line 640