OAI/Probability/FreeIsing/Ising/CovarianceTotalEnergy.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem367.IsingInnovation.covariance_eq_brownianObservationR line 13
2. lemma OAI.Problem367.IsingInnovation.posterior_eq_brownianObservationR line 28
3. theorem OAI.Problem367.IsingInnovation.covariance_timeEnergy line 42
4. theorem OAI.Problem367.IsingInnovation.covariance_timeEnergy_hasSum line 100
5. theorem OAI.Problem367.IsingInnovation.covariance_timeEnergy_integral_eq line 115