OAI/Probability/SKValue/Gaussian/GaussianSquareVariance.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKValue.gaussian_square_memLp_two line 17
  2. lemma OAI.SKValue.gaussian_centered_square_memLp_two line 26
  3. lemma OAI.SKValue.gaussian_centered_square_mean line 31
  4. def OAI.SKValue.gaussianSquareVariance line 38
  5. lemma OAI.SKValue.gaussianSquareVariance_nonneg line 41
  6. lemma OAI.SKValue.gaussian_centered_square_variance line 44
  7. lemma OAI.SKValue.predictableCenteredSquare_memLp line 49
  8. lemma OAI.SKValue.predictableCenteredSquare_variance line 58
  9. lemma OAI.SKValue.centeredSquare_dependsBefore line 78
  10. lemma OAI.SKValue.predictableCenteredSquares_orthogonal line 89
  11. lemma OAI.SKValue.orthogonal_sum_square line 106
  12. lemma OAI.SKValue.predictableCenteredSquare_sum_bound line 129
  13. def OAI.SKValue.cubicEnvelope line 156
  14. lemma OAI.SKValue.cubicEnvelope_nonneg line 159
  15. lemma OAI.SKValue.measurable_cubicEnvelope line 162
  16. lemma OAI.SKValue.abs_add_cube_memLp line 166
  17. lemma OAI.SKValue.cubicEnvelope_memLp_two line 177
  18. def OAI.SKValue.cubicEnvelopeMoment line 189
  19. lemma OAI.SKValue.cubicEnvelopeMoment_nonneg line 192
  20. lemma OAI.SKValue.cubicEnvelope_moment_eq line 195
  21. lemma OAI.SKValue.finite_sum_square_le line 200
  22. lemma OAI.SKValue.finite_envelope_L2_bound line 205