Map of a kernel by a measurable function

We define the map and comap of a kernel along a measurable function, as well as some often useful particular cases.

Main definitions

Kernels built from other kernels:

• map (κ : Kernel α β) (f : β → γ) : Kernel α γ ∫⁻ c, g c ∂(map κ f a) = ∫⁻ b, g (f b) ∂(κ a)
• comap (κ : Kernel α β) (f : γ → α) (hf : Measurable f) : Kernel γ β ∫⁻ b, g b ∂(comap κ f hf c) = ∫⁻ b, g b ∂(κ (f c))

Main statements

• lintegral_map, lintegral_comap: Lebesgue integral of a function against the map or comap of a kernel.

map, comap

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

The pushforward of a kernel along a measurable function. This is an implementation detail, use map κ f instead.

Equations

• κ.mapOfMeasurable f hf = { toFun := fun (a : α) => MeasureTheory.Measure.map f (κ a), measurable' := ⋯ }

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

The pushforward of a kernel along a function. If the function is not measurable, we use zero instead. This choice of junk value ensures that typeclass inference can infer that the map of a kernel satisfying IsZeroOrMarkovKernel again satisfies this property.

Equations

• κ.map f = if hf : Measurable f then κ.mapOfMeasurable f hf else 0

theorem ProbabilityTheory.Kernel.map_of_not_measurable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) {f : β → γ} (hf : ¬Measurable f) : κ.map f = 0

@[simp]

theorem ProbabilityTheory.Kernel.mapOfMeasurable_eq_map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) {f : β → γ} (hf : Measurable f) : κ.mapOfMeasurable f hf = κ.map f

theorem ProbabilityTheory.Kernel.map_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : β → γ} (κ : Kernel α β) (hf : Measurable f) (a : α) : (κ.map f) 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 : β → γ} (κ : Kernel α β) (hf : Measurable f) (a : α) {s : Set γ} (hs : MeasurableSet s) : ((κ.map f) a) s = (κ a) (f ⁻¹' s)

theorem ProbabilityTheory.Kernel.map_comp_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : Kernel α β) {f : β → γ} (hf : Measurable f) {g : γ → δ} (hg : Measurable g) : κ.map (g ∘ f) = (κ.map f).map g

@[simp]

theorem ProbabilityTheory.Kernel.map_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : β → γ} : map 0 f = 0

@[simp]

theorem ProbabilityTheory.Kernel.map_id {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) : κ.map id = κ

@[simp]

theorem ProbabilityTheory.Kernel.map_id' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : 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 : β → γ} (κ : Kernel α β) (hf : Measurable f) (a : α) {g' : γ → ENNReal} (hg : Measurable g') : ∫⁻ (b : γ), g' b ∂(κ.map f) a = ∫⁻ (a : β), g' (f a) ∂κ a

theorem ProbabilityTheory.Kernel.map_apply_eq_iff_map_symm_apply_eq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) {f : β ≃ᵐ γ} (η : Kernel α γ) : κ.map ⇑f = η ↔ κ = η.map ⇑f.symm

theorem ProbabilityTheory.Kernel.sum_map_seq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsSFiniteKernel κ] (f : β → γ) : (Kernel.sum fun (n : ℕ) => (κ.seq n).map f) = κ.map f

theorem ProbabilityTheory.Kernel.IsMarkovKernel.map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : β → γ} (κ : Kernel α β) [IsMarkovKernel κ] (hf : Measurable f) : IsMarkovKernel (κ.map f)

instance ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsZeroOrMarkovKernel κ] (f : β → γ) : IsZeroOrMarkovKernel (κ.map f)

instance ProbabilityTheory.Kernel.IsFiniteKernel.map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsFiniteKernel κ] (f : β → γ) : IsFiniteKernel (κ.map f)

instance ProbabilityTheory.Kernel.IsSFiniteKernel.map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsSFiniteKernel κ] (f : β → γ) : IsSFiniteKernel (κ.map f)

