OAI/MeasureTheory/Falconer/Estimates/ControlledEndpointGain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Endpoint angular gain from the two actual radial slice costs

This is the finite-scale assembly step. Its cost and scalar hypotheses are verified from the original direction law in the uniform endpoint application.

  1. theorem OAI.Falconer.controlled_endpoint_angular_gain line 20