OAI/MeasureTheory/Falconer/Angular/CapCrossIntegral.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The original cap cross term as one product-measure integral

This is the bridge between the radial/angular nonstationary estimates and the finite graph expansion. Its integrability follows from bounded endpoint symbols and the finite radial shell law.

  1. theorem OAI.Falconer.weighted_endpoint_cross_integrable line 17
  2. theorem OAI.Falconer.endpointCapCrossTerm_integrable line 58
  3. theorem OAI.Falconer.endpointCapCrossTerm_product_integral line 90