OAI/Probability/SKValue/Variation/OrderVariations.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKValue.OrderParameter.mix line 12
2. lemma OAI.SKValue.OrderParameter.mix_coeff_sub line 23
3. lemma OAI.SKValue.OrderParameter.mix_cutoff_sub line 26
4. lemma OAI.SKValue.OrderParameter.mix_difference_integral line 33
5. lemma OAI.SKValue.OrderParameter.mix_strip_difference_bound line 40
6. lemma OAI.SKValue.OrderParameter.weighted_intervalIntegrable line 50
7. lemma OAI.SKValue.IsMinimizer.mix_value_inequality line 54
8. def OAI.SKValue.gradientMoment line 80
9. lemma OAI.SKValue.gradientMoment_nonneg line 83
10. lemma OAI.SKValue.gradientMoment_bound line 87
11. lemma OAI.SKValue.IsDiffusion.gradientMoment_continuous line 97
12. lemma OAI.SKValue.IsDiffusion.weightedMoment_integrable line 111
13. lemma OAI.SKValue.IsDiffusion.weightedMean_integrable line 121
14. lemma OAI.SKValue.IsDiffusion.mix_moment_integral line 127