OAI/MeasureTheory/Falconer/Recursion/InitialProfileClass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The initial class inherits its lower profile from the actual leaf prefix counts. The label-selection loss is explicit and paid only once.

  1. theorem OAI.Falconer.block_profile_ratios_from_prefix line 11
  2. theorem OAI.Falconer.exists_initial_profile_class line 46