OAI/Geometry/CubicTorus/Reflection/AxialAreaDensity.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.normal_zero_at_reflection_height line 13
  2. lemma OAI.CubicTorus.normal_transverse_near_reflection_height line 40
  3. def OAI.CubicTorus.axialAreaDensity line 93
  4. def OAI.CubicTorus.axialSecondDensity line 96
  5. lemma OAI.CubicTorus.axialAreaDensity_integrable line 99
  6. lemma OAI.CubicTorus.axialSecondDensity_integrable line 101
  7. lemma OAI.CubicTorus.axialAreaDensity_measurable line 103
  8. lemma OAI.CubicTorus.axialSecondDensity_measurable line 105
  9. lemma OAI.CubicTorus.axialAreaDensity_pairing line 108
  10. lemma OAI.CubicTorus.axialSurfaceMarginal_ac_of_area line 116
  11. lemma OAI.CubicTorus.axialSecondDensity_pairing line 126
  12. lemma OAI.CubicTorus.axialPerimeterDensity_pairing line 140
  13. theorem OAI.CubicTorus.axial_moment_nonneg_ae line 157
  14. lemma OAI.CubicTorus.axialSecondDensity_pairing_bounded line 220
  15. lemma OAI.CubicTorus.axial_density_local_comparison line 240
  16. lemma OAI.CubicTorus.axialSliceIntegral_continuous_of_boundary_null line 291
  17. lemma OAI.CubicTorus.circle_continuous_le_of_local_ae line 332
  18. theorem OAI.CubicTorus.reflection_seam_planar_perimeter_le_flux line 348
  19. lemma OAI.CubicTorus.congruentAE_congr_ae_left line 413
  20. lemma OAI.CubicTorus.smallStandardRegion_congr_ae line 419
  21. lemma OAI.CubicTorus.standardRegionAt_congr_ae line 423
  22. lemma OAI.CubicTorus.isMinimizerAt_openRepresentative_ae_nullMeasurable line 445
  23. lemma OAI.CubicTorus.axisFixedHeights_neg_eq line 467
  24. theorem OAI.CubicTorus.isMinimizerAt_nonstandard_seam_perimeters line 476
  25. theorem OAI.CubicTorus.isMinimizerAt_missing_neighbor_seam_bound line 509
  26. theorem OAI.CubicTorus.isMinimizerAt_bottom_extent_calibration line 553
  27. def OAI.CubicTorus.planeSwap line 617
  28. def OAI.CubicTorus.planarSwap line 620
  29. lemma OAI.CubicTorus.planeSwap_apply line 623
  30. lemma OAI.CubicTorus.planarSwap_apply line 625
  31. lemma OAI.CubicTorus.planeSwap_involutive line 629
  32. lemma OAI.CubicTorus.planarSwap_involutive line 631
  33. lemma OAI.CubicTorus.planarSwap_measurePreserving line 634
  34. lemma OAI.CubicTorus.planeSwap_single line 637
  35. lemma OAI.CubicTorus.planeDivergence_swap line 642
  36. lemma OAI.CubicTorus.planarAdmissibleField_swap line 655
  37. lemma OAI.CubicTorus.planeSwap_representative line 668
  38. lemma OAI.CubicTorus.planarTorusPerimeter_swap_le line 673
  39. theorem OAI.CubicTorus.planarTorusPerimeter_swap line 692
  40. lemma OAI.CubicTorus.planar_volume_swap line 699
  41. lemma OAI.CubicTorus.planarSwap_continuous line 716
  42. lemma OAI.CubicTorus.planarSwap_closure_subset line 721
  43. lemma OAI.CubicTorus.planarRadialDownset_swap line 725
  44. lemma OAI.CubicTorus.planarSwap_zero line 732
  45. lemma OAI.CubicTorus.planarSwap_firstAxisPoint line 734
  46. lemma OAI.CubicTorus.planarSwap_secondAxisPoint line 738
  47. lemma OAI.CubicTorus.planar_radial_full_calibration line 741
  48. theorem OAI.CubicTorus.planar_radial_both_extents line 759
  49. theorem OAI.CubicTorus.isMinimizerAt_section_both_extents line 802