OAI/Probability/SKRatio/Dynamics/ClockLower.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatio.Calculus.poissonMass_nonneg line 13
2. lemma OAI.SKRatio.Calculus.poissonMass_exp_hasSum line 16
3. lemma OAI.SKRatio.Calculus.poisson_head_le line 29
4. lemma OAI.SKRatio.Calculus.exists_poisson_head_exponent line 54
5. lemma OAI.SKRatio.Calculus.continuousKernel_poisson_integral line 78
6. lemma OAI.SKRatio.Calculus.integrable_discreteKernel_poisson line 88
7. lemma OAI.SKRatio.Calculus.totalVariation_integral_le line 98
8. lemma OAI.SKRatio.Calculus.integrable_totalVariation_poisson line 114
9. lemma OAI.SKRatio.Calculus.poisson_head_integral line 124
10. lemma OAI.SKRatio.Calculus.continuous_le_poisson_head_add_discrete line 137
11. lemma OAI.SKRatio.Calculus.uniform_lower_clock_error line 175
12. theorem OAI.SKRatio.Calculus.uniform_discrete_lower_from_continuous line 218