OAI/Analysis/HardSphere/Bridges/PartialIndex.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.Wiener.partialBridge_symm line 18
  2. lemma OAI.HardSphere.Wiener.partialBridge_error line 21
  3. lemma OAI.HardSphere.Wiener.partialBridge_tendsto line 30
  4. abbrev OAI.HardSphere.Wiener.PartialIndex line 42
  5. def OAI.HardSphere.Wiener.partialEmbed line 44
  6. lemma OAI.HardSphere.Wiener.partialEmbed_injective line 48
  7. def OAI.HardSphere.Wiener.coefficient line 66
  8. def OAI.HardSphere.Wiener.partialPath line 70
  9. lemma OAI.HardSphere.Wiener.partialPath_expansion line 74
  10. lemma OAI.HardSphere.Wiener.coefficient_covariance line 91
  11. lemma OAI.HardSphere.Wiener.independent_coordinates line 111
  12. lemma OAI.HardSphere.Wiener.finite_coordinate_law line 114
  13. lemma OAI.HardSphere.Wiener.square_sum_covariance line 125
  14. lemma OAI.HardSphere.Wiener.ae_partialPath_tendsto line 139
  15. lemma OAI.HardSphere.Wiener.finite_projection_expansion line 144
  16. lemma OAI.HardSphere.Wiener.finite_projection_variance line 156
  17. lemma OAI.HardSphere.Wiener.finite_projection_law line 163
  18. lemma OAI.HardSphere.Wiener.path_projection_law line 176
  19. lemma OAI.HardSphere.Wiener.finite_linear_projection line 197
  20. lemma OAI.HardSphere.Wiener.finite_path_gaussian line 206
  21. lemma OAI.HardSphere.Wiener.path_isGaussianProcess line 223
  22. lemma OAI.HardSphere.Wiener.path_eval_law line 226
  23. lemma OAI.HardSphere.Wiener.path_mean line 230
  24. lemma OAI.HardSphere.Wiener.path_variance line 233
  25. lemma OAI.HardSphere.Wiener.path_add_law line 236
  26. lemma OAI.HardSphere.Wiener.path_covariance line 247
  27. lemma OAI.HardSphere.Wiener.wiener_projection_law line 258
  28. abbrev OAI.HardSphere.Wiener.BridgeIndex line 268
  29. abbrev OAI.HardSphere.Wiener.BridgeNoise line 269
  30. def OAI.HardSphere.Wiener.linearPath line 271
  31. def OAI.HardSphere.Wiener.rest line 272
  32. def OAI.HardSphere.Wiener.embedRest line 273
  33. def OAI.HardSphere.Wiener.bridgeMap line 274
  34. def OAI.HardSphere.Wiener.bridge line 275
  35. lemma OAI.HardSphere.Wiener.measurable_bridgeMap line 277
  36. lemma OAI.HardSphere.Wiener.measurable_rest line 285
  37. lemma OAI.HardSphere.Wiener.measurable_bridge line 286
  38. lemma OAI.HardSphere.Wiener.independent_base_rest line 288
  39. lemma OAI.HardSphere.Wiener.independent_base_bridge line 301
  40. lemma OAI.HardSphere.Wiener.bridge_eq line 304
  41. lemma OAI.HardSphere.Wiener.path_decomposition line 308
  42. lemma OAI.HardSphere.Wiener.bridge_at_zero line 312
  43. lemma OAI.HardSphere.Wiener.bridge_at_one line 313
  44. def OAI.HardSphere.Wiener.bridgeLaw line 315
  45. instance OAI.HardSphere.Wiener.(instance at line 316) line 316
  46. lemma OAI.HardSphere.Wiener.endpoint_bridge_law line 318
  47. lemma OAI.HardSphere.Wiener.wiener_disintegration line 326
  48. lemma OAI.HardSphere.Wiener.bridge_apply line 334
  49. lemma OAI.HardSphere.Wiener.bridge_projection_algebra line 341
  50. lemma OAI.HardSphere.Wiener.bridge_projection_law line 375
  51. def OAI.HardSphere.Wiener.denseEval line 389
  52. lemma OAI.HardSphere.Wiener.denseEval_embedding line 391
  53. lemma OAI.HardSphere.Wiener.continuous_path_law_ext line 398
  54. def OAI.HardSphere.Wiener.prefixTime line 428
  55. def OAI.HardSphere.Wiener.suffixTime line 433