Documentation

Mathlib.Probability.Kernel.Composition.MapComap

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:

Main statements #

map, comap #

noncomputable def ProbabilityTheory.Kernel.mapOfMeasurable {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : 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
noncomputable def ProbabilityTheory.Kernel.map {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : 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
theorem ProbabilityTheory.Kernel.map_of_not_measurable {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (κ : Kernel α β) {f : βγ} (hf : ¬Measurable f) :
κ.map f = 0
@[simp]
theorem ProbabilityTheory.Kernel.mapOfMeasurable_eq_map {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (κ : Kernel α β) {f : βγ} (hf : Measurable f) :
κ.mapOfMeasurable f hf = κ.map f
theorem ProbabilityTheory.Kernel.map_apply {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5} { : MeasurableSpace γ} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} {f : βγ} :
map 0 f = 0
@[simp]
theorem ProbabilityTheory.Kernel.map_id {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} (κ : Kernel α β) :
κ.map id = κ
@[simp]
theorem ProbabilityTheory.Kernel.map_id' {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} (κ : Kernel α β) :
(κ.map fun (a : β) => a) = κ
theorem ProbabilityTheory.Kernel.lintegral_map {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (κ : Kernel α β) {f : β ≃ᵐ γ} (η : Kernel α γ) :
κ.map f = η κ = η.map f.symm
theorem ProbabilityTheory.Kernel.sum_map_seq {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} {f : βγ} (κ : Kernel α β) [IsMarkovKernel κ] (hf : Measurable f) :
instance ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.map {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (κ : Kernel α β) [IsZeroOrMarkovKernel κ] (f : βγ) :
instance ProbabilityTheory.Kernel.IsFiniteKernel.map {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (κ : Kernel α β) [IsFiniteKernel κ] (f : βγ) :
instance ProbabilityTheory.Kernel.IsSFiniteKernel.map {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (κ : Kernel α β) [IsSFiniteKernel κ] (f : βγ) :
@[simp]
theorem ProbabilityTheory.Kernel.map_const {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (μ : MeasureTheory.Measure α) {f : αβ} (hf : Measurable f) :
def ProbabilityTheory.Kernel.comap {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (κ : Kernel α β) (g : γα) (hg : Measurable g) :
(κ.comap g hg) = κ g
theorem ProbabilityTheory.Kernel.comap_apply {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} {g : γα} (κ : Kernel α β) (hg : Measurable g) (c : γ) :
(κ.comap g hg) c = κ (g c)
theorem ProbabilityTheory.Kernel.comap_apply' {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} {g : γα} (hg : Measurable g) :
comap 0 g hg = 0
@[simp]
theorem ProbabilityTheory.Kernel.comap_id {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} (κ : Kernel α β) :
κ.comap id = κ
@[simp]
theorem ProbabilityTheory.Kernel.comap_id' {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} (κ : Kernel α β) :
κ.comap (fun (a : α) => a) = κ
theorem ProbabilityTheory.Kernel.lintegral_comap {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} {g : γα} (κ : Kernel α β) [IsMarkovKernel κ] (hg : Measurable g) :
instance ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.comap {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} {g : γα} (κ : Kernel α β) [IsZeroOrMarkovKernel κ] (hg : Measurable g) :
instance ProbabilityTheory.Kernel.IsFiniteKernel.comap {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} {g : γα} (κ : Kernel α β) [IsFiniteKernel κ] (hg : Measurable g) :
instance ProbabilityTheory.Kernel.IsSFiniteKernel.comap {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} {g : γα} (κ : Kernel α β) [IsSFiniteKernel κ] (hg : Measurable g) :
theorem ProbabilityTheory.Kernel.comap_map_comm {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5} { : MeasurableSpace γ} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} {f : αβ} (hf : Measurable f) :
@[simp]
theorem ProbabilityTheory.Kernel.id_comap {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {f : αβ} (hf : Measurable f) :
theorem ProbabilityTheory.Kernel.deterministic_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} (γ : Type u_5) [MeasurableSpace γ] (κ : Kernel α β) :
Kernel (γ × α) β

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

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

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

Equations
@[simp]
theorem ProbabilityTheory.Kernel.prodMkLeft_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α β) (ca : γ × α) :
(prodMkLeft γ κ) ca = κ ca.2
@[simp]
theorem ProbabilityTheory.Kernel.prodMkRight_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α β) (ca : α × γ) :
(prodMkRight γ κ) ca = κ ca.1
theorem ProbabilityTheory.Kernel.prodMkLeft_apply' {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} :
prodMkLeft α 0 = 0
@[simp]
theorem ProbabilityTheory.Kernel.prodMkRight_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} :
prodMkRight α 0 = 0
@[simp]
theorem ProbabilityTheory.Kernel.prodMkLeft_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ η : Kernel α β) :
prodMkLeft γ (κ + η) = prodMkLeft γ κ + prodMkLeft γ η
@[simp]
theorem ProbabilityTheory.Kernel.prodMkRight_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ η : Kernel α β) :
prodMkRight γ (κ + η) = prodMkRight γ κ + prodMkRight γ η
theorem ProbabilityTheory.Kernel.sum_prodMkLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α β) [IsMarkovKernel κ] :
instance ProbabilityTheory.Kernel.IsMarkovKernel.prodMkRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α β) [IsMarkovKernel κ] :
instance ProbabilityTheory.Kernel.IsFiniteKernel.prodMkLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α β) [IsFiniteKernel κ] :
instance ProbabilityTheory.Kernel.IsFiniteKernel.prodMkRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α β) [IsFiniteKernel κ] :
instance ProbabilityTheory.Kernel.IsSFiniteKernel.prodMkLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α β) [IsSFiniteKernel κ] :
theorem ProbabilityTheory.Kernel.map_prodMkLeft {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {δ : Type u_4} { : MeasurableSpace δ} (γ : Type u_5) [MeasurableSpace γ] (κ : Kernel α β) (f : βδ) :
(prodMkLeft γ κ).map f = prodMkLeft γ (κ.map f)
theorem ProbabilityTheory.Kernel.map_prodMkRight {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {δ : Type u_4} { : MeasurableSpace δ} (κ : Kernel α β) (γ : Type u_5) { : MeasurableSpace γ} (f : βδ) :
(prodMkRight γ κ).map f = prodMkRight γ (κ.map f)
def ProbabilityTheory.Kernel.swapLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel (α × β) γ) :
Kernel (β × α) γ

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

Equations
@[simp]
theorem ProbabilityTheory.Kernel.swapLeft_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} :
@[simp]
theorem ProbabilityTheory.Kernel.swapLeft_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : β × α) :
κ.swapLeft a = κ a.swap
theorem ProbabilityTheory.Kernel.swapLeft_apply' {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel (α × β) γ) [IsMarkovKernel κ] :
instance ProbabilityTheory.Kernel.IsFiniteKernel.swapLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel (α × β) γ) [IsFiniteKernel κ] :
instance ProbabilityTheory.Kernel.IsSFiniteKernel.swapLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel (α × β) γ) [IsSFiniteKernel κ] :
@[simp]
theorem ProbabilityTheory.Kernel.swapLeft_prodMkLeft {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} (κ : Kernel α β) (γ : Type u_5) {x✝ : MeasurableSpace γ} :
@[simp]
theorem ProbabilityTheory.Kernel.swapLeft_prodMkRight {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} (κ : Kernel α β) (γ : Type u_5) {x✝ : MeasurableSpace γ} :
noncomputable def ProbabilityTheory.Kernel.swapRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : 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
theorem ProbabilityTheory.Kernel.swapRight_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α (β × γ)) :
@[simp]
theorem ProbabilityTheory.Kernel.swapRight_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} :
theorem ProbabilityTheory.Kernel.swapRight_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α (β × γ)) (a : α) :
theorem ProbabilityTheory.Kernel.swapRight_apply' {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsMarkovKernel κ] :
instance ProbabilityTheory.Kernel.IsFiniteKernel.swapRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsFiniteKernel κ] :
instance ProbabilityTheory.Kernel.IsSFiniteKernel.swapRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsSFiniteKernel κ] :
noncomputable def ProbabilityTheory.Kernel.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α (β × γ)) :
Kernel α β

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

