OAI/Probability/FreeIsing/Gibbs/CovarianceCriticalRowConvergence.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.RowEnergyConvergence.tendsto_tsum_norm_sub_sq_of_energy_tendsto line 13
2. theorem OAI.Problem367.RowEnergyConvergence.tendsto_tsum_integral_sq_sub_of_energy_tendsto line 77
3. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsCovariance_tendsto_timeMeanSquare_real line 117
4. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsCovariance_tendsto_fullTimeRowMeanSquare line 149
5. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsCovariance_fullTime_energy_cauchy line 221