OAI/Geometry/SmoothYau/Smoothness/ContinuousSobolevFirstDerivative.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.normalized_derivative_symbol_bound line 25
  2. def OAI.YauCounterexamples.normalizedDerivativeSymbol line 47
  3. lemma OAI.YauCounterexamples.norm_normalizedDerivativeSymbol_le line 56
  4. lemma OAI.YauCounterexamples.normalizedDerivativeSymbol_hasTemperateGrowth line 62
  5. def OAI.YauCounterexamples.sobolevDerivative line 68
  6. lemma OAI.YauCounterexamples.norm_sobolevDerivative_le line 72
  7. lemma OAI.YauCounterexamples.sobolevDerivative_distribution line 82
  8. lemma OAI.YauCounterexamples.sobolevDerivative_bound line 97
  9. def OAI.YauCounterexamples.sobolevSecondDerivative line 118
  10. lemma OAI.YauCounterexamples.sobolevSecondDerivative_distribution line 122
  11. lemma OAI.YauCounterexamples.norm_sobolevSecondDerivative_le line 131
  12. def OAI.YauCounterexamples.sobolevPrincipalPerturbation line 141
  13. lemma OAI.YauCounterexamples.norm_sobolevPrincipalPerturbation_le line 147
  14. lemma OAI.YauCounterexamples.sobolevPrincipalPerturbation_representative line 168
  15. theorem OAI.YauCounterexamples.small_principal_elliptic_solve line 177
  16. lemma OAI.YauCounterexamples.sobolevDerivative_schwartz line 240
  17. lemma OAI.YauCounterexamples.contDiff_sobolevRepresentative line 265
  18. lemma OAI.YauCounterexamples.sobolevDerivative_representative line 275
  19. lemma OAI.YauCounterexamples.fourierMultiplier_add line 350
  20. lemma OAI.YauCounterexamples.secondDerivative_fourier line 357
  21. def OAI.YauCounterexamples.physicalQuadraticEquiv line 371
  22. lemma OAI.YauCounterexamples.physicalQuadraticEquiv_norm_sq line 377
  23. lemma OAI.YauCounterexamples.principal_fourierMultiplier line 385
  24. lemma OAI.YauCounterexamples.elliptic_fourierMultiplier line 420
  25. lemma OAI.YauCounterexamples.sobolevInclusion_representative line 454
  26. lemma OAI.YauCounterexamples.fourierSobolevDistribution_congr line 462
  27. lemma OAI.YauCounterexamples.sobolevRepresentative_congr line 467
  28. lemma OAI.YauCounterexamples.sobolevSecondDerivative_representative line 473
  29. def OAI.YauCounterexamples.frozenSobolevOperator line 491
  30. lemma OAI.YauCounterexamples.frozenSobolevOperator_distribution line 497
  31. lemma OAI.YauCounterexamples.localEllipticInverse_sobolev_equation line 518
  32. lemma OAI.YauCounterexamples.frozenSobolevOperator_representative line 531
  33. lemma OAI.YauCounterexamples.continuous_sobolev_firstDerivative line 564
  34. lemma OAI.YauCounterexamples.fderiv_real_sobolevRepresentative line 574
  35. lemma OAI.YauCounterexamples.continuous_real_sobolev_firstJet line 582