OAI/Geometry/CubicTorus/Reflection/ActualAxialFlux.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.isMinimizerAt_axialSlice_antitone line 13
  2. lemma OAI.CubicTorus.isMinimizerAt_axialSliceVolume_antitone line 49
  3. theorem OAI.CubicTorus.isMinimizerAt_slice_absolutelyContinuous line 72
  4. theorem OAI.CubicTorus.isMinimizerAt_nonstandard_slices_ac_measurable line 96
  5. theorem OAI.CubicTorus.isMinimizerAt_nonstandard_slices_ac line 109
  6. lemma OAI.CubicTorus.axialNormalDensity_pairing_bounded line 151
  7. lemma OAI.CubicTorus.axialNormalDensity_L1_le line 198
  8. lemma OAI.CubicTorus.normal_component_L1_le_sqrt line 243
  9. lemma OAI.CubicTorus.circle_ac_oscillation_bound line 274
  10. lemma OAI.CubicTorus.ac_on_all_intervals_comp_affine line 318
  11. theorem OAI.CubicTorus.isMinimizerAt_actual_projection_bound line 349
  12. theorem OAI.CubicTorus.isMinimizerAt_octantSliceVolume_ac line 367
  13. def OAI.CubicTorus.actualAxialFlux line 399
  14. lemma OAI.CubicTorus.actualAxialFlux_integrable line 403
  15. lemma OAI.CubicTorus.actualAxialFlux_measurable line 408
  16. lemma OAI.CubicTorus.axialSurface_density_eq_flux line 413
  17. lemma OAI.CubicTorus.actualAxialFlux_nonneg_ae line 455
  18. lemma OAI.CubicTorus.actualAxialFlux_nonneg line 464
  19. lemma OAI.CubicTorus.axialSurfaceMarginal_zero_of_boundary_gap line 487
  20. theorem OAI.CubicTorus.actualAxialFlux_zero_of_empty_boundary_height line 504
  21. theorem OAI.CubicTorus.actual_transverse_mass_eq_curvature_volume_of_empty_end line 535
  22. theorem OAI.CubicTorus.isMinimizerAt_missing_neighbor_gap line 562
  23. theorem OAI.CubicTorus.isMinimizerAt_missing_neighbor_flux line 608
  24. theorem OAI.CubicTorus.isMinimizerAt_connected_transverse_mass_pos line 649
  25. theorem OAI.CubicTorus.isMinimizerAt_missing_neighbor_flux_unrestricted line 733
  26. theorem OAI.CubicTorus.isMinimizerAt_missing_neighbor_volume_le_half line 788