OAI/MeasureTheory/Falconer/Angular/SharedAngular.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Shared-angle energy and the independent-angle bound

The shell conversion uses one shared angular variable. Cauchy--Schwarz transfers it to the positive independent-angle energy with exactly the same endpoint symbols and radial measure.

  1. theorem OAI.Falconer.real_integral_product_sq_le line 17
  2. theorem OAI.Falconer.sphere_shared_integral_sq_le line 38
  3. def OAI.Falconer.sharedAngularEnergy line 62
  4. theorem OAI.Falconer.independentAngularIntegrand_integrable line 68
  5. theorem OAI.Falconer.sharedAngularEnergy_le_independent line 85