OAI/MeasureTheory/Falconer/Fourier/InverseJetIntegration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integrating the finite inverse in its exact descriptor class

  1. theorem OAI.Falconer.bounded_sphere_phase_integrable line 12

    Also declared: OAI/MeasureTheory/Falconer/Fourier/InverseClassIntegration.lean:17 (same declaration text), OAI/MeasureTheory/Falconer/Fourier/RotatedInverseIntegration.lean:13 (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.DescriptorInverseSymbols.original_term_integrable line 39
  3. theorem OAI.Falconer.scaled_inverse_jet_integrable line 112
  4. theorem OAI.Falconer.scaled_inverse_jet_integration line 145