OAI/Probability/SKValue/Gaussian/ShiftedBrownianCoordinates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKValue.shiftedBrownianCoordinates line 29
2. lemma OAI.SKValue.shiftedBrownianCoordinates_hasLaw line 33
3. lemma OAI.SKValue.meshTime_toNNReal line 41
4. lemma OAI.SKValue.shiftedBrownianCoordinates_exact line 49
5. lemma OAI.SKValue.GradientStripCore.deriv_bound line 67
6. lemma OAI.SKValue.weighted_pathGradientResidual_integral line 78