OAI/Probability/LatticePassage/ExponentialIncrement.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CompanionFPP.exponential_weighted_density line 10
2. theorem OAI.CompanionFPP.exponential_lmoment line 26
3. lemma OAI.CompanionFPP.integrable_exponential line 35
4. theorem OAI.CompanionFPP.integral_exponential line 42
5. lemma OAI.CompanionFPP.exponential_increment_square line 48
6. lemma OAI.CompanionFPP.integrable_exponential_increment_square line 53
7. theorem OAI.CompanionFPP.integral_exponential_increment_square line 59
8. theorem OAI.CompanionFPP.exponential_half_increment_square_le line 72