OAI/Geometry/CubicTorus/Estimates/PlaneQuadraticWeight.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicTorus.planeQuadraticWeight line 13
  2. lemma OAI.CubicTorus.planeQuadraticWeight_smooth line 16
  3. lemma OAI.CubicTorus.planeQuadraticWeight_fderiv line 22
  4. lemma OAI.CubicTorus.planeQuadraticWeight_gradient line 36
  5. lemma OAI.CubicTorus.planeQuadraticWeight_hessian line 45
  6. lemma OAI.CubicTorus.planeQuadraticWeight_gradient_center line 61
  7. lemma OAI.CubicTorus.quadratic_weight_R line 65
  8. lemma OAI.CubicTorus.quadratic_weight_transport_center line 80
  9. lemma OAI.CubicTorus.plane_inner_clm_bound line 103
  10. lemma OAI.CubicTorus.plane_inner_double_clm_bound line 110
  11. lemma OAI.CubicTorus.quadratic_weight_R_lower line 118
  12. lemma OAI.CubicTorus.quadratic_weight_transport_lower line 155
  13. lemma OAI.CubicTorus.plane_ellipticity_perturb line 192
  14. theorem OAI.CubicTorus.planeCarleman_weight_exists line 204
  15. lemma OAI.CubicTorus.quadratic_weight_scalar_outside line 309
  16. lemma OAI.CubicTorus.planeQuadraticWeight_outside line 334
  17. lemma OAI.CubicTorus.plane_gradient_exp line 363
  18. lemma OAI.CubicTorus.planeElliptic_mul line 372
  19. lemma OAI.CubicTorus.planeElliptic_exp line 393
  20. theorem OAI.CubicTorus.planeCarleman_conjugation line 412
  21. lemma OAI.CubicTorus.plane_square_compact line 439
  22. theorem OAI.CubicTorus.planeCarleman_weighted line 444
  23. theorem OAI.CubicTorus.planeCarleman_vanish_above line 475
  24. lemma OAI.CubicTorus.plane_gradient_eventuallyEq line 565
  25. lemma OAI.CubicTorus.planeElliptic_congr_nhds line 570
  26. lemma OAI.CubicTorus.planeElliptic_zero line 577
  27. lemma OAI.CubicTorus.planeElliptic_zero_of_notMem_tsupport line 581
  28. lemma OAI.CubicTorus.planeElliptic_zero_on_open line 588
  29. theorem OAI.CubicTorus.planeElliptic_continue_tangent_ball line 608
  30. def OAI.CubicTorus.planeHopfBarrier line 710
  31. lemma OAI.CubicTorus.planeHopfBarrier_smooth line 713
  32. lemma OAI.CubicTorus.planeHopfBarrier_fderiv line 717
  33. lemma OAI.CubicTorus.planeHopfBarrier_gradient line 730
  34. lemma OAI.CubicTorus.planeHopfBarrier_hessian line 738
  35. lemma OAI.CubicTorus.planeFrameOperator_barrier line 755
  36. lemma OAI.CubicTorus.planeFrameOperator_barrier_pos line 764
  37. lemma OAI.CubicTorus.deriv_nonneg_of_right_min line 799
  38. lemma OAI.CubicTorus.planeHopfBarrier_inward line 808
  39. theorem OAI.CubicTorus.planeFrameOperator_hopf line 819