OAI/Geometry/CubicTorus/Reflection/ChamberPositionProducer.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.isMinimizerAt_one_vertex_position line 13
  2. theorem OAI.CubicTorus.Periodic.isMinimizerAt_full_jacobi_system line 101
  3. lemma OAI.CubicTorus.tangentialDivergence_id_derivative line 185
  4. lemma OAI.CubicTorus.tangentialDivergence_unit_normal line 193
  5. theorem OAI.CubicTorus.isMinimizerAt_positive_position_spherical line 199
  6. theorem OAI.CubicTorus.isMinimizerAt_one_vertex_spherical line 310
  7. theorem OAI.CubicTorus.isMinimizerAt_one_vertex_standard_ball line 343
  8. theorem OAI.CubicTorus.isMinimizerAt_coordinate_multiplier line 373
  9. theorem OAI.CubicTorus.isMinimizerAt_nonstandard_section_system line 385
  10. theorem OAI.CubicTorus.isMinimizerAt_axial_bv_coarea line 458
  11. theorem OAI.CubicTorus.isMinimizerAt_nonstandard_actual_coarea line 481
  12. theorem OAI.CubicTorus.isMinimizerAt_integrated_jensen line 511
  13. lemma OAI.CubicTorus.absolutelyContinuous_comp_lipschitz line 599
  14. theorem OAI.CubicTorus.ac_substitution_boundedContinuous line 618
  15. lemma OAI.CubicTorus.chamber_sign_integral_substitution line 652
  16. theorem OAI.CubicTorus.chamber_ac_area_measure line 681
  17. lemma OAI.CubicTorus.chamber_ac_area_substitution line 717
  18. theorem OAI.CubicTorus.chamber_area_lower_bound line 745