OAI/Analysis/PlanarEndpoint/Oscillation.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Gaussian regularization, Fourier evolution and endpoint maximal estimates.

  1. abbrev OAI.EndpointKernel.Space line 13
  2. def OAI.EndpointKernel.oscillation line 15
  3. lemma OAI.EndpointKernel.norm_oscillation line 18
  4. lemma OAI.EndpointKernel.contDiff_oscillation line 21
  5. lemma OAI.EndpointKernel.fderiv_oscillation line 25
  6. lemma OAI.EndpointKernel.contDiff_mul_of_tsupport line 38
  7. def OAI.EndpointKernel.weightedDiv line 51
  8. lemma OAI.EndpointKernel.contDiff_weightedDiv line 55
  9. lemma OAI.EndpointKernel.tsupport_weightedDiv_subset line 62
  10. lemma OAI.EndpointKernel.compactSupport_weightedDiv line 76
  11. lemma OAI.EndpointKernel.integration_by_parts line 80
  12. def OAI.EndpointKernel.iteratedAmplitude line 136
  13. lemma OAI.EndpointKernel.iteratedAmplitude_zero line 139
  14. lemma OAI.EndpointKernel.iteratedAmplitude_succ line 142
  15. lemma OAI.EndpointKernel.tsupport_iteratedAmplitude_subset line 146
  16. lemma OAI.EndpointKernel.contDiff_iteratedAmplitude line 154
  17. lemma OAI.EndpointKernel.compactSupport_iteratedAmplitude line 163
  18. lemma OAI.EndpointKernel.iterated_integration_by_parts line 168
  19. lemma OAI.EndpointKernel.nonstationary_phase_bound line 193
  20. lemma OAI.EndpointKernel.contDiffAt_partial_fderiv line 211
  21. lemma OAI.EndpointKernel.contDiffAt_iteratedAmplitude_family line 219
  22. lemma OAI.EndpointKernel.iteratedAmplitude_uniform_integral_bound line 245
  23. lemma OAI.EndpointKernel.uniform_nonstationary_phase line 281
  24. def OAI.EndpointKernel.quadraticPhase line 300
  25. def OAI.EndpointKernel.quadraticGradient line 303
  26. lemma OAI.EndpointKernel.contDiff_quadraticPhase line 306
  27. lemma OAI.EndpointKernel.fderiv_quadraticPhase line 309
  28. lemma OAI.EndpointKernel.fderiv_quadraticPhase_single line 319
  29. def OAI.EndpointKernel.quadraticNormalizer line 324
  30. lemma OAI.EndpointKernel.contDiffAt_quadraticNormalizer line 327
  31. lemma OAI.EndpointKernel.quadraticNormalizer_cancels line 338
  32. lemma OAI.EndpointKernel.uniform_quadratic_nonstationary line 349
  33. lemma OAI.EndpointKernel.time_dominated_decay line 359
  34. lemma OAI.EndpointKernel.spatial_dominated_decay_power line 407
  35. lemma OAI.EndpointKernel.one_add_weight_bound line 461
  36. lemma OAI.EndpointKernel.spatial_dominated_decay line 476
  37. def OAI.EndpointKernel.scaledKernel line 491
  38. lemma OAI.EndpointKernel.scaledKernel_eq line 494
  39. lemma OAI.EndpointKernel.scaledKernel_time_decay line 513
  40. lemma OAI.EndpointKernel.scaledKernel_spatial_decay line 530