OAI/MeasureTheory/FalconerCompletion/Fourier/LintegralBiUnionFinsetLe.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Fourier kernels and oscillatory estimates.

  1. theorem OAI.CriticalFourierSupport.CurrentFalconer.lintegral_biUnion_finset_le line 18
  2. theorem OAI.CriticalFourierSupport.CurrentFalconer.dyadic_scalar_cover line 28
  3. def OAI.CriticalFourierSupport.CurrentFalconer.angularFourierEnergy line 47
  4. theorem OAI.CriticalFourierSupport.CurrentFalconer.angularFourierEnergy_nonneg line 51
  5. theorem OAI.CriticalFourierSupport.CurrentFalconer.angularFourierEnergy_le_one line 54
  6. theorem OAI.CriticalFourierSupport.CurrentFalconer.angularFourierEnergy_continuous line 72