OAI/MeasureTheory/Falconer/Fourier/NormalizedInverseIntegration.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact normalized factorization of the integrated stationary inverse

The endpoint sizes are extracted before any energy estimate. All integrals remain under the original pair laws and the exact spatial Fourier kernel.

  1. theorem OAI.Falconer.normalizedEndpoint_bound_restored line 15
  2. theorem OAI.Falconer.scaled_inverse_normalized_integration line 24