OAI/MeasureTheory/Falconer/Recursion/ProfileIntervalChain.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite composition of actual profile interval estimates. Every splitting step uses the proved endpoint construction and its explicit next budget.

  1. def OAI.Falconer.profileBudgetSequence line 11
  2. theorem OAI.Falconer.profileBudgetSequence_one_le line 15
  3. theorem OAI.Falconer.profileBudgetSequence_monotone line 22
  4. theorem OAI.Falconer.profileEndpointBound_interval_chain line 29