OAI/MeasureTheory/Falconer/Recursion/BranchPotential.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFalconer.branchCost line 8
2. theorem OAI.PlanarFalconer.BranchStep.cost_nonneg line 13
3. theorem OAI.PlanarFalconer.BranchStep.paid_width line 25
4. theorem OAI.PlanarFalconer.BranchStep.potential_payment line 37
5. theorem OAI.PlanarFalconer.BranchStep.short_cost_zero line 53
6. def OAI.PlanarFalconer.DiscreteProfileLipschitz line 62
7. theorem OAI.PlanarFalconer.potential_le_final_start line 65
8. theorem OAI.PlanarFalconer.PolicyBranch.costs_le_potential line 84
9. theorem OAI.PlanarFalconer.PolicyBranch.costs_le_final_start line 98