OAI/MeasureTheory/Falconer/Recursion/ProfileGoodBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The independently proved regular incidence gain supplies the good-interval base case, on every retained reference class allowed by the induction.

  1. theorem OAI.Falconer.profileEndpointBound_good line 11