OAI/Geometry/CubicTorus/Regularity/NormalMeasureCoordinatePermutation.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.measurable_sliceJensenG line 12
  2. lemma OAI.CubicTorus.sliceJensenG_bounds line 16
  3. lemma OAI.CubicTorus.antitoneOn_sliceJensenG line 37
  4. theorem OAI.CubicTorus.isMinimizerAt_area_coordinate_jensen line 79
  5. theorem OAI.CubicTorus.isMinimizerAt_nonstandard_jensen_system line 122
  6. lemma OAI.CubicTorus.chamberFoldLift_opposite_coordinate line 159
  7. theorem OAI.CubicTorus.isMinimizerAt_vacant_axial_section line 182
  8. lemma OAI.CubicTorus.axialSectionArea_eq_zero_of_empty line 198
  9. lemma OAI.CubicTorus.axialSectionIntegral_eq_zero_of_empty line 206
  10. lemma OAI.CubicTorus.axialSlicePerimeter_eq_zero_of_empty line 215
  11. theorem OAI.CubicTorus.contDiffAt_continuous_implicit_root line 232
  12. lemma OAI.CubicTorus.real_clm_isInvertible line 246
  13. theorem OAI.CubicTorus.contDiffAt_continuous_implicit_root_of_deriv line 257
  14. theorem OAI.CubicTorus.isMinimizerAt_smooth_boundary_exit line 285
  15. lemma OAI.CubicTorus.unitAngle_contDiff line 357
  16. theorem OAI.CubicTorus.isMinimizerAt_smooth_radial_section line 361
  17. def OAI.CubicTorus.permuteNormal line 487
  18. lemma OAI.CubicTorus.measurable_permuteNormal line 491
  19. lemma OAI.CubicTorus.permuteNormal_periodic_eval line 498
  20. lemma OAI.CubicTorus.permuteNormal_mass line 505
  21. lemma OAI.CubicTorus.coverCoordinatePermute_inner line 512
  22. theorem OAI.CubicTorus.isNormalMeasure_coordinatePermute line 517
  23. lemma OAI.CubicTorus.permuted_normal_ae line 534
  24. lemma OAI.CubicTorus.axialFluxWeight_permute line 552
  25. lemma OAI.CubicTorus.finitePerimeter_coordinatePermute line 575
  26. theorem OAI.CubicTorus.isMinimizerAt_coordinatePermute line 581
  27. lemma OAI.CubicTorus.volumeSupport_coordinatePermute line 590
  28. lemma OAI.CubicTorus.openRepresentative_coordinatePermute line 606
  29. lemma OAI.CubicTorus.frontier_openRepresentative_coordinatePermute line 612
  30. lemma OAI.CubicTorus.coordinateReflection_coordinatePermute line 618
  31. lemma OAI.CubicTorus.reflection_invariant_coordinatePermute line 625
  32. lemma OAI.CubicTorus.coordinateHalf_coordinatePermute line 637
  33. lemma OAI.CubicTorus.chamberVertex_coordinatePermute line 641
  34. lemma OAI.CubicTorus.chamberSign_coordinatePermute line 646
  35. lemma OAI.CubicTorus.firstCornerPolynomial0_piece0 line 675
  36. lemma OAI.CubicTorus.firstCornerPolynomial0_piece1 line 691
  37. lemma OAI.CubicTorus.firstCornerPolynomial0_piece2 line 707
  38. lemma OAI.CubicTorus.firstCornerPolynomial0_piece3 line 723
  39. lemma OAI.CubicTorus.firstCornerPolynomial0_nonneg line 739
  40. lemma OAI.CubicTorus.firstCornerPolynomial1_piece0 line 749
  41. lemma OAI.CubicTorus.firstCornerPolynomial1_piece1 line 769
  42. lemma OAI.CubicTorus.firstCornerPolynomial1_piece2 line 789
  43. lemma OAI.CubicTorus.firstCornerPolynomial1_piece3 line 809
  44. lemma OAI.CubicTorus.firstCornerPolynomial1_nonneg line 829