OAI/MeasureTheory/Falconer/Recursion/TwoProfileInverseIntegrable.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Integrability of the two-profile original inverse family

  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/InverseJetIntegration.lean:12 (same declaration text), OAI/MeasureTheory/Falconer/Fourier/RotatedInverseIntegration.lean:13 (same declaration text), OAI/MeasureTheory/Falconer/Fourier/TwoProfileInverseIntegration.lean:18 (same declaration text).

  2. def OAI.Falconer.DescriptorInverseSymbols.twoProfilePairIntegral line 39
  3. theorem OAI.Falconer.DescriptorInverseSymbols.two_profile_original_term_integrable line 52
  4. theorem OAI.Falconer.two_profile_scaled_inverse_integrable line 125
  5. theorem OAI.Falconer.two_profile_scaled_inverse_integration line 158