OAI/Geometry/SmoothYau/Smoothness/DistanceSquare.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.coefficientTransport line 16
  2. def OAI.YauCounterexamples.carlemanSymmetric line 19
  3. def OAI.YauCounterexamples.carlemanSkew line 23
  4. lemma OAI.YauCounterexamples.testMultiplier_skew_pair line 27
  5. lemma OAI.YauCounterexamples.derivative_product_energy line 46
  6. theorem OAI.YauCounterexamples.carleman_commutator line 65
  7. lemma OAI.YauCounterexamples.testPair_cauchy_shift line 87
  8. lemma OAI.YauCounterexamples.SmoothScalar.sum_apply line 103
  9. def OAI.YauCounterexamples.coefficientGradient line 111
  10. def OAI.YauCounterexamples.coefficientNorm line 114
  11. def OAI.YauCounterexamples.convexifyPhase line 117
  12. lemma OAI.YauCounterexamples.phase_derivative line 120
  13. lemma OAI.YauCounterexamples.phase_gradient line 130
  14. lemma OAI.YauCounterexamples.phase_norm line 138
  15. lemma OAI.YauCounterexamples.SmoothScalar.directional_one line 146
  16. lemma OAI.YauCounterexamples.phase_gradient_at line 151
  17. lemma OAI.YauCounterexamples.phase_norm_at line 159
  18. lemma OAI.YauCounterexamples.phase_gradient_derivative_at line 167
  19. lemma OAI.YauCounterexamples.phase_transport_norm_at line 179
  20. def OAI.YauCounterexamples.exponentialWeight line 220
  21. lemma OAI.YauCounterexamples.exponentialWeight_apply line 222
  22. lemma OAI.YauCounterexamples.exponentialWeight_derivative line 225
  23. lemma OAI.YauCounterexamples.testMultiply_one line 237
  24. lemma OAI.YauCounterexamples.testMultiply_exponential_inverse line 240
  25. lemma OAI.YauCounterexamples.coefficientElliptic_exponential line 246
  26. lemma OAI.YauCounterexamples.testElliptic_product line 280
  27. lemma OAI.YauCounterexamples.testElliptic_exponential line 313
  28. lemma OAI.YauCounterexamples.carleman_conjugation line 339
  29. def OAI.YauCounterexamples.distanceSquare line 361
  30. lemma OAI.YauCounterexamples.distanceSquare_apply line 365
  31. lemma OAI.YauCounterexamples.distanceSquare_derivative_center line 367
  32. def OAI.YauCounterexamples.tangentPhase line 375
  33. lemma OAI.YauCounterexamples.tangentPhase_at line 376
  34. lemma OAI.YauCounterexamples.tangentPhase_derivative_center line 378
  35. lemma OAI.YauCounterexamples.tangentPhase_annular_gap line 385