OAI/Probability/FreeIsing/Conditioning/StrictPosteriorInformation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.strictInformationCoefficient line 14
2. theorem OAI.Problem367.strictInformationCoefficient_pos line 18
3. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsSpinMean_brownian_strict_secondMoment line 25
4. theorem OAI.Problem367.HasFreeIsingLaw.infiniteGibbsSpinMean_brownian_strict_secondMoment line 85
5. theorem OAI.Problem367.IsingConditionalCopyBounds.posteriorInformation_le_strict line 106
6. theorem OAI.Problem367.IsingConditionalCopyBounds.canonical_fieldDifference_secondMoment_le_strict line 136