OAI/Probability/LatticePassage/ProductVariance.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CompanionFPP.square_integral_le_integral_square line 15
2. theorem OAI.CompanionFPP.integral_independent_square_difference line 22
3. lemma OAI.CompanionFPP.bounded_memLp_two line 37
4. lemma OAI.CompanionFPP.abs_integral_le_bound line 41
5. theorem OAI.CompanionFPP.product_variance_decomposition line 46
6. theorem OAI.CompanionFPP.variance_integral_le_integral_variance line 72
7. theorem OAI.CompanionFPP.product_variance_le line 112
8. lemma OAI.CompanionFPP.measurable_section_variance line 120
9. lemma OAI.CompanionFPP.variance_le_bound_square line 132
10. lemma OAI.CompanionFPP.integrable_section_variance line 140