OAI/Analysis/PlanarEndpoint/GraphDual.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Gaussian regularization, Fourier evolution and endpoint maximal estimates.

  1. def OAI.PlanarEndpoint.graphFourier line 14
  2. def OAI.PlanarEndpoint.graphDual line 17
  3. lemma OAI.PlanarEndpoint.measurable_graph_phase line 20
  4. lemma OAI.PlanarEndpoint.integrable_graph_phase line 25
  5. lemma OAI.PlanarEndpoint.norm_graphFourier_le line 35
  6. lemma OAI.PlanarEndpoint.continuous_graphFourier line 45
  7. lemma OAI.PlanarEndpoint.graphDual_memLp line 61
  8. lemma OAI.PlanarEndpoint.phase_mul_conj line 74
  9. lemma OAI.PlanarEndpoint.phase_eq_kernel_oscillation line 82
  10. def OAI.PlanarEndpoint.frequencyKernel line 86
  11. lemma OAI.PlanarEndpoint.integrable_graph_pairing line 89
  12. lemma OAI.PlanarEndpoint.graphDual_pairing line 106
  13. lemma OAI.PlanarEndpoint.norm_graphDual_pairing_le line 136
  14. lemma OAI.PlanarEndpoint.frequencyKernel_scaled line 157
  15. lemma OAI.PlanarEndpoint.frequencyKernel_time_decay line 165
  16. lemma OAI.PlanarEndpoint.frequencyKernel_spatial_decay line 176
  17. def OAI.PlanarEndpoint.graphLp line 187
  18. lemma OAI.PlanarEndpoint.graphLp_ae line 193
  19. lemma OAI.PlanarEndpoint.inner_graphLp line 200
  20. lemma OAI.PlanarEndpoint.graphLp_add_measure line 211
  21. lemma OAI.PlanarEndpoint.graphLp_zero_measure line 226
  22. lemma OAI.PlanarEndpoint.graphLp_finsetSum_measure line 233