OAI/Geometry/CubicTorus/Estimates/MinimizerLevelSliceIsoperimetric.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.isMinimizerAt_radial_slice_length_of_level_vertices line 13
  2. theorem OAI.CubicTorus.isMinimizerAt_slice_isoperimetric_of_level_vertices line 47
  3. lemma OAI.CubicTorus.isMinimizerAt_axial_flux_nonneg line 87
  4. lemma OAI.CubicTorus.isMinimizerAt_axialFluxWeight_pos line 101
  5. theorem OAI.CubicTorus.isMinimizerAt_missing_axis_flux line 127
  6. lemma OAI.CubicTorus.isMinimizerAt_axial_chamberTop_perimeter line 200
  7. theorem OAI.CubicTorus.isMinimizerAt_corner_endpoint_flux line 225
  8. lemma OAI.CubicTorus.isMinimizerAt_vertex_vacant_of_not_occupied line 269
  9. lemma OAI.CubicTorus.chamberVertex_top_section_real line 284
  10. lemma OAI.CubicTorus.chamberVertex_top_section_imag line 290
  11. theorem OAI.CubicTorus.isMinimizerAt_two_missing_vertices_top_flux line 296
  12. lemma OAI.CubicTorus.isMinimizerAt_complement_frontier line 331
  13. lemma OAI.CubicTorus.coordinateHalf_not_reflected line 339
  14. theorem OAI.CubicTorus.isMinimizerAt_complement_chamber_sign line 351
  15. lemma OAI.CubicTorus.normal_reverse_mass line 392
  16. lemma OAI.CubicTorus.axialFluxWeight_reverse line 400
  17. lemma OAI.CubicTorus.directionalFlux_reverse line 411
  18. lemma OAI.CubicTorus.periodicNormalFirstVariation_reverse line 433
  19. theorem OAI.CubicTorus.complement_firstVariation_same_multiplier line 450
  20. lemma OAI.CubicTorus.axialSectionArea_compl line 472
  21. lemma OAI.CubicTorus.isMinimizerAt_openRepresentative_compl line 484
  22. theorem OAI.CubicTorus.isMinimizerAt_axial_complement_area line 490
  23. lemma OAI.CubicTorus.quotientMap_chamberVertex_complement line 538
  24. lemma OAI.CubicTorus.axialSectionArea_complementary_corner line 549
  25. lemma OAI.CubicTorus.reflection_symmetry_compl line 558
  26. theorem OAI.CubicTorus.isMinimizerAt_two_occupied_vertices_bottom_flux line 579
  27. lemma OAI.CubicTorus.axialSplit_symm_neg_axis line 634
  28. lemma OAI.CubicTorus.axialSection_reflection line 643
  29. lemma OAI.CubicTorus.axialSectionArea_reflection line 651
  30. lemma OAI.CubicTorus.axialSectionArea_reflection_one_sub line 656
  31. lemma OAI.CubicTorus.axialSectionArea_bounds_Icc line 661
  32. theorem OAI.CubicTorus.isMinimizerAt_endpoint_volume_bounds line 695
  33. theorem OAI.CubicTorus.isMinimizerAt_coordinate_multiplier_nonneg line 742
  34. lemma OAI.CubicTorus.isMinimizerAt_halfMass_competitor_bounds line 766
  35. theorem OAI.CubicTorus.isMinimizerAt_four_corner_necessary_data line 785