OAI/Probability/FreeIsing/Ising/CanonicalMartingales.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem367.IsingObservationFactor.evaluation_progressive line 14
2. theorem OAI.Problem367.IsingObservationFactor.canonical_posterior_martingale line 19
3. theorem OAI.Problem367.IsingObservationFactor.continuousPosterior_martingale line 36
4. def OAI.Problem367.IsingObservationFactor.canonicalCovarianceEnergy line 45
5. lemma OAI.Problem367.IsingObservationFactor.canonicalCovarianceEnergy_progressive line 49
6. def OAI.Problem367.IsingObservationFactor.canonicalCovarianceCompensator line 53
7. lemma OAI.Problem367.IsingObservationFactor.canonicalCovarianceCompensator_uniformObservation line 56
8. theorem OAI.Problem367.IsingObservationFactor.canonical_compensatedSquare_martingale line 75
9. theorem OAI.Problem367.IsingObservationFactor.continuousPosterior_compensatedSquare_martingale line 111