OAI/Probability/LatticePassage/LocalizationMean.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CompanionFPP.integrable_trail_exp line 8
2. lemma OAI.CompanionFPP.integral_trail_exp line 15
3. lemma OAI.CompanionFPP.integrable_trail_cost line 21
4. lemma OAI.CompanionFPP.localPassageTime_le_pathCost line 29
5. lemma OAI.CompanionFPP.passageTime_le_localPassageTime line 34
6. theorem OAI.CompanionFPP.integrable_localPassageTime line 41
7. lemma OAI.CompanionFPP.rare_cost_pointwise line 52
8. theorem OAI.CompanionFPP.rare_cost_integral line 68
9. theorem OAI.CompanionFPP.localPassageTime_mean_error line 83
10. theorem OAI.CompanionFPP.localPassageTime_mean_error_exponential line 120