OAI/Probability/FreeIsing/Ising/CovarianceTimeL2.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem367.IsingInnovation.measurable_finiteCovariance_joint line 13
2. theorem OAI.Problem367.IsingInnovation.finiteCovariance_tendsto_ae line 24
3. theorem OAI.Problem367.IsingInnovation.finiteCovariance_tendsto_finiteMeasureMeanSquare line 37
4. theorem OAI.Problem367.IsingInnovation.finiteCovariance_tendsto_timeMeanSquare line 67
5. lemma OAI.Problem367.IsingInnovation.memLp_finiteCovariance_time line 81
6. lemma OAI.Problem367.IsingInnovation.memLp_covariance_time line 96