OAI/Probability/FreeIsing/Posterior/FieldL2Limit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.measurable_artanh_field line 13
2. theorem OAI.Problem367.tendsto_integral_sq_sub_posterior_fields line 17
3. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsField_tendsto_ae line 67
4. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsField_tendsto_meanSquare line 96
5. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsField_brownian_tendsto_ae line 130
6. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsField_brownian_tendsto_meanSquare line 156
7. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsField_brownian_discrepancy_bound line 193
8. theorem OAI.Problem367.HasFreeIsingLaw.finiteGibbsField_brownian_tendsto_timeMeanSquare line 221