OAI/Probability/SpanningForest/CanonicalBrownianReference.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem336.CanonicalBrownianReference.Space line 16
  2. def OAI.Problem336.CanonicalBrownianReference.noiseLaw line 18
  3. instance OAI.Problem336.CanonicalBrownianReference.noiseLaw_probability line 21
  4. def OAI.Problem336.CanonicalBrownianReference.law line 25
  5. instance OAI.Problem336.CanonicalBrownianReference.law_probability line 28
  6. def OAI.Problem336.CanonicalBrownianReference.hidden line 33
  7. def OAI.Problem336.CanonicalBrownianReference.noise line 35
  8. def OAI.Problem336.CanonicalBrownianReference.observation line 37
  9. theorem OAI.Problem336.CanonicalBrownianReference.hidden_measurable line 42
  10. theorem OAI.Problem336.CanonicalBrownianReference.hidden_hasLaw line 44
  11. theorem OAI.Problem336.CanonicalBrownianReference.paths_hasLaw line 47
  12. theorem OAI.Problem336.CanonicalBrownianReference.raw_noise_hasLaw line 51
  13. theorem OAI.Problem336.CanonicalBrownianReference.noise_measurable line 61
  14. theorem OAI.Problem336.CanonicalBrownianReference.noise_jointlyMeasurable line 64
  15. theorem OAI.Problem336.CanonicalBrownianReference.noise_continuous line 69
  16. theorem OAI.Problem336.CanonicalBrownianReference.noise_brownian line 72
  17. theorem OAI.Problem336.CanonicalBrownianReference.noise_independent line 76
  18. theorem OAI.Problem336.CanonicalBrownianReference.hidden_independent_flat_noise line 82
  19. theorem OAI.Problem336.CanonicalBrownianReference.hidden_independent_noise line 88
  20. theorem OAI.Problem336.CanonicalBrownianReference.bit_hidden_measurable line 93
  21. theorem OAI.Problem336.CanonicalBrownianReference.bit_hidden_independent_noise line 100
  22. theorem OAI.Problem336.CanonicalBrownianReference.bit_hidden_mem_Icc line 107
  23. theorem OAI.Problem336.CanonicalBrownianReference.observation_continuous line 111
  24. theorem OAI.Problem336.CanonicalBrownianReference.observation_jointlyMeasurable line 115
  25. theorem OAI.Problem336.CanonicalBrownianReference.posterior line 123