OAI/Probability/SKValue/Gaussian/ProfileSplit.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKValue.profileTime_append line 12
2. lemma OAI.SKValue.profileValue_append_zero line 16
3. lemma OAI.SKValue.profileValue_append_before line 21
4. lemma OAI.SKValue.profileCoeff_append_before line 38
5. lemma OAI.SKValue.BackwardShape.diffusion_prefix_coercivity line 53
6. lemma OAI.SKValue.profileCoeff_append_after line 109
7. def OAI.SKValue.splitLength line 124
8. def OAI.SKValue.OrderParameter.splitSegment line 126
9. lemma OAI.SKValue.splitLength_mul line 130
10. lemma OAI.SKValue.OrderParameter.splitSegment_time line 135
11. lemma OAI.SKValue.split_sample_mem line 138
12. lemma OAI.SKValue.OrderParameter.splitSegment_mono line 145
13. lemma OAI.SKValue.OrderParameter.splitSegment_sample line 155
14. def OAI.SKValue.OrderParameter.splitGrid line 173
15. lemma OAI.SKValue.OrderParameter.splitGrid_time line 175
16. lemma OAI.SKValue.OrderParameter.splitGrid_mono line 179
17. lemma OAI.SKValue.OrderParameter.splitGrid_sample line 197