OAI/MeasureTheory/Falconer/Fourier/RotatedInverseIntegration.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Integration of the rotated finite inverse on the original pair laws

  1. theorem OAI.Falconer.bounded_sphere_phase_integrable line 13

    Also declared: OAI/MeasureTheory/Falconer/Fourier/InverseClassIntegration.lean:17 (same declaration text), OAI/MeasureTheory/Falconer/Fourier/InverseJetIntegration.lean:12 (same declaration text), OAI/MeasureTheory/Falconer/Fourier/TwoProfileInverseIntegration.lean:18 (same declaration text), OAI/MeasureTheory/Falconer/Recursion/TwoProfileInverseIntegrable.lean:12 (same declaration text).

  2. theorem OAI.Falconer.RotatedRootSymbols.integration line 39
  3. theorem OAI.Falconer.RotatedRootSymbols.original_term_integrable line 130
  4. theorem OAI.Falconer.rotated_inverse_jet_integrable line 198
  5. theorem OAI.Falconer.rotated_inverse_jet_integration line 226