OAI/Geometry/CubicTorus/Estimates/PlaneScaleEquiv.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.smooth_directional_commute line 14
  2. lemma OAI.CubicTorus.smooth_laplacian line 23
  3. lemma OAI.CubicTorus.laplacian_directional line 32
  4. lemma OAI.CubicTorus.PlaneWeakGradient.harmonic_component line 49
  5. lemma OAI.CubicTorus.scalar_convolution_norm_le line 79
  6. lemma OAI.CubicTorus.first_deriv_convolution_le line 91
  7. lemma OAI.CubicTorus.compact_convolution_value_lipschitz line 105
  8. theorem OAI.CubicTorus.plane_weak_harmonic_value_lipschitz line 137
  9. theorem OAI.CubicTorus.plane_L2_harmonic_value_lipschitz line 176
  10. theorem OAI.CubicTorus.plane_harmonic_gradient_bound line 228
  11. lemma OAI.CubicTorus.planeChange_real line 300
  12. lemma OAI.CubicTorus.planeChangeFactor_le_four line 307
  13. lemma OAI.CubicTorus.planeChange_setIntegral line 322
  14. lemma OAI.CubicTorus.planeChange_closedBall_L1 line 331
  15. theorem OAI.CubicTorus.frozen_cmc_gradient_bound line 382
  16. def OAI.CubicTorus.planeScaleEquiv line 471
  17. lemma OAI.CubicTorus.planeScaleEquiv_apply line 474
  18. lemma OAI.CubicTorus.planeScaleEquiv_symm_apply line 477
  19. lemma OAI.CubicTorus.planeScaleEquiv_preimage_ball line 480
  20. lemma OAI.CubicTorus.planeScaleEquiv_preimage_closedBall line 487
  21. lemma OAI.CubicTorus.planeScaleFactor line 494
  22. lemma OAI.CubicTorus.planeScale_setIntegral line 504
  23. lemma OAI.CubicTorus.constant_divergence_scale line 512
  24. theorem OAI.CubicTorus.frozen_cmc_gradient_scaled line 560
  25. lemma OAI.CubicTorus.L2_vector_norm_sq_integrable line 665
  26. lemma OAI.CubicTorus.plane_closedBall_mass_le line 670
  27. lemma OAI.CubicTorus.L2_local_L1 line 680
  28. theorem OAI.CubicTorus.cmc_replacement_bounds line 714
  29. theorem OAI.CubicTorus.forced_cmc_replacement_bounds line 787
  30. lemma OAI.CubicTorus.plane_L2_sub_const_integrable line 872