OAI/MeasureTheory/Falconer/Recursion/TwoProfileEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Separating the two original regularized profiles

Cauchy--Schwarz uses the same radial shell measure on both sides and keeps exactly the common dimension-dependent normalization. Each resulting energy duplicates one original endpoint law, cell and symbol.

  1. theorem OAI.Falconer.independentAngularEnergy_sq_le_self line 16
  2. theorem OAI.Falconer.independentAngularEnergy_le_self_sqrt line 40
  3. theorem OAI.Falconer.angularEnvelope_two_profile line 51