OAI/Geometry/CubicTorus/Estimates/InteriorBallSubset.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.interior_ball_subset line 13
  2. theorem OAI.CubicTorus.cmc_uniform_energy line 23
  3. theorem OAI.CubicTorus.forced_cmc_uniform_energy line 70
  4. lemma OAI.CubicTorus.optimized_oscillation_scale line 165
  5. lemma OAI.CubicTorus.optimized_oscillation_identity line 174
  6. lemma OAI.CubicTorus.optimized_power_identity line 217
  7. lemma OAI.CubicTorus.forced_optimized_oscillation_bound line 224
  8. theorem OAI.CubicTorus.forced_cmc_uniform_oscillation line 263
  9. theorem OAI.CubicTorus.cmc_uniform_oscillation line 353
  10. lemma OAI.CubicTorus.plane_ball_real_at line 432
  11. lemma OAI.CubicTorus.plane_L2_sub_const_integrable_at line 438
  12. lemma OAI.CubicTorus.plane_L2_sub_const_mono line 445
  13. lemma OAI.CubicTorus.campanato_constant_distance line 451
  14. lemma OAI.CubicTorus.campanato_point_limit line 500
  15. lemma OAI.CubicTorus.campanato_holder_field line 583
  16. lemma OAI.CubicTorus.plane_closedBall_ae_ball line 651
  17. lemma OAI.CubicTorus.campanato_average_distance line 662
  18. lemma OAI.CubicTorus.campanato_identify_ae line 717
  19. lemma OAI.CubicTorus.continuousOn_of_power_distance line 774
  20. theorem OAI.CubicTorus.plane_campanato_regularity line 789
  21. theorem OAI.CubicTorus.cmc_linearized_holder_gradient line 801