OAI/Probability/FreeIsing/Conditioning/FactorRecovery.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Problem367.exists_ae_equivariant_recovery_of_conditionalCopiesline 14 - theorem
OAI.Problem367.isFactorOfIID_of_invariant_conditionalCopiesline 35 - theorem
OAI.Problem367.isFactorOfIID_of_invariant_product_conditionalCopiesline 58