OAI/Geometry/SmoothYau/Spectrum/AnisotropicConstant.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.YauCounterexamples.FourierSobolevSpace line 17
  2. def OAI.YauCounterexamples.fourierSobolevDistribution line 19
  3. lemma OAI.YauCounterexamples.fourierSobolevDistribution_apply line 26
  4. lemma OAI.YauCounterexamples.weighted_fourier_fourierSobolevDistribution line 31
  5. lemma OAI.YauCounterexamples.fourierSobolevDistribution_injective line 49
  6. theorem OAI.YauCounterexamples.range_fourierSobolevDistribution line 58
  7. lemma OAI.YauCounterexamples.norm_bounded_toLp_top_le line 80
  8. def OAI.YauCounterexamples.sobolevBoundedMultiplier line 89
  9. lemma OAI.YauCounterexamples.norm_sobolevBoundedMultiplier_le line 99
  10. lemma OAI.YauCounterexamples.sobolevBoundedMultiplier_distribution line 103
  11. lemma OAI.YauCounterexamples.besselPotential_fourierSobolevDistribution line 116
  12. lemma OAI.YauCounterexamples.inverse_quadratic_hasTemperateGrowth line 133
  13. def OAI.YauCounterexamples.uniformResolventSymbol line 150
  14. lemma OAI.YauCounterexamples.uniformResolventSymbol_hasTemperateGrowth line 161
  15. lemma OAI.YauCounterexamples.norm_uniformResolventSymbol_le line 170
  16. def OAI.YauCounterexamples.uniformEuclideanResolvent line 179
  17. lemma OAI.YauCounterexamples.quadraticMultiplier_eq line 183
  18. lemma OAI.YauCounterexamples.uniformEuclideanResolvent_equation line 199
  19. def OAI.YauCounterexamples.uniformSobolevResolvent line 215
  20. lemma OAI.YauCounterexamples.uniformSobolevResolvent_distribution line 219
  21. lemma OAI.YauCounterexamples.norm_uniformSobolevResolvent_le line 254
  22. theorem OAI.YauCounterexamples.uniformSobolevResolvent_equation line 258
  23. def OAI.YauCounterexamples.sobolevInclusionSymbol line 288
  24. lemma OAI.YauCounterexamples.sobolevInclusionSymbol_hasTemperateGrowth line 299
  25. lemma OAI.YauCounterexamples.norm_sobolevInclusionSymbol_le line 305
  26. def OAI.YauCounterexamples.sobolevInclusion line 313
  27. lemma OAI.YauCounterexamples.norm_sobolevInclusion_le line 318
  28. lemma OAI.YauCounterexamples.sobolevInclusion_distribution line 322
  29. lemma OAI.YauCounterexamples.sobolevInclusion_injective line 341
  30. lemma OAI.YauCounterexamples.sobolevInclusion_trans line 347
  31. def OAI.YauCounterexamples.massResolventSymbol line 354
  32. lemma OAI.YauCounterexamples.massResolventSymbol_hasTemperateGrowth line 365
  33. lemma OAI.YauCounterexamples.norm_massResolventSymbol_le line 370
  34. def OAI.YauCounterexamples.massSobolevResolvent line 378
  35. lemma OAI.YauCounterexamples.norm_massSobolevResolvent_le line 383
  36. lemma OAI.YauCounterexamples.massSobolevResolvent_distribution line 387
  37. lemma OAI.YauCounterexamples.uniformSobolevResolvent_mass_bound line 393
  38. lemma OAI.YauCounterexamples.halfResolvent_scalar_bound line 423
  39. def OAI.YauCounterexamples.halfResolventSymbol line 441
  40. lemma OAI.YauCounterexamples.halfResolventSymbol_hasTemperateGrowth line 458
  41. lemma OAI.YauCounterexamples.norm_halfResolventSymbol_le line 468
  42. def OAI.YauCounterexamples.halfSobolevResolvent line 476
  43. lemma OAI.YauCounterexamples.norm_halfSobolevResolvent_le line 481
  44. lemma OAI.YauCounterexamples.halfSobolevResolvent_distribution line 485
  45. lemma OAI.YauCounterexamples.uniformSobolevResolvent_half_bound line 512
  46. def OAI.YauCounterexamples.anisotropicConstant line 545
  47. lemma OAI.YauCounterexamples.anisotropic_norm_bound line 548
  48. lemma OAI.YauCounterexamples.anisotropic_inverse_hasTemperateGrowth line 563
  49. def OAI.YauCounterexamples.anisotropicResolventSymbol line 568
  50. lemma OAI.YauCounterexamples.anisotropicResolventSymbol_hasTemperateGrowth line 581
  51. lemma OAI.YauCounterexamples.norm_anisotropicResolventSymbol_le line 590
  52. def OAI.YauCounterexamples.anisotropicSobolevResolvent line 600
  53. lemma OAI.YauCounterexamples.norm_anisotropicSobolevResolvent_le line 605
  54. lemma OAI.YauCounterexamples.anisotropicSobolevResolvent_distribution line 609
  55. theorem OAI.YauCounterexamples.anisotropicSobolevResolvent_equation line 637
  56. lemma OAI.YauCounterexamples.anisotropic_half_scalar_bound line 658
  57. def OAI.YauCounterexamples.anisotropicHalfResolventSymbol line 679
  58. lemma OAI.YauCounterexamples.anisotropicHalfResolventSymbol_hasTemperateGrowth line 696
  59. lemma OAI.YauCounterexamples.norm_anisotropicHalfResolventSymbol_le line 706
  60. def OAI.YauCounterexamples.anisotropicHalfSobolevResolvent line 714
  61. lemma OAI.YauCounterexamples.norm_anisotropicHalfSobolevResolvent_le line 719
  62. lemma OAI.YauCounterexamples.anisotropicHalfSobolevResolvent_distribution line 723
  63. lemma OAI.YauCounterexamples.anisotropicSobolevResolvent_half_bound line 750