OAI/Geometry/SmoothYau/Smoothness/SobolevRepresentativeOrderCongr.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.scalarAffine_hasFDerivAt line 22
  2. lemma OAI.YauCounterexamples.fderiv_scalarAffine line 27
  3. lemma OAI.YauCounterexamples.differentiable_directional line 36
  4. lemma OAI.YauCounterexamples.second_fderiv_scalarAffine line 41
  5. lemma OAI.YauCounterexamples.second_fderiv_mul line 56
  6. def OAI.YauCounterexamples.euclideanElliptic line 82
  7. lemma OAI.YauCounterexamples.euclideanElliptic_mul line 88
  8. lemma OAI.YauCounterexamples.euclideanElliptic_scalarAffine line 101
  9. lemma OAI.YauCounterexamples.euclideanElliptic_congr line 129
  10. lemma OAI.YauCounterexamples.second_fderiv_add_at line 137
  11. lemma OAI.YauCounterexamples.euclideanElliptic_add_at line 155
  12. lemma OAI.YauCounterexamples.second_fderiv_const_mul_at line 164
  13. lemma OAI.YauCounterexamples.euclideanElliptic_const_mul_at line 179
  14. lemma OAI.YauCounterexamples.euclideanElliptic_zero line 187
  15. lemma OAI.YauCounterexamples.fderiv_inverseScalarAffine line 200
  16. lemma OAI.YauCounterexamples.unscale_local_equation line 212
  17. def OAI.YauCounterexamples.ellipticCommutator line 235
  18. lemma OAI.YauCounterexamples.cutoff_parametrix_equation line 241
  19. lemma OAI.YauCounterexamples.support_ellipticCommutator line 256
  20. lemma OAI.YauCounterexamples.ellipticCommutator_congr_coeff line 267
  21. lemma OAI.YauCounterexamples.sobolevRepresentative_order_congr line 291
  22. def OAI.YauCounterexamples.firstOrderSobolev line 297
  23. lemma OAI.YauCounterexamples.firstOrderSobolev_representative line 305
  24. lemma OAI.YauCounterexamples.contDiff_directional line 330
  25. lemma OAI.YauCounterexamples.contDiff_euclideanElliptic line 334
  26. lemma OAI.YauCounterexamples.hasCompactSupport_euclideanElliptic line 349
  27. def OAI.YauCounterexamples.ellipticCutoffSchwartz line 361
  28. def OAI.YauCounterexamples.cutoffDerivativeSchwartz line 367
  29. lemma OAI.YauCounterexamples.cutoffDerivativeSchwartz_apply line 372
  30. def OAI.YauCounterexamples.scalarAffineHomeomorph line 379
  31. lemma OAI.YauCounterexamples.hasCompactSupport_comp_scalarAffine line 387
  32. def OAI.YauCounterexamples.affineSchwartz line 391
  33. lemma OAI.YauCounterexamples.affineSchwartz_apply line 394