OAI/MeasureTheory/Falconer/Angular/FarAngularStep.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The conditional angular far branch, with the actual near child

This is the analytic far step of the recursive argument. Its inputs are geometric scale data; only the cited gnomonic and quadratic stationary results are published hypotheses.

  1. def OAI.Falconer.JetStateFarData.energy line 19
  2. def OAI.Falconer.JetStateFarData.nearBound line 25
  3. theorem OAI.Falconer.exists_far_angular_step line 36