OAI/Probability/FreeIsing/Ising/CopyInformationBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.abs_artanh_le_two_mul_of_abs_le_half line 13
2. theorem OAI.Problem367.artanh_sub_sq_le_information line 32
3. def OAI.Problem367.IsingConditionalCopyBounds.posteriorInformation line 61
4. theorem OAI.Problem367.IsingConditionalCopyBounds.posteriorInformation_eq_gaussian line 65
5. theorem OAI.Problem367.IsingConditionalCopyBounds.fieldDifference_secondMoment_le_information line 87
6. theorem OAI.Problem367.IsingConditionalCopyBounds.fieldDifference_secondMoment_le_horizon_information line 137