OAI/Geometry/CubicTorus/Reflection/DelaunayPeriodicMoments.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.periodic_revolution_flux_integral line 12
  2. lemma OAI.CubicTorus.revolution_flux_coefficients_normal line 47
  3. lemma OAI.CubicTorus.periodic_deriv_real line 67
  4. theorem OAI.CubicTorus.TrueRadialTube.revolution_area_le_perimeter line 73
  5. def OAI.CubicTorus.delaunayRecurrence line 149
  6. lemma OAI.CubicTorus.delaunayRecurrence_continuous line 152
  7. lemma OAI.CubicTorus.hasDerivAt_delaunay_moment line 163
  8. theorem OAI.CubicTorus.delaunay_periodic_moment_recurrence line 184
  9. lemma OAI.CubicTorus.periodic_radius_extrema line 210
  10. theorem OAI.CubicTorus.delaunay_nonconstant_parameters line 223
  11. lemma OAI.CubicTorus.delaunay_energy line 278
  12. def OAI.CubicTorus.delaunayAmplitude line 290
  13. def OAI.CubicTorus.delaunaySquare line 293
  14. lemma OAI.CubicTorus.delaunay_z_bounds line 296
  15. lemma OAI.CubicTorus.delaunaySquare_amplitude line 307
  16. lemma OAI.CubicTorus.delaunayAmplitude_b line 323
  17. lemma OAI.CubicTorus.delaunayAmplitude_a line 330
  18. lemma OAI.CubicTorus.hasDerivAt_delaunayAmplitude line 336
  19. lemma OAI.CubicTorus.delaunay_weight_pair_nonneg line 384
  20. theorem OAI.CubicTorus.delaunay_weighted_mean_bound line 424
  21. lemma OAI.CubicTorus.delaunaySquare_continuous line 476
  22. lemma OAI.CubicTorus.delaunaySquare_bounds line 480
  23. lemma OAI.CubicTorus.delaunaySquare_reflect line 487
  24. theorem OAI.CubicTorus.delaunay_half_mean_bound line 493
  25. lemma OAI.CubicTorus.even_periodic_reflect_one line 564
  26. lemma OAI.CubicTorus.even_periodic_deriv_endpoints line 568
  27. lemma OAI.CubicTorus.even_periodic_integral_half line 586
  28. lemma OAI.CubicTorus.delaunay_radius_at_zero_slope line 613
  29. theorem OAI.CubicTorus.delaunay_even_monotone_mean line 623
  30. theorem OAI.CubicTorus.delaunay_chamber_monotone_mean line 659
  31. theorem OAI.CubicTorus.delaunay_area_moment line 700
  32. lemma OAI.CubicTorus.delaunay_area_scalar_gt line 732
  33. theorem OAI.CubicTorus.delaunay_area_gt_cylinder line 750
  34. theorem OAI.CubicTorus.isMinimizerAt_first_transition_standard line 773