OAI/Geometry/SmoothYau/Smoothness/MomentBesselLp.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.boundedDistribution line 21
  2. lemma OAI.YauCounterexamples.boundedDistribution_apply line 24
  3. def OAI.YauCounterexamples.inverseFourierL1 line 31
  4. lemma OAI.YauCounterexamples.inverseFourierL1_apply line 35
  5. theorem OAI.YauCounterexamples.inverseFourierL1_distribution line 39
  6. theorem OAI.YauCounterexamples.sobolev_continuous_representative line 56
  7. lemma OAI.YauCounterexamples.memLp_bessel_weight line 64
  8. lemma OAI.YauCounterexamples.norm_pow_mul_bessel_weight_le line 87
  9. lemma OAI.YauCounterexamples.memLp_moment_bessel_weight line 102
  10. theorem OAI.YauCounterexamples.sobolev_fourier_moments line 113
  11. theorem OAI.YauCounterexamples.sobolev_Ck_representative line 157
  12. theorem OAI.YauCounterexamples.boundedDistribution_injective line 169
  13. theorem OAI.YauCounterexamples.sobolev_smooth_representative line 183
  14. lemma OAI.YauCounterexamples.norm_inverseFourierL1_le line 199
  15. theorem OAI.YauCounterexamples.sobolev_quantitative_representative line 209
  16. lemma OAI.YauCounterexamples.lintegral_mul_sq_le line 255
  17. theorem OAI.YauCounterexamples.young_lintegral_sq line 275
  18. theorem OAI.YauCounterexamples.young_eLpNorm_two line 296
  19. theorem OAI.YauCounterexamples.young_memLp_two line 321
  20. def OAI.YauCounterexamples.sobolevWeight line 327
  21. lemma OAI.YauCounterexamples.sobolevWeight_pos line 330
  22. lemma OAI.YauCounterexamples.continuous_sobolevWeight line 334
  23. lemma OAI.YauCounterexamples.sobolevWeight_add_le line 340
  24. def OAI.YauCounterexamples.weightedSchwartz line 360
  25. lemma OAI.YauCounterexamples.weightedSchwartz_apply line 364
  26. lemma OAI.YauCounterexamples.norm_weightedSchwartz line 373
  27. lemma OAI.YauCounterexamples.integrable_sobolevWeight_norm line 378
  28. lemma OAI.YauCounterexamples.integrable_norm_mul_sub line 382
  29. lemma OAI.YauCounterexamples.weighted_convolution_pointwise line 389
  30. lemma OAI.YauCounterexamples.stronglyMeasurable_mulConvolution line 414
  31. lemma OAI.YauCounterexamples.mulConvolution_comm line 422
  32. theorem OAI.YauCounterexamples.weighted_convolution_eLpNorm line 427
  33. lemma OAI.YauCounterexamples.memLp_inverse_sobolevWeight line 463
  34. lemma OAI.YauCounterexamples.schwartz_eLpNorm_one_le_weighted line 483
  35. theorem OAI.YauCounterexamples.weighted_convolution_algebra_eLpNorm line 505
  36. lemma OAI.YauCounterexamples.schwartz_fourierInv_convolution line 522
  37. lemma OAI.YauCounterexamples.schwartz_fourier_product line 530
  38. def OAI.YauCounterexamples.schwartzToSobolev line 557
  39. lemma OAI.YauCounterexamples.schwartzToSobolev_apply line 562
  40. lemma OAI.YauCounterexamples.weightedSchwartz_neg_cancel line 566
  41. lemma OAI.YauCounterexamples.denseRange_schwartzToSobolev line 578
  42. lemma OAI.YauCounterexamples.schwartz_smul_distribution line 588
  43. lemma OAI.YauCounterexamples.schwartzToSobolev_distribution line 599
  44. def OAI.YauCounterexamples.sobolevAlgebraConstant line 609
  45. lemma OAI.YauCounterexamples.sobolevAlgebraConstant_nonneg line 613
  46. lemma OAI.YauCounterexamples.schwartz_sobolev_product_bound line 616
  47. def OAI.YauCounterexamples.schwartzSobolevProduct line 642
  48. def OAI.YauCounterexamples.sobolevProduct line 649
  49. lemma OAI.YauCounterexamples.sobolevProduct_schwartz line 656
  50. lemma OAI.YauCounterexamples.sobolevProduct_bound line 662
  51. def OAI.YauCounterexamples.inverseBesselLp line 667
  52. def OAI.YauCounterexamples.sobolevFourierL1 line 672
  53. def OAI.YauCounterexamples.sobolevRepresentative line 681
  54. lemma OAI.YauCounterexamples.sobolevRepresentative_distribution line 685
  55. lemma OAI.YauCounterexamples.boundedDistribution_schwartz line 693
  56. lemma OAI.YauCounterexamples.sobolevRepresentative_schwartz line 699
  57. theorem OAI.YauCounterexamples.sobolevRepresentative_product line 706
  58. def OAI.YauCounterexamples.momentBesselLp line 734
  59. lemma OAI.YauCounterexamples.fourierL1_moment_norm line 739
  60. theorem OAI.YauCounterexamples.sobolevRepresentative_jet_bound line 771