@[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) : (const γ μ).map f = const γ (MeasureTheory.Measure.map f μ)

def ProbabilityTheory.Kernel.comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) (g : γ → α) (hg : Measurable g) : Kernel γ β

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' := ⋯ }

@[simp]

theorem ProbabilityTheory.Kernel.coe_comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) (g : γ → α) (hg : Measurable g) : ⇑(κ.comap g hg) = ⇑κ ∘ g

theorem ProbabilityTheory.Kernel.comap_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γ → α} (κ : 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 : γ → α} (κ : 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) : comap 0 g hg = 0

@[simp]

theorem ProbabilityTheory.Kernel.comap_id {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) : κ.comap id ⋯ = κ

@[simp]

theorem ProbabilityTheory.Kernel.comap_id' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : 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 : γ → α} (κ : 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 : γ → α} (κ : Kernel α β) [IsSFiniteKernel κ] (hg : Measurable g) : (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 : γ → α} (κ : Kernel α β) [IsMarkovKernel κ] (hg : Measurable g) : IsMarkovKernel (κ.comap g hg)

instance ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γ → α} (κ : Kernel α β) [IsZeroOrMarkovKernel κ] (hg : Measurable g) : IsZeroOrMarkovKernel (κ.comap g hg)

instance ProbabilityTheory.Kernel.IsFiniteKernel.comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γ → α} (κ : Kernel α β) [IsFiniteKernel κ] (hg : Measurable g) : IsFiniteKernel (κ.comap g hg)

instance ProbabilityTheory.Kernel.IsSFiniteKernel.comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γ → α} (κ : Kernel α β) [IsSFiniteKernel κ] (hg : Measurable g) : IsSFiniteKernel (κ.comap g hg)

theorem ProbabilityTheory.Kernel.comap_comp_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {g : γ → α} (κ : Kernel α β) {f : δ → γ} (hf : Measurable f) (hg : Measurable g) : κ.comap (g ∘ f) ⋯ = (κ.comap g hg).comap f hf

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 δ} (κ : Kernel β γ) {f : α → β} {g : γ → δ} (hf : Measurable f) (hg : Measurable g) : (κ.map g).comap f hf = (κ.comap f hf).map g

@[simp]

theorem ProbabilityTheory.Kernel.id_map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : Measurable f) : Kernel.id.map f = deterministic f hf

@[simp]

theorem ProbabilityTheory.Kernel.id_comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : Measurable f) : Kernel.id.comap f hf = deterministic f hf

theorem ProbabilityTheory.Kernel.deterministic_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β} (hf : Measurable f) {g : β → γ} (hg : Measurable g) : (deterministic f hf).map g = deterministic (g ∘ f) ⋯

def ProbabilityTheory.Kernel.prodMkLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (γ : Type u_5) [MeasurableSpace γ] (κ : Kernel α β) : Kernel (γ × α) β

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

Equations

• ProbabilityTheory.Kernel.prodMkLeft γ κ = κ.comap Prod.snd ⋯

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

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

Equations

• ProbabilityTheory.Kernel.prodMkRight γ κ = κ.comap Prod.fst ⋯

@[simp]

theorem ProbabilityTheory.Kernel.prodMkLeft_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α β) (ca : γ × α) : (prodMkLeft γ κ) ca = κ ca.2

@[simp]

theorem ProbabilityTheory.Kernel.prodMkRight_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α β) (ca : α × γ) : (prodMkRight γ κ) ca = κ ca.1

theorem ProbabilityTheory.Kernel.prodMkLeft_apply' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α β) (ca : γ × α) (s : Set β) : ((prodMkLeft γ κ) ca) s = (κ ca.2) s

theorem ProbabilityTheory.Kernel.prodMkRight_apply' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α β) (ca : α × γ) (s : Set β) : ((prodMkRight γ κ) ca) s = (κ ca.1) s

