OAI/Analysis/Mahler/HannerBodies.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SymmetricMahler.hannerProduct line 11

    Also declared: ComparatorChallenges/SymmetricMahlerEquality.lean:21 (same declaration text).

  2. def OAI.SymmetricMahler.hannerJoin line 15

    Also declared: ComparatorChallenges/SymmetricMahlerEquality.lean:25 (same declaration text).

  3. inductive OAI.SymmetricMahler.IsHanner line 21

    Also declared: ComparatorChallenges/SymmetricMahlerEquality.lean:31 (same declaration text).

  4. def OAI.SymmetricMahler.IsLinearHanner line 29

    Also declared: ComparatorChallenges/SymmetricMahlerEquality.lean:39 (same declaration text).

  5. structure OAI.SymmetricMahler.RealNormData line 33
  6. instance OAI.SymmetricMahler.RealNormData.(instance at line 41) line 41
  7. lemma OAI.SymmetricMahler.RealNormData.apply_zero line 43
  8. lemma OAI.SymmetricMahler.RealNormData.apply_neg line 44
  9. lemma OAI.SymmetricMahler.RealNormData.nonneg line 46
  10. lemma OAI.SymmetricMahler.RealNormData.add_le line 47
  11. lemma OAI.SymmetricMahler.RealNormData.eq_zero line 49
  12. def OAI.SymmetricMahler.RealNormData.sum line 52
  13. def OAI.SymmetricMahler.RealNormData.max line 68
  14. lemma OAI.SymmetricMahler.RealNormData.sum_apply line 88
  15. lemma OAI.SymmetricMahler.RealNormData.max_apply line 90
  16. def OAI.SymmetricMahler.RealNormData.unit line 93
  17. lemma OAI.SymmetricMahler.RealNormData.zero_mem_unit line 95
  18. lemma OAI.SymmetricMahler.RealNormData.unit_max line 96
  19. lemma OAI.SymmetricMahler.RealNormData.convex_unit line 99
  20. lemma OAI.SymmetricMahler.RealNormData.exists_smul_unit line 109
  21. lemma OAI.SymmetricMahler.RealNormData.unit_sum line 120
  22. def OAI.SymmetricMahler.RealNormData.comap line 141
  23. lemma OAI.SymmetricMahler.RealNormData.comap_apply line 153
  24. lemma OAI.SymmetricMahler.RealNormData.unit_comap line 156
  25. lemma OAI.SymmetricMahler.RealNormData.measure_unit line 171
  26. lemma OAI.SymmetricMahler.RealNormData.measureReal_unit line 179
  27. lemma OAI.SymmetricMahler.RealNormData.measureReal_unit_sum line 184
  28. lemma OAI.SymmetricMahler.RealNormData.measureReal_unit_max line 200
  29. def OAI.SymmetricMahler.appendEquiv line 207
  30. lemma OAI.SymmetricMahler.appendEquiv_apply line 215
  31. lemma OAI.SymmetricMahler.measurePreserving_appendEquiv line 218
  32. lemma OAI.SymmetricMahler.volume_appendEquiv_image line 229
  33. lemma OAI.SymmetricMahler.dot_append line 238
  34. lemma OAI.SymmetricMahler.hannerProduct_eq_append_image line 243
  35. def OAI.SymmetricMahler.RealNormData.coordSum line 254
  36. def OAI.SymmetricMahler.RealNormData.coordMax line 257
  37. lemma OAI.SymmetricMahler.RealNormData.coordSum_append line 260
  38. lemma OAI.SymmetricMahler.RealNormData.coordMax_append line 266
  39. lemma OAI.SymmetricMahler.RealNormData.unit_coordMax line 272
  40. lemma OAI.SymmetricMahler.RealNormData.unit_coordSum line 277
  41. lemma OAI.SymmetricMahler.RealNormData.volumeReal_unit_coordMax line 285
  42. lemma OAI.SymmetricMahler.RealNormData.volumeReal_unit_coordSum line 290
  43. def OAI.SymmetricMahler.RealNormData.interval line 302
  44. lemma OAI.SymmetricMahler.RealNormData.interval_apply line 318
  45. lemma OAI.SymmetricMahler.RealNormData.unit_interval line 321
  46. lemma OAI.SymmetricMahler.RealNormData.volumeReal_unit_interval line 327
  47. def OAI.SymmetricMahler.RealNormData.IsDual line 333
  48. lemma OAI.SymmetricMahler.RealNormData.IsDual.polar_unit line 337
  49. lemma OAI.SymmetricMahler.RealNormData.interval_isDual line 351
  50. theorem OAI.SymmetricMahler.RealNormData.IsDual.coordMax_sum line 368
  51. theorem OAI.SymmetricMahler.RealNormData.IsDual.coordSum_max line 390
  52. lemma OAI.SymmetricMahler.IsHanner.dim_pos line 420
  53. lemma OAI.SymmetricMahler.hanner_volume_recursion line 426
  54. theorem OAI.SymmetricMahler.IsHanner.gauges line 439
  55. theorem OAI.SymmetricMahler.IsHanner.polar line 475
  56. theorem OAI.SymmetricMahler.IsHanner.volumeProduct line 480
  57. def OAI.SymmetricMahler.coordinateTransposeMap line 485
  58. lemma OAI.SymmetricMahler.det_coordinateTransposeMap line 489
  59. def OAI.SymmetricMahler.coordinateTranspose line 494
  60. lemma OAI.SymmetricMahler.coordinateTranspose_apply line 499
  61. lemma OAI.SymmetricMahler.det_coordinateTranspose line 508
  62. lemma OAI.SymmetricMahler.coordinatePolar_image line 512
  63. lemma OAI.SymmetricMahler.coordinatePolar_image_eq line 519
  64. theorem OAI.SymmetricMahler.volumeProduct_linear_image line 524
  65. theorem OAI.SymmetricMahler.IsLinearHanner.volumeProduct line 537
  66. theorem OAI.SymmetricMahler.IsLinearHanner.polar line 544
  67. def OAI.SymmetricMahler.RealNormData.Space line 557
  68. instance OAI.SymmetricMahler.RealNormData.Space.(instance at line 560) line 560
  69. instance OAI.SymmetricMahler.RealNormData.Space.(instance at line 561) line 561
  70. instance OAI.SymmetricMahler.RealNormData.Space.(instance at line 562) line 562
  71. instance OAI.SymmetricMahler.RealNormData.Space.(instance at line 564) line 564
  72. instance OAI.SymmetricMahler.RealNormData.Space.(instance at line 569) line 569
  73. instance OAI.SymmetricMahler.RealNormData.Space.(instance at line 571) line 571
  74. def OAI.SymmetricMahler.RealNormData.spaceEquiv line 575
  75. lemma OAI.SymmetricMahler.RealNormData.space_norm line 577
  76. lemma OAI.SymmetricMahler.RealNormData.continuous line 582
  77. lemma OAI.SymmetricMahler.RealNormData.unit_eq_image_closedBall line 586
  78. lemma OAI.SymmetricMahler.RealNormData.isCompact_unit line 595
  79. lemma OAI.SymmetricMahler.RealNormData.unit_nhds line 599
  80. lemma OAI.SymmetricMahler.RealNormData.symmetric_unit line 605
  81. lemma OAI.SymmetricMahler.RealNormData.interior_unit_nonempty line 609
  82. lemma OAI.SymmetricMahler.body_nhds_zero line 614
  83. def OAI.SymmetricMahler.bodyNorm line 618
  84. lemma OAI.SymmetricMahler.bodyNorm_unit line 634
  85. lemma OAI.SymmetricMahler.RealNormData.dot_continuous line 644
  86. theorem OAI.SymmetricMahler.RealNormData.isDual_of_polar line 647
  87. lemma OAI.SymmetricMahler.coordinatePolar_bipolar line 709
  88. lemma OAI.SymmetricMahler.RealNormData.IsDual.symm line 725
  89. lemma OAI.SymmetricMahler.RealNormData.coordinate_of_dual line 729
  90. lemma OAI.SymmetricMahler.RealNormData.equality_segment_lift line 751