Markov Kernels #
A kernel from a measurable space α to another measurable space β is a measurable map
α → MeasureTheory.Measure β, where the measurable space instance on measure β is the one defined
in MeasureTheory.Measure.instMeasurableSpace. That is, a kernel κ verifies that for all
measurable sets s of β, a ↦ κ a s is measurable.
Main definitions #
Classes of kernels:
ProbabilityTheory.kernel α β: kernels fromαtoβ, defined as theAddSubmonoidof the measurable functions inα → Measure β.ProbabilityTheory.IsMarkovKernel κ: a kernel fromαtoβis said to be a Markov kernel if for alla : α,k ais a probability measure.ProbabilityTheory.IsFiniteKernel κ: a kernel fromαtoβis said to be finite if there existsC : ℝ≥0∞such thatC < ∞and for alla : α,κ a univ ≤ C. This implies in particular that all measures in the image ofκare finite, but is stronger since it requires a uniform bound. This stronger condition is necessary to ensure that the composition of two finite kernels is finite.ProbabilityTheory.IsSFiniteKernel κ: a kernel is called s-finite if it is a countable sum of finite kernels.
Particular kernels:
ProbabilityTheory.kernel.deterministic (f : α → β) (hf : Measurable f): kernela ↦ Measure.dirac (f a).ProbabilityTheory.kernel.const α (μβ : measure β): constant kernela ↦ μβ.ProbabilityTheory.kernel.restrict κ (hs : MeasurableSet s): kernel for which the image ofa : αis(κ a).restrict s. Integral:∫⁻ b, f b ∂(kernel.restrict κ hs a) = ∫⁻ b in s, f b ∂(κ a)
Main statements #
ProbabilityTheory.kernel.ext_fun: if∫⁻ b, f b ∂(κ a) = ∫⁻ b, f b ∂(η a)for all measurable functionsfand alla, then the two kernelsκandηare equal.
noncomputable def
ProbabilityTheory.kernel
(α : Type u_1)
(β : Type u_2)
[MeasurableSpace α]
[MeasurableSpace β]
:
AddSubmonoid (α → MeasureTheory.Measure β)
A kernel from a measurable space α to another measurable space β is a measurable function
κ : α → Measure β. The measurable space structure on MeasureTheory.Measure β is given by
MeasureTheory.Measure.instMeasurableSpace. A map κ : α → MeasureTheory.Measure β is measurable
iff ∀ s : Set β, MeasurableSet s → Measurable (fun a ↦ κ a s).
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
ProbabilityTheory.instFunLikeSubtypeForAllMeasureMemAddSubmonoidAddZeroClassToAddZeroClassToAddMonoidInstAddCommMonoidInstMembershipInstSetLikeAddSubmonoidKernel
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
:
FunLike (↥(ProbabilityTheory.kernel α β)) α (MeasureTheory.Measure β)
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
ProbabilityTheory.kernel.coeFn_zero
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
:
⇑0 = 0
@[simp]
theorem
ProbabilityTheory.kernel.coeFn_add
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
(η : ↥(ProbabilityTheory.kernel α β))
:
def
ProbabilityTheory.kernel.coeAddHom
(α : Type u_4)
(β : Type u_5)
[MeasurableSpace α]
[MeasurableSpace β]
:
↥(ProbabilityTheory.kernel α β) →+ α → MeasureTheory.Measure β
Coercion to a function as an additive monoid homomorphism.
Equations
Instances For
@[simp]
theorem
ProbabilityTheory.kernel.zero_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(a : α)
:
0 a = 0
@[simp]
theorem
ProbabilityTheory.kernel.coe_finset_sum
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(I : Finset ι)
(κ : ι → ↥(ProbabilityTheory.kernel α β))
:
⇑(Finset.sum I fun (i : ι) => κ i) = Finset.sum I fun (i : ι) => ⇑(κ i)
theorem
ProbabilityTheory.kernel.finset_sum_apply
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(I : Finset ι)
(κ : ι → ↥(ProbabilityTheory.kernel α β))
(a : α)
:
(Finset.sum I fun (i : ι) => κ i) a = Finset.sum I fun (i : ι) => (κ i) a
theorem
ProbabilityTheory.kernel.finset_sum_apply'
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(I : Finset ι)
(κ : ι → ↥(ProbabilityTheory.kernel α β))
(a : α)
(s : Set β)
:
↑↑((Finset.sum I fun (i : ι) => κ i) a) s = Finset.sum I fun (i : ι) => ↑↑((κ i) a) s
class
ProbabilityTheory.IsMarkovKernel
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
:
A kernel is a Markov kernel if every measure in its image is a probability measure.
- isProbabilityMeasure : ∀ (a : α), MeasureTheory.IsProbabilityMeasure (κ a)
Instances
class
ProbabilityTheory.IsFiniteKernel
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
:
A kernel is finite if every measure in its image is finite, with a uniform bound.
Instances
noncomputable def
ProbabilityTheory.IsFiniteKernel.bound
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
[h : ProbabilityTheory.IsFiniteKernel κ]
:
A constant C : ℝ≥0∞ such that C < ∞ (ProbabilityTheory.IsFiniteKernel.bound_lt_top κ) and
for all a : α and s : Set β, κ a s ≤ C (ProbabilityTheory.kernel.measure_le_bound κ a s).
Porting note: TODO: does it make sense to make ProbabilityTheory.IsFiniteKernel.bound the least
possible bound? Should it be an NNReal number?
Equations
- ProbabilityTheory.IsFiniteKernel.bound κ = Exists.choose (_ : ∃ C < ⊤, ∀ (a : α), ↑↑(κ a) Set.univ ≤ C)
Instances For
theorem
ProbabilityTheory.IsFiniteKernel.bound_lt_top
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
[h : ProbabilityTheory.IsFiniteKernel κ]
:
theorem
ProbabilityTheory.IsFiniteKernel.bound_ne_top
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsFiniteKernel κ]
:
theorem
ProbabilityTheory.kernel.measure_le_bound
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
[h : ProbabilityTheory.IsFiniteKernel κ]
(a : α)
(s : Set β)
:
↑↑(κ a) s ≤ ProbabilityTheory.IsFiniteKernel.bound κ
instance
ProbabilityTheory.isFiniteKernel_zero
(α : Type u_4)
(β : Type u_5)
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
:
Equations
- (_ : ProbabilityTheory.IsFiniteKernel 0) = (_ : ProbabilityTheory.IsFiniteKernel 0)
instance
ProbabilityTheory.IsFiniteKernel.add
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
(η : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
:
Equations
- (_ : ProbabilityTheory.IsFiniteKernel (κ + η)) = (_ : ProbabilityTheory.IsFiniteKernel (κ + η))
instance
ProbabilityTheory.IsMarkovKernel.is_probability_measure'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsMarkovKernel κ]
(a : α)
:
Equations
- (_ : MeasureTheory.IsProbabilityMeasure (κ a)) = (_ : MeasureTheory.IsProbabilityMeasure (κ a))
instance
ProbabilityTheory.IsFiniteKernel.isFiniteMeasure
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsFiniteKernel κ]
(a : α)
:
Equations
- (_ : MeasureTheory.IsFiniteMeasure (κ a)) = (_ : MeasureTheory.IsFiniteMeasure (κ a))
instance
ProbabilityTheory.IsMarkovKernel.isFiniteKernel
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsMarkovKernel κ]
:
Equations
- (_ : ProbabilityTheory.IsFiniteKernel κ) = (_ : ProbabilityTheory.IsFiniteKernel κ)
theorem
ProbabilityTheory.kernel.ext
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
{η : ↥(ProbabilityTheory.kernel α β)}
(h : ∀ (a : α), κ a = η a)
:
κ = η
theorem
ProbabilityTheory.kernel.ext_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
{η : ↥(ProbabilityTheory.kernel α β)}
:
theorem
ProbabilityTheory.kernel.ext_iff'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
{η : ↥(ProbabilityTheory.kernel α β)}
:
κ = η ↔ ∀ (a : α) (s : Set β), MeasurableSet s → ↑↑(κ a) s = ↑↑(η a) s
theorem
ProbabilityTheory.kernel.ext_fun
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
{η : ↥(ProbabilityTheory.kernel α β)}
(h : ∀ (a : α) (f : β → ENNReal), Measurable f → ∫⁻ (b : β), f b ∂κ a = ∫⁻ (b : β), f b ∂η a)
:
κ = η
theorem
ProbabilityTheory.kernel.ext_fun_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
{η : ↥(ProbabilityTheory.kernel α β)}
:
κ = η ↔ ∀ (a : α) (f : β → ENNReal), Measurable f → ∫⁻ (b : β), f b ∂κ a = ∫⁻ (b : β), f b ∂η a
theorem
ProbabilityTheory.kernel.measurable
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
:
Measurable ⇑κ
theorem
ProbabilityTheory.kernel.measurable_coe
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
{s : Set β}
(hs : MeasurableSet s)
:
Measurable fun (a : α) => ↑↑(κ a) s
theorem
ProbabilityTheory.kernel.IsFiniteKernel.integrable
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsFiniteKernel κ]
{s : Set β}
(hs : MeasurableSet s)
:
MeasureTheory.Integrable fun (x : α) => ENNReal.toReal (↑↑(κ x) s)
theorem
ProbabilityTheory.kernel.IsMarkovKernel.integrable
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsMarkovKernel κ]
{s : Set β}
(hs : MeasurableSet s)
:
MeasureTheory.Integrable fun (x : α) => ENNReal.toReal (↑↑(κ x) s)
noncomputable def
ProbabilityTheory.kernel.sum
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[Countable ι]
(κ : ι → ↥(ProbabilityTheory.kernel α β))
:
↥(ProbabilityTheory.kernel α β)
Sum of an indexed family of kernels.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ProbabilityTheory.kernel.sum_apply
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[Countable ι]
(κ : ι → ↥(ProbabilityTheory.kernel α β))
(a : α)
:
(ProbabilityTheory.kernel.sum κ) a = MeasureTheory.Measure.sum fun (n : ι) => (κ n) a
theorem
ProbabilityTheory.kernel.sum_apply'
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[Countable ι]
(κ : ι → ↥(ProbabilityTheory.kernel α β))
(a : α)
{s : Set β}
(hs : MeasurableSet s)
:
↑↑((ProbabilityTheory.kernel.sum κ) a) s = ∑' (n : ι), ↑↑((κ n) a) s
@[simp]
theorem
ProbabilityTheory.kernel.sum_zero
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[Countable ι]
:
(ProbabilityTheory.kernel.sum fun (x : ι) => 0) = 0
theorem
ProbabilityTheory.kernel.sum_comm
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[Countable ι]
(κ : ι → ι → ↥(ProbabilityTheory.kernel α β))
:
(ProbabilityTheory.kernel.sum fun (n : ι) => ProbabilityTheory.kernel.sum (κ n)) = ProbabilityTheory.kernel.sum fun (m : ι) => ProbabilityTheory.kernel.sum fun (n : ι) => κ n m
@[simp]
theorem
ProbabilityTheory.kernel.sum_fintype
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[Fintype ι]
(κ : ι → ↥(ProbabilityTheory.kernel α β))
:
ProbabilityTheory.kernel.sum κ = Finset.sum Finset.univ fun (i : ι) => κ i
theorem
ProbabilityTheory.kernel.sum_add
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[Countable ι]
(κ : ι → ↥(ProbabilityTheory.kernel α β))
(η : ι → ↥(ProbabilityTheory.kernel α β))
:
(ProbabilityTheory.kernel.sum fun (n : ι) => κ n + η n) = ProbabilityTheory.kernel.sum κ + ProbabilityTheory.kernel.sum η
class
ProbabilityTheory.IsSFiniteKernel
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
:
A kernel is s-finite if it can be written as the sum of countably many finite kernels.
- tsum_finite : ∃ (κs : ℕ → ↥(ProbabilityTheory.kernel α β)), (∀ (n : ℕ), ProbabilityTheory.IsFiniteKernel (κs n)) ∧ κ = ProbabilityTheory.kernel.sum κs
Instances
instance
ProbabilityTheory.kernel.IsFiniteKernel.isSFiniteKernel
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
[h : ProbabilityTheory.IsFiniteKernel κ]
:
Equations
- (_ : ProbabilityTheory.IsSFiniteKernel κ) = (_ : ProbabilityTheory.IsSFiniteKernel κ)
noncomputable def
ProbabilityTheory.kernel.seq
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
[h : ProbabilityTheory.IsSFiniteKernel κ]
:
ℕ → ↥(ProbabilityTheory.kernel α β)
A sequence of finite kernels such that κ = ProbabilityTheory.kernel.sum (seq κ). See
ProbabilityTheory.kernel.isFiniteKernel_seq and ProbabilityTheory.kernel.kernel_sum_seq.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ProbabilityTheory.kernel.kernel_sum_seq
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
[h : ProbabilityTheory.IsSFiniteKernel κ]
:
theorem
ProbabilityTheory.kernel.measure_sum_seq
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
[h : ProbabilityTheory.IsSFiniteKernel κ]
(a : α)
:
(MeasureTheory.Measure.sum fun (n : ℕ) => (ProbabilityTheory.kernel.seq κ n) a) = κ a
instance
ProbabilityTheory.kernel.isFiniteKernel_seq
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
[h : ProbabilityTheory.IsSFiniteKernel κ]
(n : ℕ)
:
Equations
- One or more equations did not get rendered due to their size.
instance
ProbabilityTheory.kernel.IsSFiniteKernel.sFinite
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
(a : α)
:
MeasureTheory.SFinite (κ a)
Equations
- (_ : MeasureTheory.SFinite (κ a)) = (_ : MeasureTheory.SFinite (κ a))
instance
ProbabilityTheory.kernel.IsSFiniteKernel.add
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
(η : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
:
Equations
- (_ : ProbabilityTheory.IsSFiniteKernel (κ + η)) = (_ : ProbabilityTheory.IsSFiniteKernel (κ + η))
theorem
ProbabilityTheory.kernel.IsSFiniteKernel.finset_sum
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κs : ι → ↥(ProbabilityTheory.kernel α β)}
(I : Finset ι)
(h : ∀ i ∈ I, ProbabilityTheory.IsSFiniteKernel (κs i))
:
ProbabilityTheory.IsSFiniteKernel (Finset.sum I fun (i : ι) => κs i)
theorem
ProbabilityTheory.kernel.isSFiniteKernel_sum_of_denumerable
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[Denumerable ι]
{κs : ι → ↥(ProbabilityTheory.kernel α β)}
(hκs : ∀ (n : ι), ProbabilityTheory.IsSFiniteKernel (κs n))
:
theorem
ProbabilityTheory.kernel.isSFiniteKernel_sum
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[Countable ι]
{κs : ι → ↥(ProbabilityTheory.kernel α β)}
(hκs : ∀ (n : ι), ProbabilityTheory.IsSFiniteKernel (κs n))
:
noncomputable def
ProbabilityTheory.kernel.deterministic
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(f : α → β)
(hf : Measurable f)
:
↥(ProbabilityTheory.kernel α β)
Kernel which to a associates the dirac measure at f a. This is a Markov kernel.
Equations
- ProbabilityTheory.kernel.deterministic f hf = { val := fun (a : α) => MeasureTheory.Measure.dirac (f a), property := (_ : Measurable fun (a : α) => MeasureTheory.Measure.dirac (f a)) }
Instances For
theorem
ProbabilityTheory.kernel.deterministic_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : α → β}
(hf : Measurable f)
(a : α)
:
(ProbabilityTheory.kernel.deterministic f hf) a = MeasureTheory.Measure.dirac (f a)
theorem
ProbabilityTheory.kernel.deterministic_apply'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : α → β}
(hf : Measurable f)
(a : α)
{s : Set β}
(hs : MeasurableSet s)
:
↑↑((ProbabilityTheory.kernel.deterministic f hf) a) s = Set.indicator s (fun (x : β) => 1) (f a)
instance
ProbabilityTheory.kernel.isMarkovKernel_deterministic
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : α → β}
(hf : Measurable f)
:
Equations
theorem
ProbabilityTheory.kernel.lintegral_deterministic'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : β → ENNReal}
{g : α → β}
{a : α}
(hg : Measurable g)
(hf : Measurable f)
:
∫⁻ (x : β), f x ∂(ProbabilityTheory.kernel.deterministic g hg) a = f (g a)
@[simp]
theorem
ProbabilityTheory.kernel.lintegral_deterministic
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : β → ENNReal}
{g : α → β}
{a : α}
(hg : Measurable g)
[MeasurableSingletonClass β]
:
∫⁻ (x : β), f x ∂(ProbabilityTheory.kernel.deterministic g hg) a = f (g a)
theorem
ProbabilityTheory.kernel.set_lintegral_deterministic'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : β → ENNReal}
{g : α → β}
{a : α}
(hg : Measurable g)
(hf : Measurable f)
{s : Set β}
(hs : MeasurableSet s)
[Decidable (g a ∈ s)]
:
∫⁻ (x : β) in s, f x ∂(ProbabilityTheory.kernel.deterministic g hg) a = if g a ∈ s then f (g a) else 0
@[simp]
theorem
ProbabilityTheory.kernel.set_lintegral_deterministic
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : β → ENNReal}
{g : α → β}
{a : α}
(hg : Measurable g)
[MeasurableSingletonClass β]
(s : Set β)
[Decidable (g a ∈ s)]
:
∫⁻ (x : β) in s, f x ∂(ProbabilityTheory.kernel.deterministic g hg) a = if g a ∈ s then f (g a) else 0
theorem
ProbabilityTheory.kernel.integral_deterministic'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : β → E}
{g : α → β}
{a : α}
(hg : Measurable g)
(hf : MeasureTheory.StronglyMeasurable f)
:
∫ (x : β), f x ∂(ProbabilityTheory.kernel.deterministic g hg) a = f (g a)
@[simp]
theorem
ProbabilityTheory.kernel.integral_deterministic
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : β → E}
{g : α → β}
{a : α}
(hg : Measurable g)
[MeasurableSingletonClass β]
:
∫ (x : β), f x ∂(ProbabilityTheory.kernel.deterministic g hg) a = f (g a)
theorem
ProbabilityTheory.kernel.set_integral_deterministic'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : β → E}
{g : α → β}
{a : α}
(hg : Measurable g)
(hf : MeasureTheory.StronglyMeasurable f)
{s : Set β}
(hs : MeasurableSet s)
[Decidable (g a ∈ s)]
:
∫ (x : β) in s, f x ∂(ProbabilityTheory.kernel.deterministic g hg) a = if g a ∈ s then f (g a) else 0
@[simp]
theorem
ProbabilityTheory.kernel.set_integral_deterministic
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : β → E}
{g : α → β}
{a : α}
(hg : Measurable g)
[MeasurableSingletonClass β]
(s : Set β)
[Decidable (g a ∈ s)]
:
∫ (x : β) in s, f x ∂(ProbabilityTheory.kernel.deterministic g hg) a = if g a ∈ s then f (g a) else 0
def
ProbabilityTheory.kernel.const
(α : Type u_4)
{β : Type u_5}
[MeasurableSpace α]
:
{x : MeasurableSpace β} → MeasureTheory.Measure β → ↥(ProbabilityTheory.kernel α β)
Constant kernel, which always returns the same measure.
Equations
- ProbabilityTheory.kernel.const α μβ = { val := fun (x : α) => μβ, property := (_ : Measurable fun (x : α) => μβ) }
Instances For
@[simp]
theorem
ProbabilityTheory.kernel.const_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μβ : MeasureTheory.Measure β)
(a : α)
:
(ProbabilityTheory.kernel.const α μβ) a = μβ
@[simp]
theorem
ProbabilityTheory.kernel.const_zero
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
:
theorem
ProbabilityTheory.kernel.sum_const
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[Countable ι]
(μ : ι → MeasureTheory.Measure β)
:
(ProbabilityTheory.kernel.sum fun (n : ι) => ProbabilityTheory.kernel.const α (μ n)) = ProbabilityTheory.kernel.const α (MeasureTheory.Measure.sum μ)
instance
ProbabilityTheory.kernel.isFiniteKernel_const
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μβ : MeasureTheory.Measure β}
[MeasureTheory.IsFiniteMeasure μβ]
:
Equations
instance
ProbabilityTheory.kernel.isSFiniteKernel_const
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μβ : MeasureTheory.Measure β}
[MeasureTheory.SFinite μβ]
:
Equations
instance
ProbabilityTheory.kernel.isMarkovKernel_const
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μβ : MeasureTheory.Measure β}
[hμβ : MeasureTheory.IsProbabilityMeasure μβ]
:
Equations
@[simp]
theorem
ProbabilityTheory.kernel.lintegral_const
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : β → ENNReal}
{μ : MeasureTheory.Measure β}
{a : α}
:
∫⁻ (x : β), f x ∂(ProbabilityTheory.kernel.const α μ) a = ∫⁻ (x : β), f x ∂μ
@[simp]
theorem
ProbabilityTheory.kernel.set_lintegral_const
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : β → ENNReal}
{μ : MeasureTheory.Measure β}
{a : α}
{s : Set β}
:
∫⁻ (x : β) in s, f x ∂(ProbabilityTheory.kernel.const α μ) a = ∫⁻ (x : β) in s, f x ∂μ
@[simp]
theorem
ProbabilityTheory.kernel.integral_const
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : β → E}
{μ : MeasureTheory.Measure β}
{a : α}
:
∫ (x : β), f x ∂(ProbabilityTheory.kernel.const α μ) a = ∫ (x : β), f x ∂μ
@[simp]
theorem
ProbabilityTheory.kernel.set_integral_const
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : β → E}
{μ : MeasureTheory.Measure β}
{a : α}
{s : Set β}
:
∫ (x : β) in s, f x ∂(ProbabilityTheory.kernel.const α μ) a = ∫ (x : β) in s, f x ∂μ
def
ProbabilityTheory.kernel.ofFunOfCountable
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
:
{x : MeasurableSpace β} →
[inst : Countable α] →
[inst : MeasurableSingletonClass α] → (α → MeasureTheory.Measure β) → ↥(ProbabilityTheory.kernel α β)
In a countable space with measurable singletons, every function α → MeasureTheory.Measure β
defines a kernel.
Equations
- ProbabilityTheory.kernel.ofFunOfCountable f = { val := f, property := (_ : Measurable f) }
Instances For
noncomputable def
ProbabilityTheory.kernel.restrict
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{s : Set β}
(κ : ↥(ProbabilityTheory.kernel α β))
(hs : MeasurableSet s)
:
↥(ProbabilityTheory.kernel α β)
Kernel given by the restriction of the measures in the image of a kernel to a set.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ProbabilityTheory.kernel.restrict_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{s : Set β}
(κ : ↥(ProbabilityTheory.kernel α β))
(hs : MeasurableSet s)
(a : α)
:
(ProbabilityTheory.kernel.restrict κ hs) a = MeasureTheory.Measure.restrict (κ a) s
theorem
ProbabilityTheory.kernel.restrict_apply'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{s : Set β}
{t : Set β}
(κ : ↥(ProbabilityTheory.kernel α β))
(hs : MeasurableSet s)
(a : α)
(ht : MeasurableSet t)
:
↑↑((ProbabilityTheory.kernel.restrict κ hs) a) t = ↑↑(κ a) (t ∩ s)
@[simp]
theorem
ProbabilityTheory.kernel.restrict_univ
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
:
ProbabilityTheory.kernel.restrict κ (_ : MeasurableSet Set.univ) = κ
@[simp]
theorem
ProbabilityTheory.kernel.lintegral_restrict
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{s : Set β}
(κ : ↥(ProbabilityTheory.kernel α β))
(hs : MeasurableSet s)
(a : α)
(f : β → ENNReal)
:
∫⁻ (b : β), f b ∂(ProbabilityTheory.kernel.restrict κ hs) a = ∫⁻ (b : β) in s, f b ∂κ a
@[simp]
theorem
ProbabilityTheory.kernel.set_lintegral_restrict
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{s : Set β}
(κ : ↥(ProbabilityTheory.kernel α β))
(hs : MeasurableSet s)
(a : α)
(f : β → ENNReal)
(t : Set β)
:
∫⁻ (b : β) in t, f b ∂(ProbabilityTheory.kernel.restrict κ hs) a = ∫⁻ (b : β) in t ∩ s, f b ∂κ a
@[simp]
theorem
ProbabilityTheory.kernel.set_integral_restrict
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
{s : Set β}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : β → E}
{a : α}
(hs : MeasurableSet s)
(t : Set β)
:
∫ (x : β) in t, f x ∂(ProbabilityTheory.kernel.restrict κ hs) a = ∫ (x : β) in t ∩ s, f x ∂κ a
instance
ProbabilityTheory.kernel.IsFiniteKernel.restrict
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{s : Set β}
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsFiniteKernel κ]
(hs : MeasurableSet s)
:
Equations
instance
ProbabilityTheory.kernel.IsSFiniteKernel.restrict
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{s : Set β}
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsSFiniteKernel κ]
(hs : MeasurableSet s)
:
Equations
noncomputable def
ProbabilityTheory.kernel.comapRight
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
{f : γ → β}
(κ : ↥(ProbabilityTheory.kernel α β))
(hf : MeasurableEmbedding f)
:
↥(ProbabilityTheory.kernel α γ)
Kernel with value (κ a).comap f, for a measurable embedding f. That is, for a measurable set
t : Set β, ProbabilityTheory.kernel.comapRight κ hf a t = κ a (f '' t).
Equations
- ProbabilityTheory.kernel.comapRight κ hf = { val := fun (a : α) => MeasureTheory.Measure.comap f (κ a), property := (_ : Measurable fun (a : α) => MeasureTheory.Measure.comap f (κ a)) }
Instances For
theorem
ProbabilityTheory.kernel.comapRight_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
{f : γ → β}
(κ : ↥(ProbabilityTheory.kernel α β))
(hf : MeasurableEmbedding f)
(a : α)
:
(ProbabilityTheory.kernel.comapRight κ hf) a = MeasureTheory.Measure.comap f (κ a)
theorem
ProbabilityTheory.kernel.comapRight_apply'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
{f : γ → β}
(κ : ↥(ProbabilityTheory.kernel α β))
(hf : MeasurableEmbedding f)
(a : α)
{t : Set γ}
(ht : MeasurableSet t)
:
↑↑((ProbabilityTheory.kernel.comapRight κ hf) a) t = ↑↑(κ a) (f '' t)
theorem
ProbabilityTheory.kernel.IsMarkovKernel.comapRight
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
{f : γ → β}
(κ : ↥(ProbabilityTheory.kernel α β))
(hf : MeasurableEmbedding f)
(hκ : ∀ (a : α), ↑↑(κ a) (Set.range f) = 1)
:
instance
ProbabilityTheory.kernel.IsFiniteKernel.comapRight
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
{f : γ → β}
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsFiniteKernel κ]
(hf : MeasurableEmbedding f)
:
Equations
instance
ProbabilityTheory.kernel.IsSFiniteKernel.comapRight
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
{f : γ → β}
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsSFiniteKernel κ]
(hf : MeasurableEmbedding f)
:
Equations
def
ProbabilityTheory.kernel.piecewise
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{s : Set α}
[DecidablePred fun (x : α) => x ∈ s]
(hs : MeasurableSet s)
(κ : ↥(ProbabilityTheory.kernel α β))
(η : ↥(ProbabilityTheory.kernel α β))
:
↥(ProbabilityTheory.kernel α β)
ProbabilityTheory.kernel.piecewise hs κ η is the kernel equal to κ on the measurable set s
and to η on its complement.
Equations
- ProbabilityTheory.kernel.piecewise hs κ η = { val := fun (a : α) => if a ∈ s then κ a else η a, property := (_ : Measurable (Set.piecewise s (fun (a : α) => κ a) fun (a : α) => η a)) }
Instances For
theorem
ProbabilityTheory.kernel.piecewise_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
{η : ↥(ProbabilityTheory.kernel α β)}
{s : Set α}
{hs : MeasurableSet s}
[DecidablePred fun (x : α) => x ∈ s]
(a : α)
:
(ProbabilityTheory.kernel.piecewise hs κ η) a = if a ∈ s then κ a else η a
theorem
ProbabilityTheory.kernel.piecewise_apply'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
{η : ↥(ProbabilityTheory.kernel α β)}
{s : Set α}
{hs : MeasurableSet s}
[DecidablePred fun (x : α) => x ∈ s]
(a : α)
(t : Set β)
:
↑↑((ProbabilityTheory.kernel.piecewise hs κ η) a) t = if a ∈ s then ↑↑(κ a) t else ↑↑(η a) t
instance
ProbabilityTheory.kernel.IsMarkovKernel.piecewise
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
{η : ↥(ProbabilityTheory.kernel α β)}
{s : Set α}
{hs : MeasurableSet s}
[DecidablePred fun (x : α) => x ∈ s]
[ProbabilityTheory.IsMarkovKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
:
Equations
- (_ : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.kernel.piecewise hs κ η)) = (_ : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.kernel.piecewise hs κ η))
instance
ProbabilityTheory.kernel.IsFiniteKernel.piecewise
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
{η : ↥(ProbabilityTheory.kernel α β)}
{s : Set α}
{hs : MeasurableSet s}
[DecidablePred fun (x : α) => x ∈ s]
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
:
Equations
- (_ : ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.kernel.piecewise hs κ η)) = (_ : ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.kernel.piecewise hs κ η))
instance
ProbabilityTheory.kernel.IsSFiniteKernel.piecewise
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
{η : ↥(ProbabilityTheory.kernel α β)}
{s : Set α}
{hs : MeasurableSet s}
[DecidablePred fun (x : α) => x ∈ s]
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
:
Equations
- (_ : ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.kernel.piecewise hs κ η)) = (_ : ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.kernel.piecewise hs κ η))
theorem
ProbabilityTheory.kernel.lintegral_piecewise
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
{η : ↥(ProbabilityTheory.kernel α β)}
{s : Set α}
{hs : MeasurableSet s}
[DecidablePred fun (x : α) => x ∈ s]
(a : α)
(g : β → ENNReal)
:
∫⁻ (b : β), g b ∂(ProbabilityTheory.kernel.piecewise hs κ η) a = if a ∈ s then ∫⁻ (b : β), g b ∂κ a else ∫⁻ (b : β), g b ∂η a
theorem
ProbabilityTheory.kernel.set_lintegral_piecewise
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
{η : ↥(ProbabilityTheory.kernel α β)}
{s : Set α}
{hs : MeasurableSet s}
[DecidablePred fun (x : α) => x ∈ s]
(a : α)
(g : β → ENNReal)
(t : Set β)
:
∫⁻ (b : β) in t, g b ∂(ProbabilityTheory.kernel.piecewise hs κ η) a = if a ∈ s then ∫⁻ (b : β) in t, g b ∂κ a else ∫⁻ (b : β) in t, g b ∂η a
theorem
ProbabilityTheory.kernel.integral_piecewise
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
{η : ↥(ProbabilityTheory.kernel α β)}
{s : Set α}
{hs : MeasurableSet s}
[DecidablePred fun (x : α) => x ∈ s]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(a : α)
(g : β → E)
:
∫ (b : β), g b ∂(ProbabilityTheory.kernel.piecewise hs κ η) a = if a ∈ s then ∫ (b : β), g b ∂κ a else ∫ (b : β), g b ∂η a
theorem
ProbabilityTheory.kernel.set_integral_piecewise
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
{η : ↥(ProbabilityTheory.kernel α β)}
{s : Set α}
{hs : MeasurableSet s}
[DecidablePred fun (x : α) => x ∈ s]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(a : α)
(g : β → E)
(t : Set β)
:
∫ (b : β) in t, g b ∂(ProbabilityTheory.kernel.piecewise hs κ η) a = if a ∈ s then ∫ (b : β) in t, g b ∂κ a else ∫ (b : β) in t, g b ∂η a