Results about the composition-product of measures #
Main definitions #
FooBar
Main statements #
fooBar_unique
Notation #
Implementation details #
Pretty printer defined by notation3 command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Composition of a measure and a kernel.
Defined using MeasureTheory.Measure.bind
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ProbabilityTheory.Measure.map_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(μ : MeasureTheory.Measure α)
(κ : ProbabilityTheory.Kernel α β)
{f : β → γ}
(hf : Measurable f)
:
MeasureTheory.Measure.map f (μ.bind ⇑κ) = μ.bind ⇑(κ.map f)
theorem
ProbabilityTheory.Measure.comp_assoc
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel β γ}
:
(μ.bind ⇑κ).bind ⇑η = μ.bind ⇑(η.comp κ)
theorem
ProbabilityTheory.Measure.comp_deterministic_eq_map
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : Measurable f)
:
μ.bind ⇑(ProbabilityTheory.Kernel.deterministic f hf) = MeasureTheory.Measure.map f μ
theorem
ProbabilityTheory.Measure.comp_id
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
μ.bind ⇑ProbabilityTheory.Kernel.id = μ
theorem
ProbabilityTheory.Measure.comp_eq_snd_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : MeasureTheory.Measure α)
[MeasureTheory.SFinite μ]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsSFiniteKernel κ]
:
μ.bind ⇑κ = (μ.compProd κ).snd
theorem
ProbabilityTheory.Measure.fst_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : MeasureTheory.Measure α)
[MeasureTheory.SFinite μ]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsMarkovKernel κ]
:
(μ.compProd κ).fst = μ
theorem
ProbabilityTheory.Measure.snd_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : MeasureTheory.Measure α)
[MeasureTheory.SFinite μ]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsSFiniteKernel κ]
:
(μ.compProd κ).snd = μ.bind ⇑κ
theorem
ProbabilityTheory.Measure.compProd_eq_comp
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : MeasureTheory.Measure α)
[MeasureTheory.SFinite μ]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsSFiniteKernel κ]
:
μ.compProd κ = μ.bind ⇑(ProbabilityTheory.Kernel.id.prod κ)
theorem
ProbabilityTheory.Measure.compProd_id
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SFinite μ]
:
μ.compProd ProbabilityTheory.Kernel.id = MeasureTheory.Measure.map (fun (x : α) => (x, x)) μ
@[simp]
theorem
ProbabilityTheory.Measure.compProd_const
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite μ]
[MeasureTheory.SFinite ν]
:
μ.compProd (ProbabilityTheory.Kernel.const α ν) = μ.prod ν
The composition product of a measure and a constant kernel is the product between the two measures.
@[simp]
theorem
ProbabilityTheory.Measure.comp_const
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
:
μ.bind ⇑(ProbabilityTheory.Kernel.const α ν) = μ Set.univ • ν
theorem
ProbabilityTheory.Measure.compProd_apply_toReal
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
[MeasureTheory.SFinite μ]
[ProbabilityTheory.IsFiniteKernel κ]
{s : Set (α × β)}
(hs : MeasurableSet s)
:
theorem
ProbabilityTheory.Measure.compProd_univ_toReal
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
[MeasureTheory.SFinite μ]
[ProbabilityTheory.IsFiniteKernel κ]
:
((μ.compProd κ) Set.univ).toReal = ∫ (x : α), ((κ x) Set.univ).toReal ∂μ
theorem
ProbabilityTheory.Measure.fst_sum
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{ι : Type u_4}
(μ : ι → MeasureTheory.Measure (α × β))
:
(MeasureTheory.Measure.sum μ).fst = MeasureTheory.Measure.sum fun (n : ι) => (μ n).fst
theorem
ProbabilityTheory.Measure.snd_sum
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{ι : Type u_4}
(μ : ι → MeasureTheory.Measure (α × β))
:
(MeasureTheory.Measure.sum μ).snd = MeasureTheory.Measure.sum fun (n : ι) => (μ n).snd
instance
ProbabilityTheory.instSFiniteFstOfProd_testingLowerBounds
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure (α × β)}
[MeasureTheory.SFinite μ]
:
MeasureTheory.SFinite μ.fst
Equations
- ⋯ = ⋯
instance
ProbabilityTheory.instSFiniteSndOfProd_testingLowerBounds
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure (α × β)}
[MeasureTheory.SFinite μ]
:
MeasureTheory.SFinite μ.snd
Equations
- ⋯ = ⋯
instance
ProbabilityTheory.instSFiniteBindCoeKernelMeasureOfIsSFiniteKernel_testingLowerBounds
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SFinite μ]
{κ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel κ]
:
MeasureTheory.SFinite (μ.bind ⇑κ)
Equations
- ⋯ = ⋯
instance
ProbabilityTheory.instIsFiniteMeasureBindCoeKernelMeasureOfIsFiniteKernel_testingLowerBounds
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{κ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsFiniteKernel κ]
:
MeasureTheory.IsFiniteMeasure (μ.bind ⇑κ)
Equations
- ⋯ = ⋯
instance
ProbabilityTheory.instIsProbabilityMeasureBindCoeKernelMeasureOfIsMarkovKernel_testingLowerBounds
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsProbabilityMeasure μ]
{κ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsMarkovKernel κ]
:
MeasureTheory.IsProbabilityMeasure (μ.bind ⇑κ)
Equations
- ⋯ = ⋯
theorem
ProbabilityTheory.Measure.fst_swap_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
[MeasureTheory.SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
:
(MeasureTheory.Measure.map Prod.swap (μ.compProd κ)).fst = μ.bind ⇑κ
theorem
ProbabilityTheory.compProd_apply_toReal
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
[MeasureTheory.SFinite μ]
[ProbabilityTheory.IsFiniteKernel κ]
{s : Set (α × β)}
(hs : MeasurableSet s)
:
theorem
ProbabilityTheory.compProd_univ_toReal
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
[MeasureTheory.SFinite μ]
[ProbabilityTheory.IsFiniteKernel κ]
:
((μ.compProd κ) Set.univ).toReal = ∫ (x : α), ((κ x) Set.univ).toReal ∂μ
theorem
ProbabilityTheory.Measure.compProd_apply_univ
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
[MeasureTheory.SFinite μ]
[ProbabilityTheory.IsMarkovKernel κ]
:
(μ.compProd κ) Set.univ = μ Set.univ
theorem
ProbabilityTheory.Measure.comp_apply_univ
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsMarkovKernel κ]
:
(μ.bind ⇑κ) Set.univ = μ Set.univ
@[simp]
theorem
ProbabilityTheory.Measure.fst_add
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure (α × β)}
{ν : MeasureTheory.Measure (α × β)}
:
@[simp]
theorem
ProbabilityTheory.Measure.snd_add
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure (α × β)}
{ν : MeasureTheory.Measure (α × β)}
:
theorem
ProbabilityTheory.Measure.comp_add_right
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
[MeasureTheory.SFinite μ]
[MeasureTheory.SFinite ν]
[ProbabilityTheory.IsSFiniteKernel κ]
:
theorem
ProbabilityTheory.Measure.comp_add_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
[MeasureTheory.SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
:
theorem
ProbabilityTheory.Measure.compProd_smul_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
(a : ENNReal)
[MeasureTheory.SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
:
theorem
ProbabilityTheory.Measure.comp_smul_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
(a : ENNReal)
:
theorem
MeasureTheory.Measure.prod_comp_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure β)
[MeasureTheory.SFinite ν]
(κ : ProbabilityTheory.Kernel β γ)
[ProbabilityTheory.IsSFiniteKernel κ]
:
μ.prod (ν.bind ⇑κ) = (μ.prod ν).bind ⇑(ProbabilityTheory.Kernel.id.parallelComp κ)
theorem
MeasureTheory.Measure.prod_comp_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(μ : MeasureTheory.Measure α)
[MeasureTheory.SFinite μ]
(ν : MeasureTheory.Measure β)
[MeasureTheory.SFinite ν]
(κ : ProbabilityTheory.Kernel α γ)
[ProbabilityTheory.IsSFiniteKernel κ]
:
(μ.bind ⇑κ).prod ν = (μ.prod ν).bind ⇑(κ.parallelComp ProbabilityTheory.Kernel.id)
theorem
ProbabilityTheory.Kernel.parallelComp_comp_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{δ : Type u_4}
{mδ : MeasurableSpace δ}
{α' : Type u_5}
:
∀ {x : MeasurableSpace α'} (κ : ProbabilityTheory.Kernel α β) [inst : ProbabilityTheory.IsSFiniteKernel κ]
(η : ProbabilityTheory.Kernel α' γ) [inst : ProbabilityTheory.IsSFiniteKernel η] (ξ : ProbabilityTheory.Kernel γ δ)
[inst : ProbabilityTheory.IsSFiniteKernel ξ],
κ.parallelComp (ξ.comp η) = (ProbabilityTheory.Kernel.id.parallelComp ξ).comp (κ.parallelComp η)
theorem
ProbabilityTheory.Kernel.parallelComp_comp_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{δ : Type u_4}
{mδ : MeasurableSpace δ}
{α' : Type u_5}
:
∀ {x : MeasurableSpace α'} (κ : ProbabilityTheory.Kernel α β) [inst : ProbabilityTheory.IsSFiniteKernel κ]
(η : ProbabilityTheory.Kernel α' γ) [inst : ProbabilityTheory.IsSFiniteKernel η] (ξ : ProbabilityTheory.Kernel γ δ)
[inst : ProbabilityTheory.IsSFiniteKernel ξ],
(ξ.comp η).parallelComp κ = (ξ.parallelComp ProbabilityTheory.Kernel.id).comp (η.parallelComp κ)
theorem
ProbabilityTheory.Kernel.parallelComp_comm
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{δ : Type u_4}
{mδ : MeasurableSpace δ}
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsSFiniteKernel κ]
(η : ProbabilityTheory.Kernel γ δ)
[ProbabilityTheory.IsSFiniteKernel η]
:
(ProbabilityTheory.Kernel.id.parallelComp κ).comp (η.parallelComp ProbabilityTheory.Kernel.id) = (η.parallelComp ProbabilityTheory.Kernel.id).comp (ProbabilityTheory.Kernel.id.parallelComp κ)
theorem
ProbabilityTheory.Kernel.parallelComp_comp_parallelComp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{α' : Type u_5}
{β' : Type u_6}
{γ' : Type u_7}
{mα' : MeasurableSpace α'}
{mβ' : MeasurableSpace β'}
{mγ' : MeasurableSpace γ'}
{κ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ProbabilityTheory.Kernel β γ}
[ProbabilityTheory.IsSFiniteKernel η]
{κ' : ProbabilityTheory.Kernel α' β'}
[ProbabilityTheory.IsSFiniteKernel κ']
{η' : ProbabilityTheory.Kernel β' γ'}
[ProbabilityTheory.IsSFiniteKernel η']
:
(η.parallelComp η').comp (κ.parallelComp κ') = (η.comp κ).parallelComp (η'.comp κ')
theorem
ProbabilityTheory.Kernel.parallelComp_comp_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{β' : Type u_5}
{γ' : Type u_6}
{mβ' : MeasurableSpace β'}
{mγ' : MeasurableSpace γ'}
{κ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ProbabilityTheory.Kernel β γ}
[ProbabilityTheory.IsSFiniteKernel η]
{κ' : ProbabilityTheory.Kernel α β'}
[ProbabilityTheory.IsSFiniteKernel κ']
{η' : ProbabilityTheory.Kernel β' γ'}
[ProbabilityTheory.IsSFiniteKernel η']
:
(η.parallelComp η').comp (κ.prod κ') = (η.comp κ).prod (η'.comp κ')
theorem
ProbabilityTheory.Kernel.parallelComp_comp_id_left_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{δ : Type u_4}
{mδ : MeasurableSpace δ}
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsSFiniteKernel κ]
(η : ProbabilityTheory.Kernel γ δ)
[ProbabilityTheory.IsSFiniteKernel η]
:
(ProbabilityTheory.Kernel.id.parallelComp η).comp (κ.parallelComp ProbabilityTheory.Kernel.id) = κ.parallelComp η
theorem
ProbabilityTheory.Kernel.parallelComp_comp_id_right_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{δ : Type u_4}
{mδ : MeasurableSpace δ}
{κ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel κ]
(η : ProbabilityTheory.Kernel γ δ)
[ProbabilityTheory.IsSFiniteKernel η]
:
(κ.parallelComp ProbabilityTheory.Kernel.id).comp (ProbabilityTheory.Kernel.id.parallelComp η) = κ.parallelComp η
theorem
ProbabilityTheory.Kernel.parallelComp_comp_id_left_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{δ : Type u_4}
{mδ : MeasurableSpace δ}
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsSFiniteKernel κ]
(η : ProbabilityTheory.Kernel β γ)
[ProbabilityTheory.IsSFiniteKernel η]
:
(ProbabilityTheory.Kernel.id.parallelComp η).comp (ProbabilityTheory.Kernel.id.parallelComp κ) = ProbabilityTheory.Kernel.id.parallelComp (η.comp κ)
theorem
ProbabilityTheory.Kernel.parallelComp_comp_id_right_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel κ]
(η : ProbabilityTheory.Kernel β γ)
[ProbabilityTheory.IsSFiniteKernel η]
:
(η.parallelComp ProbabilityTheory.Kernel.id).comp (κ.parallelComp ProbabilityTheory.Kernel.id) = (η.comp κ).parallelComp ProbabilityTheory.Kernel.id
theorem
ProbabilityTheory.Measure.parallelComp_comp_compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SFinite μ]
{κ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ProbabilityTheory.Kernel β γ}
[ProbabilityTheory.IsSFiniteKernel η]
:
(μ.compProd κ).bind ⇑(ProbabilityTheory.Kernel.id.parallelComp η) = μ.compProd (η.comp κ)
theorem
ProbabilityTheory.Measure.absolutelyContinuous_comp
{α : Type u_1}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α γ}
{η : ProbabilityTheory.Kernel α γ}
[MeasureTheory.SFinite μ]
[MeasureTheory.SFinite ν]
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
(hμν : μ.AbsolutelyContinuous ν)
(hκη : ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
:
(μ.bind ⇑κ).AbsolutelyContinuous (ν.bind ⇑η)
theorem
ProbabilityTheory.Measure.absolutelyContinuous_comp_left
{α : Type u_1}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.SFinite μ]
[MeasureTheory.SFinite ν]
(hμν : μ.AbsolutelyContinuous ν)
(κ : ProbabilityTheory.Kernel α γ)
[ProbabilityTheory.IsSFiniteKernel κ]
:
(μ.bind ⇑κ).AbsolutelyContinuous (ν.bind ⇑κ)
theorem
ProbabilityTheory.Measure.absolutelyContinuous_comp_right
{α : Type u_1}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
(μ : MeasureTheory.Measure α)
{κ : ProbabilityTheory.Kernel α γ}
{η : ProbabilityTheory.Kernel α γ}
[MeasureTheory.SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
(hκη : ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
:
(μ.bind ⇑κ).AbsolutelyContinuous (μ.bind ⇑η)