OAI/MeasureTheory/FalconerCompletion/Graphs/SpherePlaneWaveSub.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. lemma OAI.CurrentFalconer.spherePlaneWaveND_sub line 17
  2. lemma OAI.CurrentFalconer.angular_pair_joint_integrableND line 25
  3. theorem OAI.CurrentFalconer.angular_pair_factorizationND line 49
  4. lemma OAI.CurrentFalconer.sourceAngularTransformND_measurable line 102
  5. lemma OAI.CurrentFalconer.sourceAngularTransformND_norm_le line 118
  6. lemma OAI.CurrentFalconer.angular_pair_joint_integrableND_ae line 132
  7. theorem OAI.CurrentFalconer.angular_pair_factorizationND_ae line 156
  8. def OAI.CurrentFalconer.graphPairMoment line 211
  9. def OAI.CurrentFalconer.graphPairAmplitude line 216
  10. lemma OAI.CurrentFalconer.graphPairAmplitude_measurable line 220
  11. lemma OAI.CurrentFalconer.graphAxis_measurable line 228
  12. lemma OAI.CurrentFalconer.graphPairMoment_factorization line 241
  13. lemma OAI.CurrentFalconer.graphPairMoment_measurable line 263
  14. lemma OAI.CurrentFalconer.graphPairAmplitude_bound line 276
  15. lemma OAI.CurrentFalconer.graphAxis_integrable line 286
  16. def OAI.CurrentFalconer.graphSpatialKernel line 297
  17. lemma OAI.CurrentFalconer.graphSpatial_integrable line 315
  18. theorem OAI.CurrentFalconer.graph_four_spatial_factorization line 347