OAI/Probability/FreeIsing/Posterior/VarianceTimeIntegral.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.integrable_prod_of_nonneg_section_bound line 12
2. theorem OAI.Problem367.measurable_brownian_gibbs_posterior_real_time line 39
3. theorem OAI.Problem367.posterior_moment_bound_mono line 61
4. theorem OAI.Problem367.HasFreeIsingLaw.brownian_gibbs_posterior_exponential_time_moment line 73
5. theorem OAI.Problem367.HasFreeIsingLaw.brownian_gibbs_posterior_inverse_variance_time_moment line 106
6. theorem OAI.Problem367.HasFreeIsingLaw.ae_locally_integrable_brownian_inverse_variance_pow line 146