Equations
theorem ProbabilityTheory.Kernel.fst_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α (β × γ)) :
theorem ProbabilityTheory.Kernel.fst_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α (β × γ)) (a : α) :
theorem ProbabilityTheory.Kernel.fst_apply' {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} :
fst 0 = 0
theorem ProbabilityTheory.Kernel.lintegral_fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsMarkovKernel κ] :
instance ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsZeroOrMarkovKernel κ] :
instance ProbabilityTheory.Kernel.IsFiniteKernel.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsFiniteKernel κ] :
instance ProbabilityTheory.Kernel.IsSFiniteKernel.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsSFiniteKernel κ] :
@[instance 100]
instance ProbabilityTheory.Kernel.isFiniteKernel_of_isFiniteKernel_fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} {κ : Kernel α (β × γ)} [h : IsFiniteKernel κ.fst] :
theorem ProbabilityTheory.Kernel.fst_map_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} {δ : Type u_4} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (δ : Type u_5) [MeasurableSpace δ] (κ : Kernel α (β × γ)) :
(prodMkLeft δ κ).fst = prodMkLeft δ κ.fst
theorem ProbabilityTheory.Kernel.fst_prodMkRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α (β × γ)) (δ : Type u_5) [MeasurableSpace δ] :
noncomputable def ProbabilityTheory.Kernel.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α (β × γ)) :
Kernel α γ

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

