OAI/Probability/SphericalField/Control/Filtration.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptron.brownianEval_measurable line 16
  2. lemma OAI.SphericalPerceptron.usualBrownianSigma_le_completion line 19
  3. lemma OAI.SphericalPerceptron.progressive_joint_complete line 34
  4. lemma OAI.SphericalPerceptron.progressive_time_measurable line 45
  5. lemma OAI.SphericalPerceptron.drift_sq_le_cost line 50
  6. def OAI.SphericalPerceptron.controlDrift line 92
  7. def OAI.SphericalPerceptron.pathControlCost line 95
  8. lemma OAI.SphericalPerceptron.controlDrift_aemeasurable line 98
  9. lemma OAI.SphericalPerceptron.pathControlCost_aemeasurable line 106
  10. lemma OAI.SphericalPerceptron.controlDrift_sq_integrable line 114
  11. lemma OAI.SphericalPerceptron.integral_controlDrift_sq_le line 126
  12. lemma OAI.SphericalPerceptron.brownianEval_one_sq_integral line 140
  13. lemma OAI.SphericalPerceptron.controlledTerminal_sq_integral_le line 147
  14. lemma OAI.SphericalPerceptron.controlledTerminal_aemeasurable line 171
  15. lemma OAI.SphericalPerceptron.controlReward_integrable line 176