OAI/Probability/FreeIsing/Posterior/UniformTimeApproximation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsSpinMean_brownian_secondMoment_continuous line 13
2. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsSpinMean_gaussian_secondMoment_monotone line 49
3. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsSpinMean_brownian_secondMoment_monotone line 81
4. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsSpinMean_brownian_secondMoment_tendstoUniformlyOn line 97
5. theorem OAI.Problem367.integral_sq_sub_eq_sub_of_condExp line 123
6. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsSpinMean_gaussian_meanSquare_eq_secondMoment_sub line 156
7. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsSpinMean_brownian_meanSquare_eq_secondMoment_sub line 212
8. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsSpinMean_brownian_meanSquare_tendstoUniformlyOn line 242