OAI/Probability/SKRatio/Dynamics/PositiveLag.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatio.Calculus.dimensionDecay line 13
2. lemma OAI.SKRatio.Calculus.dimensionDecay_pos line 15
3. lemma OAI.SKRatio.Calculus.dimensionDecay_tendsto_zero line 18
4. lemma OAI.SKRatio.Calculus.log_pow_mul_dimensionDecay_tendsto_zero line 25
5. lemma OAI.SKRatio.Calculus.nat_mul_dimensionDecay line 31
6. def OAI.SKRatio.Calculus.logarithmicVarianceBound line 39
7. lemma OAI.SKRatio.Calculus.logarithmicVarianceBound_nonneg line 44
8. lemma OAI.SKRatio.Calculus.logarithmicVarianceBound_tendsto_zero line 51
9. def OAI.SKRatio.Calculus.logarithmicSmoothingBound line 64
10. lemma OAI.SKRatio.Calculus.logarithmicSmoothingBound_tendsto_zero line 68
11. lemma OAI.SKRatio.Calculus.logarithmic_smoothing_of_small_set_gradient line 76
12. theorem OAI.SKRatio.Calculus.uniform_positive_lag_of_small_set_gradient line 151