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)
:
∫⁻ (x : β),
↑↑((ProbabilityTheory.kernel.condKernel κ) (a, x)) {y : Ω | (x, y) ∈ s} ∂(ProbabilityTheory.kernel.fst κ) a = ↑↑(κ a) s
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)
:
∫⁻ (b : β) in s, ↑↑((ProbabilityTheory.kernel.condKernel κ) (a, b)) t ∂(ProbabilityTheory.kernel.fst κ) a = ↑↑(κ a) (s ×ˢ t)
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 : α)
:
∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂(ProbabilityTheory.kernel.condKernel κ) (a, b) ∂(ProbabilityTheory.kernel.fst κ) a = ∫⁻ (x : β × Ω), f x ∂κ a
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)
:
∫⁻ (b : β) in s,
∫⁻ (ω : Ω) in t, f (b, ω) ∂(ProbabilityTheory.kernel.condKernel κ) (a, b) ∂(ProbabilityTheory.kernel.fst κ) a = ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂κ a
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)
:
∫⁻ (b : β) in s,
∫⁻ (ω : Ω), f (b, ω) ∂(ProbabilityTheory.kernel.condKernel κ) (a, b) ∂(ProbabilityTheory.kernel.fst κ) a = ∫⁻ (x : β × Ω) in s ×ˢ Set.univ, f x ∂κ a
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)
:
∫⁻ (b : β),
∫⁻ (ω : Ω) in t, f (b, ω) ∂(ProbabilityTheory.kernel.condKernel κ) (a, b) ∂(ProbabilityTheory.kernel.fst κ) a = ∫⁻ (x : β × Ω) in Set.univ ×ˢ t, f x ∂κ a
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) ∂(ProbabilityTheory.kernel.condKernel κ) (a, x))
((ProbabilityTheory.kernel.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))
:
∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂(ProbabilityTheory.kernel.condKernel κ) (a, b) ∂(ProbabilityTheory.kernel.fst κ) a = ∫ (x : β × Ω), f x ∂κ 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))
:
∫ (b : β) in s,
∫ (ω : Ω) in t, f (b, ω) ∂(ProbabilityTheory.kernel.condKernel κ) (a, b) ∂(ProbabilityTheory.kernel.fst κ) a = ∫ (x : β × Ω) in s ×ˢ t, f x ∂κ 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))
:
∫ (b : β) in s,
∫ (ω : Ω) in t, f (b, ω) ∂(ProbabilityTheory.kernel.condKernel κ) (a, b) ∂(ProbabilityTheory.kernel.fst κ) a = ∫ (x : β × Ω) in s ×ˢ t, f x ∂κ 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))
:
∫ (b : β) in s,
∫ (ω : Ω), f (b, ω) ∂(ProbabilityTheory.kernel.condKernel κ) (a, b) ∂(ProbabilityTheory.kernel.fst κ) a = ∫ (x : β × Ω) in s ×ˢ Set.univ, f x ∂κ 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))
:
∫ (b : β) in s,
∫ (ω : Ω), f (b, ω) ∂(ProbabilityTheory.kernel.condKernel κ) (a, b) ∂(ProbabilityTheory.kernel.fst κ) a = ∫ (x : β × Ω) in s ×ˢ Set.univ, f x ∂κ 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))
:
∫ (b : β),
∫ (ω : Ω) in t, f (b, ω) ∂(ProbabilityTheory.kernel.condKernel κ) (a, b) ∂(ProbabilityTheory.kernel.fst κ) a = ∫ (x : β × Ω) in Set.univ ×ˢ t, f x ∂κ 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))
:
∫ (b : β),
∫ (ω : Ω) in t, f (b, ω) ∂(ProbabilityTheory.kernel.condKernel κ) (a, b) ∂(ProbabilityTheory.kernel.fst κ) a = ∫ (x : β × Ω) in Set.univ ×ˢ t, f x ∂κ a
Alias of ProbabilityTheory.setIntegral_condKernel_univ_left.
theorem
MeasureTheory.Measure.lintegral_condKernel_mem
{β : Type u_2}
{Ω : Type u_3}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{s : Set (β × Ω)}
(hs : MeasurableSet s)
:
∫⁻ (x : β), ↑↑((MeasureTheory.Measure.condKernel ρ) x) {y : Ω | (x, y) ∈ s} ∂MeasureTheory.Measure.fst ρ = ↑↑ρ s
theorem
MeasureTheory.Measure.set_lintegral_condKernel_eq_measure_prod
{β : Type u_2}
{Ω : Type u_3}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{s : Set β}
(hs : MeasurableSet s)
{t : Set Ω}
(ht : MeasurableSet t)
:
∫⁻ (b : β) in s, ↑↑((MeasureTheory.Measure.condKernel ρ) b) t ∂MeasureTheory.Measure.fst ρ = ↑↑ρ (s ×ˢ t)
theorem
MeasureTheory.Measure.lintegral_condKernel
{β : Type u_2}
{Ω : Type u_3}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : β × Ω → ENNReal}
(hf : Measurable f)
:
∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂(MeasureTheory.Measure.condKernel ρ) b ∂MeasureTheory.Measure.fst ρ = ∫⁻ (x : β × Ω), f x ∂ρ
theorem
MeasureTheory.Measure.set_lintegral_condKernel
{β : Type u_2}
{Ω : Type u_3}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : β × Ω → ENNReal}
(hf : Measurable f)
{s : Set β}
(hs : MeasurableSet s)
{t : Set Ω}
(ht : MeasurableSet t)
:
∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂(MeasureTheory.Measure.condKernel ρ) b ∂MeasureTheory.Measure.fst ρ = ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂ρ
theorem
MeasureTheory.Measure.set_lintegral_condKernel_univ_right
{β : Type u_2}
{Ω : Type u_3}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : β × Ω → ENNReal}
(hf : Measurable f)
{s : Set β}
(hs : MeasurableSet s)
:
∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂(MeasureTheory.Measure.condKernel ρ) b ∂MeasureTheory.Measure.fst ρ = ∫⁻ (x : β × Ω) in s ×ˢ Set.univ, f x ∂ρ
theorem
MeasureTheory.Measure.set_lintegral_condKernel_univ_left
{β : Type u_2}
{Ω : Type u_3}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : β × Ω → ENNReal}
(hf : Measurable f)
{t : Set Ω}
(ht : MeasurableSet t)
:
∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂(MeasureTheory.Measure.condKernel ρ) b ∂MeasureTheory.Measure.fst ρ = ∫⁻ (x : β × Ω) in Set.univ ×ˢ t, f x ∂ρ
theorem
MeasureTheory.AEStronglyMeasurable.integral_condKernel
{β : Type u_2}
{Ω : Type u_3}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{E : Type u_4}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(hf : MeasureTheory.AEStronglyMeasurable f ρ)
:
MeasureTheory.AEStronglyMeasurable (fun (x : β) => ∫ (y : Ω), f (x, y) ∂(MeasureTheory.Measure.condKernel ρ) x)
(MeasureTheory.Measure.fst ρ)
theorem
MeasureTheory.Measure.integral_condKernel
{β : Type u_2}
{Ω : Type u_3}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{E : Type u_4}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(hf : MeasureTheory.Integrable f ρ)
:
∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂(MeasureTheory.Measure.condKernel ρ) b ∂MeasureTheory.Measure.fst ρ = ∫ (x : β × Ω), f x ∂ρ
theorem
MeasureTheory.Measure.setIntegral_condKernel
{β : Type u_2}
{Ω : Type u_3}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{E : Type u_4}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : Set β}
(hs : MeasurableSet s)
{t : Set Ω}
(ht : MeasurableSet t)
(hf : MeasureTheory.IntegrableOn f (s ×ˢ t) ρ)
:
∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂(MeasureTheory.Measure.condKernel ρ) b ∂MeasureTheory.Measure.fst ρ = ∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ
@[deprecated MeasureTheory.Measure.setIntegral_condKernel]
theorem
MeasureTheory.Measure.set_integral_condKernel
{β : Type u_2}
{Ω : Type u_3}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{E : Type u_4}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : Set β}
(hs : MeasurableSet s)
{t : Set Ω}
(ht : MeasurableSet t)
(hf : MeasureTheory.IntegrableOn f (s ×ˢ t) ρ)
:
∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂(MeasureTheory.Measure.condKernel ρ) b ∂MeasureTheory.Measure.fst ρ = ∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ
theorem
MeasureTheory.Measure.setIntegral_condKernel_univ_right
{β : Type u_2}
{Ω : Type u_3}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{E : Type u_4}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : Set β}
(hs : MeasurableSet s)
(hf : MeasureTheory.IntegrableOn f (s ×ˢ Set.univ) ρ)
:
∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂(MeasureTheory.Measure.condKernel ρ) b ∂MeasureTheory.Measure.fst ρ = ∫ (x : β × Ω) in s ×ˢ Set.univ, f x ∂ρ
@[deprecated MeasureTheory.Measure.setIntegral_condKernel_univ_right]
theorem
MeasureTheory.Measure.set_integral_condKernel_univ_right
{β : Type u_2}
{Ω : Type u_3}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{E : Type u_4}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : Set β}
(hs : MeasurableSet s)
(hf : MeasureTheory.IntegrableOn f (s ×ˢ Set.univ) ρ)
:
∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂(MeasureTheory.Measure.condKernel ρ) b ∂MeasureTheory.Measure.fst ρ = ∫ (x : β × Ω) in s ×ˢ Set.univ, f x ∂ρ
Alias of MeasureTheory.Measure.setIntegral_condKernel_univ_right.
theorem
MeasureTheory.Measure.setIntegral_condKernel_univ_left
{β : Type u_2}
{Ω : Type u_3}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{E : Type u_4}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{t : Set Ω}
(ht : MeasurableSet t)
(hf : MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) ρ)
:
∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂(MeasureTheory.Measure.condKernel ρ) b ∂MeasureTheory.Measure.fst ρ = ∫ (x : β × Ω) in Set.univ ×ˢ t, f x ∂ρ
@[deprecated MeasureTheory.Measure.setIntegral_condKernel_univ_left]
theorem
MeasureTheory.Measure.set_integral_condKernel_univ_left
{β : Type u_2}
{Ω : Type u_3}
{mβ : MeasurableSpace β}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{ρ : MeasureTheory.Measure (β × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{E : Type u_4}
{f : β × Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{t : Set Ω}
(ht : MeasurableSet t)
(hf : MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) ρ)
:
∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂(MeasureTheory.Measure.condKernel ρ) b ∂MeasureTheory.Measure.fst ρ = ∫ (x : β × Ω) in Set.univ ×ˢ t, f x ∂ρ
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 : α) ∂MeasureTheory.Measure.fst ρ,
MeasureTheory.Integrable (fun (ω : Ω) => f (a, ω)) ((MeasureTheory.Measure.condKernel ρ) a)) ∧ MeasureTheory.Integrable (fun (a : α) => ∫ (ω : Ω), ‖f (a, ω)‖ ∂(MeasureTheory.Measure.condKernel ρ) a)
(MeasureTheory.Measure.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 : α) ∂MeasureTheory.Measure.fst ρ,
MeasureTheory.Integrable (fun (ω : Ω) => f (a, ω)) ((MeasureTheory.Measure.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)‖ ∂(MeasureTheory.Measure.condKernel ρ) x)
(MeasureTheory.Measure.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) ∂(MeasureTheory.Measure.condKernel ρ) x‖)
(MeasureTheory.Measure.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) ∂(MeasureTheory.Measure.condKernel ρ) x)
(MeasureTheory.Measure.fst ρ)