OAI/MeasureTheory/Falconer/Recursion/ScalarBunchingLedger.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A finite greedy ledger for porous bunches. Its intervals partition a terminal range, and every omitted tail has a controlled weight loss.

  1. structure OAI.Falconer.ScalarBunch line 9
  2. inductive OAI.Falconer.ScalarBunchChain line 16
  3. structure OAI.Falconer.ScalarBunchGood line 21
  4. theorem OAI.Falconer.scalar_minimal_heavy_suffix_of_exists line 27
  5. theorem OAI.Falconer.scalar_bunching_ledger line 46
  6. theorem OAI.Falconer.ScalarBunchChain.start_le line 88
  7. theorem OAI.Falconer.ScalarBunchChain.total_length line 94