@[simp]

theorem ProbabilityTheory.Kernel.prodMkLeft_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} : prodMkLeft α 0 = 0

@[simp]

theorem ProbabilityTheory.Kernel.prodMkRight_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} : prodMkRight α 0 = 0

@[simp]

theorem ProbabilityTheory.Kernel.prodMkLeft_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ η : Kernel α β) : prodMkLeft γ (κ + η) = prodMkLeft γ κ + prodMkLeft γ η

@[simp]

theorem ProbabilityTheory.Kernel.prodMkRight_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ η : Kernel α β) : prodMkRight γ (κ + η) = prodMkRight γ κ + prodMkRight γ η

theorem ProbabilityTheory.Kernel.sum_prodMkLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {ι : Type u_5} [Countable ι] {κ : ι → Kernel α β} : (Kernel.sum fun (i : ι) => prodMkLeft γ (κ i)) = prodMkLeft γ (Kernel.sum κ)

theorem ProbabilityTheory.Kernel.sum_prodMkRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {ι : Type u_5} [Countable ι] {κ : ι → Kernel α β} : (Kernel.sum fun (i : ι) => prodMkRight γ (κ i)) = prodMkRight γ (Kernel.sum κ)

theorem ProbabilityTheory.Kernel.lintegral_prodMkLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α β) (ca : γ × α) (g : β → ENNReal) : ∫⁻ (b : β), g b ∂(prodMkLeft γ κ) ca = ∫⁻ (b : β), g b ∂κ ca.2

theorem ProbabilityTheory.Kernel.lintegral_prodMkRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α β) (ca : α × γ) (g : β → ENNReal) : ∫⁻ (b : β), g b ∂(prodMkRight γ κ) ca = ∫⁻ (b : β), g b ∂κ ca.1

instance ProbabilityTheory.Kernel.IsMarkovKernel.prodMkLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsMarkovKernel κ] : IsMarkovKernel (Kernel.prodMkLeft γ κ)

instance ProbabilityTheory.Kernel.IsMarkovKernel.prodMkRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsMarkovKernel κ] : IsMarkovKernel (Kernel.prodMkRight γ κ)

instance ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.prodMkLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsZeroOrMarkovKernel κ] : IsZeroOrMarkovKernel (Kernel.prodMkLeft γ κ)

instance ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.prodMkRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsZeroOrMarkovKernel κ] : IsZeroOrMarkovKernel (Kernel.prodMkRight γ κ)

instance ProbabilityTheory.Kernel.IsFiniteKernel.prodMkLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsFiniteKernel κ] : IsFiniteKernel (Kernel.prodMkLeft γ κ)

instance ProbabilityTheory.Kernel.IsFiniteKernel.prodMkRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsFiniteKernel κ] : IsFiniteKernel (Kernel.prodMkRight γ κ)

instance ProbabilityTheory.Kernel.IsSFiniteKernel.prodMkLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsSFiniteKernel κ] : IsSFiniteKernel (Kernel.prodMkLeft γ κ)

instance ProbabilityTheory.Kernel.IsSFiniteKernel.prodMkRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsSFiniteKernel κ] : IsSFiniteKernel (Kernel.prodMkRight γ κ)

theorem ProbabilityTheory.Kernel.isSFiniteKernel_prodMkLeft_unit {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} : IsSFiniteKernel (prodMkLeft Unit κ) ↔ IsSFiniteKernel κ

theorem ProbabilityTheory.Kernel.isSFiniteKernel_prodMkRight_unit {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} : IsSFiniteKernel (prodMkRight Unit κ) ↔ IsSFiniteKernel κ

theorem ProbabilityTheory.Kernel.map_prodMkLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {δ : Type u_4} {mδ : MeasurableSpace δ} (γ : Type u_5) [MeasurableSpace γ] (κ : Kernel α β) (f : β → δ) : (prodMkLeft γ κ).map f = prodMkLeft γ (κ.map f)

