OAI/Geometry/SmoothYau/Smoothness/LpNormTwoBounds.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.besselPotential_two_eq line 19
  2. def OAI.YauCounterexamples.schwartzEllipticShift line 26
  3. lemma OAI.YauCounterexamples.schwartzEllipticShift_apply line 30
  4. lemma OAI.YauCounterexamples.schwartzEllipticShift_distribution line 34
  5. lemma OAI.YauCounterexamples.schwartzToSobolev_shift line 39
  6. lemma OAI.YauCounterexamples.schwartzToSobolev_zero line 47
  7. lemma OAI.YauCounterexamples.norm_schwartzToSobolev_zero line 54
  8. lemma OAI.YauCounterexamples.schwartzToSobolev_iterate_shift line 58
  9. theorem OAI.YauCounterexamples.norm_schwartzToSobolev_even line 69
  10. lemma OAI.YauCounterexamples.sobolevInclusion_schwartz line 76
  11. lemma OAI.YauCounterexamples.norm_schwartzToSobolev_mono line 81
  12. lemma OAI.YauCounterexamples.schwartz_derivative_norm_bound line 88
  13. lemma OAI.YauCounterexamples.norm_schwartz_word_bound line 105
  14. lemma OAI.YauCounterexamples.schwartz_word_L2_bound line 125
  15. lemma OAI.YauCounterexamples.norm_schwartz_shift_le line 148
  16. def OAI.YauCounterexamples.SchwartzWordBound line 168
  17. lemma OAI.YauCounterexamples.SchwartzWordBound.mono line 172
  18. lemma OAI.YauCounterexamples.SchwartzWordBound.second line 176
  19. theorem OAI.YauCounterexamples.sobolev_even_le_word_bound line 187
  20. lemma OAI.YauCounterexamples.schwartz_word_eLpNorm_bound line 231
  21. theorem OAI.YauCounterexamples.iteratedFDeriv_eLpNorm_bound line 241
  22. def OAI.YauCounterexamples.jetMajorant line 306
  23. lemma OAI.YauCounterexamples.jetMajorant_nonneg line 310
  24. lemma OAI.YauCounterexamples.le_jetMajorant line 314
  25. lemma OAI.YauCounterexamples.continuous_jetMajorant line 322
  26. theorem OAI.YauCounterexamples.jetMajorant_eLpNorm_bound line 328
  27. lemma OAI.YauCounterexamples.compact_derivative_bound line 378
  28. lemma OAI.YauCounterexamples.cutoff_comp_derivative_bound line 395
  29. lemma OAI.YauCounterexamples.cutoff_comp_derivative_zero line 443
  30. def OAI.YauCounterexamples.cutoffPullback line 466
  31. lemma OAI.YauCounterexamples.cutoffPullback_apply line 471
  32. lemma OAI.YauCounterexamples.supported_pullback_eLpNorm_le line 475
  33. lemma OAI.YauCounterexamples.cutoffPullback_derivative_L2 line 509
  34. lemma OAI.YauCounterexamples.lp_norm_le_two_bounds line 568
  35. lemma OAI.YauCounterexamples.power_interpolation line 595
  36. lemma OAI.YauCounterexamples.norm_schwartz_interpolation line 608
  37. lemma OAI.YauCounterexamples.sobolev_interpolation line 625