OAI/Probability/Perceptron/Pressure/TerminalVariational.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.terminalVariational line 14
  2. lemma OAI.SphericalPerceptronFreeEnergy.variationalValue_eq_terminal line 17
  3. lemma OAI.SphericalPerceptronFreeEnergy.terminalVariational_bounds line 20
  4. lemma OAI.SphericalPerceptronFreeEnergy.terminalVariational_coe_toReal line 38
  5. lemma OAI.SphericalPerceptronFreeEnergy.terminalVariational_toReal_sub_le line 45
  6. lemma OAI.SphericalPerceptronFreeEnergy.terminalVariational_abs_sub_le line 68
  7. lemma OAI.SphericalPerceptronFreeEnergy.indep_eventuallyMeasurable_left line 78
  8. lemma OAI.SphericalPerceptronFreeEnergy.nullSigma_le_eventuallyMeasurable line 86
  9. def OAI.SphericalPerceptronFreeEnergy.rawBrownianSigma line 93
  10. lemma OAI.SphericalPerceptronFreeEnergy.rawBrownianSigma_le line 97
  11. lemma OAI.SphericalPerceptronFreeEnergy.rawBrownianSigma_le_past_comap line 102
  12. lemma OAI.SphericalPerceptronFreeEnergy.usualBrownianSigma_le_ae_raw line 110
  13. lemma OAI.SphericalPerceptronFreeEnergy.brownian_future_indep_raw line 116
  14. lemma OAI.SphericalPerceptronFreeEnergy.brownian_future_indep_usual_earlier line 124
  15. lemma OAI.SphericalPerceptronFreeEnergy.indep_setIntegral_eq_mul_null line 133
  16. lemma OAI.SphericalPerceptronFreeEnergy.indep_comap_of_ae_tendsto line 153
  17. lemma OAI.SphericalPerceptronFreeEnergy.brownian_increment_indep_usual line 178
  18. def OAI.SphericalPerceptronFreeEnergy.clipControl line 197
  19. lemma OAI.SphericalPerceptronFreeEnergy.progressive_clipControl line 200
  20. lemma OAI.SphericalPerceptronFreeEnergy.abs_clip_le line 205
  21. lemma OAI.SphericalPerceptronFreeEnergy.clip_cost_gain line 209
  22. lemma OAI.SphericalPerceptronFreeEnergy.clip_sq_le line 222
  23. lemma OAI.SphericalPerceptronFreeEnergy.pathControlCost_clip_le line 227
  24. lemma OAI.SphericalPerceptronFreeEnergy.controlCost_clip_le line 234
  25. lemma OAI.SphericalPerceptronFreeEnergy.weightedTime_integrable line 238
  26. lemma OAI.SphericalPerceptronFreeEnergy.integral_pathControlCost line 257
  27. lemma OAI.SphericalPerceptronFreeEnergy.clipping_drift_gain line 263
  28. lemma OAI.SphericalPerceptronFreeEnergy.controlPayoff_le_clipControl line 297
  29. lemma OAI.SphericalPerceptronFreeEnergy.controlValue_le_of_bounded_controls line 327
  30. lemma OAI.SphericalPerceptronFreeEnergy.pathControlCost_le_bound line 338
  31. lemma OAI.SphericalPerceptronFreeEnergy.controlCost_le_bound line 351
  32. lemma OAI.SphericalPerceptronFreeEnergy.trial_abs_sub_integrable line 359
  33. lemma OAI.SphericalPerceptronFreeEnergy.bounded_drift_trial_diff line 367
  34. lemma OAI.SphericalPerceptronFreeEnergy.bounded_pathCost_trial_diff line 384
  35. lemma OAI.SphericalPerceptronFreeEnergy.controlPayoff_trial_diff_bound line 412