theorem ProbabilityTheory.Kernel.map_prodMkRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {δ : Type u_4} {mδ : MeasurableSpace δ} (κ : Kernel α β) (γ : Type u_5) {mγ : MeasurableSpace γ} (f : β → δ) : (prodMkRight γ κ).map f = prodMkRight γ (κ.map f)

def ProbabilityTheory.Kernel.swapLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) : Kernel (β × α) γ

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

Equations

• κ.swapLeft = κ.comap Prod.swap ⋯

@[simp]

theorem ProbabilityTheory.Kernel.swapLeft_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} : swapLeft 0 = 0

@[simp]

theorem ProbabilityTheory.Kernel.swapLeft_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : β × α) : κ.swapLeft a = κ a.swap

theorem ProbabilityTheory.Kernel.swapLeft_apply' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : β × α) (s : Set γ) : (κ.swapLeft a) s = (κ a.swap) s

theorem ProbabilityTheory.Kernel.lintegral_swapLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : β × α) (g : γ → ENNReal) : ∫⁻ (c : γ), g c ∂κ.swapLeft a = ∫⁻ (c : γ), g c ∂κ a.swap

instance ProbabilityTheory.Kernel.IsMarkovKernel.swapLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) [IsMarkovKernel κ] : IsMarkovKernel κ.swapLeft

instance ProbabilityTheory.Kernel.IsFiniteKernel.swapLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) [IsFiniteKernel κ] : IsFiniteKernel κ.swapLeft

instance ProbabilityTheory.Kernel.IsSFiniteKernel.swapLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) [IsSFiniteKernel κ] : IsSFiniteKernel κ.swapLeft

@[simp]

theorem ProbabilityTheory.Kernel.swapLeft_prodMkLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) (γ : Type u_5) {x✝ : MeasurableSpace γ} : (prodMkLeft γ κ).swapLeft = prodMkRight γ κ

@[simp]

theorem ProbabilityTheory.Kernel.swapLeft_prodMkRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) (γ : Type u_5) {x✝ : MeasurableSpace γ} : (prodMkRight γ κ).swapLeft = prodMkLeft γ κ

noncomputable def ProbabilityTheory.Kernel.swapRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) : Kernel α (γ × β)

Define a Kernel α (γ × β) from a Kernel α (β × γ) by taking the map of Prod.swap. We use mapOfMeasurable in the definition for better defeqs.

Equations

• κ.swapRight = κ.mapOfMeasurable Prod.swap ⋯

theorem ProbabilityTheory.Kernel.swapRight_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) : κ.swapRight = κ.map Prod.swap

@[simp]

theorem ProbabilityTheory.Kernel.swapRight_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} : swapRight 0 = 0

theorem ProbabilityTheory.Kernel.swapRight_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) (a : α) : κ.swapRight a = MeasureTheory.Measure.map Prod.swap (κ a)

theorem ProbabilityTheory.Kernel.swapRight_apply' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : 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} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) (a : α) {g : γ × β → ENNReal} (hg : Measurable g) : ∫⁻ (c : γ × β), g c ∂κ.swapRight a = ∫⁻ (bc : β × γ), g bc.swap ∂κ a

instance ProbabilityTheory.Kernel.IsMarkovKernel.swapRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsMarkovKernel κ] : IsMarkovKernel κ.swapRight

instance ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.swapRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsZeroOrMarkovKernel κ] : IsZeroOrMarkovKernel κ.swapRight

instance ProbabilityTheory.Kernel.IsFiniteKernel.swapRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsFiniteKernel κ] : IsFiniteKernel κ.swapRight

instance ProbabilityTheory.Kernel.IsSFiniteKernel.swapRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsSFiniteKernel κ] : IsSFiniteKernel κ.swapRight

noncomputable def ProbabilityTheory.Kernel.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) : Kernel α β

