OAI/Probability/SpanningForest/DenseBrownian.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.DenseBrownian.evaluationChar line 15
  2. def OAI.Problem336.DenseBrownian.brownianChar line 19
  3. lemma OAI.Problem336.DenseBrownian.continuous_evaluationChar line 22
  4. lemma OAI.Problem336.DenseBrownian.continuous_brownianChar line 40
  5. theorem OAI.Problem336.DenseBrownian.characteristic_of_dense line 45
  6. lemma OAI.Problem336.DenseBrownian.evaluationChar_reindex line 57
  7. lemma OAI.Problem336.DenseBrownian.brownianChar_reindex line 66
  8. def OAI.Problem336.DenseBrownian.timeCovariance line 82
  9. lemma OAI.Problem336.DenseBrownian.timeCovariance_posSemidef line 85
  10. lemma OAI.Problem336.DenseBrownian.characteristic_of_gaussian_hasLaw line 95
  11. theorem OAI.Problem336.DenseBrownian.isPreBrownian_of_characteristic line 123
  12. theorem OAI.Problem336.DenseBrownian.isBrownian_of_dense_characteristic line 167
  13. theorem OAI.Problem336.DenseBrownian.isBrownian_of_dense_characteristic_fin line 177
  14. def OAI.Problem336.DenseBrownian.dyadicTimes line 189
  15. lemma OAI.Problem336.DenseBrownian.dense_dyadicTimes line 192
  16. theorem OAI.Problem336.DenseBrownian.isBrownian_of_dyadic_characteristic_fin line 204
  17. theorem OAI.Problem336.DenseBrownian.isBrownian_of_dyadic_gaussian_fin line 211