OAI/Geometry/CubicTorus/Profiles/SiblingPlaneCarlemanS.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.plane_elliptic_weight_identity line 13
  2. lemma OAI.CubicTorus.plane_elliptic_transport_identity line 51
  3. theorem OAI.CubicTorus.plane_rellich_identity line 84
  4. def OAI.CubicTorus.sibling_planeCarlemanS line 121
  5. def OAI.CubicTorus.sibling_planeCarlemanP line 125
  6. lemma OAI.CubicTorus.planeCarlemanS_contDiff line 129
  7. lemma OAI.CubicTorus.planeCarlemanS_compact line 135
  8. lemma OAI.CubicTorus.sibling_planeCarlemanP_contDiff line 139
  9. lemma OAI.CubicTorus.sibling_planeCarlemanP_compact line 146
  10. lemma OAI.CubicTorus.plane_transport_weight_identity line 151
  11. theorem OAI.CubicTorus.plane_carleman_identity line 191
  12. lemma OAI.CubicTorus.plane_gradient_scaled_exp line 246
  13. lemma OAI.CubicTorus.planeElliptic_product line 256
  14. lemma OAI.CubicTorus.planeElliptic_scaled_exp line 279
  15. theorem OAI.CubicTorus.plane_elliptic_conjugation line 302
  16. theorem OAI.CubicTorus.plane_elliptic_conjugation_forward line 324
  17. def OAI.CubicTorus.planeBentHessian line 351
  18. lemma OAI.CubicTorus.planeBentHessian_apply line 354
  19. lemma OAI.CubicTorus.planeBentHessian_symm line 358
  20. lemma OAI.CubicTorus.planeBentHessian_quadratic line 364
  21. def OAI.CubicTorus.planeBentWeight line 370
  22. lemma OAI.CubicTorus.planeBentWeight_formula line 373
  23. lemma OAI.CubicTorus.planeBentWeight_contDiff line 378
  24. lemma OAI.CubicTorus.planeBentWeight_gradient line 384
  25. lemma OAI.CubicTorus.planeBentWeight_gradient_fderiv line 403
  26. lemma OAI.CubicTorus.planeBentWeight_gradient_center line 417
  27. lemma OAI.CubicTorus.planeBentWeight_center line 421
  28. lemma OAI.CubicTorus.plane_inner_clm_abs line 424
  29. lemma OAI.CubicTorus.plane_quadratic_coercive_near line 430
  30. lemma OAI.CubicTorus.plane_inner_bilinear_bound line 454
  31. lemma OAI.CubicTorus.plane_weight_center_gradient_bound line 462
  32. lemma OAI.CubicTorus.plane_weight_center_mass line 506
  33. lemma OAI.CubicTorus.plane_weight_positive_center line 532
  34. theorem OAI.CubicTorus.plane_local_carleman_weight line 597
  35. def OAI.CubicTorus.planeCarlemanG line 678
  36. lemma OAI.CubicTorus.planeCarlemanG_contDiff line 683
  37. lemma OAI.CubicTorus.planeCarlemanG_compact line 694
  38. lemma OAI.CubicTorus.plane_gradient_eq_zero_of_not_mem_tsupport line 700
  39. lemma OAI.CubicTorus.plane_carleman_integrated_identity line 705
  40. theorem OAI.CubicTorus.plane_carleman_estimate line 735
  41. theorem OAI.CubicTorus.plane_weighted_carleman_near line 842