Define a Kernel α β from a Kernel α (β × γ) by taking the map of the first projection. We use mapOfMeasurable for better defeqs.

Equations

• κ.fst = κ.mapOfMeasurable Prod.fst ⋯

theorem ProbabilityTheory.Kernel.fst_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) : κ.fst = κ.map Prod.fst

theorem ProbabilityTheory.Kernel.fst_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) (a : α) : κ.fst a = MeasureTheory.Measure.map Prod.fst (κ a)

theorem ProbabilityTheory.Kernel.fst_apply' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) (a : α) {s : Set β} (hs : MeasurableSet s) : (κ.fst a) s = (κ a) {p : β × γ | p.1 ∈ s}

theorem ProbabilityTheory.Kernel.fst_real_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) (a : α) {s : Set β} (hs : MeasurableSet s) : (κ.fst a).real s = (κ a).real {p : β × γ | p.1 ∈ s}

@[simp]

theorem ProbabilityTheory.Kernel.fst_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} : fst 0 = 0

theorem ProbabilityTheory.Kernel.lintegral_fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) (a : α) {g : β → ENNReal} (hg : Measurable g) : ∫⁻ (c : β), g c ∂κ.fst a = ∫⁻ (bc : β × γ), g bc.1 ∂κ a

instance ProbabilityTheory.Kernel.IsMarkovKernel.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsMarkovKernel κ] : IsMarkovKernel κ.fst

instance ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsZeroOrMarkovKernel κ] : IsZeroOrMarkovKernel κ.fst

instance ProbabilityTheory.Kernel.IsFiniteKernel.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsFiniteKernel κ] : IsFiniteKernel κ.fst

instance ProbabilityTheory.Kernel.IsSFiniteKernel.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsSFiniteKernel κ] : IsSFiniteKernel κ.fst

@[instance 100]

instance ProbabilityTheory.Kernel.isFiniteKernel_of_isFiniteKernel_fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {κ : Kernel α (β × γ)} [h : IsFiniteKernel κ.fst] : IsFiniteKernel κ

theorem ProbabilityTheory.Kernel.fst_map_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {δ : Type u_4} {mδ : MeasurableSpace δ} (κ : Kernel α β) {f : β → γ} {g : β → δ} (hg : Measurable g) : (κ.map fun (x : β) => (f x, g x)).fst = κ.map f

theorem ProbabilityTheory.Kernel.fst_map_id_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α β) {f : β → γ} (hf : Measurable f) : (κ.map fun (a : β) => (a, f a)).fst = κ

theorem ProbabilityTheory.Kernel.fst_prodMkLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (δ : Type u_5) [MeasurableSpace δ] (κ : Kernel α (β × γ)) : (prodMkLeft δ κ).fst = prodMkLeft δ κ.fst

theorem ProbabilityTheory.Kernel.fst_prodMkRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) (δ : Type u_5) [MeasurableSpace δ] : (prodMkRight δ κ).fst = prodMkRight δ κ.fst

noncomputable def ProbabilityTheory.Kernel.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) : Kernel α γ

Define a Kernel α γ from a Kernel α (β × γ) by taking the map of the second projection. We use mapOfMeasurable for better defeqs.

Equations

• κ.snd = κ.mapOfMeasurable Prod.snd ⋯

theorem ProbabilityTheory.Kernel.snd_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) : κ.snd = κ.map Prod.snd

theorem ProbabilityTheory.Kernel.snd_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) (a : α) : κ.snd a = MeasureTheory.Measure.map Prod.snd (κ a)

theorem ProbabilityTheory.Kernel.snd_apply' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) (a : α) {s : Set γ} (hs : MeasurableSet s) : (κ.snd a) s = (κ a) (Prod.snd ⁻¹' s)

@[simp]

theorem ProbabilityTheory.Kernel.snd_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} : snd 0 = 0

