OAI/Analysis/PlanarEndpoint/GraphScaling.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Gaussian regularization, Fourier evolution and endpoint maximal estimates.

  1. def OAI.PlanarEndpoint.affineScale line 16
  2. def OAI.PlanarEndpoint.scaledTime line 18
  3. lemma OAI.PlanarEndpoint.measurable_affineScale line 21
  4. lemma OAI.PlanarEndpoint.measurable_scaledTime line 25
  5. lemma OAI.PlanarEndpoint.integral_affineScale line 29
  6. lemma OAI.PlanarEndpoint.setIntegral_affineScale line 37
  7. lemma OAI.PlanarEndpoint.volumeReal_affineScale line 48
  8. lemma OAI.PlanarEndpoint.phase_affineScale line 53
  9. lemma OAI.PlanarEndpoint.graphDual_affineScale line 69
  10. lemma OAI.PlanarEndpoint.graphLp_norm_sq_integral line 94
  11. lemma OAI.PlanarEndpoint.norm_graphDual_affineScale line 103
  12. lemma OAI.PlanarEndpoint.graphLp_norm_sq_affineScale line 112
  13. lemma OAI.PlanarEndpoint.affineScale_preimage_ball line 133
  14. lemma OAI.PlanarEndpoint.annular_support_rescale line 142
  15. lemma OAI.PlanarEndpoint.rpow_mass_sq_le line 160
  16. lemma OAI.PlanarEndpoint.graph_ball_bound_of_shortTime line 173