OAI/Geometry/CubicTorus/Profiles/AxisCircleLebesgue.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicTorus.axisCircleLebesgue line 13
  2. lemma OAI.CubicTorus.axialSurfaceMarginal_integral line 16
  3. lemma OAI.CubicTorus.axialVolumeMarginal_integral line 33
  4. lemma OAI.CubicTorus.axisCircleLebesgue_integral line 42
  5. lemma OAI.CubicTorus.axial_circle_flux_integral line 50
  6. theorem OAI.CubicTorus.axial_circle_flux_measure line 64
  7. lemma OAI.CubicTorus.axisCircleLebesgue_eq_volume line 104
  8. lemma OAI.CubicTorus.torus_axis_measurePreserving line 109
  9. lemma OAI.CubicTorus.cube_axis_measurePreserving line 115
  10. lemma OAI.CubicTorus.axialVolumeMarginal_le line 120
  11. lemma OAI.CubicTorus.axialVolumeMarginal_absolutelyContinuous line 128
  12. theorem OAI.CubicTorus.axialSurfaceMarginal_absolutelyContinuous line 132
  13. lemma OAI.CubicTorus.normal_axisCircle_continuous line 156
  14. lemma OAI.CubicTorus.axial_null_normal_sq line 161
  15. lemma OAI.CubicTorus.normalSphere_two_sq_le line 186
  16. theorem OAI.CubicTorus.normalMeasure_two_null_axes line 194
  17. def OAI.CubicTorus.upperFold line 222
  18. lemma OAI.CubicTorus.upperFold_continuous line 224
  19. lemma OAI.CubicTorus.upperFold_mem line 227
  20. lemma OAI.CubicTorus.circle_norm_upper line 234
  21. lemma OAI.CubicTorus.upperFold_quotient line 245
  22. lemma OAI.CubicTorus.upperFold_eq_flip line 252
  23. lemma OAI.CubicTorus.upperFold_phase line 270
  24. theorem OAI.CubicTorus.octant_downset_closure line 275
  25. lemma OAI.CubicTorus.orientedCoordinateLE_reverse line 335
  26. theorem OAI.CubicTorus.isMinimizerAt_closed_octant_order line 340
  27. lemma OAI.CubicTorus.compact_smooth_cutoff line 388
  28. theorem OAI.CubicTorus.exists_periodic_position line 440
  29. def OAI.CubicTorus.centeredLiftCell line 494
  30. lemma OAI.CubicTorus.centeredLiftCell_compact line 496
  31. lemma OAI.CubicTorus.mem_centeredLiftCell line 499
  32. lemma OAI.CubicTorus.exists_centeredLiftCell line 517
  33. theorem OAI.CubicTorus.exists_boundary_periodic_position line 526
  34. lemma OAI.CubicTorus.orientedUpperVertex_origin_apply line 559
  35. theorem OAI.CubicTorus.isMinimizerAt_strict_support line 563
  36. lemma OAI.CubicTorus.circle_norm_half line 644
  37. lemma OAI.CubicTorus.upperFold_cell_face line 648
  38. theorem OAI.CubicTorus.isMinimizerAt_one_vertex_gap line 666
  39. lemma OAI.CubicTorus.reflection_invariant_frontier line 729
  40. lemma OAI.CubicTorus.isMinimizerAt_frontier_nonempty_null line 742
  41. def OAI.CubicTorus.axialSeamFunction line 758
  42. lemma OAI.CubicTorus.axialSeamFunction_continuous line 760
  43. lemma OAI.CubicTorus.axialSeamFunction_periodic line 764
  44. lemma OAI.CubicTorus.axialSeamFunction_reflection line 773
  45. lemma OAI.CubicTorus.axialSeamFunction_zero_fold line 781
  46. theorem OAI.CubicTorus.connected_reflected_boundary_meets_axial_seam line 803
  47. def OAI.CubicTorus.axisFixedHeights line 836
  48. lemma OAI.CubicTorus.axisFixedHeights_finite line 838
  49. lemma OAI.CubicTorus.axisCircle_singleton_null line 839