OAI/Probability/LatticePassage/FiniteVariance.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompanionFPP.measurable_finCons line 11
  2. lemma OAI.CompanionFPP.finCons_preserving line 20
  3. lemma OAI.CompanionFPP.integral_finCons line 28
  4. def OAI.CompanionFPP.coordinateVariance line 38
  5. lemma OAI.CompanionFPP.measurable_coordinateVariance line 42
  6. lemma OAI.CompanionFPP.coordinateVariance_bound line 49
  7. lemma OAI.CompanionFPP.integrable_coordinateVariance line 56
  8. lemma OAI.CompanionFPP.coordinateVariance_cons_zero line 64
  9. lemma OAI.CompanionFPP.coordinateVariance_cons_succ line 70
  10. lemma OAI.CompanionFPP.integral_coordinateVariance_zero line 76
  11. lemma OAI.CompanionFPP.integral_coordinateVariance_succ line 84
  12. theorem OAI.CompanionFPP.variance_fin_le_sum_coordinateVariance line 93
  13. lemma OAI.CompanionFPP.reindex_preserving line 140
  14. lemma OAI.CompanionFPP.coordinateVariance_reindex line 148
  15. theorem OAI.CompanionFPP.variance_pi_le_sum_coordinateVariance line 167