OAI/Analysis/PlanarEndpoint/DualMass.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Gaussian regularization, Fourier evolution and endpoint maximal estimates.

  1. lemma OAI.PlanarEndpoint.integrable_of_memLp_annular line 16
  2. lemma OAI.PlanarEndpoint.frequency_graph_integral_bound line 32
  3. lemma OAI.PlanarEndpoint.graphFourier_frequency_pairing line 62
  4. lemma OAI.PlanarEndpoint.norm_toLp_le_const_mul line 91
  5. lemma OAI.PlanarEndpoint.memLp_mul_conj_bounded line 110
  6. lemma OAI.PlanarEndpoint.graphLp_dual_test_identity line 120
  7. lemma OAI.PlanarEndpoint.graph_mass_bound_of_shortTime line 139