OAI/Analysis/FourierExtension/L2Fourier.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Bounded pullback densities and graph Fourier L4 estimates.

  1. lemma OAI.DiagonalExtension.BoundedPullback.comp_memLp line 25
  2. lemma OAI.DiagonalExtension.BoundedPullback.comp_ae line 29
  3. def OAI.DiagonalExtension.BoundedPullback.pullbackLinear line 33
  4. lemma OAI.DiagonalExtension.BoundedPullback.pullbackLinear_ae line 53
  5. lemma OAI.DiagonalExtension.BoundedPullback.enorm_pullbackLinear_le line 57
  6. lemma OAI.DiagonalExtension.BoundedPullback.norm_pullbackLinear_le line 68
  7. def OAI.DiagonalExtension.BoundedPullback.pullback line 76
  8. lemma OAI.DiagonalExtension.BoundedPullback.pullback_ae line 81
  9. lemma OAI.DiagonalExtension.BoundedPullback.norm_pullback_le line 85
  10. theorem OAI.DiagonalExtension.BoundedPullback.exists_density line 89
  11. theorem OAI.DiagonalExtension.BoundedPullback.exists_density_mul line 113
  12. lemma OAI.DiagonalExtension.BoundedPullback.map_restrict_le_restrict line 133
  13. lemma OAI.DiagonalExtension.BoundedPullback.density_support line 156
  14. theorem OAI.DiagonalExtension.BoundedPullback.exists_integrable_density line 183
  15. lemma OAI.DiagonalExtension.BoundedPullback.density_bounded_test line 226
  16. lemma OAI.DiagonalExtension.TensorL2.memLp_mul_prod line 261
  17. lemma OAI.DiagonalExtension.TensorL2.norm_sq_toLp line 267
  18. lemma OAI.DiagonalExtension.TensorL2.norm_mul_prod line 277
  19. lemma OAI.DiagonalExtension.FourierCompatibility.integral_fourier_swap line 296
  20. theorem OAI.DiagonalExtension.FourierCompatibility.fourier_ae line 304
  21. lemma OAI.DiagonalExtension.FourierCompatibility.fourier_memLp line 323
  22. def OAI.DiagonalExtension.GraphFourier.transform line 346
  23. def OAI.DiagonalExtension.GraphFourier.pairMap line 349
  24. lemma OAI.DiagonalExtension.GraphFourier.pairMap_continuous line 353
  25. lemma OAI.DiagonalExtension.GraphFourier.character_continuous line 357
  26. lemma OAI.DiagonalExtension.GraphFourier.continuous_transform line 363
  27. lemma OAI.DiagonalExtension.GraphFourier.character_add line 376
  28. theorem OAI.DiagonalExtension.GraphFourier.square_density line 381
  29. lemma OAI.DiagonalExtension.GraphFourier.integrable_compact_L2 line 444
  30. lemma OAI.DiagonalExtension.GraphFourier.eLpNorm'_square line 449
  31. lemma OAI.DiagonalExtension.GraphFourier.eLpNorm_square line 461
  32. theorem OAI.DiagonalExtension.GraphFourier.memLp_four_and_bound line 470