OAI/Probability/SKValue/Equations/RawIncrement.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKValue.rawIncrement line 28
  2. lemma OAI.SKValue.rawIncrement_memLp line 31
  3. lemma OAI.SKValue.rawIncrement_mean line 43
  4. lemma OAI.SKValue.rawIncrement_variance line 52
  5. lemma OAI.SKValue.rawIncrement_depends line 64
  6. lemma OAI.SKValue.rawIncrement_past_product line 71
  7. lemma OAI.SKValue.rawIncrement_pair line 81
  8. lemma OAI.SKValue.finiteRaw_memLp line 96
  9. lemma OAI.SKValue.finiteRaw_isometry line 110
  10. lemma OAI.SKValue.coupled_mesh_general_moment_bounds line 134
  11. lemma OAI.SKValue.integral_product_CS line 186
  12. lemma OAI.SKValue.rawIncrement_coordinate_pair line 196
  13. lemma OAI.SKValue.finiteRaw_coordinate_coefficient line 224
  14. lemma OAI.SKValue.finiteRaw_brownian_covariance line 247
  15. lemma OAI.SKValue.second_moment_L2_perturbation line 265
  16. lemma OAI.SKValue.perturbed_grid_riemann_tendsto line 292
  17. lemma OAI.SKValue.derivative_joint_continuous line 320
  18. lemma OAI.SKValue.mean_derivative_square_continuous line 334
  19. lemma OAI.SKValue.mesh_terminal_memLp line 357
  20. lemma OAI.SKValue.bounded_second_moment line 363
  21. lemma OAI.SKValue.mesh_raw_stochastic_square_bound line 373
  22. lemma OAI.SKValue.mesh_terminal_stochastic_second_moment_error line 394