OAI/Geometry/CubicTorus/Reflection/AxialFluxDensity.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.deriv_ae_eq_of_integrable_weak_derivative line 13
  2. lemma OAI.CubicTorus.axial_section_weak_derivative_of_density line 92
  3. theorem OAI.CubicTorus.axial_section_derivative_density line 140
  4. theorem OAI.CubicTorus.isMinimizerAt_axial_endFlux line 170
  5. def OAI.CubicTorus.axialCircleArea line 235
  6. lemma OAI.CubicTorus.axialCircleArea_coe line 238
  7. lemma OAI.CubicTorus.integral_axialCircleArea_mul line 242
  8. theorem OAI.CubicTorus.axialWeightedHeight_density line 251
  9. def OAI.CubicTorus.axialSectionIntegral line 305
  10. lemma OAI.CubicTorus.axialSectionIntegral_periodic line 309
  11. lemma OAI.CubicTorus.continuous_axialSectionIntegral_of_boundary_null line 321
  12. lemma OAI.CubicTorus.integrable_axialWeightedIndicator line 353
  13. theorem OAI.CubicTorus.axial_weighted_section_fubini line 367
  14. lemma OAI.CubicTorus.axialSectionIntegral_mul_height line 387
  15. lemma OAI.CubicTorus.divergence_height_tangent line 405
  16. lemma OAI.CubicTorus.axial_slice_flux_moment line 413
  17. lemma OAI.CubicTorus.unit_normal_tangent_quadratic_bound line 432
  18. theorem OAI.CubicTorus.axial_slice_flux_quadratic_bound line 442
  19. lemma OAI.CubicTorus.axial_density_moment line 483
  20. lemma OAI.CubicTorus.periodic_smooth_lipschitz line 520
  21. lemma OAI.CubicTorus.half_abs_sin_bound line 526
  22. theorem OAI.CubicTorus.isMinimizerAt_normal_reflection_rate line 538
  23. lemma OAI.CubicTorus.abs_sin_height_periodic line 613
  24. theorem OAI.CubicTorus.circle_quadratic_contact line 619
  25. theorem OAI.CubicTorus.axial_slice_endpoint_bound line 735
  26. theorem OAI.CubicTorus.isMinimizerAt_axial_slice_endpoint_bound line 798