OAI/MeasureTheory/Falconer/Recursion/BranchLedger.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The scheduled branch ledger with the ambient dimension retained

The policy branches and their payment identities are scalar combinatorics. Their final-potential bound uses the dimension-dependent Lipschitz constant.

  1. theorem OAI.Falconer.dimension_profile_increment_le line 16
  2. theorem OAI.Falconer.dimension_branch_cost_le line 31
  3. theorem OAI.Falconer.dimension_ancestor_exponent_bound line 52
  4. theorem OAI.Falconer.dimension_branch_cost_bound line 73
  5. theorem OAI.Falconer.dimension_source_branch_exponent line 110