OAI/Analysis/ProductSpaces/TailCoefficients.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.IndependentProducts.pathVector_ae line 17
  2. lemma OAI.IndependentProducts.representative_sum line 21
  3. lemma OAI.IndependentProducts.representative_sub line 38
  4. lemma OAI.IndependentProducts.norm_eq_integral_abs_rep line 46
  5. lemma OAI.IndependentProducts.integrable_rep line 54
  6. lemma OAI.IndependentProducts.FiniteHead.relativeVector_ae line 61
  7. lemma OAI.IndependentProducts.FiniteHead.head_representative line 66
  8. lemma OAI.IndependentProducts.FiniteHead.tail_representative line 71
  9. def OAI.IndependentProducts.residualProduct line 81

    Source documentation

    Descendant-only factor after the first exit.

    def residualProduct (v : Vertex) (e : Edge) (ω : Sample) : ℝ :=
…

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

  10. lemma OAI.IndependentProducts.measurable_residualProduct line 84
  11. lemma OAI.IndependentProducts.integrable_residualProduct line 88
  12. lemma OAI.IndependentProducts.integral_residualProduct line 93
  13. def OAI.IndependentProducts.FiniteHead.tailCoefficient line 106

    Source documentation

    Coefficients conditionally independent below the exit forest.

    noncomputable def tailCoefficient (old : Sample) (i : ι) (desc : Sample) : ℝ :=
…

    Mentions: OAI.IndependentProducts.Sample

  14. lemma OAI.IndependentProducts.FiniteHead.measurable_tailCoefficient line 110
  15. lemma OAI.IndependentProducts.FiniteHead.integrable_tailCoefficient line 123
  16. lemma OAI.IndependentProducts.FiniteHead.integral_tailCoefficient line 136
  17. lemma OAI.IndependentProducts.FiniteHead.sum_tailCoefficient line 157
  18. lemma OAI.IndependentProducts.FiniteHead.sum_tailCoefficient_mean line 170