OAI/Probability/FreeIsing/Conditioning/CopyVariance.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.integral_sq_sub_copies_eq_two_variance line 14
2. theorem OAI.Problem367.integral_sq_sub_copies line 30
3. theorem OAI.Problem367.ae_eq_integral_of_copies_ae_eq line 36
4. theorem OAI.Problem367.ae_memLp_two_of_compProd line 52
5. theorem OAI.Problem367.exists_measurable_recovery_of_copies_ae_eq line 68
6. theorem OAI.Problem367.exists_measurable_recovery_of_memLp_copies_ae_eq line 83
7. theorem OAI.Problem367.exists_measurable_recovery_array_of_copies_ae_eq line 90