OAI/Probability/SKValue/GroundState/PredictableNormalizer.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKValue.independent_of_coordinate_not_in line 12
  2. lemma OAI.SKValue.measurable_coordinate line 39
  3. lemma OAI.SKValue.coordinate_eq_apply line 42
  4. lemma OAI.SKValue.euler_depends_on_past line 46
  5. lemma OAI.SKValue.measurable_euler line 56
  6. lemma OAI.SKValue.euler_coefficient_independent line 70
  7. lemma OAI.SKValue.gaussian_mean line 97
  8. lemma OAI.SKValue.gaussian_memLp line 101
  9. lemma OAI.SKValue.gaussian_second_moment line 108
  10. def OAI.SKValue.predictableNormalizer line 114
  11. def OAI.SKValue.normalizedIncrement line 117
  12. lemma OAI.SKValue.predictableNormalizer_pos line 120
  13. lemma OAI.SKValue.normalizedIncrement_mean line 125
  14. lemma OAI.SKValue.normalizedIncrement_second_moment line 135
  15. lemma OAI.SKValue.normalizedIncrement_memLp_two line 151
  16. lemma OAI.SKValue.normalizedIncrement_gaussian_coefficient line 162
  17. lemma OAI.SKValue.predictable_product_mean_zero line 176
  18. lemma OAI.SKValue.coordinate_hasLaw line 193
  19. def OAI.SKValue.DependsBefore line 198
  20. lemma OAI.SKValue.DependsBefore.independent line 201
  21. lemma OAI.SKValue.DependsBefore.mono line 212
  22. lemma OAI.SKValue.DependsBefore.prodMk line 216
  23. lemma OAI.SKValue.DependsBefore.mul line 223
  24. lemma OAI.SKValue.eulerCoefficient_dependsBefore line 230
  25. lemma OAI.SKValue.normalizedIncrement_dependsBefore line 241
  26. lemma OAI.SKValue.measurable_normalizedIncrement line 251
  27. lemma OAI.SKValue.normalizedIncrements_orthogonal line 256
  28. lemma OAI.SKValue.euler_normalized_increment_properties line 269