OAI/Probability/FreeIsing/Conditioning/Copies.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.measurePreserving_conditionalCopy_fst line 15
2. theorem OAI.Problem367.measurePreserving_conditionalCopy_snd line 21
3. theorem OAI.Problem367.memLp_conditionalCopy_fst line 29
4. theorem OAI.Problem367.memLp_conditionalCopy_snd line 35
5. theorem OAI.Problem367.ae_memLp_conditionalCopies_fiber line 41
6. theorem OAI.Problem367.integral_sq_sub_conditionalCopies line 50
7. theorem OAI.Problem367.integrable_variance_kernel line 67
8. theorem OAI.Problem367.conditionalCopies_ae_eq_of_integral_variance_eq_zero line 84
9. theorem OAI.Problem367.condExp_sq_sub_conditionalCopies line 102
10. theorem OAI.Problem367.condExp_sub_conditionalCopies line 115