# 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 #

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

Instances For

source
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

Instances For

source
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
source
@[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
source
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)
source
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)
source
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
source
@[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
source
@[simp]
theorem ProbabilityTheory.Kernel.map_id {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) :
κ.map id = κ
source
@[simp]
theorem ProbabilityTheory.Kernel.map_id' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) :
(κ.map fun (a : β) => a) = κ
source
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
source
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
source
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
source
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)
source
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)
source
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)
source
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)
source
@[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 μ)
source
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' := ⋯ }

Instances For

source
@[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
source
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)
source
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
source
@[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
source
@[simp]
theorem ProbabilityTheory.Kernel.comap_id {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) :
κ.comap id ⋯ = κ
source
@[simp]
theorem ProbabilityTheory.Kernel.comap_id' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) :
κ.comap (fun (a : α) => a) ⋯ = κ
source
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)
source
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
source
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)
source
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)
source
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)
source
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)
source
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
source
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
source
@[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
source
@[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
source
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) ⋯
source
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 ⋯

Instances For

source
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 ⋯

Instances For

source
@[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
source
@[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
source
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
source
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
source
@[simp]
theorem ProbabilityTheory.Kernel.prodMkLeft_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} :
prodMkLeft α 0 = 0
source
@[simp]
theorem ProbabilityTheory.Kernel.prodMkRight_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} :
prodMkRight α 0 = 0
source
@[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 γ η
source
@[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 γ η
source
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 κ)
source
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 κ)
source
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
source
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
source
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 γ κ)
source
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 γ κ)
source
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 γ κ)
source
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 γ κ)
source
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 γ κ)
source
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 γ κ)
source
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 γ κ)
source
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 γ κ)
source
theorem ProbabilityTheory.Kernel.isSFiniteKernel_prodMkLeft_unit {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} :
IsSFiniteKernel (prodMkLeft Unit κ) ↔ IsSFiniteKernel κ
source
theorem ProbabilityTheory.Kernel.isSFiniteKernel_prodMkRight_unit {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} :
IsSFiniteKernel (prodMkRight Unit κ) ↔ IsSFiniteKernel κ
source
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)
source
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)
source
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 ⋯

Instances For

source
@[simp]
theorem ProbabilityTheory.Kernel.swapLeft_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} :
swapLeft 0 = 0
source
@[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
source
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
source
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
source
instance ProbabilityTheory.Kernel.IsMarkovKernel.swapLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) [IsMarkovKernel κ] :
IsMarkovKernel κ.swapLeft
source
instance ProbabilityTheory.Kernel.IsFiniteKernel.swapLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) [IsFiniteKernel κ] :
IsFiniteKernel κ.swapLeft
source
instance ProbabilityTheory.Kernel.IsSFiniteKernel.swapLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) [IsSFiniteKernel κ] :
IsSFiniteKernel κ.swapLeft
source
@[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 γ κ
source
@[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 γ κ
source
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 ⋯

Instances For

source
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
source
@[simp]
theorem ProbabilityTheory.Kernel.swapRight_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} :
swapRight 0 = 0
source
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)
source
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}
source
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
source
instance ProbabilityTheory.Kernel.IsMarkovKernel.swapRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsMarkovKernel κ] :
IsMarkovKernel κ.swapRight
source
instance ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.swapRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsZeroOrMarkovKernel κ] :
IsZeroOrMarkovKernel κ.swapRight
source
instance ProbabilityTheory.Kernel.IsFiniteKernel.swapRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsFiniteKernel κ] :
IsFiniteKernel κ.swapRight
source
instance ProbabilityTheory.Kernel.IsSFiniteKernel.swapRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsSFiniteKernel κ] :
IsSFiniteKernel κ.swapRight
source
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 ⋯

Instances For

source
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
source
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)
source
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}
source
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}
source
@[simp]
theorem ProbabilityTheory.Kernel.fst_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} :
fst 0 = 0
source
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
source
instance ProbabilityTheory.Kernel.IsMarkovKernel.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsMarkovKernel κ] :
IsMarkovKernel κ.fst
source
instance ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsZeroOrMarkovKernel κ] :
IsZeroOrMarkovKernel κ.fst
source
instance ProbabilityTheory.Kernel.IsFiniteKernel.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsFiniteKernel κ] :
IsFiniteKernel κ.fst
source
instance ProbabilityTheory.Kernel.IsSFiniteKernel.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsSFiniteKernel κ] :
IsSFiniteKernel κ.fst
source
@[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 κ
source
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
source
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 = κ
source
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
source
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
source
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 ⋯

Instances For

source
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
source
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)
source
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)
source
@[simp]
theorem ProbabilityTheory.Kernel.snd_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} :
snd 0 = 0
source
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
source
instance ProbabilityTheory.Kernel.IsMarkovKernel.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsMarkovKernel κ] :
IsMarkovKernel κ.snd
source
instance ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsZeroOrMarkovKernel κ] :
IsZeroOrMarkovKernel κ.snd
source
instance ProbabilityTheory.Kernel.IsFiniteKernel.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsFiniteKernel κ] :
IsFiniteKernel κ.snd
source
instance ProbabilityTheory.Kernel.IsSFiniteKernel.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsSFiniteKernel κ] :
IsSFiniteKernel κ.snd
source
@[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 κ
source
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
source
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 = κ
source
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
source
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
source
@[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
source
@[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
source
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)) ⋯

Instances For

source
@[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)
source
@[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
source
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)
source
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)
source
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)
source
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)
source
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)
source
@[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 κ
source
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)) ⋯
source
@[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
source
@[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 = κ
source
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)) ⋯

Instances For

source
@[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)
source
@[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
source
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)
source
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)
source
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)
source
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)
source
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)
source
@[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 κ
source
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)) ⋯
source
@[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 = κ
source
@[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
source
@[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
source
@[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
source
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 κ
source
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 κ