OAI/Geometry/CubicTorus/Estimates/L2ReplacementBallBound.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.L2_replacement_ball_bound line 13
  2. lemma OAI.CubicTorus.L2_replacement_energy_decay line 48
  3. lemma OAI.CubicTorus.L2_replacement_oscillation_decay line 57
  4. lemma OAI.CubicTorus.weak_divergence_local_congr line 85
  5. lemma OAI.CubicTorus.L2_gradient_truncate line 101
  6. lemma OAI.CubicTorus.plane_L2_energy_mono line 122
  7. lemma OAI.CubicTorus.forced_replacement_energy_algebra line 140
  8. theorem OAI.CubicTorus.forced_cmc_replacement_decay line 149
  9. lemma OAI.CubicTorus.memLp_gradient_test_integrable line 236
  10. lemma OAI.CubicTorus.local_divergence_source line 244
  11. lemma OAI.CubicTorus.forced_divergence_localize line 285
  12. lemma OAI.CubicTorus.PlaneWeakGradient.comp_add line 335
  13. lemma OAI.CubicTorus.variable_divergence_comp_add line 355
  14. lemma OAI.CubicTorus.translate_preimage_ball line 377
  15. lemma OAI.CubicTorus.translate_setIntegral line 382
  16. lemma OAI.CubicTorus.L2_translate line 390
  17. theorem OAI.CubicTorus.forced_cmc_replacement_decay_at line 422
  18. theorem OAI.CubicTorus.cmc_replacement_decay line 488
  19. lemma OAI.CubicTorus.geometric_modulus_exponent line 551
  20. lemma OAI.CubicTorus.holder_bound_of_geometric_modulus line 563
  21. lemma OAI.CubicTorus.geometric_energy_decay line 606
  22. lemma OAI.CubicTorus.exists_decay_contraction line 652
  23. theorem OAI.CubicTorus.cmc_energy_decay line 702
  24. lemma OAI.CubicTorus.linearized_cmc_translate line 747
  25. theorem OAI.CubicTorus.cmc_replacement_decay_at line 771
  26. theorem OAI.CubicTorus.cmc_energy_decay_at line 796
  27. lemma OAI.CubicTorus.exists_small_power_scale line 834