OAI/MeasureTheory/Falconer/Fourier/TwoProfileInverseIntegration.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Two-profile original-pair integration of the exact inverse 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 18

    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/Recursion/TwoProfileInverseIntegrable.lean:12 (same declaration text).

  2. theorem OAI.Falconer.DescriptorInverseSymbols.two_profile_integration line 45