OAI/MeasureTheory/Falconer/Fourier/InverseClassIntegration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Original-pair integration of the exact inverse symbol family

The finite factors are the actual output symbols. The original endpoint measures, both normalizing masses, and every descriptor remain explicit.

  1. theorem OAI.Falconer.bounded_sphere_phase_integrable line 17

    Also declared: 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), OAI/MeasureTheory/Falconer/Recursion/TwoProfileInverseIntegrable.lean:12 (same declaration text).

  2. def OAI.Falconer.DescriptorInverseSymbols.coefficient line 44
  3. theorem OAI.Falconer.DescriptorInverseSymbols.coefficient_abs_le line 48
  4. theorem OAI.Falconer.DescriptorInverseSymbols.integration line 67