OAI/Probability/Perceptron/Control/ControlDrift.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.abs_hamiltonian_update_sub_le line 14
  2. lemma OAI.SphericalPerceptronFreeEnergy.abs_pressure_update_sub_le line 33
  3. lemma OAI.SphericalPerceptronFreeEnergy.variance_pressure_le line 51
  4. lemma OAI.SphericalPerceptronFreeEnergy.variance_pressure_le_rate line 58
  5. lemma OAI.SphericalPerceptronFreeEnergy.pressure_deviation_le line 73
  6. theorem OAI.SphericalPerceptronFreeEnergy.pressure_concentrates line 98
  7. theorem OAI.SphericalPerceptronFreeEnergy.pressure_probability_of_expected_limit line 113
  8. lemma OAI.SphericalPerceptronFreeEnergy.brownianEval_measurable line 132
  9. lemma OAI.SphericalPerceptronFreeEnergy.usualBrownianSigma_le_completion line 135
  10. lemma OAI.SphericalPerceptronFreeEnergy.progressive_joint_complete line 150
  11. lemma OAI.SphericalPerceptronFreeEnergy.progressive_time_measurable line 161
  12. lemma OAI.SphericalPerceptronFreeEnergy.drift_sq_le_cost line 166
  13. def OAI.SphericalPerceptronFreeEnergy.controlDrift line 208
  14. def OAI.SphericalPerceptronFreeEnergy.pathControlCost line 211
  15. lemma OAI.SphericalPerceptronFreeEnergy.controlDrift_aemeasurable line 214
  16. lemma OAI.SphericalPerceptronFreeEnergy.pathControlCost_aemeasurable line 222
  17. lemma OAI.SphericalPerceptronFreeEnergy.controlDrift_sq_integrable line 230
  18. lemma OAI.SphericalPerceptronFreeEnergy.integral_controlDrift_sq_le line 242
  19. lemma OAI.SphericalPerceptronFreeEnergy.brownianEval_one_sq_integral line 256
  20. lemma OAI.SphericalPerceptronFreeEnergy.controlledTerminal_sq_integral_le line 263
  21. lemma OAI.SphericalPerceptronFreeEnergy.controlledTerminal_aemeasurable line 287
  22. lemma OAI.SphericalPerceptronFreeEnergy.controlReward_integrable line 292
  23. lemma OAI.SphericalPerceptronFreeEnergy.controlPayoff_compact_bound line 301
  24. lemma OAI.SphericalPerceptronFreeEnergy.controlValue_le_of_cost_cutoff line 352
  25. lemma OAI.SphericalPerceptronFreeEnergy.controlValue_compact_bound line 367
  26. lemma OAI.SphericalPerceptronFreeEnergy.controlValue_uniform_of_compact line 407