OAI/Geometry/SmoothYau/Smoothness/TestAsSmooth.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.testAsSmooth line 13
  2. lemma OAI.YauCounterexamples.testAsSmooth_apply line 14
  3. lemma OAI.YauCounterexamples.testAsSmooth_derivative line 16
  4. lemma OAI.YauCounterexamples.testAsSmooth_multiply line 18
  5. lemma OAI.YauCounterexamples.testAsSmooth_sum line 21
  6. lemma OAI.YauCounterexamples.testAsSmooth_add line 26
  7. lemma OAI.YauCounterexamples.SmoothScalar.eventuallyEq_directional line 29
  8. lemma OAI.YauCounterexamples.coefficientElliptic_eq_of_eventuallyEq line 36
  9. def OAI.YauCounterexamples.coefficientSchrodinger line 50
  10. lemma OAI.YauCounterexamples.coefficientSchrodinger_eq_of_eventuallyEq line 53
  11. lemma OAI.YauCounterexamples.testSchrodinger_asSmooth line 59
  12. lemma OAI.YauCounterexamples.testSchrodinger_eval_congr line 65
  13. lemma OAI.YauCounterexamples.testSchrodinger_zero_of_eventually_zero line 72