Lebesgue and Bochner integrals of conditional kernels #
Integrals of ProbabilityTheory.Kernel.condKernel and MeasureTheory.Measure.condKernel.
Main statements #
ProbabilityTheory.setIntegral_condKernel: the integral∫ b in s, ∫ ω in t, f (b, ω) ∂(Kernel.condKernel κ (a, b)) ∂(Kernel.fst κ a)is equal to∫ x in s ×ˢ t, f x ∂(κ a).MeasureTheory.Measure.setIntegral_condKernel:∫ b in s, ∫ ω in t, f (b, ω) ∂(ρ.condKernel b) ∂ρ.fst = ∫ x in s ×ˢ t, f x ∂ρ
Corresponding statements for the Lebesgue integral and/or without the sets s and t are also
provided.
theorem
ProbabilityTheory.lintegral_condKernel_mem
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSpace.CountableOrCountablyGenerated α β]
{κ : ProbabilityTheory.Kernel α (β × Ω)}
[ProbabilityTheory.IsFiniteKernel κ]
(a : α)
{s : Set (β × Ω)}
(hs : MeasurableSet s)
:
theorem
ProbabilityTheory.setLIntegral_condKernel_eq_measure_prod
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSpace.CountableOrCountablyGenerated α β]
{κ : ProbabilityTheory.Kernel α (β × Ω)}
[ProbabilityTheory.IsFiniteKernel κ]
(a : α)
{s : Set β}
(hs : MeasurableSet s)
{t : Set Ω}
(ht : MeasurableSet t)
:
@[deprecated ProbabilityTheory.setLIntegral_condKernel_eq_measure_prod]
theorem
ProbabilityTheory.set_lintegral_condKernel_eq_measure_prod
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSpace.CountableOrCountablyGenerated α β]
{κ : ProbabilityTheory.Kernel α (β × Ω)}
[ProbabilityTheory.IsFiniteKernel κ]
(a : α)
{s : Set β}
(hs : MeasurableSet s)
{t : Set Ω}
(ht : MeasurableSet t)
:
Alias of ProbabilityTheory.setLIntegral_condKernel_eq_measure_prod.
theorem
ProbabilityTheory.lintegral_condKernel
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSpace.CountableOrCountablyGenerated α β]
{κ : ProbabilityTheory.Kernel α (β × Ω)}
[ProbabilityTheory.IsFiniteKernel κ]
{f : β × Ω → ENNReal}
(hf : Measurable f)
(a : α)
:
theorem
ProbabilityTheory.setLIntegral_condKernel
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSpace.CountableOrCountablyGenerated α β]
{κ : ProbabilityTheory.Kernel α (β × Ω)}
[ProbabilityTheory.IsFiniteKernel κ]
{f : β × Ω → ENNReal}
(hf : Measurable f)
(a : α)
{s : Set β}
(hs : MeasurableSet s)
{t : Set Ω}
(ht : MeasurableSet t)
:
@[deprecated ProbabilityTheory.setLIntegral_condKernel]
theorem
ProbabilityTheory.set_lintegral_condKernel
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSpace.CountableOrCountablyGenerated α β]
{κ : ProbabilityTheory.Kernel α (β × Ω)}
[ProbabilityTheory.IsFiniteKernel κ]
{f : β × Ω → ENNReal}
(hf : Measurable f)
(a : α)
{s : Set β}
(hs : MeasurableSet s)
{t : Set Ω}
(ht : MeasurableSet t)
:
theorem
ProbabilityTheory.setLIntegral_condKernel_univ_right
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSpace.CountableOrCountablyGenerated α β]
{κ : ProbabilityTheory.Kernel α (β × Ω)}
[ProbabilityTheory.IsFiniteKernel κ]
{f : β × Ω → ENNReal}
(hf : Measurable f)
(a : α)
{s : Set β}
(hs : MeasurableSet s)
:
@[deprecated ProbabilityTheory.setLIntegral_condKernel_univ_right]
theorem
ProbabilityTheory.set_lintegral_condKernel_univ_right
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSpace.CountableOrCountablyGenerated α β]
{κ : ProbabilityTheory.Kernel α (β × Ω)}
[ProbabilityTheory.IsFiniteKernel κ]
{f : β × Ω → ENNReal}
(hf : Measurable f)
(a : α)
{s : Set β}
(hs : MeasurableSet s)
:
Alias of ProbabilityTheory.setLIntegral_condKernel_univ_right.
theorem
ProbabilityTheory.setLIntegral_condKernel_univ_left
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSpace.CountableOrCountablyGenerated α β]
{κ : ProbabilityTheory.Kernel α (β × Ω)}
[ProbabilityTheory.IsFiniteKernel κ]
{f : β × Ω → ENNReal}
(hf : Measurable f)
(a : α)
{t : Set Ω}
(ht : MeasurableSet t)
:
@[deprecated ProbabilityTheory.setLIntegral_condKernel_univ_left]
theorem
ProbabilityTheory.set_lintegral_condKernel_univ_left
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSpace.CountableOrCountablyGenerated α β]
{κ : ProbabilityTheory.Kernel α (β × Ω)}
[ProbabilityTheory.IsFiniteKernel κ]
{f : β × Ω → ENNReal}
(hf : Measurable f)
(a : α)
{t : Set Ω}
(ht : MeasurableSet t)
:
Alias of ProbabilityTheory.setLIntegral_condKernel_univ_left.
theorem
MeasureTheory.AEStronglyMeasurable.integral_kernel_condKernel
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSpace.CountableOrCountablyGenerated α β]
{κ : ProbabilityTheory.Kernel α (β × Ω)}
[ProbabilityTheory.IsFiniteKernel κ]
{E : Type u_4}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(a : α)
(hf : MeasureTheory.AEStronglyMeasurable f (κ a))
:
MeasureTheory.AEStronglyMeasurable (fun (x : β) => ∫ (y : Ω), f (x, y) ∂κ.condKernel (a, x)) (κ.fst a)
theorem
ProbabilityTheory.integral_condKernel
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSpace.CountableOrCountablyGenerated α β]
{κ : ProbabilityTheory.Kernel α (β × Ω)}
[ProbabilityTheory.IsFiniteKernel κ]
{E : Type u_4}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(a : α)
(hf : MeasureTheory.Integrable f (κ a))
:
theorem
ProbabilityTheory.setIntegral_condKernel
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSpace.CountableOrCountablyGenerated α β]
{κ : ProbabilityTheory.Kernel α (β × Ω)}
[ProbabilityTheory.IsFiniteKernel κ]
{E : Type u_4}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(a : α)
{s : Set β}
(hs : MeasurableSet s)
{t : Set Ω}
(ht : MeasurableSet t)
(hf : MeasureTheory.IntegrableOn f (s ×ˢ t) (κ a))
:
@[deprecated ProbabilityTheory.setIntegral_condKernel]
theorem
ProbabilityTheory.set_integral_condKernel
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSpace.CountableOrCountablyGenerated α β]
{κ : ProbabilityTheory.Kernel α (β × Ω)}
[ProbabilityTheory.IsFiniteKernel κ]
{E : Type u_4}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(a : α)
{s : Set β}
(hs : MeasurableSet s)
{t : Set Ω}
(ht : MeasurableSet t)
(hf : MeasureTheory.IntegrableOn f (s ×ˢ t) (κ a))
:
Alias of ProbabilityTheory.setIntegral_condKernel.
theorem
ProbabilityTheory.setIntegral_condKernel_univ_right
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSpace.CountableOrCountablyGenerated α β]
{κ : ProbabilityTheory.Kernel α (β × Ω)}
[ProbabilityTheory.IsFiniteKernel κ]
{E : Type u_4}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(a : α)
{s : Set β}
(hs : MeasurableSet s)
(hf : MeasureTheory.IntegrableOn f (s ×ˢ Set.univ) (κ a))
:
@[deprecated ProbabilityTheory.setIntegral_condKernel_univ_right]
theorem
ProbabilityTheory.set_integral_condKernel_univ_right
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSpace.CountableOrCountablyGenerated α β]
{κ : ProbabilityTheory.Kernel α (β × Ω)}
[ProbabilityTheory.IsFiniteKernel κ]
{E : Type u_4}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(a : α)
{s : Set β}
(hs : MeasurableSet s)
(hf : MeasureTheory.IntegrableOn f (s ×ˢ Set.univ) (κ a))
:
Alias of ProbabilityTheory.setIntegral_condKernel_univ_right.
theorem
ProbabilityTheory.setIntegral_condKernel_univ_left
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSpace.CountableOrCountablyGenerated α β]
{κ : ProbabilityTheory.Kernel α (β × Ω)}
[ProbabilityTheory.IsFiniteKernel κ]
{E : Type u_4}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(a : α)
{t : Set Ω}
(ht : MeasurableSet t)
(hf : MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) (κ a))
:
@[deprecated ProbabilityTheory.setIntegral_condKernel_univ_left]
theorem
ProbabilityTheory.set_integral_condKernel_univ_left
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSpace.CountableOrCountablyGenerated α β]
{κ : ProbabilityTheory.Kernel α (β × Ω)}
[ProbabilityTheory.IsFiniteKernel κ]
{E : Type u_4}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(a : α)
{t : Set Ω}
(ht : MeasurableSet t)
(hf : MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) (κ a))
:
Alias of ProbabilityTheory.setIntegral_condKernel_univ_left.
theorem
MeasureTheory.Measure.lintegral_condKernel_mem
{β : Type u_1}
{Ω : Type u_2}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{s : Set (β × Ω)}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.Measure.setLIntegral_condKernel_eq_measure_prod
{β : Type u_1}
{Ω : Type u_2}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{s : Set β}
(hs : MeasurableSet s)
{t : Set Ω}
(ht : MeasurableSet t)
:
@[deprecated MeasureTheory.Measure.setLIntegral_condKernel_eq_measure_prod]
theorem
MeasureTheory.Measure.set_lintegral_condKernel_eq_measure_prod
{β : Type u_1}
{Ω : Type u_2}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{s : Set β}
(hs : MeasurableSet s)
{t : Set Ω}
(ht : MeasurableSet t)
:
Alias of MeasureTheory.Measure.setLIntegral_condKernel_eq_measure_prod.
theorem
MeasureTheory.Measure.lintegral_condKernel
{β : Type u_1}
{Ω : Type u_2}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : β × Ω → ENNReal}
(hf : Measurable f)
:
theorem
MeasureTheory.Measure.setLIntegral_condKernel
{β : Type u_1}
{Ω : Type u_2}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : β × Ω → ENNReal}
(hf : Measurable f)
{s : Set β}
(hs : MeasurableSet s)
{t : Set Ω}
(ht : MeasurableSet t)
:
@[deprecated MeasureTheory.Measure.setLIntegral_condKernel]
theorem
MeasureTheory.Measure.set_lintegral_condKernel
{β : Type u_1}
{Ω : Type u_2}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : β × Ω → ENNReal}
(hf : Measurable f)
{s : Set β}
(hs : MeasurableSet s)
{t : Set Ω}
(ht : MeasurableSet t)
:
theorem
MeasureTheory.Measure.setLIntegral_condKernel_univ_right
{β : Type u_1}
{Ω : Type u_2}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : β × Ω → ENNReal}
(hf : Measurable f)
{s : Set β}
(hs : MeasurableSet s)
:
@[deprecated MeasureTheory.Measure.setLIntegral_condKernel_univ_right]
theorem
MeasureTheory.Measure.set_lintegral_condKernel_univ_right
{β : Type u_1}
{Ω : Type u_2}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : β × Ω → ENNReal}
(hf : Measurable f)
{s : Set β}
(hs : MeasurableSet s)
:
Alias of MeasureTheory.Measure.setLIntegral_condKernel_univ_right.
theorem
MeasureTheory.Measure.setLIntegral_condKernel_univ_left
{β : Type u_1}
{Ω : Type u_2}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : β × Ω → ENNReal}
(hf : Measurable f)
{t : Set Ω}
(ht : MeasurableSet t)
:
@[deprecated MeasureTheory.Measure.setLIntegral_condKernel_univ_left]
theorem
MeasureTheory.Measure.set_lintegral_condKernel_univ_left
{β : Type u_1}
{Ω : Type u_2}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : β × Ω → ENNReal}
(hf : Measurable f)
{t : Set Ω}
(ht : MeasurableSet t)
:
Alias of MeasureTheory.Measure.setLIntegral_condKernel_univ_left.
theorem
MeasureTheory.AEStronglyMeasurable.integral_condKernel
{β : Type u_1}
{Ω : Type u_2}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{E : Type u_3}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(hf : MeasureTheory.AEStronglyMeasurable f ρ)
:
MeasureTheory.AEStronglyMeasurable (fun (x : β) => ∫ (y : Ω), f (x, y) ∂ρ.condKernel x) ρ.fst
theorem
MeasureTheory.Measure.integral_condKernel
{β : Type u_1}
{Ω : Type u_2}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{E : Type u_3}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(hf : MeasureTheory.Integrable f ρ)
:
theorem
MeasureTheory.Measure.setIntegral_condKernel
{β : Type u_1}
{Ω : Type u_2}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{E : Type u_3}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : Set β}
(hs : MeasurableSet s)
{t : Set Ω}
(ht : MeasurableSet t)
(hf : MeasureTheory.IntegrableOn f (s ×ˢ t) ρ)
:
@[deprecated MeasureTheory.Measure.setIntegral_condKernel]
theorem
MeasureTheory.Measure.set_integral_condKernel
{β : Type u_1}
{Ω : Type u_2}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{E : Type u_3}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : Set β}
(hs : MeasurableSet s)
{t : Set Ω}
(ht : MeasurableSet t)
(hf : MeasureTheory.IntegrableOn f (s ×ˢ t) ρ)
:
theorem
MeasureTheory.Measure.setIntegral_condKernel_univ_right
{β : Type u_1}
{Ω : Type u_2}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{E : Type u_3}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : Set β}
(hs : MeasurableSet s)
(hf : MeasureTheory.IntegrableOn f (s ×ˢ Set.univ) ρ)
:
@[deprecated MeasureTheory.Measure.setIntegral_condKernel_univ_right]
theorem
MeasureTheory.Measure.set_integral_condKernel_univ_right
{β : Type u_1}
{Ω : Type u_2}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{E : Type u_3}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : Set β}
(hs : MeasurableSet s)
(hf : MeasureTheory.IntegrableOn f (s ×ˢ Set.univ) ρ)
:
Alias of MeasureTheory.Measure.setIntegral_condKernel_univ_right.
theorem
MeasureTheory.Measure.setIntegral_condKernel_univ_left
{β : Type u_1}
{Ω : Type u_2}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{E : Type u_3}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{t : Set Ω}
(ht : MeasurableSet t)
(hf : MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) ρ)
:
@[deprecated MeasureTheory.Measure.setIntegral_condKernel_univ_left]
theorem
MeasureTheory.Measure.set_integral_condKernel_univ_left
{β : Type u_1}
{Ω : Type u_2}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{E : Type u_3}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{t : Set Ω}
(ht : MeasurableSet t)
(hf : MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) ρ)
:
Alias of MeasureTheory.Measure.setIntegral_condKernel_univ_left.
Integrability #
We place these lemmas in the MeasureTheory namespace to enable dot notation.
theorem
MeasureTheory.AEStronglyMeasurable.ae_integrable_condKernel_iff
{α : Type u_1}
{Ω : Type u_2}
{F : Type u_4}
{mα : MeasurableSpace α}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{ρ : MeasureTheory.Measure (α × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : α × Ω → F}
(hf : MeasureTheory.AEStronglyMeasurable f ρ)
:
(∀ᵐ (a : α) ∂ρ.fst, MeasureTheory.Integrable (fun (ω : Ω) => f (a, ω)) (ρ.condKernel a)) ∧ MeasureTheory.Integrable (fun (a : α) => ∫ (ω : Ω), ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst ↔ MeasureTheory.Integrable f ρ
theorem
MeasureTheory.Integrable.condKernel_ae
{α : Type u_1}
{Ω : Type u_2}
{F : Type u_4}
{mα : MeasurableSpace α}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{ρ : MeasureTheory.Measure (α × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : α × Ω → F}
(hf_int : MeasureTheory.Integrable f ρ)
:
∀ᵐ (a : α) ∂ρ.fst, MeasureTheory.Integrable (fun (ω : Ω) => f (a, ω)) (ρ.condKernel a)
theorem
MeasureTheory.Integrable.integral_norm_condKernel
{α : Type u_1}
{Ω : Type u_2}
{F : Type u_4}
{mα : MeasurableSpace α}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{ρ : MeasureTheory.Measure (α × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : α × Ω → F}
(hf_int : MeasureTheory.Integrable f ρ)
:
MeasureTheory.Integrable (fun (x : α) => ∫ (y : Ω), ‖f (x, y)‖ ∂ρ.condKernel x) ρ.fst
theorem
MeasureTheory.Integrable.norm_integral_condKernel
{α : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mα : MeasurableSpace α}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{ρ : MeasureTheory.Measure (α × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : α × Ω → E}
(hf_int : MeasureTheory.Integrable f ρ)
:
MeasureTheory.Integrable (fun (x : α) => ‖∫ (y : Ω), f (x, y) ∂ρ.condKernel x‖) ρ.fst
theorem
MeasureTheory.Integrable.integral_condKernel
{α : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mα : MeasurableSpace α}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{ρ : MeasureTheory.Measure (α × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : α × Ω → E}
(hf_int : MeasureTheory.Integrable f ρ)
:
MeasureTheory.Integrable (fun (x : α) => ∫ (y : Ω), f (x, y) ∂ρ.condKernel x) ρ.fst