OAI/Probability/SKValue/Equations/FiniteRounded.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKValue.finiteRounded line 20
  2. def OAI.SKValue.finiteRawMartingale line 24
  3. lemma OAI.SKValue.finiteRawMartingale_eq_normalized line 28
  4. lemma OAI.SKValue.finiteRawMartingale_memLp line 41
  5. lemma OAI.SKValue.finiteRawMartingale_normalized_coefficient line 51
  6. lemma OAI.SKValue.finiteRawMartingale_coordinate_coefficient line 65
  7. lemma OAI.SKValue.finite_coefficient_L2_errors line 82
  8. lemma OAI.SKValue.finiteRounded_measurable line 125
  9. lemma OAI.SKValue.finiteRounded_memLp line 131
  10. lemma OAI.SKValue.finiteRounded_square_le_one line 139
  11. lemma OAI.SKValue.finiteRounded_coordinate_norms line 150
  12. lemma OAI.SKValue.sqrt_div_normalizer_sq line 165
  13. lemma OAI.SKValue.sqrt_div_normalizer_bound line 171