theorem ProbabilityTheory.Kernel.lintegral_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) (a : α) {g : γ → ENNReal} (hg : Measurable g) : ∫⁻ (c : γ), g c ∂κ.snd a = ∫⁻ (bc : β × γ), g bc.2 ∂κ a

instance ProbabilityTheory.Kernel.IsMarkovKernel.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsMarkovKernel κ] : IsMarkovKernel κ.snd

instance ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsZeroOrMarkovKernel κ] : IsZeroOrMarkovKernel κ.snd

instance ProbabilityTheory.Kernel.IsFiniteKernel.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsFiniteKernel κ] : IsFiniteKernel κ.snd

instance ProbabilityTheory.Kernel.IsSFiniteKernel.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsSFiniteKernel κ] : IsSFiniteKernel κ.snd

@[instance 100]

instance ProbabilityTheory.Kernel.isFiniteKernel_of_isFiniteKernel_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {κ : Kernel α (β × γ)} [h : IsFiniteKernel κ.snd] : IsFiniteKernel κ

theorem ProbabilityTheory.Kernel.snd_map_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {δ : Type u_4} {mδ : MeasurableSpace δ} (κ : Kernel α β) {f : β → γ} {g : β → δ} (hf : Measurable f) : (κ.map fun (x : β) => (f x, g x)).snd = κ.map g

theorem ProbabilityTheory.Kernel.snd_map_prod_id {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α β) {f : β → γ} (hf : Measurable f) : (κ.map fun (a : β) => (f a, a)).snd = κ

theorem ProbabilityTheory.Kernel.snd_prodMkLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (δ : Type u_5) [MeasurableSpace δ] (κ : Kernel α (β × γ)) : (prodMkLeft δ κ).snd = prodMkLeft δ κ.snd

theorem ProbabilityTheory.Kernel.snd_prodMkRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) (δ : Type u_5) [MeasurableSpace δ] : (prodMkRight δ κ).snd = prodMkRight δ κ.snd

@[simp]

theorem ProbabilityTheory.Kernel.fst_swapRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) : κ.swapRight.fst = κ.snd

@[simp]

theorem ProbabilityTheory.Kernel.snd_swapRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) : κ.swapRight.snd = κ.fst

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

Define a Kernel α γ from a Kernel (α × β) γ by taking the comap of fun a ↦ (a, b) for a given b : β.

Equations

• κ.sectL b = κ.comap (fun (a : α) => (a, b)) ⋯

@[simp]

theorem ProbabilityTheory.Kernel.sectL_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (b : β) (a : α) : (κ.sectL b) a = κ (a, b)

@[simp]

theorem ProbabilityTheory.Kernel.sectL_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (b : β) : sectL 0 b = 0

instance ProbabilityTheory.Kernel.instIsMarkovKernelSectLOfProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (b : β) [IsMarkovKernel κ] : IsMarkovKernel (κ.sectL b)

instance ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelSectLOfProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (b : β) [IsZeroOrMarkovKernel κ] : IsZeroOrMarkovKernel (κ.sectL b)

instance ProbabilityTheory.Kernel.instIsFiniteKernelSectLOfProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (b : β) [IsFiniteKernel κ] : IsFiniteKernel (κ.sectL b)

instance ProbabilityTheory.Kernel.instIsSFiniteKernelSectLOfProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (b : β) [IsSFiniteKernel κ] : IsSFiniteKernel (κ.sectL b)

