OAI/Geometry/SmoothYau/Smoothness/TestDerivativeComm.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.YauCounterexamples.smoothScalarAlgebra line 12
  2. abbrev OAI.YauCounterexamples.SmoothScalar line 29
  3. instance OAI.YauCounterexamples.SmoothScalar.(instance at line 33) line 33
  4. lemma OAI.YauCounterexamples.SmoothScalar.contDiff line 34
  5. def OAI.YauCounterexamples.SmoothScalar.directional line 36
  6. lemma OAI.YauCounterexamples.SmoothScalar.directional_apply line 55
  7. lemma OAI.YauCounterexamples.SmoothScalar.directional_mul line 57
  8. abbrev OAI.YauCounterexamples.EllipticTest line 71
  9. def OAI.YauCounterexamples.testDerivative line 72
  10. lemma OAI.YauCounterexamples.testDerivative_apply line 76
  11. def OAI.YauCounterexamples.testMultiply line 80
  12. lemma OAI.YauCounterexamples.testMultiply_apply line 82
  13. lemma OAI.YauCounterexamples.testProductRule line 85
  14. lemma OAI.YauCounterexamples.testMultiply_add line 99
  15. lemma OAI.YauCounterexamples.testMultiply_smul line 103
  16. lemma OAI.YauCounterexamples.testPair_integrable line 110
  17. def OAI.YauCounterexamples.testPair line 115
  18. lemma OAI.YauCounterexamples.testPair_comm line 117
  19. lemma OAI.YauCounterexamples.testPair_add_left line 119
  20. lemma OAI.YauCounterexamples.testPair_smul_left line 123
  21. lemma OAI.YauCounterexamples.testPair_nonneg line 127
  22. lemma OAI.YauCounterexamples.testDerivative_skew line 130
  23. lemma OAI.YauCounterexamples.testMultiply_symmetric line 142
  24. lemma OAI.YauCounterexamples.testDerivative_comm line 157
  25. lemma OAI.YauCounterexamples.testMultiply_mul line 170
  26. lemma OAI.YauCounterexamples.testPair_add_right line 176
  27. lemma OAI.YauCounterexamples.testPair_smul_right line 179
  28. lemma OAI.YauCounterexamples.testPair_zero_left line 182
  29. lemma OAI.YauCounterexamples.testPair_zero_right line 183
  30. lemma OAI.YauCounterexamples.testPair_neg_left line 184
  31. lemma OAI.YauCounterexamples.testPair_neg_right line 186
  32. lemma OAI.YauCounterexamples.testPair_sub_left line 188
  33. lemma OAI.YauCounterexamples.testPair_sub_right line 191
  34. lemma OAI.YauCounterexamples.testPair_sum_left line 194
  35. lemma OAI.YauCounterexamples.testPair_sum_right line 200
  36. lemma OAI.YauCounterexamples.testPair_weighted_derivative line 207
  37. lemma OAI.YauCounterexamples.testPair_weighted_self_derivative line 215