OAI/Geometry/Cannon/Beltrami/MultiplyLp.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonBeltrami.memLp_multiply line 25
  2. def OAI.CannonBeltrami.multiplyLp line 34
  3. lemma OAI.CannonBeltrami.multiplyLp_ae line 38
  4. lemma OAI.CannonBeltrami.multiplyLp_add line 43
  5. lemma OAI.CannonBeltrami.multiplyLp_smul line 53
  6. lemma OAI.CannonBeltrami.norm_multiplyLp_le line 63
  7. def OAI.CannonBeltrami.multiplier line 71
  8. lemma OAI.CannonBeltrami.multiplier_ae line 79
  9. lemma OAI.CannonBeltrami.norm_multiplier_le line 83
  10. lemma OAI.CannonBeltrami.norm_multiplier_eq line 87
  11. abbrev OAI.CannonBeltrami.PlaneL2 line 98
  12. def OAI.CannonBeltrami.beurlingSymbol line 100
  13. lemma OAI.CannonBeltrami.measurable_beurlingSymbol line 102
  14. lemma OAI.CannonBeltrami.norm_beurlingSymbol line 105
  15. def OAI.CannonBeltrami.symbolMultiplier line 110
  16. def OAI.CannonBeltrami.planeFourier line 114
  17. def OAI.CannonBeltrami.beurling line 116
  18. lemma OAI.CannonBeltrami.norm_symbolMultiplier line 120
  19. lemma OAI.CannonBeltrami.norm_beurling line 124
  20. lemma OAI.CannonBeltrami.fourier_beurling_ae line 128
  21. theorem OAI.CannonBeltrami.solve_beltrami_l2 line 135
  22. def OAI.CannonBeltrami.translateL2 line 171
  23. lemma OAI.CannonBeltrami.translateL2_ae line 174
  24. lemma OAI.CannonBeltrami.translate_schwartz line 178
  25. def OAI.CannonBeltrami.translationPhase line 188
  26. lemma OAI.CannonBeltrami.continuous_translationPhase line 190
  27. lemma OAI.CannonBeltrami.norm_translationPhase line 193
  28. def OAI.CannonBeltrami.phaseMultiplier line 195
  29. lemma OAI.CannonBeltrami.fourier_translate_schwartz line 199
  30. lemma OAI.CannonBeltrami.fourier_translateL2 line 219
  31. lemma OAI.CannonBeltrami.multipliers_commute line 228
  32. lemma OAI.CannonBeltrami.translate_beurling line 240
  33. def OAI.CannonBeltrami.directionSymbol line 248
  34. lemma OAI.CannonBeltrami.continuous_directionSymbol line 250
  35. lemma OAI.CannonBeltrami.translationPhase_derivative line 254
  36. lemma OAI.CannonBeltrami.translationPhase_slope line 261
  37. theorem OAI.CannonBeltrami.memLp_directionSymbol_of_translation_bound line 266
  38. lemma OAI.CannonBeltrami.dominated_toLp_zero_filter line 314
  39. lemma OAI.CannonBeltrami.phase_slope_norm_le line 344
  40. lemma OAI.CannonBeltrami.fourier_difference_quotient_ae line 365
  41. lemma OAI.CannonBeltrami.translateL2_zero line 379
  42. theorem OAI.CannonBeltrami.hasDerivAt_translateL2 line 383
  43. lemma OAI.CannonBeltrami.translate_toLp_ae line 423
  44. theorem OAI.CannonBeltrami.translation_bound_of_increment_bound line 428
  45. theorem OAI.CannonBeltrami.translation_derivative_eq_ae line 451
  46. theorem OAI.CannonBeltrami.memLp_fderiv_of_increment_bound line 481
  47. lemma OAI.CannonBeltrami.fourier_derivative_distribution line 500
  48. lemma OAI.CannonBeltrami.fourier_derivative_weak line 526
  49. theorem OAI.CannonBeltrami.weak_fderiv_of_increment_bound line 535