OAI/Probability/SphericalField/Control/Truncation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.controlCost_clip_le line 17
2. lemma OAI.SphericalPerceptron.weightedTime_integrable line 21
3. lemma OAI.SphericalPerceptron.integral_pathControlCost line 40
4. lemma OAI.SphericalPerceptron.clipping_drift_gain line 46
5. lemma OAI.SphericalPerceptron.controlPayoff_le_clipControl line 80
6. lemma OAI.SphericalPerceptron.controlValue_le_of_bounded_controls line 110
7. lemma OAI.SphericalPerceptron.pathControlCost_le_bound line 121
8. lemma OAI.SphericalPerceptron.controlCost_le_bound line 134
9. lemma OAI.SphericalPerceptron.trial_abs_sub_integrable line 142
10. lemma OAI.SphericalPerceptron.bounded_drift_trial_diff line 150
11. lemma OAI.SphericalPerceptron.bounded_pathCost_trial_diff line 167
12. lemma OAI.SphericalPerceptron.controlPayoff_trial_diff_bound line 195