OAI/Analysis/PlanarEndpoint/SpatialOrthogonal.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Gaussian regularization, Fourier evolution and endpoint maximal estimates.

  1. def OAI.PlanarEndpoint.spatialDecay line 15
  2. lemma OAI.PlanarEndpoint.spatialDecay_nonneg line 17
  3. lemma OAI.PlanarEndpoint.spatialDecay_le line 21
  4. lemma OAI.PlanarEndpoint.spatialDecay_one_integrable line 27
  5. lemma OAI.PlanarEndpoint.spatialDecay_scale line 34
  6. lemma OAI.PlanarEndpoint.spatialDecay_integrable line 38
  7. lemma OAI.PlanarEndpoint.integral_spatialDecay line 43
  8. lemma OAI.PlanarEndpoint.integrable_spatialDecay_prod line 50
  9. lemma OAI.PlanarEndpoint.spatialDecay_schur line 66
  10. lemma OAI.PlanarEndpoint.norm_graphDual_pairing_le_integral line 77
  11. lemma OAI.PlanarEndpoint.finite_sum_prod_integral line 93
  12. lemma OAI.PlanarEndpoint.graphPartition_near_far line 106