Documentation

Mathlib.Probability.Kernel.Composition

Product and composition of kernels #

We define

A note on names: The composition-product Kernel α β → Kernel (α × β) γ → Kernel α (β × γ) is named composition in [Kal21] and product on the wikipedia article on transition kernels. Most papers studying categories of kernels call composition the map we call composition. We adopt that convention because it fits better with the use of the name comp elsewhere in mathlib.

Main definitions #

Kernels built from other kernels:

Main statements #

Notations #

Composition-Product of kernels #

We define a kernel composition-product compProd : Kernel α β → Kernel (α × β) γ → Kernel α (β × γ).

noncomputable def ProbabilityTheory.Kernel.compProdFun {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ) (a : α) (s : Set (β × γ)) :

Auxiliary function for the definition of the composition-product of two kernels. For all a : α, compProdFun κ η a is a countably additive function with value zero on the empty set, and the composition-product of kernels is defined in Kernel.compProd through Measure.ofMeasurable.

Equations
  • κ.compProdFun η a s = ∫⁻ (b : β), (η (a, b)) {c : γ | (b, c) s}κ a
Instances For
    theorem ProbabilityTheory.Kernel.compProdFun_empty {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ) (a : α) :
    κ.compProdFun η a = 0
    theorem ProbabilityTheory.Kernel.compProdFun_iUnion {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) (f : Set (β × γ)) (hf_meas : ∀ (i : ), MeasurableSet (f i)) (hf_disj : Pairwise (Disjoint on f)) :
    κ.compProdFun η a (⋃ (i : ), f i) = ∑' (i : ), κ.compProdFun η a (f i)
    theorem ProbabilityTheory.Kernel.compProdFun_tsum_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) (hs : MeasurableSet s) :
    κ.compProdFun η a s = ∑' (n : ), κ.compProdFun (η.seq n) a s
    theorem ProbabilityTheory.Kernel.compProdFun_tsum_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel κ] (a : α) (s : Set (β × γ)) :
    κ.compProdFun η a s = ∑' (n : ), (κ.seq n).compProdFun η a s
    theorem ProbabilityTheory.Kernel.compProdFun_eq_tsum {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) (hs : MeasurableSet s) :
    κ.compProdFun η a s = ∑' (n : ) (m : ), (κ.seq n).compProdFun (η.seq m) a s
    theorem ProbabilityTheory.Kernel.measurable_compProdFun_of_finite {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsFiniteKernel η] (hs : MeasurableSet s) :
    Measurable fun (a : α) => κ.compProdFun η a s

    Auxiliary lemma for measurable_compProdFun.

    theorem ProbabilityTheory.Kernel.measurable_compProdFun {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (hs : MeasurableSet s) :
    Measurable fun (a : α) => κ.compProdFun η a s
    noncomputable def ProbabilityTheory.Kernel.compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ) :

    Composition-Product of kernels. For s-finite kernels, it satisfies ∫⁻ bc, f bc ∂(compProd κ η a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η (a, b)) ∂(κ a) (see ProbabilityTheory.Kernel.lintegral_compProd). If either of the kernels is not s-finite, compProd is given the junk value 0.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem ProbabilityTheory.Kernel.compProd_apply_eq_compProdFun {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) (hs : MeasurableSet s) :
        ((κ.compProd η) a) s = κ.compProdFun η a s
        theorem ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ) (h : ¬ProbabilityTheory.IsSFiniteKernel κ) :
        κ.compProd η = 0
        theorem ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ) (h : ¬ProbabilityTheory.IsSFiniteKernel η) :
        κ.compProd η = 0
        theorem ProbabilityTheory.Kernel.compProd_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) (hs : MeasurableSet s) :
        ((κ.compProd η) a) s = ∫⁻ (b : β), (η (a, b)) {c : γ | (b, c) s}κ a
        theorem ProbabilityTheory.Kernel.le_compProd_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) (s : Set (β × γ)) :
        ∫⁻ (b : β), (η (a, b)) {c : γ | (b, c) s}κ a ((κ.compProd η) a) s
        @[simp]
        theorem ProbabilityTheory.Kernel.compProd_zero_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) :
        @[simp]
        theorem ProbabilityTheory.Kernel.compProd_zero_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) (γ : Type u_5) [MeasurableSpace γ] :
        κ.compProd 0 = 0

        ae filter of the composition-product #

        theorem ProbabilityTheory.Kernel.ae_kernel_lt_top {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] (a : α) (h2s : ((κ.compProd η) a) s ) :
        ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) <
        theorem ProbabilityTheory.Kernel.compProd_null {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] (a : α) (hs : MeasurableSet s) :
        ((κ.compProd η) a) s = 0 (fun (b : β) => (η (a, b)) (Prod.mk b ⁻¹' s)) =ᵐ[κ a] 0
        theorem ProbabilityTheory.Kernel.ae_null_of_compProd_null {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] {a : α} (h : ((κ.compProd η) a) s = 0) :
        (fun (b : β) => (η (a, b)) (Prod.mk b ⁻¹' s)) =ᵐ[κ a] 0
        theorem ProbabilityTheory.Kernel.ae_ae_of_ae_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] {a : α} {p : β × γProp} (h : ∀ᵐ (bc : β × γ) ∂(κ.compProd η) a, p bc) :
        ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
        theorem ProbabilityTheory.Kernel.ae_compProd_of_ae_ae {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] {a : α} {p : β × γProp} (hp : MeasurableSet {x : β × γ | p x}) (h : ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)) :
        ∀ᵐ (bc : β × γ) ∂(κ.compProd η) a, p bc
        theorem ProbabilityTheory.Kernel.ae_compProd_iff {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] {a : α} {p : β × γProp} (hp : MeasurableSet {x : β × γ | p x}) :
        (∀ᵐ (bc : β × γ) ∂(κ.compProd η) a, p bc) ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
        theorem ProbabilityTheory.Kernel.compProd_restrict {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] {s : Set β} {t : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t) :
        (κ.restrict hs).compProd (η.restrict ht) = (κ.compProd η).restrict
        theorem ProbabilityTheory.Kernel.compProd_restrict_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] {s : Set β} (hs : MeasurableSet s) :
        (κ.restrict hs).compProd η = (κ.compProd η).restrict
        theorem ProbabilityTheory.Kernel.compProd_restrict_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] {t : Set γ} (ht : MeasurableSet t) :
        κ.compProd (η.restrict ht) = (κ.compProd η).restrict

        Lebesgue integral #

        theorem ProbabilityTheory.Kernel.lintegral_compProd' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {f : βγENNReal} (hf : Measurable (Function.uncurry f)) :
        ∫⁻ (bc : β × γ), f bc.1 bc.2(κ.compProd η) a = ∫⁻ (b : β), ∫⁻ (c : γ), f b cη (a, b)κ a

        Lebesgue integral against the composition-product of two kernels.

        theorem ProbabilityTheory.Kernel.lintegral_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {f : β × γENNReal} (hf : Measurable f) :
        ∫⁻ (bc : β × γ), f bc(κ.compProd η) a = ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c)η (a, b)κ a

        Lebesgue integral against the composition-product of two kernels.

        theorem ProbabilityTheory.Kernel.lintegral_compProd₀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {f : β × γENNReal} (hf : AEMeasurable f ((κ.compProd η) a)) :
        ∫⁻ (z : β × γ), f z(κ.compProd η) a = ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y)η (a, x)κ a

        Lebesgue integral against the composition-product of two kernels.

        theorem ProbabilityTheory.Kernel.setLIntegral_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {f : β × γENNReal} (hf : Measurable f) {s : Set β} {t : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t) :
        ∫⁻ (z : β × γ) in s ×ˢ t, f z(κ.compProd η) a = ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y)η (a, x)κ a
        @[deprecated ProbabilityTheory.Kernel.setLIntegral_compProd]
        theorem ProbabilityTheory.Kernel.set_lintegral_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {f : β × γENNReal} (hf : Measurable f) {s : Set β} {t : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t) :
        ∫⁻ (z : β × γ) in s ×ˢ t, f z(κ.compProd η) a = ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y)η (a, x)κ a

        Alias of ProbabilityTheory.Kernel.setLIntegral_compProd.

        theorem ProbabilityTheory.Kernel.setLIntegral_compProd_univ_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {f : β × γENNReal} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) :
        ∫⁻ (z : β × γ) in s ×ˢ Set.univ, f z(κ.compProd η) a = ∫⁻ (x : β) in s, ∫⁻ (y : γ), f (x, y)η (a, x)κ a
        @[deprecated ProbabilityTheory.Kernel.setLIntegral_compProd_univ_right]
        theorem ProbabilityTheory.Kernel.set_lintegral_compProd_univ_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {f : β × γENNReal} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) :
        ∫⁻ (z : β × γ) in s ×ˢ Set.univ, f z(κ.compProd η) a = ∫⁻ (x : β) in s, ∫⁻ (y : γ), f (x, y)η (a, x)κ a

        Alias of ProbabilityTheory.Kernel.setLIntegral_compProd_univ_right.

        theorem ProbabilityTheory.Kernel.setLIntegral_compProd_univ_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {f : β × γENNReal} (hf : Measurable f) {t : Set γ} (ht : MeasurableSet t) :
        ∫⁻ (z : β × γ) in Set.univ ×ˢ t, f z(κ.compProd η) a = ∫⁻ (x : β), ∫⁻ (y : γ) in t, f (x, y)η (a, x)κ a
        @[deprecated ProbabilityTheory.Kernel.setLIntegral_compProd_univ_left]
        theorem ProbabilityTheory.Kernel.set_lintegral_compProd_univ_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {f : β × γENNReal} (hf : Measurable f) {t : Set γ} (ht : MeasurableSet t) :
        ∫⁻ (z : β × γ) in Set.univ ×ˢ t, f z(κ.compProd η) a = ∫⁻ (x : β), ∫⁻ (y : γ) in t, f (x, y)η (a, x)κ a

        Alias of ProbabilityTheory.Kernel.setLIntegral_compProd_univ_left.

        theorem ProbabilityTheory.Kernel.compProd_eq_tsum_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) (hs : MeasurableSet s) :
        ((κ.compProd η) a) s = ∑' (n : ) (m : ), (((κ.seq n).compProd (η.seq m)) a) s
        theorem ProbabilityTheory.Kernel.compProd_eq_sum_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] :
        κ.compProd η = ProbabilityTheory.Kernel.sum fun (n : ) => ProbabilityTheory.Kernel.sum fun (m : ) => (κ.seq n).compProd (η.seq m)
        theorem ProbabilityTheory.Kernel.compProd_eq_sum_compProd_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) :
        κ.compProd η = ProbabilityTheory.Kernel.sum fun (n : ) => (κ.seq n).compProd η
        theorem ProbabilityTheory.Kernel.compProd_eq_sum_compProd_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] :
        κ.compProd η = ProbabilityTheory.Kernel.sum fun (n : ) => κ.compProd (η.seq n)
        theorem ProbabilityTheory.Kernel.compProd_apply_univ_le {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsFiniteKernel η] (a : α) :
        ((κ.compProd η) a) Set.univ (κ a) Set.univ * ProbabilityTheory.IsFiniteKernel.bound η
        instance ProbabilityTheory.Kernel.IsSFiniteKernel.compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ) :
        Equations
        • =
        theorem ProbabilityTheory.Kernel.compProd_add_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (μ : ProbabilityTheory.Kernel α β) (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel μ] [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η] :
        (μ + κ).compProd η = μ.compProd η + κ.compProd η
        theorem ProbabilityTheory.Kernel.compProd_add_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (μ : ProbabilityTheory.Kernel α β) (κ : ProbabilityTheory.Kernel (α × β) γ) (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel μ] [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η] :
        μ.compProd (κ + η) = μ.compProd κ + μ.compProd η
        theorem ProbabilityTheory.Kernel.comapRight_compProd_id_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {δ : Type u_5} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] {f : δγ} (hf : MeasurableEmbedding f) :
        (κ.compProd η).comapRight = κ.compProd (η.comapRight hf)

        map, comap #

        noncomputable def ProbabilityTheory.Kernel.map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (f : βγ) (hf : Measurable f) :

        The pushforward of a kernel along a measurable function. We include measurability in the assumptions instead of using junk values to make sure that typeclass inference can infer that the map of a Markov kernel is again a Markov kernel.

        Equations
        Instances For
          theorem ProbabilityTheory.Kernel.map_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : βγ} (κ : ProbabilityTheory.Kernel α β) (hf : Measurable f) (a : α) :
          (κ.map f hf) a = MeasureTheory.Measure.map f (κ a)
          theorem ProbabilityTheory.Kernel.map_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : βγ} (κ : ProbabilityTheory.Kernel α β) (hf : Measurable f) (a : α) {s : Set γ} (hs : MeasurableSet s) :
          ((κ.map f hf) a) s = (κ a) (f ⁻¹' s)
          @[simp]
          theorem ProbabilityTheory.Kernel.map_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : βγ} (hf : Measurable f) :
          @[simp]
          theorem ProbabilityTheory.Kernel.map_id {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) :
          κ.map id = κ
          @[simp]
          theorem ProbabilityTheory.Kernel.map_id' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) :
          κ.map (fun (a : β) => a) = κ
          theorem ProbabilityTheory.Kernel.lintegral_map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : βγ} (κ : ProbabilityTheory.Kernel α β) (hf : Measurable f) (a : α) {g' : γENNReal} (hg : Measurable g') :
          ∫⁻ (b : γ), g' b(κ.map f hf) a = ∫⁻ (a : β), g' (f a)κ a
          theorem ProbabilityTheory.Kernel.sum_map_seq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : βγ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (hf : Measurable f) :
          (ProbabilityTheory.Kernel.sum fun (n : ) => (κ.seq n).map f hf) = κ.map f hf
          instance ProbabilityTheory.Kernel.IsMarkovKernel.map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : βγ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel κ] (hf : Measurable f) :
          Equations
          • =
          instance ProbabilityTheory.Kernel.IsFiniteKernel.map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : βγ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] (hf : Measurable f) :
          Equations
          • =
          instance ProbabilityTheory.Kernel.IsSFiniteKernel.map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : βγ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (hf : Measurable f) :
          Equations
          • =
          @[simp]
          theorem ProbabilityTheory.Kernel.map_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (μ : MeasureTheory.Measure α) {f : αβ} (hf : Measurable f) :
          def ProbabilityTheory.Kernel.comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (g : γα) (hg : Measurable g) :

          Pullback of a kernel, such that for each set s comap κ g hg c s = κ (g c) s. We include measurability in the assumptions instead of using junk values to make sure that typeclass inference can infer that the comap of a Markov kernel is again a Markov kernel.

          Equations
          • κ.comap g hg = { toFun := fun (a : γ) => κ (g a), measurable' := }
          Instances For
            theorem ProbabilityTheory.Kernel.comap_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γα} (κ : ProbabilityTheory.Kernel α β) (hg : Measurable g) (c : γ) :
            (κ.comap g hg) c = κ (g c)
            theorem ProbabilityTheory.Kernel.comap_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γα} (κ : ProbabilityTheory.Kernel α β) (hg : Measurable g) (c : γ) (s : Set β) :
            ((κ.comap g hg) c) s = (κ (g c)) s
            @[simp]
            theorem ProbabilityTheory.Kernel.comap_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γα} (hg : Measurable g) :
            @[simp]
            theorem ProbabilityTheory.Kernel.comap_id {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) :
            κ.comap id = κ
            @[simp]
            theorem ProbabilityTheory.Kernel.comap_id' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) :
            κ.comap (fun (a : α) => a) = κ
            theorem ProbabilityTheory.Kernel.lintegral_comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γα} (κ : ProbabilityTheory.Kernel α β) (hg : Measurable g) (c : γ) (g' : βENNReal) :
            ∫⁻ (b : β), g' b(κ.comap g hg) c = ∫⁻ (b : β), g' bκ (g c)
            theorem ProbabilityTheory.Kernel.sum_comap_seq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γα} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (hg : Measurable g) :
            (ProbabilityTheory.Kernel.sum fun (n : ) => (κ.seq n).comap g hg) = κ.comap g hg
            instance ProbabilityTheory.Kernel.IsMarkovKernel.comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γα} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel κ] (hg : Measurable g) :
            Equations
            • =
            instance ProbabilityTheory.Kernel.IsFiniteKernel.comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γα} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] (hg : Measurable g) :
            Equations
            • =
            instance ProbabilityTheory.Kernel.IsSFiniteKernel.comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γα} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (hg : Measurable g) :
            Equations
            • =
            theorem ProbabilityTheory.Kernel.comap_map_comm {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel β γ) {f : αβ} {g : γδ} (hf : Measurable f) (hg : Measurable g) :
            (κ.map g hg).comap f hf = (κ.comap f hf).map g hg
            def ProbabilityTheory.Kernel.prodMkLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (γ : Type u_5) [MeasurableSpace γ] (κ : ProbabilityTheory.Kernel α β) :

            Define a Kernel (γ × α) β from a Kernel α β by taking the comap of the projection.

            Equations
            Instances For
              def ProbabilityTheory.Kernel.prodMkRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (γ : Type u_5) [MeasurableSpace γ] (κ : ProbabilityTheory.Kernel α β) :

              Define a Kernel (α × γ) β from a Kernel α β by taking the comap of the projection.

              Equations
              Instances For
                @[simp]
                theorem ProbabilityTheory.Kernel.prodMkLeft_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (ca : γ × α) :
                @[simp]
                theorem ProbabilityTheory.Kernel.prodMkRight_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (ca : α × γ) :
                theorem ProbabilityTheory.Kernel.prodMkLeft_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (ca : γ × α) (s : Set β) :
                ((ProbabilityTheory.Kernel.prodMkLeft γ κ) ca) s = (κ ca.2) s
                theorem ProbabilityTheory.Kernel.prodMkRight_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (ca : α × γ) (s : Set β) :
                ((ProbabilityTheory.Kernel.prodMkRight γ κ) ca) s = (κ ca.1) s
                @[simp]
                theorem ProbabilityTheory.Kernel.prodMkLeft_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} :
                @[simp]
                theorem ProbabilityTheory.Kernel.prodMkRight_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} :
                theorem ProbabilityTheory.Kernel.lintegral_prodMkLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (ca : γ × α) (g : βENNReal) :
                ∫⁻ (b : β), g b(ProbabilityTheory.Kernel.prodMkLeft γ κ) ca = ∫⁻ (b : β), g bκ ca.2
                theorem ProbabilityTheory.Kernel.lintegral_prodMkRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (ca : α × γ) (g : βENNReal) :
                ∫⁻ (b : β), g b(ProbabilityTheory.Kernel.prodMkRight γ κ) ca = ∫⁻ (b : β), g bκ ca.1
                theorem ProbabilityTheory.Kernel.map_prodMkLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {δ : Type u_4} {mδ : MeasurableSpace δ} (γ : Type u_6) [MeasurableSpace γ] (κ : ProbabilityTheory.Kernel α β) {f : βδ} (hf : Measurable f) :
                theorem ProbabilityTheory.Kernel.map_prodMkRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {δ : Type u_4} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel α β) (γ : Type u_6) [MeasurableSpace γ] {f : βδ} (hf : Measurable f) :
                def ProbabilityTheory.Kernel.swapLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) :

                Define a Kernel (β × α) γ from a Kernel (α × β) γ by taking the comap of Prod.swap.

                Equations
                • κ.swapLeft = κ.comap Prod.swap
                Instances For
                  @[simp]
                  theorem ProbabilityTheory.Kernel.swapLeft_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) (a : β × α) :
                  κ.swapLeft a = κ a.swap
                  theorem ProbabilityTheory.Kernel.swapLeft_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) (a : β × α) (s : Set γ) :
                  (κ.swapLeft a) s = (κ a.swap) s
                  theorem ProbabilityTheory.Kernel.lintegral_swapLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) (a : β × α) (g : γENNReal) :
                  ∫⁻ (c : γ), g cκ.swapLeft a = ∫⁻ (c : γ), g cκ a.swap
                  Equations
                  • =
                  Equations
                  • =
                  Equations
                  • =
                  noncomputable def ProbabilityTheory.Kernel.swapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) :

                  Define a Kernel α (γ × β) from a Kernel α (β × γ) by taking the map of Prod.swap.

                  Equations
                  • κ.swapRight = κ.map Prod.swap
                  Instances For
                    theorem ProbabilityTheory.Kernel.swapRight_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (a : α) :
                    κ.swapRight a = MeasureTheory.Measure.map Prod.swap (κ a)
                    theorem ProbabilityTheory.Kernel.swapRight_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (a : α) {s : Set (γ × β)} (hs : MeasurableSet s) :
                    (κ.swapRight a) s = (κ a) {p : β × γ | p.swap s}
                    theorem ProbabilityTheory.Kernel.lintegral_swapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (a : α) {g : γ × βENNReal} (hg : Measurable g) :
                    ∫⁻ (c : γ × β), g cκ.swapRight a = ∫⁻ (bc : β × γ), g bc.swapκ a
                    Equations
                    • =
                    Equations
                    • =
                    Equations
                    • =
                    noncomputable def ProbabilityTheory.Kernel.fst {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) :

                    Define a Kernel α β from a Kernel α (β × γ) by taking the map of the first projection.

                    Equations
                    • κ.fst = κ.map Prod.fst
                    Instances For
                      theorem ProbabilityTheory.Kernel.fst_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (a : α) :
                      κ.fst a = MeasureTheory.Measure.map Prod.fst (κ a)
                      theorem ProbabilityTheory.Kernel.fst_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (a : α) {s : Set β} (hs : MeasurableSet s) :
                      (κ.fst a) s = (κ a) {p : β × γ | p.1 s}
                      @[simp]
                      theorem ProbabilityTheory.Kernel.fst_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} :
                      theorem ProbabilityTheory.Kernel.lintegral_fst {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (a : α) {g : βENNReal} (hg : Measurable g) :
                      ∫⁻ (c : β), g cκ.fst a = ∫⁻ (bc : β × γ), g bc.1κ a
                      Equations
                      • =
                      Equations
                      • =
                      @[instance 100]
                      Equations
                      • =
                      theorem ProbabilityTheory.Kernel.fst_map_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {δ : Type u_4} {mδ : MeasurableSpace δ} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) {f : βγ} {g : βδ} (hf : Measurable f) (hg : Measurable g) :
                      (κ.map (fun (x : β) => (f x, g x)) ).fst = κ.map f hf
                      theorem ProbabilityTheory.Kernel.fst_map_id_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) {γ : Type u_6} {mγ : MeasurableSpace γ} {f : βγ} (hf : Measurable f) :
                      (κ.map (fun (a : β) => (a, f a)) ).fst = κ
                      @[simp]
                      theorem ProbabilityTheory.Kernel.fst_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsMarkovKernel η] :
                      (κ.compProd η).fst = κ
                      noncomputable def ProbabilityTheory.Kernel.snd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) :

                      Define a Kernel α γ from a Kernel α (β × γ) by taking the map of the second projection.

                      Equations
                      • κ.snd = κ.map Prod.snd
                      Instances For
                        theorem ProbabilityTheory.Kernel.snd_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (a : α) :
                        κ.snd a = MeasureTheory.Measure.map Prod.snd (κ a)
                        theorem ProbabilityTheory.Kernel.snd_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (a : α) {s : Set γ} (hs : MeasurableSet s) :
                        (κ.snd a) s = (κ a) {p : β × γ | p.2 s}
                        @[simp]
                        theorem ProbabilityTheory.Kernel.snd_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} :
                        theorem ProbabilityTheory.Kernel.lintegral_snd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (a : α) {g : γENNReal} (hg : Measurable g) :
                        ∫⁻ (c : γ), g cκ.snd a = ∫⁻ (bc : β × γ), g bc.2κ a
                        Equations
                        • =
                        Equations
                        • =
                        @[instance 100]
                        Equations
                        • =
                        theorem ProbabilityTheory.Kernel.snd_map_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {δ : Type u_4} {mδ : MeasurableSpace δ} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) {f : βγ} {g : βδ} (hf : Measurable f) (hg : Measurable g) :
                        (κ.map (fun (x : β) => (f x, g x)) ).snd = κ.map g hg
                        theorem ProbabilityTheory.Kernel.snd_map_prod_id {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) {γ : Type u_6} {mγ : MeasurableSpace γ} {f : βγ} (hf : Measurable f) :
                        (κ.map (fun (a : β) => (f a, a)) ).snd = κ
                        @[simp]
                        theorem ProbabilityTheory.Kernel.fst_swapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) :
                        κ.swapRight.fst = κ.snd
                        @[simp]
                        theorem ProbabilityTheory.Kernel.snd_swapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) :
                        κ.swapRight.snd = κ.fst

                        Composition of two kernels #

                        noncomputable def ProbabilityTheory.Kernel.comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (η : ProbabilityTheory.Kernel β γ) (κ : ProbabilityTheory.Kernel α β) :

                        Composition of two kernels.

                        Equations
                        • η.comp κ = { toFun := fun (a : α) => (κ a).bind η, measurable' := }
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            theorem ProbabilityTheory.Kernel.comp_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (η : ProbabilityTheory.Kernel β γ) (κ : ProbabilityTheory.Kernel α β) (a : α) :
                            (η.comp κ) a = (κ a).bind η
                            theorem ProbabilityTheory.Kernel.comp_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (η : ProbabilityTheory.Kernel β γ) (κ : ProbabilityTheory.Kernel α β) (a : α) {s : Set γ} (hs : MeasurableSet s) :
                            ((η.comp κ) a) s = ∫⁻ (b : β), (η b) sκ a
                            theorem ProbabilityTheory.Kernel.lintegral_comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (η : ProbabilityTheory.Kernel β γ) (κ : ProbabilityTheory.Kernel α β) (a : α) {g : γENNReal} (hg : Measurable g) :
                            ∫⁻ (c : γ), g c(η.comp κ) a = ∫⁻ (b : β), ∫⁻ (c : γ), g cη bκ a
                            theorem ProbabilityTheory.Kernel.comp_assoc {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {δ : Type u_5} {mδ : MeasurableSpace δ} (ξ : ProbabilityTheory.Kernel γ δ) [ProbabilityTheory.IsSFiniteKernel ξ] (η : ProbabilityTheory.Kernel β γ) (κ : ProbabilityTheory.Kernel α β) :
                            (ξ.comp η).comp κ = ξ.comp (η.comp κ)

                            Composition of kernels is associative.

                            theorem ProbabilityTheory.Kernel.deterministic_comp_eq_map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : βγ} (hf : Measurable f) (κ : ProbabilityTheory.Kernel α β) :
                            (ProbabilityTheory.Kernel.deterministic f hf).comp κ = κ.map f hf
                            theorem ProbabilityTheory.Kernel.comp_deterministic_eq_comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γα} (κ : ProbabilityTheory.Kernel α β) (hg : Measurable g) :
                            κ.comp (ProbabilityTheory.Kernel.deterministic g hg) = κ.comap g hg

                            Product of two kernels #

                            noncomputable def ProbabilityTheory.Kernel.prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α γ) :

                            Product of two kernels. This is meaningful only when the kernels are s-finite.

                            Equations
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                theorem ProbabilityTheory.Kernel.prod_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {s : Set (β × γ)} (hs : MeasurableSet s) :
                                ((κ.prod η) a) s = ∫⁻ (b : β), (η a) {c : γ | (b, c) s}κ a
                                theorem ProbabilityTheory.Kernel.prod_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) :
                                (κ.prod η) a = (κ a).prod (η a)
                                theorem ProbabilityTheory.Kernel.lintegral_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {g : β × γENNReal} (hg : Measurable g) :
                                ∫⁻ (c : β × γ), g c(κ.prod η) a = ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c)η aκ a
                                instance ProbabilityTheory.Kernel.IsSFiniteKernel.prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α γ) :
                                Equations
                                • =
                                @[simp]
                                theorem ProbabilityTheory.Kernel.fst_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.IsMarkovKernel η] :
                                (κ.prod η).fst = κ
                                @[simp]
                                theorem ProbabilityTheory.Kernel.snd_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel κ] (η : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.IsSFiniteKernel η] :
                                (κ.prod η).snd = η