OAI/Analysis/ProductSpaces/RandomSigns.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentProducts.euclidSize line 15

    Source documentation

    The ordinary Euclidean size of a finite real coefficient list.

    def euclidSize {ι : Type uι} [Fintype ι] (a : ι → ℝ) : ℝ := Real.sqrt (∑ i, a i ^ 2)
  2. lemma OAI.IndependentProducts.euclidSize_nonneg line 17
  3. lemma OAI.IndependentProducts.euclidSize_sq line 19
  4. lemma OAI.IndependentProducts.euclidSize_le_sum_abs line 22
  5. lemma OAI.IndependentProducts.integrable_euclidSize line 29
  6. lemma OAI.IndependentProducts.integral_abs_le_sqrt_sq line 39
  7. def OAI.IndependentProducts.signLaw line 49
  8. instance OAI.IndependentProducts.signLaw_probability line 50
  9. def OAI.IndependentProducts.randomSign line 52
  10. lemma OAI.IndependentProducts.measurable_randomSign line 54
  11. lemma OAI.IndependentProducts.randomSign_sq line 56
  12. lemma OAI.IndependentProducts.randomSign_abs line 57
  13. lemma OAI.IndependentProducts.randomSign_memLp line 59
  14. lemma OAI.IndependentProducts.integral_signLaw line 63
  15. lemma OAI.IndependentProducts.integral_randomSign line 68
  16. lemma OAI.IndependentProducts.variance_randomSign line 71
  17. def OAI.IndependentProducts.signVector line 78
  18. instance OAI.IndependentProducts.(instance at line 79) line 79
  19. lemma OAI.IndependentProducts.sign_vector_memLp line 81
  20. lemma OAI.IndependentProducts.sign_vector_mean line 88
  21. lemma OAI.IndependentProducts.sign_vector_second_moment line 100
  22. lemma OAI.IndependentProducts.sign_vector_abs_le line 109
  23. def OAI.IndependentProducts.selectivelySwap line 121
  24. lemma OAI.IndependentProducts.measurePreserving_selectivelySwap line 124
  25. lemma OAI.IndependentProducts.selectivelySwap_difference line 141
  26. lemma OAI.IndependentProducts.sign_vector_difference_abs_le line 148
  27. lemma OAI.IndependentProducts.integrable_signed_sum line 166
  28. lemma OAI.IndependentProducts.independent_difference_abs_le line 181
  29. lemma OAI.IndependentProducts.independent_centered_sum_abs_le line 219