OAI/Geometry/CubicTorus/Reflection/AxialAreaMarginal.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.axisFixedHeights_null line 13
  2. lemma OAI.CubicTorus.normal_zero_on_cell_seam line 17
  3. theorem OAI.CubicTorus.strict_normal_component_ne_zero_ae line 63
  4. def OAI.CubicTorus.axialAreaMarginal line 104
  5. lemma OAI.CubicTorus.normal_transverse_positive_ae line 107
  6. theorem OAI.CubicTorus.axialAreaMarginal_absolutelyContinuous line 117
  7. lemma OAI.CubicTorus.isMinimizerAt_nonstandard_strict_signs_of_actual_normal line 137
  8. theorem OAI.CubicTorus.isMinimizerAt_nonstandard_area_marginals line 157
  9. abbrev OAI.CubicTorus.TransverseProduct line 184
  10. def OAI.CubicTorus.torusAxialSplit line 186
  11. lemma OAI.CubicTorus.torusAxialSplit_measurePreserving line 190
  12. lemma OAI.CubicTorus.torusAxialSplit_fst line 195
  13. lemma OAI.CubicTorus.torusAxialSplit_symm_apply line 197
  14. lemma OAI.CubicTorus.torusAxialSplit_symm_same line 200
  15. lemma OAI.CubicTorus.torusAxialSplit_symm_succAbove line 205
  16. def OAI.CubicTorus.axialSlice line 211
  17. def OAI.CubicTorus.axialSliceVolume line 214
  18. lemma OAI.CubicTorus.axialSlice_measurable line 217
  19. lemma OAI.CubicTorus.axialSliceVolume_measurable line 221
  20. lemma OAI.CubicTorus.axialSliceVolume_le_one line 225
  21. lemma OAI.CubicTorus.axialSliceVolume_lintegral line 229
  22. lemma OAI.CubicTorus.axialVolumeMarginal_apply line 236
  23. theorem OAI.CubicTorus.axialVolumeMarginal_eq_withDensity line 253
  24. def OAI.CubicTorus.axialPlanePoint line 287
  25. lemma OAI.CubicTorus.axialPlanePoint_dist line 290
  26. lemma OAI.CubicTorus.axialPlanePoint_continuous line 298
  27. lemma OAI.CubicTorus.axialPlane_local_antilipschitz line 301
  28. lemma OAI.CubicTorus.axialPlane_preimage_hausdorff_null line 314
  29. lemma OAI.CubicTorus.transverse_quotient_measurePreserving line 338
  30. lemma OAI.CubicTorus.axialSlice_hausdorff_null line 345
  31. lemma OAI.CubicTorus.normal_component_abs_le_one line 375
  32. def OAI.CubicTorus.axialPositiveFluxMarginal line 380
  33. lemma OAI.CubicTorus.axialPositiveFluxMarginal_absolutelyContinuous line 389
  34. lemma OAI.CubicTorus.axialPositiveFluxMarginal_integral line 399
  35. lemma OAI.CubicTorus.axialAreaMarginal_integral line 412
  36. def OAI.CubicTorus.axialNormalDensity line 419
  37. lemma OAI.CubicTorus.axialNormalDensity_integrable line 423
  38. lemma OAI.CubicTorus.axialNormalDensity_measurable line 427
  39. lemma OAI.CubicTorus.axialNormalDensity_pairing line 431
  40. lemma OAI.CubicTorus.axialSliceVolume_real_integrable line 453
  41. theorem OAI.CubicTorus.axialSliceVolume_weak_derivative line 460
  42. lemma OAI.CubicTorus.circle_integrable_mul_continuous line 501
  43. lemma OAI.CubicTorus.circle_integral_eq_interval line 506
  44. lemma OAI.CubicTorus.circle_intervalIntegrable line 518
  45. lemma OAI.CubicTorus.circle_lift_smoothing_integral_tendsto line 524
  46. lemma OAI.CubicTorus.integrable_circle_eq_zero_of_continuous_pairing line 550
  47. theorem OAI.CubicTorus.integrable_circle_constant_of_weak_derivative_zero line 585
  48. lemma OAI.CubicTorus.interval_primitive_absolutelyContinuous line 635
  49. lemma OAI.CubicTorus.circle_ac_primitive line 645
  50. theorem OAI.CubicTorus.circle_weak_integrable_has_ac_representative line 688
  51. lemma OAI.CubicTorus.axialSlice_point_continuous line 742
  52. lemma OAI.CubicTorus.isMinimizerAt_boundary_slice_null line 750
  53. lemma OAI.CubicTorus.axialSliceVolume_continuous_of_boundary_null line 772
  54. theorem OAI.CubicTorus.isMinimizerAt_nonstandard_slice_continuous line 802
  55. def OAI.CubicTorus.octantHeight line 824
  56. lemma OAI.CubicTorus.octantHeight_mem line 827
  57. lemma OAI.CubicTorus.upperFold_slice_same line 833
  58. lemma OAI.CubicTorus.upperFold_slice_succAbove line 839