OAI/Probability/SKValue/Control/Regularity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKValue.phi_even line 13
2. lemma OAI.SKValue.phi_gradient_zero line 19
3. theorem OAI.SKValue.sourceStripRegularity line 22
4. lemma OAI.SKValue.ValueStrip.drift_one_step line 54
5. def OAI.SKValue.crossFeedback line 88
6. lemma OAI.SKValue.crossFeedback_bound line 91
7. lemma OAI.SKValue.cross_generator_identity line 99
8. lemma OAI.SKValue.cross_value_one_step line 103