OAI/Probability/FreeIsing/Conditioning/SelectedPosteriorEvenConditioning.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.integral_cond_spin_eq_of_ae_flip line 15
2. theorem OAI.Problem367.identDistrib_cond_spin_of_ae_flip line 55
3. theorem OAI.Problem367.selectedPosterior_even_identDistrib_cond_spin line 79
4. theorem OAI.Problem367.artanh_neg_unrestricted line 111
5. theorem OAI.Problem367.measurable_artanh_evenConditioning line 129
6. theorem OAI.Problem367.selectedField_abs_identDistrib_cond_spin line 134
7. theorem OAI.Problem367.HasFreeIsingLaw.selected_gaussian_field_abs_identDistrib_cond_spin line 155