OAI/Probability/LatticeSurface/Brownian/BrownianPathSupport.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BrownianForcing.Path line 11
  2. instance OAI.BrownianForcing.(instance at line 13) line 13
  3. instance OAI.BrownianForcing.(instance at line 15) line 15
  4. def OAI.BrownianForcing.halfTime line 17
  5. def OAI.BrownianForcing.lastTime line 19
  6. def OAI.BrownianForcing.twoPiece line 21
  7. lemma OAI.BrownianForcing.twoPiece_kernel line 30
  8. lemma OAI.BrownianForcing.twoPiece_half line 40
  9. lemma OAI.BrownianForcing.twoPiece_last line 43
  10. lemma OAI.BrownianForcing.twoPiece_zero line 46
  11. lemma OAI.BrownianForcing.twoPiece_representer line 48