instance ProbabilityTheory.Kernel.instNeZeroMeasureCoeSectLOfProdMk {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((κ.sectL b) a)

@[instance 100]

instance ProbabilityTheory.Kernel.instIsMarkovKernelProdOfSectL {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {κ : Kernel (α × β) γ} [∀ (b : β), IsMarkovKernel (κ.sectL b)] : IsMarkovKernel κ

theorem ProbabilityTheory.Kernel.comap_sectL {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : Kernel (α × β) γ) (b : β) {f : δ → α} (hf : Measurable f) : (κ.sectL b).comap f hf = κ.comap (fun (d : δ) => (f d, b)) ⋯

@[simp]

theorem ProbabilityTheory.Kernel.sectL_prodMkLeft {β : Type u_2} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (α : Type u_6) [MeasurableSpace α] (κ : Kernel β γ) (a : α) {b : β} : ((prodMkLeft α κ).sectL b) a = κ b

@[simp]

theorem ProbabilityTheory.Kernel.sectL_prodMkRight {α : Type u_1} {mα : MeasurableSpace α} {γ : Type u_4} {mγ : MeasurableSpace γ} (β : Type u_6) [MeasurableSpace β] (κ : Kernel α γ) (b : β) : (prodMkRight β κ).sectL b = κ

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

Define a Kernel β γ from a Kernel (α × β) γ by taking the comap of fun b ↦ (a, b) for a given a : α.

Equations

• κ.sectR a = κ.comap (fun (b : β) => (a, b)) ⋯

@[simp]

theorem ProbabilityTheory.Kernel.sectR_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (b : β) (a : α) : (κ.sectR a) b = κ (a, b)

@[simp]

theorem ProbabilityTheory.Kernel.sectR_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (a : α) : sectR 0 a = 0

instance ProbabilityTheory.Kernel.instIsMarkovKernelSectROfProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : α) [IsMarkovKernel κ] : IsMarkovKernel (κ.sectR a)

instance ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelSectROfProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : α) [IsZeroOrMarkovKernel κ] : IsZeroOrMarkovKernel (κ.sectR a)

instance ProbabilityTheory.Kernel.instIsFiniteKernelSectROfProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : α) [IsFiniteKernel κ] : IsFiniteKernel (κ.sectR a)

instance ProbabilityTheory.Kernel.instIsSFiniteKernelSectROfProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : α) [IsSFiniteKernel κ] : IsSFiniteKernel (κ.sectR a)

instance ProbabilityTheory.Kernel.instNeZeroMeasureCoeSectROfProdMk {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((κ.sectR a) b)

@[instance 100]

instance ProbabilityTheory.Kernel.instIsMarkovKernelProdOfSectR {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {κ : Kernel (α × β) γ} [∀ (b : α), IsMarkovKernel (κ.sectR b)] : IsMarkovKernel κ

theorem ProbabilityTheory.Kernel.comap_sectR {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : Kernel (α × β) γ) (a : α) {f : δ → β} (hf : Measurable f) : (κ.sectR a).comap f hf = κ.comap (fun (d : δ) => (a, f d)) ⋯

@[simp]

theorem ProbabilityTheory.Kernel.sectR_prodMkLeft {β : Type u_2} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (α : Type u_6) [MeasurableSpace α] (κ : Kernel β γ) (a : α) : (prodMkLeft α κ).sectR a = κ

@[simp]

theorem ProbabilityTheory.Kernel.sectR_prodMkRight {α : Type u_1} {mα : MeasurableSpace α} {γ : Type u_4} {mγ : MeasurableSpace γ} (β : Type u_6) [MeasurableSpace β] (κ : Kernel α γ) (b : β) {a : α} : ((prodMkRight β κ).sectR a) b = κ a

@[simp]

theorem ProbabilityTheory.Kernel.sectL_swapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) : κ.swapLeft.sectL = κ.sectR

@[simp]

theorem ProbabilityTheory.Kernel.sectR_swapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) : κ.swapLeft.sectR = κ.sectL

theorem ProbabilityTheory.Kernel.isSFiniteKernel_prodMkLeft_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [Nonempty γ] {κ : Kernel α β} : IsSFiniteKernel (prodMkLeft γ κ) ↔ IsSFiniteKernel κ

theorem ProbabilityTheory.Kernel.isSFiniteKernel_prodMkRight_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [Nonempty γ] {κ : Kernel α β} : IsSFiniteKernel (prodMkRight γ κ) ↔ IsSFiniteKernel κ