Equations
theorem ProbabilityTheory.Kernel.snd_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α (β × γ)) :
theorem ProbabilityTheory.Kernel.snd_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α (β × γ)) (a : α) :
theorem ProbabilityTheory.Kernel.snd_apply' {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} :
snd 0 = 0
theorem ProbabilityTheory.Kernel.lintegral_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsMarkovKernel κ] :
instance ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsZeroOrMarkovKernel κ] :
instance ProbabilityTheory.Kernel.IsFiniteKernel.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsFiniteKernel κ] :
instance ProbabilityTheory.Kernel.IsSFiniteKernel.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsSFiniteKernel κ] :
@[instance 100]
instance ProbabilityTheory.Kernel.isFiniteKernel_of_isFiniteKernel_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} {κ : Kernel α (β × γ)} [h : IsFiniteKernel κ.snd] :
theorem ProbabilityTheory.Kernel.snd_map_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} {δ : Type u_4} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (δ : Type u_5) [MeasurableSpace δ] (κ : Kernel α (β × γ)) :
(prodMkLeft δ κ).snd = prodMkLeft δ κ.snd
theorem ProbabilityTheory.Kernel.snd_prodMkRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α (β × γ)) (δ : Type u_5) [MeasurableSpace δ] :
@[simp]
theorem ProbabilityTheory.Kernel.fst_swapRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α (β × γ)) :
@[simp]
theorem ProbabilityTheory.Kernel.snd_swapRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} { : MeasurableSpace β} { : MeasurableSpace γ} (κ : Kernel α (β × γ)) :
noncomputable def ProbabilityTheory.Kernel.sectL {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (κ : Kernel (α × β) γ) (b : β) :
Kernel α γ

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

Equations
@[simp]
theorem ProbabilityTheory.Kernel.sectL_apply {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (κ : Kernel (α × β) γ) (b : β) (a : α) :
(κ.sectL b) a = κ (a, b)
@[simp]
theorem ProbabilityTheory.Kernel.sectL_zero {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (b : β) :
sectL 0 b = 0
instance ProbabilityTheory.Kernel.instIsMarkovKernelSectLOfProd {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (κ : Kernel (α × β) γ) (b : β) [IsMarkovKernel κ] :
instance ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelSectLOfProd {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (κ : Kernel (α × β) γ) (b : β) [IsZeroOrMarkovKernel κ] :
instance ProbabilityTheory.Kernel.instIsFiniteKernelSectLOfProd {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (κ : Kernel (α × β) γ) (b : β) [IsFiniteKernel κ] :
instance ProbabilityTheory.Kernel.instIsSFiniteKernelSectLOfProd {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (κ : Kernel (α × β) γ) (b : β) [IsSFiniteKernel κ] :
instance ProbabilityTheory.Kernel.instNeZeroMeasureCoeSectLOfProdMk {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] :
NeZero ((κ.sectL b) a)
@[instance 100]
instance ProbabilityTheory.Kernel.instIsMarkovKernelProdOfSectL {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} {κ : Kernel (α × β) γ} [∀ (b : β), IsMarkovKernel (κ.sectL b)] :
theorem ProbabilityTheory.Kernel.comap_sectL {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5} { : MeasurableSpace γ} { : 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} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (α : Type u_6) [MeasurableSpace α] (κ : Kernel β γ) (a : α) {b : β} :
((prodMkLeft α κ).sectL b) a = κ b
@[simp]
theorem ProbabilityTheory.Kernel.sectL_prodMkRight {α : Type u_1} { : MeasurableSpace α} {γ : Type u_4} { : MeasurableSpace γ} (β : Type u_6) [MeasurableSpace β] (κ : Kernel α γ) (b : β) :
(prodMkRight β κ).sectL b = κ
noncomputable def ProbabilityTheory.Kernel.sectR {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : α) :
Kernel β γ

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

Equations
@[simp]
theorem ProbabilityTheory.Kernel.sectR_apply {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (κ : Kernel (α × β) γ) (b : β) (a : α) :
(κ.sectR a) b = κ (a, b)
@[simp]
theorem ProbabilityTheory.Kernel.sectR_zero {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (a : α) :
sectR 0 a = 0
instance ProbabilityTheory.Kernel.instIsMarkovKernelSectROfProd {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : α) [IsMarkovKernel κ] :
instance ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelSectROfProd {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : α) [IsZeroOrMarkovKernel κ] :
instance ProbabilityTheory.Kernel.instIsFiniteKernelSectROfProd {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : α) [IsFiniteKernel κ] :
instance ProbabilityTheory.Kernel.instIsSFiniteKernelSectROfProd {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : α) [IsSFiniteKernel κ] :
instance ProbabilityTheory.Kernel.instNeZeroMeasureCoeSectROfProdMk {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] :
NeZero ((κ.sectR a) b)
@[instance 100]
instance ProbabilityTheory.Kernel.instIsMarkovKernelProdOfSectR {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} {κ : Kernel (α × β) γ} [∀ (b : α), IsMarkovKernel (κ.sectR b)] :
theorem ProbabilityTheory.Kernel.comap_sectR {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5} { : MeasurableSpace γ} { : 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} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (α : Type u_6) [MeasurableSpace α] (κ : Kernel β γ) (a : α) :
(prodMkLeft α κ).sectR a = κ
@[simp]
theorem ProbabilityTheory.Kernel.sectR_prodMkRight {α : Type u_1} { : MeasurableSpace α} {γ : Type u_4} { : 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} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (κ : Kernel (α × β) γ) :
@[simp]
theorem ProbabilityTheory.Kernel.sectR_swapRight {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} {γ : Type u_4} { : MeasurableSpace γ} (κ : Kernel (α × β) γ) :