OAI/Probability/FreeIsing/Brownian/Existence.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.BrownianExistence.exists_preWienerMeasure line 10
2. def OAI.Problem367.BrownianExistence.preWienerMeasure line 16
3. instance OAI.Problem367.BrownianExistence.(instance at line 18) line 18
4. theorem OAI.Problem367.BrownianExistence.preWienerMeasure_projectiveLimit line 21
5. theorem OAI.Problem367.BrownianExistence.coordinate_isPreBrownianReal line 25