OAI/Probability/SKValue/Equations/CubicEnvelopeMean.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKValue.GradientStripCore.continuous_second line 28
2. lemma OAI.SKValue.GradientStripCore.continuous_deriv line 34
3. lemma OAI.SKValue.pathGradientResidual_aestronglyMeasurable line 39
4. def OAI.SKValue.cubicEnvelopeMean line 64
5. lemma OAI.SKValue.pathGradientResidual_L1_bound line 67
6. lemma OAI.SKValue.pathGradientResidual_L1_tendsto line 137
7. lemma OAI.SKValue.weighted_pathGradientResidual_tendsto line 174