OAI/Probability/FreeIsing/Posterior/ContinuousPosteriorInterior.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.HasFreeIsingLaw.continuous_posterior_all_time_field_bound line 14
2. theorem OAI.Problem367.HasFreeIsingLaw.continuous_posterior_compact_localization line 60
3. theorem OAI.Problem367.HasFreeIsingLaw.posterior_version_initial_zero line 86
4. theorem OAI.Problem367.isStronglyProgressive_artanh line 108