OAI/MeasureTheory/Falconer/Recursion/PolicyBranchCoefficients.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Dimension-dependent coefficient payments in the scalar branch ledger

  1. def OAI.Falconer.dimensionalBranchReserve line 12
  2. theorem OAI.Falconer.dimensionalBranchReserve_nonneg line 14
  3. theorem OAI.Falconer.graph_loss_le_branch_reserve line 19
  4. theorem OAI.Falconer.near_loss_le_branch_reserve line 27
  5. theorem OAI.Falconer.absorbed_power_coefficient line 33
  6. theorem OAI.Falconer.eventual_policy_graph_coefficient line 46
  7. theorem OAI.Falconer.eventual_policy_near_coefficient line 82