OAI/MeasureTheory/Falconer/Incidence/ParentQuarterIncidence.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Normal and good interval bounds in the fixed chart of the recursive endpoint construction. Retention is measured inside the active parent.

  1. theorem OAI.Falconer.blockClass_parent_quarter_normal_ratio line 31
  2. theorem OAI.Falconer.blockClass_parent_quarter_midscale_cover line 68
  3. theorem OAI.Falconer.blockClass_parent_quarter_good_gain line 100