OAI/Analysis/IrrationalRotation/Couplings/ConditionalL2Tail.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InvariantProjection.l2_tsum_ofReal_sq line 13
2. theorem OAI.InvariantProjection.lintegral_l2_sq_le_one line 19
3. theorem OAI.InvariantProjection.lintegral_l2_masked_tail_le_of_condExp line 31
4. theorem OAI.InvariantProjection.integral_l2_masked_tail_le_of_condExp line 64
5. theorem OAI.InvariantProjection.integral_l2_masked_tail_le_of_condExp_right line 104