OAI/Geometry/CubicTorus/Reflection/AxialSectionCoordinates.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicTorus.axialSplit line 13
  2. lemma OAI.CubicTorus.axialSplit_measurePreserving line 16
  3. lemma OAI.CubicTorus.axialSplit_fst line 19
  4. lemma OAI.CubicTorus.axialSplit_symm_axis line 22
  5. lemma OAI.CubicTorus.continuous_axialSplit line 25
  6. lemma OAI.CubicTorus.continuous_axialSplit_symm line 28
  7. def OAI.CubicTorus.transverseSquare line 31
  8. lemma OAI.CubicTorus.measurableSet_transverseSquare line 33
  9. lemma OAI.CubicTorus.transverseSquare_subset_ball line 39
  10. lemma OAI.CubicTorus.volume_transverseSquare_lt_top line 50
  11. lemma OAI.CubicTorus.mem_axialSplit_cube line 53
  12. lemma OAI.CubicTorus.axialSplit_preimage_cube line 71
  13. def OAI.CubicTorus.axialSection line 76
  14. def OAI.CubicTorus.axialSectionArea line 79
  15. lemma OAI.CubicTorus.measurableSet_axialSection line 82
  16. lemma OAI.CubicTorus.volume_axialSection_lt_top line 87
  17. lemma OAI.CubicTorus.axialSectionArea_nonneg line 91
  18. lemma OAI.CubicTorus.volume_axialSquare line 106
  19. lemma OAI.CubicTorus.volume_axialRectangle line 113
  20. lemma OAI.CubicTorus.axialSectionArea_le_one line 117
  21. lemma OAI.CubicTorus.axial_section_inner line 122
  22. lemma OAI.CubicTorus.integrable_axialIndicator line 142
  23. theorem OAI.CubicTorus.axial_section_fubini line 163
  24. lemma OAI.CubicTorus.integrable_axialSectionArea line 186
  25. lemma OAI.CubicTorus.integral_axialSectionArea line 196
  26. lemma OAI.CubicTorus.periodic_deriv line 214
  27. lemma OAI.CubicTorus.axial_section_periodic_flux line 220
  28. theorem OAI.CubicTorus.axial_section_integrable_weak_derivative line 243
  29. lemma OAI.CubicTorus.axialSplit_symm_transverse_line line 308
  30. theorem OAI.CubicTorus.isMinimizerAt_axial_boundary_null line 329
  31. lemma OAI.CubicTorus.continuous_axialSectionArea_of_boundary_null line 380
  32. theorem OAI.CubicTorus.isMinimizerAt_continuous_axial_sections line 409
  33. lemma OAI.CubicTorus.mem_coordinateHalf_of_interval line 435
  34. lemma OAI.CubicTorus.axialSplit_symm_axis_line line 452
  35. theorem OAI.CubicTorus.isMinimizerAt_axialSection_nested line 467
  36. lemma OAI.CubicTorus.isMinimizerAt_antitoneOn_axialSectionArea_open line 510
  37. lemma OAI.CubicTorus.antitoneOn_closed_of_open line 535
  38. theorem OAI.CubicTorus.isMinimizerAt_antitoneOn_axialSectionArea line 563
  39. theorem OAI.CubicTorus.isMinimizerAt_absolutelyContinuous_axialSectionArea line 591
  40. lemma OAI.CubicTorus.chamber_interval_subset_unit line 613
  41. theorem OAI.CubicTorus.isMinimizerAt_axialSection_fundamentalTheorem line 621
  42. lemma OAI.CubicTorus.periodic_unit_sine line 652
  43. def OAI.CubicTorus.circleUnitSine line 657
  44. lemma OAI.CubicTorus.continuous_circleUnitSine line 659
  45. lemma OAI.CubicTorus.circleUnitSine_coe line 662
  46. def OAI.CubicTorus.chamberHeightSign line 665
  47. lemma OAI.CubicTorus.measurable_chamberHeightSign line 668
  48. lemma OAI.CubicTorus.norm_chamberHeightSign line 675
  49. lemma OAI.CubicTorus.chamberHeightSign_left line 679
  50. lemma OAI.CubicTorus.chamberHeightSign_right line 685
  51. lemma OAI.CubicTorus.chamberHeightSign_eq_half line 693
  52. theorem OAI.CubicTorus.isMinimizerAt_normal_chamberHeightSign line 703
  53. lemma OAI.CubicTorus.axialSection_periodic line 752
  54. lemma OAI.CubicTorus.axialSectionArea_periodic line 764
  55. lemma OAI.CubicTorus.chamberSign_integral_deriv line 768