OAI/Probability/Perceptron/Control/ControlledPrefix.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.heatLog_control_step_error line 14
  2. lemma OAI.SphericalPerceptronFreeEnergy.usualBrownianSigma_mono line 84
  3. lemma OAI.SphericalPerceptronFreeEnergy.brownianEval_usual_measurable line 90
  4. lemma OAI.SphericalPerceptronFreeEnergy.progressive_prefix_integral_measurable line 99
  5. lemma OAI.SphericalPerceptronFreeEnergy.progressive_interval_integral_aemeasurable line 115
  6. def OAI.SphericalPerceptronFreeEnergy.controlledPrefix line 124
  7. lemma OAI.SphericalPerceptronFreeEnergy.controlledPrefix_usual_measurable line 127
  8. def OAI.SphericalPerceptronFreeEnergy.timeSpan line 132
  9. lemma OAI.SphericalPerceptronFreeEnergy.timeSpan_coe line 134
  10. lemma OAI.SphericalPerceptronFreeEnergy.timeSpan_le_one line 137
  11. lemma OAI.SphericalPerceptronFreeEnergy.timeLaw_real_Ioc line 141
  12. lemma OAI.SphericalPerceptronFreeEnergy.timeLaw_integral_const_Ioc line 146
  13. lemma OAI.SphericalPerceptronFreeEnergy.bounded_control_integrable line 151
  14. lemma OAI.SphericalPerceptronFreeEnergy.controlledPrefix_increment line 157
  15. lemma OAI.SphericalPerceptronFreeEnergy.bounded_interval_drift line 172
  16. def OAI.SphericalPerceptronFreeEnergy.intervalControlCost line 188
  17. lemma OAI.SphericalPerceptronFreeEnergy.intervalControlCost_nonneg line 191
  18. lemma OAI.SphericalPerceptronFreeEnergy.intervalControlCost_aemeasurable line 194
  19. lemma OAI.SphericalPerceptronFreeEnergy.intervalControlCost_le_bound line 199
  20. lemma OAI.SphericalPerceptronFreeEnergy.intervalControlCost_integrable line 213
  21. lemma OAI.SphericalPerceptronFreeEnergy.interval_square_completion line 222
  22. lemma OAI.SphericalPerceptronFreeEnergy.brownian_increment_timeSpan line 245
  23. lemma OAI.SphericalPerceptronFreeEnergy.brownian_control_cell_upper line 256
  24. lemma OAI.SphericalPerceptronFreeEnergy.antitoneOn_of_superlinear_increment line 300
  25. lemma OAI.SphericalPerceptronFreeEnergy.timeSpan_add line 334
  26. lemma OAI.SphericalPerceptronFreeEnergy.intervalControlCost_add line 340
  27. lemma OAI.SphericalPerceptronFreeEnergy.expected_intervalControlCost_add line 349
  28. lemma OAI.SphericalPerceptronFreeEnergy.brownian_control_interval_upper line 358
  29. def OAI.SphericalPerceptronFreeEnergy.patchControl line 387
  30. lemma OAI.SphericalPerceptronFreeEnergy.progressive_patchControl line 390
  31. lemma OAI.SphericalPerceptronFreeEnergy.patchControl_bound line 409