OAI/Probability/LatticePassage/MeanPositivity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CompanionFPP.passageTime_mean_lower_of_tail line 9
2. lemma OAI.CompanionFPP.small_tail_at_most_half line 30
3. theorem OAI.CompanionFPP.passageTime_mean_linear_lower line 44
4. lemma OAI.CompanionFPP.latticeDistance_scaleVertex line 53
5. theorem OAI.CompanionFPP.directionalMeanConstant_linear_lower line 57
6. theorem OAI.CompanionFPP.directionalMeanConstant_pos line 73