OAI/Analysis/ProductSpaces/PathMoments.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.IndependentProducts.productMeasure_probability line 15
  2. theorem OAI.IndependentProducts.pathProduct_root line 20
  3. lemma OAI.IndependentProducts.pathPrefix_length line 23
  4. lemma OAI.IndependentProducts.pathPrefix_injective line 28
  5. def OAI.IndependentProducts.pathEdges line 35

    Source documentation

    The finite set of multiplier coordinates on a path.

    def pathEdges (v : Vertex) : Finset Edge :=
…

    Mentions: OAI.IndependentProducts.Vertex, OAI.IndependentProducts.Edge

  6. lemma OAI.IndependentProducts.pathProduct_eq_prod_pathEdges line 38
  7. lemma OAI.IndependentProducts.measurable_pathProduct line 42
  8. lemma OAI.IndependentProducts.measurePreserving_coordinates line 48
  9. lemma OAI.IndependentProducts.integrable_coordinates_prod line 57
  10. lemma OAI.IndependentProducts.integral_coordinates_prod line 64
  11. lemma OAI.IndependentProducts.integrable_finset_coordinates_prod line 75
  12. lemma OAI.IndependentProducts.integral_finset_coordinates_prod line 84
  13. lemma OAI.IndependentProducts.pathProduct_memLp line 94
  14. lemma OAI.IndependentProducts.integral_pathProduct line 101
  15. lemma OAI.IndependentProducts.integral_pathProduct_sq line 107
  16. lemma OAI.IndependentProducts.pathProduct_pos line 113
  17. def OAI.IndependentProducts.pathL1 line 122

    Source documentation

    The integrable path product as an actual L1 element.

    def pathL1 (h₂ : MemLp (fun w : ℝ => w) 2 μ) (v : Vertex) : Lp ℝ 1 (productMeasure μ) :=
…

    Mentions: OAI.IndependentProducts.Vertex, OAI.IndependentProducts.productMeasure

  18. lemma OAI.IndependentProducts.pathL1_ae line 125
  19. lemma OAI.IndependentProducts.pathL1_mem line 129
  20. def OAI.IndependentProducts.pathVector line 135

    Source documentation

    Path products viewed in the closed span itself.

    def pathVector (h₂ : MemLp (fun w : ℝ => w) 2 μ) (v : Vertex) : productSpan μ :=
…

    Mentions: OAI.IndependentProducts.Vertex, OAI.IndependentProducts.productSpan

  21. lemma OAI.IndependentProducts.norm_pathVector line 138
  22. lemma OAI.IndependentProducts.child_length line 155
  23. def OAI.IndependentProducts.childEdge line 161

    Source documentation

    The new coordinate on the edge from a vertex to one of its children.

    def childEdge (v : Vertex) (n : ℕ) : Edge :=
…

    Mentions: OAI.IndependentProducts.Vertex, OAI.IndependentProducts.Edge

  24. lemma OAI.IndependentProducts.childEdge_injective line 164
  25. lemma OAI.IndependentProducts.childEdge_not_mem_pathEdges line 173
  26. lemma OAI.IndependentProducts.pathProduct_child line 180
  27. lemma OAI.IndependentProducts.measurable_childIncrement line 201
  28. lemma OAI.IndependentProducts.indepFun_path_coordinate line 208
  29. lemma OAI.IndependentProducts.indepFun_finset_coordinates line 218
  30. lemma OAI.IndependentProducts.integral_coordinate line 242
  31. lemma OAI.IndependentProducts.integral_path_mul_coordinate line 248
  32. lemma OAI.IndependentProducts.norm_child_difference line 256
  33. lemma OAI.IndependentProducts.mean_abs_deviation_pos line 280