OAI/Probability/SKSupport/Foundations/SumRangeBlocks.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ZeroTemperatureSK.WeakIto.sum_range_blocks line 16
2. lemma OAI.ZeroTemperatureSK.WeakIto.controlledGrid_formula line 25
3. lemma OAI.ZeroTemperatureSK.WeakIto.stepDrift_subdivision line 35
4. lemma OAI.ZeroTemperatureSK.WeakIto.stepCost_subdivision line 61
5. lemma OAI.ZeroTemperatureSK.WeakIto.refined_time line 75
6. lemma OAI.ZeroTemperatureSK.WeakIto.refined_coefficient line 81
7. lemma OAI.ZeroTemperatureSK.WeakIto.grid_drift_refinement line 85
8. lemma OAI.ZeroTemperatureSK.WeakIto.grid_cost_refinement line 108
9. lemma OAI.ZeroTemperatureSK.WeakIto.controlledGrid_refinement line 131
10. lemma OAI.ZeroTemperatureSK.WeakIto.refinement_successor line 150
11. lemma OAI.ZeroTemperatureSK.WeakIto.refined_cell_subset line 167
12. lemma OAI.ZeroTemperatureSK.WeakIto.verificationError_mono line 187