OAI/Probability/SKRatio/Variational/UniformDrift.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatio.Calculus.replace_difference_le line 14
2. lemma OAI.SKRatio.Calculus.oscillation_le_of_halfDiff line 30
3. lemma OAI.SKRatio.Calculus.halfDiff_le_sqrt_gradient line 49
4. lemma OAI.SKRatio.Calculus.mean_difference_le_of_oscillation line 56
5. theorem OAI.SKRatio.Calculus.distance_upper_of_uniform_gradient_drift line 72
6. theorem OAI.SKRatio.Calculus.uniform_median_upper_of_uniform_gradient line 92
7. theorem OAI.SKRatio.Calculus.ratio_cutoff_of_uniform_gradient line 120