OAI/Probability/FreeIsing/Posterior/SelectedPosteriorSymmetry.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.selectedPosterior_abs_le_one line 13
2. theorem OAI.Problem367.integrable_selectedPosterior_abs_pow line 23
3. def OAI.Problem367.plantedMarkFlipEquiv line 36
4. theorem OAI.Problem367.measurePreserving_plantedMarkFlip line 47
5. theorem OAI.Problem367.measurable_plantedMarkFlip_selectedObservationField line 67
6. theorem OAI.Problem367.selectedPosterior_flip_ae line 85
7. theorem OAI.Problem367.selectedPosteriorLaw_neg_invariant line 119
8. theorem OAI.Problem367.HasFreeIsingLaw.selected_gaussian_posteriorLaw_neg_invariant line 137