OAI/Probability/FreeIsing/Ising/CanonicalArtanh.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem367.IsingObservationFactor.canonicalCovarianceEnergy_uniformObservation_real line 11
2. theorem OAI.Problem367.IsingObservationFactor.canonicalCovarianceEnergy_integrable line 26
3. theorem OAI.Problem367.IsingObservationFactor.canonical_posterior_initial_zero line 61
4. theorem OAI.Problem367.IsingObservationFactor.continuousPosterior_initial_zero line 73
5. def OAI.Problem367.IsingObservationFactor.canonicalResponseDrift line 81
6. lemma OAI.Problem367.IsingObservationFactor.canonicalResponseDrift_progressive line 85
7. def OAI.Problem367.IsingObservationFactor.canonicalPosteriorExit line 90
8. theorem OAI.Problem367.IsingObservationFactor.canonicalPosteriorExit_localizing line 94
9. theorem OAI.Problem367.IsingObservationFactor.canonical_artanh_decomposition line 110