OAI/Geometry/CubicTorus/Estimates/BVInteriorMultiplier.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.isMinimizerAt_actual_sequential_decay line 15
  2. lemma OAI.CubicTorus.spatial_tilt_closedBall_le_oriented line 60
  3. theorem OAI.CubicTorus.isMinimizerAt_epsilon_improvement line 108
  4. lemma OAI.CubicTorus.choose_excess_scale line 169
  5. theorem OAI.CubicTorus.isMinimizerAt_excess_contraction line 189
  6. lemma OAI.CubicTorus.polar_tilt_difference line 232
  7. lemma OAI.CubicTorus.polar_normal_step_bound line 253
  8. lemma OAI.CubicTorus.dependent_sequence line 303
  9. lemma OAI.CubicTorus.geometric_error_ratio line 315
  10. lemma OAI.CubicTorus.excess_normal_iteration line 329
  11. def OAI.CubicTorus.interiorWallWeight line 393
  12. lemma OAI.CubicTorus.interiorWallWeight_smooth line 395
  13. lemma OAI.CubicTorus.interiorWallWeight_nonneg line 401
  14. lemma OAI.CubicTorus.interiorWallWeight_periodic line 407
  15. lemma OAI.CubicTorus.interiorWallWeight_face line 411
  16. lemma OAI.CubicTorus.interiorWallWeight_center line 415
  17. theorem OAI.CubicTorus.isMinimizerAt_exists_interior_positive_flux line 422
  18. theorem OAI.CubicTorus.isMinimizerAt_centered_multiplier line 480
  19. theorem OAI.CubicTorus.isMinimizerAt_centered_tilt_iteration line 501
  20. def OAI.CubicTorus.MovingCenter.InteriorCenter line 553
  21. instance OAI.CubicTorus.MovingCenter.(instance at line 555) line 555
  22. lemma OAI.CubicTorus.MovingCenter.coords line 557
  23. def OAI.CubicTorus.MovingCenter.cubeBall line 566
  24. lemma OAI.CubicTorus.MovingCenter.measurableSet_cubeBall line 568
  25. lemma OAI.CubicTorus.MovingCenter.coverBall_subset_cube line 571
  26. lemma OAI.CubicTorus.MovingCenter.cubeBall_lift line 582
  27. lemma OAI.CubicTorus.MovingCenter.volume_cubeBall line 595
  28. def OAI.CubicTorus.MovingCenter.radialBump line 602
  29. def OAI.CubicTorus.MovingCenter.radialCore line 608
  30. def OAI.CubicTorus.MovingCenter.radialSquared line 610
  31. lemma OAI.CubicTorus.MovingCenter.radialCore_contDiff line 612
  32. lemma OAI.CubicTorus.MovingCenter.radialCore_compactSupport line 615
  33. lemma OAI.CubicTorus.MovingCenter.radialCore_tsupport line 618
  34. lemma OAI.CubicTorus.MovingCenter.radialSquared_contDiff line 630
  35. lemma OAI.CubicTorus.MovingCenter.radialSquared_periodic line 633
  36. lemma OAI.CubicTorus.MovingCenter.radialSquared_eq_on_cube line 637
  37. lemma OAI.CubicTorus.MovingCenter.radialSquared_eventuallyEq_norm_sq line 644
  38. lemma OAI.CubicTorus.MovingCenter.radialSquared_sublevel_iff line 656
  39. lemma OAI.CubicTorus.MovingCenter.representative_mem_fundamentalCube line 679
  40. lemma OAI.CubicTorus.MovingCenter.sublevelRegion_radialSquared line 683
  41. lemma OAI.CubicTorus.MovingCenter.norm_gradient_radialSquared_of_mem_cube line 691
  42. lemma OAI.CubicTorus.MovingCenter.norm_gradient_radialSquared line 710
  43. lemma OAI.CubicTorus.MovingCenter.cubeBall_eq_metricBall line 718
  44. lemma OAI.CubicTorus.MovingCenter.closedBall_interior line 733
  45. lemma OAI.CubicTorus.MovingCenter.center_add_mem line 756
  46. lemma OAI.CubicTorus.MovingCenter.torusGraphRegion_symmDiff_ball_le line 765