OAI/Geometry/CubicTorus/Estimates/BVSharpUpperBound.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.polar_normal_rescaled_equicontinuity line 15
  2. theorem OAI.CubicTorus.isMinimizerAt_singular_cone_obstruction line 64
  3. lemma OAI.CubicTorus.halfspace_line_invariance_orthogonal line 140
  4. lemma OAI.CubicTorus.radial_cone_secondary_halfspace_orthogonal line 182
  5. theorem OAI.CubicTorus.isMinimizerAt_singular_dimension_reduction line 213
  6. def OAI.CubicTorus.UpperComparison.fieldMove line 306
  7. def OAI.CubicTorus.UpperComparison.fieldMoveDeriv line 308
  8. def OAI.CubicTorus.UpperComparison.derivativeEntry line 311
  9. def OAI.CubicTorus.UpperComparison.secondJacobian line 314
  10. def OAI.CubicTorus.UpperComparison.thirdJacobian line 322
  11. lemma OAI.CubicTorus.UpperComparison.fieldMove_hasFDerivAt line 325
  12. lemma OAI.CubicTorus.UpperComparison.fieldMoveDeriv_det line 330
  13. lemma OAI.CubicTorus.UpperComparison.fieldMove_injective line 348
  14. lemma OAI.CubicTorus.UpperComparison.continuous_derivativeEntry line 370
  15. lemma OAI.CubicTorus.UpperComparison.continuous_secondJacobian line 375
  16. lemma OAI.CubicTorus.UpperComparison.continuous_thirdJacobian line 385
  17. lemma OAI.CubicTorus.UpperComparison.integral_det_fieldMove line 390
  18. lemma OAI.CubicTorus.UpperComparison.integral_det_fieldMove_le_volume line 426
  19. lemma OAI.CubicTorus.UpperComparison.realVolume_cover_ball line 444
  20. lemma OAI.CubicTorus.UpperComparison.fieldMove_ball_subset line 450
  21. lemma OAI.CubicTorus.UpperComparison.flux_cover_ball_le line 463
  22. def OAI.CubicTorus.UpperComparison.cubeCenter line 513
  23. def OAI.CubicTorus.UpperComparison.cubeBall line 515
  24. lemma OAI.CubicTorus.UpperComparison.measurableSet_cubeBall line 517
  25. lemma OAI.CubicTorus.UpperComparison.coverBall_subset_cube line 520
  26. lemma OAI.CubicTorus.UpperComparison.cubeBall_lift line 530
  27. lemma OAI.CubicTorus.UpperComparison.volume_cubeBall line 543
  28. lemma OAI.CubicTorus.UpperComparison.perimeter_cubeBall_le line 550
  29. lemma OAI.CubicTorus.UpperComparison.finitePerimeter_cubeBall line 557
  30. lemma OAI.CubicTorus.UpperComparison.dist_representative_cubeCenter line 566
  31. lemma OAI.CubicTorus.UpperComparison.cubeBall_eq_metricBall line 586
  32. lemma OAI.CubicTorus.UpperComparison.centeredBall_eq_cubeBall_preimage line 592
  33. lemma OAI.CubicTorus.UpperComparison.volume_centeredBall line 599
  34. lemma OAI.CubicTorus.UpperComparison.perimeter_centeredBall_le line 604
  35. abbrev OAI.CubicTorus.UpperComparison.Plane line 614
  36. def OAI.CubicTorus.UpperComparison.discProjection line 616
  37. lemma OAI.CubicTorus.UpperComparison.discProjection_apply line 622
  38. lemma OAI.CubicTorus.UpperComparison.discProjection_norm_le line 625
  39. def OAI.CubicTorus.UpperComparison.tubeSplit line 632
  40. lemma OAI.CubicTorus.UpperComparison.tubeSplit_apply line 638
  41. lemma OAI.CubicTorus.UpperComparison.tubeSplit_symm_zero line 641
  42. lemma OAI.CubicTorus.UpperComparison.tubeSplit_symm_succ line 644
  43. lemma OAI.CubicTorus.UpperComparison.continuous_tubeSplit line 648
  44. lemma OAI.CubicTorus.UpperComparison.continuous_tubeSplit_symm line 652
  45. lemma OAI.CubicTorus.UpperComparison.tubeSplit_measurePreserving line 662
  46. def OAI.CubicTorus.UpperComparison.discCenter line 667
  47. def OAI.CubicTorus.UpperComparison.coverTube line 669
  48. lemma OAI.CubicTorus.UpperComparison.measurableSet_coverTube line 672
  49. lemma OAI.CubicTorus.UpperComparison.isCompact_closure_coverTube line 675
  50. lemma OAI.CubicTorus.UpperComparison.volume_coverTube line 684
  51. lemma OAI.CubicTorus.UpperComparison.volumeReal_coverTube line 694
  52. def OAI.CubicTorus.UpperComparison.axialProjection line 698
  53. lemma OAI.CubicTorus.UpperComparison.axialProjection_zero line 702
  54. lemma OAI.CubicTorus.UpperComparison.axialProjection_succ line 705
  55. lemma OAI.CubicTorus.UpperComparison.axialProjection_norm_le line 709
  56. lemma OAI.CubicTorus.UpperComparison.fieldMove_coverTube_subset line 717
  57. lemma OAI.CubicTorus.UpperComparison.tubeSplit_symm_line line 744
  58. lemma OAI.CubicTorus.UpperComparison.hasDerivAt_tubeLine line 751
  59. lemma OAI.CubicTorus.UpperComparison.axial_integral_eq_zero line 761
  60. lemma OAI.CubicTorus.UpperComparison.integral_axial_coverTube line 781
  61. lemma OAI.CubicTorus.UpperComparison.divergence_axialProjection line 802
  62. lemma OAI.CubicTorus.UpperComparison.flux_axialProjection line 811
  63. lemma OAI.CubicTorus.UpperComparison.flux_coverTube_axial_le line 829
  64. lemma OAI.CubicTorus.UpperComparison.flux_coverTube_le line 874
  65. lemma OAI.CubicTorus.UpperComparison.representative_mem_cube line 892
  66. lemma OAI.CubicTorus.UpperComparison.coverTube_subset_cube line 898
  67. def OAI.CubicTorus.UpperComparison.cubeTube line 909
  68. lemma OAI.CubicTorus.UpperComparison.measurableSet_cubeTube line 911
  69. lemma OAI.CubicTorus.UpperComparison.cubeTube_lift line 914
  70. lemma OAI.CubicTorus.UpperComparison.volume_cubeTube line 927
  71. lemma OAI.CubicTorus.UpperComparison.perimeter_cubeTube_le line 933
  72. lemma OAI.CubicTorus.UpperComparison.norm_representative_sub_half line 940
  73. def OAI.CubicTorus.UpperComparison.centeredTube line 953
  74. lemma OAI.CubicTorus.UpperComparison.mem_cubeTube_iff line 955
  75. lemma OAI.CubicTorus.UpperComparison.centeredTube_eq_cubeTube_preimage line 966
  76. lemma OAI.CubicTorus.UpperComparison.measurableSet_centeredTube line 971
  77. lemma OAI.CubicTorus.UpperComparison.volume_centeredTube line 976
  78. lemma OAI.CubicTorus.UpperComparison.perimeter_centeredTube_le line 982
  79. lemma OAI.CubicTorus.UpperComparison.cube_cuberoot line 992
  80. lemma OAI.CubicTorus.UpperComparison.cube_two_thirds line 996
  81. lemma OAI.CubicTorus.UpperComparison.canonicalBall_radius_properties line 1000
  82. lemma OAI.CubicTorus.UpperComparison.ballArea_formula line 1019
  83. lemma OAI.CubicTorus.UpperComparison.volume_canonicalBall line 1033
  84. lemma OAI.CubicTorus.UpperComparison.perimeter_canonicalBall_le line 1039
  85. lemma OAI.CubicTorus.UpperComparison.finitePerimeter_canonicalBall line 1046
  86. lemma OAI.CubicTorus.UpperComparison.canonicalTube_radius_properties line 1051
  87. lemma OAI.CubicTorus.UpperComparison.tubeArea_formula line 1064
  88. lemma OAI.CubicTorus.UpperComparison.volume_canonicalTube line 1075
  89. lemma OAI.CubicTorus.UpperComparison.perimeter_canonicalTube_le line 1081
  90. lemma OAI.CubicTorus.UpperComparison.finitePerimeter_canonicalTube line 1087
  91. theorem OAI.CubicTorus.UpperComparison.isMinimizerAt_perimeter_le_envelope line 1092
  92. theorem OAI.CubicTorus.UpperComparison.isMinimizerAt_perimeter_le_candidateProfile line 1107
  93. theorem OAI.CubicTorus.isMinimizerAt_perimeter_le_candidateProfile line 1123