OAI/Probability/SKSupport/Regularity/TimeFields.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ZeroTemperatureSK.TimeField line 13
2. def OAI.ZeroTemperatureSK.TimeField.add line 26
3. def OAI.ZeroTemperatureSK.TimeField.const_mul line 35
4. def OAI.ZeroTemperatureSK.TimeField.mul line 44
5. lemma OAI.ZeroTemperatureSK.TimeField.integral_rate line 55
6. def OAI.ZeroTemperatureSK.TimeField.generator line 63
7. lemma OAI.ZeroTemperatureSK.TimeField.generator_add line 66
8. lemma OAI.ZeroTemperatureSK.TimeField.generator_const_mul line 80
9. lemma OAI.ZeroTemperatureSK.TimeField.generator_mul line 90
10. def OAI.ZeroTemperatureSK.TimeField.expected line 107
11. lemma OAI.ZeroTemperatureSK.TimeField.expected_continuous line 110
12. lemma OAI.ZeroTemperatureSK.TimeField.expected_hasDerivWithinAt_right line 125