OAI/Probability/Perceptron/Variational/BackwardScore.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.patchControl_prefix line 14
  2. lemma OAI.SphericalPerceptronFreeEnergy.patchControl_cost_prefix line 24
  3. lemma OAI.SphericalPerceptronFreeEnergy.patchControl_drift_cell line 33
  4. lemma OAI.SphericalPerceptronFreeEnergy.patchControl_cost_cell line 44
  5. lemma OAI.SphericalPerceptronFreeEnergy.brownian_control_feedback_cell line 55
  6. def OAI.SphericalPerceptronFreeEnergy.backwardScore line 109
  7. lemma OAI.SphericalPerceptronFreeEnergy.brownian_control_patch_gain line 114
  8. def OAI.SphericalPerceptronFreeEnergy.timeMesh line 159
  9. lemma OAI.SphericalPerceptronFreeEnergy.timeMesh_coe line 162
  10. lemma OAI.SphericalPerceptronFreeEnergy.timeMesh_zero line 173
  11. lemma OAI.SphericalPerceptronFreeEnergy.timeMesh_last line 178
  12. lemma OAI.SphericalPerceptronFreeEnergy.timeMesh_between line 185
  13. lemma OAI.SphericalPerceptronFreeEnergy.timeMesh_step line 197
  14. lemma OAI.SphericalPerceptronFreeEnergy.timeMesh_step_size line 208
  15. lemma OAI.SphericalPerceptronFreeEnergy.brownian_control_interval_lower_mesh line 214
  16. lemma OAI.SphericalPerceptronFreeEnergy.brownian_control_interval_lower line 274
  17. inductive OAI.SphericalPerceptronFreeEnergy.HeatChain line 296
  18. lemma OAI.SphericalPerceptronFreeEnergy.HeatChain.left_le_right line 302
  19. lemma OAI.SphericalPerceptronFreeEnergy.controls_equal_prefix line 308
  20. lemma OAI.SphericalPerceptronFreeEnergy.controls_equal_cost_prefix line 318
  21. lemma OAI.SphericalPerceptronFreeEnergy.HeatChain.upper line 327
  22. lemma OAI.SphericalPerceptronFreeEnergy.HeatChain.lower line 343
  23. lemma OAI.SphericalPerceptronFreeEnergy.controlledPrefix_one line 375
  24. lemma OAI.SphericalPerceptronFreeEnergy.controlledPrefix_zero line 381
  25. lemma OAI.SphericalPerceptronFreeEnergy.intervalControlCost_full line 388
  26. lemma OAI.SphericalPerceptronFreeEnergy.expected_intervalControlCost_full line 398
  27. lemma OAI.SphericalPerceptronFreeEnergy.Jet3.lipschitz line 404
  28. lemma OAI.SphericalPerceptronFreeEnergy.HeatChain.controlValue_eq line 410