OAI/Geometry/CubicTorus/Profiles/SiblingCmcSecant.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.planeBentWeight_outside_ball line 13
  2. lemma OAI.CubicTorus.planeBentWeight_lower_near line 57
  3. lemma OAI.CubicTorus.continuous_square_integrable line 78
  4. lemma OAI.CubicTorus.weighted_square_integrable line 85
  5. lemma OAI.CubicTorus.weighted_square_lower line 92
  6. lemma OAI.CubicTorus.weighted_square_upper line 111
  7. lemma OAI.CubicTorus.carleman_polynomial_mass_zero line 127
  8. theorem OAI.CubicTorus.carleman_zero_on_open line 146
  9. lemma OAI.CubicTorus.planeElliptic_germ line 188
  10. lemma OAI.CubicTorus.sibling_planeElliptic_zero line 194
  11. lemma OAI.CubicTorus.planeElliptic_zero_on line 198
  12. lemma OAI.CubicTorus.planeElliptic_support line 206
  13. lemma OAI.CubicTorus.planeBumpCutoff_eq line 228
  14. lemma OAI.CubicTorus.planeBumpCutoff_germ line 232
  15. lemma OAI.CubicTorus.planeBumpCutoff_error line 237
  16. theorem OAI.CubicTorus.plane_elliptic_zero_ball_extension line 267
  17. lemma OAI.CubicTorus.plane_interior_tangent_ball line 349
  18. lemma OAI.CubicTorus.plane_interior_tangent_ball_at line 387
  19. theorem OAI.CubicTorus.plane_elliptic_unique_continuation line 411
  20. def OAI.CubicTorus.sibling_cmcSecant line 456
  21. lemma OAI.CubicTorus.sibling_cmcSecant_apply line 461
  22. lemma OAI.CubicTorus.sibling_cmcSecant_symmetric line 467
  23. lemma OAI.CubicTorus.cmcSecant_self line 473
  24. lemma OAI.CubicTorus.cmcSecant_positive line 482
  25. lemma OAI.CubicTorus.cmcSecant_flux_difference line 501
  26. lemma OAI.CubicTorus.sibling_cmcSecant_contDiff line 517
  27. def OAI.CubicTorus.planeCMC line 547
  28. lemma OAI.CubicTorus.sibling_planeDivergence_sub line 550
  29. lemma OAI.CubicTorus.planeCMC_germ line 556
  30. lemma OAI.CubicTorus.cmcSecant_equation line 562
  31. theorem OAI.CubicTorus.smooth_CMC_graph_coincidence line 577
  32. lemma OAI.CubicTorus.plane_local_smooth_extension line 593
  33. theorem OAI.CubicTorus.CMC_graph_coincidence line 610
  34. lemma OAI.CubicTorus.normalGraph_tangent_normal line 658
  35. lemma OAI.CubicTorus.graph_projection_injective line 671
  36. def OAI.CubicTorus.graphProjectionEquiv line 695
  37. lemma OAI.CubicTorus.graphProjectionEquiv_coe line 703
  38. lemma OAI.CubicTorus.normalGraph_contDiff line 709
  39. theorem OAI.CubicTorus.sibling_normalGraph_regraph line 713
  40. lemma OAI.CubicTorus.graph_normal_tangent_vector_eq line 796
  41. lemma OAI.CubicTorus.graph_normal_tangent_positive line 816
  42. lemma OAI.CubicTorus.normalGraph_gradient_zero_of_normal line 827