OAI/Geometry/CubicTorus/Regularity/BVStationaryDensity.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.isMinimizerAt_moving_limit_comparison line 16
  2. theorem OAI.CubicTorus.isMinimizerAt_moving_limit_perimeter line 99
  3. lemma OAI.CubicTorus.radial_cone_secondary_unit_line line 148
  4. theorem OAI.CubicTorus.actual_cone_secondary_product_comparison line 167
  5. lemma OAI.CubicTorus.normalScalarTest_plane_derivative line 222
  6. lemma OAI.CubicTorus.divergence_planar_product_test line 244
  7. lemma OAI.CubicTorus.line_product_euclidean line 253
  8. theorem OAI.CubicTorus.planar_product_flux line 275
  9. theorem OAI.CubicTorus.weakCMC_moving_blowup_limit_stationary line 329
  10. theorem OAI.CubicTorus.moving_blowup_normal_limit_flux line 349
  11. theorem OAI.CubicTorus.moving_blowup_normal_cluster line 377
  12. theorem OAI.CubicTorus.isMinimizerAt_moving_paired_normal_limit line 400
  13. def OAI.CubicTorus.euclideanRadialMass line 462
  14. def OAI.CubicTorus.euclideanBallMass line 465
  15. lemma OAI.CubicTorus.integrable_euclideanRadialWeight line 468
  16. lemma OAI.CubicTorus.integrable_euclideanRadialSlope line 476
  17. lemma OAI.CubicTorus.hasDerivAt_euclideanRadialMass line 486
  18. lemma OAI.CubicTorus.euclideanRadialMass_nonneg line 516
  19. theorem OAI.CubicTorus.stationary_euclideanRadialMass_ode line 520
  20. lemma OAI.CubicTorus.euclideanRadialMass_tendsto line 544
  21. theorem OAI.CubicTorus.stationary_euclideanBallMass_monotone line 565
  22. theorem OAI.CubicTorus.stationary_euclideanBallMass_density line 588
  23. lemma OAI.CubicTorus.stationary_euclideanBallMass_upper line 598
  24. def OAI.CubicTorus.euclideanNormalMap line 621
  25. lemma OAI.CubicTorus.continuous_euclideanNormalMap line 624
  26. def OAI.CubicTorus.euclideanNormalMeasure line 630
  27. lemma OAI.CubicTorus.euclideanNormalMeasure_mass line 635
  28. lemma OAI.CubicTorus.euclideanNormalMap_mem line 647
  29. lemma OAI.CubicTorus.euclideanNormalMeasure_supported line 656
  30. theorem OAI.CubicTorus.euclideanNormalMeasure_cluster line 672
  31. lemma OAI.CubicTorus.integral_euclideanNormalMeasure line 707
  32. lemma OAI.CubicTorus.integral_euclidean_normal_test line 719
  33. lemma OAI.CubicTorus.stationary_euclidean_normal_identity line 730
  34. theorem OAI.CubicTorus.stationary_euclidean_normal_limit line 748
  35. lemma OAI.CubicTorus.euclidean_normal_scaled_flux line 783
  36. theorem OAI.CubicTorus.euclidean_normal_limit_flux line 816