OAI/Geometry/CubicTorus/Curvature/CmcStretch.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.PlaneWeakGradient.weak_laplacian line 14
  2. lemma OAI.CubicTorus.L2_constant_operator_coercive line 64
  3. lemma OAI.CubicTorus.hilbert_coercive_replacement line 75
  4. theorem OAI.CubicTorus.plane_constant_elliptic_replacement line 112
  5. lemma OAI.CubicTorus.L2_divergence_orthogonal line 141
  6. lemma OAI.CubicTorus.hilbert_coercive_replacement_error line 156
  7. theorem OAI.CubicTorus.plane_frozen_elliptic_replacement line 177
  8. lemma OAI.CubicTorus.bounded_coefficient_memLp line 204
  9. lemma OAI.CubicTorus.Lp.norm_le_mul_of_ae line 215
  10. lemma OAI.CubicTorus.frozen_coefficient_residual_bound line 226
  11. lemma OAI.CubicTorus.frozen_coefficient_local_residual_bound line 239
  12. lemma OAI.CubicTorus.cmcJacobian_uniform_lipschitz line 255
  13. lemma OAI.CubicTorus.plane_gradient_dist line 274
  14. theorem OAI.CubicTorus.WeakCMCGraph.holder_symbol_extension line 278
  15. def OAI.CubicTorus.cmcStretch line 317
  16. def OAI.CubicTorus.cmcCompress line 320
  17. lemma OAI.CubicTorus.cmcStretch_apply line 323
  18. lemma OAI.CubicTorus.cmcCompress_apply line 328
  19. lemma OAI.CubicTorus.cmcCompress_stretch line 333
  20. lemma OAI.CubicTorus.cmcStretch_compress line 347
  21. def OAI.CubicTorus.cmcMetricEquiv line 361
  22. lemma OAI.CubicTorus.cmcCompress_symm line 369
  23. lemma OAI.CubicTorus.cmcStretch_symm line 374
  24. lemma OAI.CubicTorus.cmcCompress_sq line 379
  25. lemma OAI.CubicTorus.cmcJacobian_compress line 394
  26. lemma OAI.CubicTorus.cmcStretch_jacobian line 398
  27. lemma OAI.CubicTorus.cmcStretch_norm line 402
  28. lemma OAI.CubicTorus.cmcCompress_norm line 420
  29. def OAI.CubicTorus.planeChangeFactor line 450
  30. lemma OAI.CubicTorus.planeChangeFactor_pos line 453
  31. lemma OAI.CubicTorus.planeChange_map line 457
  32. lemma OAI.CubicTorus.planeChange_integral line 462
  33. lemma OAI.CubicTorus.planeChange_memLp line 470
  34. lemma OAI.CubicTorus.planeChange_ae line 478
  35. lemma OAI.CubicTorus.PlaneWeakGradient.comp_selfAdjoint line 484
  36. lemma OAI.CubicTorus.cmcMetricEquiv_apply line 525
  37. lemma OAI.CubicTorus.cmcMetricEquiv_symm_apply line 526
  38. lemma OAI.CubicTorus.frozen_cmc_divergence_change line 528
  39. theorem OAI.CubicTorus.frozen_cmc_weak_harmonic line 562
  40. theorem OAI.CubicTorus.plane_L2_weak_harmonic_smooth line 604
  41. lemma OAI.CubicTorus.C1_weak_gradient line 656
  42. lemma OAI.CubicTorus.PlaneWeakGradient.local_congr line 672
  43. lemma OAI.CubicTorus.PlaneWeakGradient.unique line 694
  44. lemma OAI.CubicTorus.PlaneWeakGradient.mono line 729
  45. lemma OAI.CubicTorus.planeChange_ae_prop line 734
  46. lemma OAI.CubicTorus.cmcMetricEquiv_norm line 740
  47. lemma OAI.CubicTorus.cmcMetricEquiv_symm_norm line 743
  48. lemma OAI.CubicTorus.cmcMetricEquiv_ball line 746
  49. theorem OAI.CubicTorus.frozen_cmc_smooth line 753
  50. lemma OAI.CubicTorus.frozen_replacement_divergence line 803
  51. theorem OAI.CubicTorus.cmc_frozen_replacement line 816