OAI/Probability/StrongRayleigh/InnovationPathCriterion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem336AdditiveD139.exists_measurable_iid_brownian_path_version line 17
2. theorem OAI.Problem336AdditiveD139.exists_iid_path_version_of_eventwise_characteristic line 56