OAI/Geometry/CubicTorus/Reflection/AxialWeightedHeight.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.circle_continuous_integrable line 13
  2. theorem OAI.CubicTorus.circle_moment_absolutelyContinuous line 17
  3. def OAI.CubicTorus.axialBundleHeight line 66
  4. def OAI.CubicTorus.axialCoverHeight line 68
  5. lemma OAI.CubicTorus.continuous_axialBundleHeight line 70
  6. lemma OAI.CubicTorus.continuous_axialCoverHeight line 74
  7. def OAI.CubicTorus.axialWeightedHeight line 77
  8. instance OAI.CubicTorus.axialWeightedHeight_finite line 81
  9. def OAI.CubicTorus.axialVolumeHeight line 87
  10. instance OAI.CubicTorus.axialVolumeHeight_finite line 90
  11. lemma OAI.CubicTorus.axialVolumeHeight_le line 95
  12. lemma OAI.CubicTorus.integral_axialWeightedHeight line 103
  13. lemma OAI.CubicTorus.integral_axialVolumeHeight line 118
  14. theorem OAI.CubicTorus.axialWeightedHeight_absolutelyContinuous line 126
  15. lemma OAI.CubicTorus.isMinimizerAt_spatialNormalMeasure_noAtoms line 156
  16. def OAI.CubicTorus.axialCriticalLift line 163
  17. theorem OAI.CubicTorus.isMinimizerAt_countable_axialCriticalLift line 166
  18. lemma OAI.CubicTorus.axialNormalWeight_zero_coordinates line 206
  19. theorem OAI.CubicTorus.isMinimizerAt_axialNormalWeight_pos_ae line 221
  20. theorem OAI.CubicTorus.axialHeight_absolutelyContinuous line 263
  21. theorem OAI.CubicTorus.isMinimizerAt_axialHeight_absolutelyContinuous line 277
  22. lemma OAI.CubicTorus.absolutelyContinuous_congrOn line 305
  23. lemma OAI.CubicTorus.integral_compact_eq_interval line 318
  24. theorem OAI.CubicTorus.absolutelyContinuous_of_integrable_weak_derivative line 326
  25. lemma OAI.CubicTorus.circlePeriodize_unit_eventuallyEq line 399
  26. lemma OAI.CubicTorus.circle_weighted_density_nonneg line 418
  27. theorem OAI.CubicTorus.circle_weighted_density line 444
  28. lemma OAI.CubicTorus.circle_integrable_preimage_Icc line 481
  29. lemma OAI.CubicTorus.circle_weighted_density_nonneg_measurable line 498
  30. theorem OAI.CubicTorus.circle_weighted_density_bounded line 524
  31. lemma OAI.CubicTorus.circle_integral_withDensity_ofReal line 574
  32. theorem OAI.CubicTorus.circle_ae_eq_zero_of_smooth_moments line 582
  33. lemma OAI.CubicTorus.circle_ae_eq_of_smooth_moments line 627
  34. lemma OAI.CubicTorus.circle_nonneg_weighted_density line 656
  35. theorem OAI.CubicTorus.circle_ae_le_of_ordered_weighted_moments line 683
  36. theorem OAI.CubicTorus.circle_positive_density_of_smooth_moments line 729