OAI/Probability/FreeIsing/Conditioning/FiniteObservationInformation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.iIndep_observationFields_cond_spin line 13
2. theorem OAI.Problem367.condExp_finite_observation_secondMoment_le_sum line 46
3. theorem OAI.Problem367.condExp_finite_observation_secondMoment_le_sum_sub_loss line 59
4. theorem OAI.Problem367.condExp_own_and_finite_observation_secondMoment_le_sum_sub_loss line 81