Documentation

Mathlib.Probability.Kernel.Disintegration.Integral

Lebesgue and Bochner integrals of conditional kernels #

Integrals of ProbabilityTheory.kernel.condKernel and MeasureTheory.Measure.condKernel.

Main statements #

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.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) :
∫⁻ (b : β) in s, ((ProbabilityTheory.kernel.condKernel κ) (a, b)) t(ProbabilityTheory.kernel.fst κ) a = (κ a) (s ×ˢ 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) :
∫⁻ (b : β) in s, ((ProbabilityTheory.kernel.condKernel κ) (a, b)) t(ProbabilityTheory.kernel.fst κ) a = (κ a) (s ×ˢ 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 : α) :
∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω)(ProbabilityTheory.kernel.condKernel κ) (a, b)(ProbabilityTheory.kernel.fst κ) a = ∫⁻ (x : β × Ω), f xκ 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) :
∫⁻ (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.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) :
∫⁻ (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.setLIntegral_condKernel.

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) :
∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω)(ProbabilityTheory.kernel.condKernel κ) (a, b)(ProbabilityTheory.kernel.fst κ) a = ∫⁻ (x : β × Ω) in s ×ˢ Set.univ, f xκ a
@[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) :
∫⁻ (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.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) :
∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω)(ProbabilityTheory.kernel.condKernel κ) (a, b)(ProbabilityTheory.kernel.fst κ) a = ∫⁻ (x : β × Ω) in Set.univ ×ˢ t, f xκ a
@[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) :
∫⁻ (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.setLIntegral_condKernel_univ_left.

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 : β), (ρ.condKernel x) {y : Ω | (x, y) s}ρ.fst = ρ s
theorem MeasureTheory.Measure.setLIntegral_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, (ρ.condKernel b) tρ.fst = ρ (s ×ˢ t)
@[deprecated MeasureTheory.Measure.setLIntegral_condKernel_eq_measure_prod]
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, (ρ.condKernel b) tρ.fst = ρ (s ×ˢ t)

Alias of MeasureTheory.Measure.setLIntegral_condKernel_eq_measure_prod.

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, ω)ρ.condKernel bρ.fst = ∫⁻ (x : β × Ω), f xρ
theorem MeasureTheory.Measure.setLIntegral_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, ω)ρ.condKernel bρ.fst = ∫⁻ (x : β × Ω) in s ×ˢ t, f xρ
@[deprecated MeasureTheory.Measure.setLIntegral_condKernel]
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, ω)ρ.condKernel bρ.fst = ∫⁻ (x : β × Ω) in s ×ˢ t, f xρ

Alias of MeasureTheory.Measure.setLIntegral_condKernel.

theorem MeasureTheory.Measure.setLIntegral_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, ω)ρ.condKernel bρ.fst = ∫⁻ (x : β × Ω) in s ×ˢ Set.univ, f xρ
@[deprecated MeasureTheory.Measure.setLIntegral_condKernel_univ_right]
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, ω)ρ.condKernel bρ.fst = ∫⁻ (x : β × Ω) in s ×ˢ Set.univ, f xρ

Alias of MeasureTheory.Measure.setLIntegral_condKernel_univ_right.

theorem MeasureTheory.Measure.setLIntegral_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, ω)ρ.condKernel bρ.fst = ∫⁻ (x : β × Ω) in Set.univ ×ˢ t, f xρ
@[deprecated MeasureTheory.Measure.setLIntegral_condKernel_univ_left]
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, ω)ρ.condKernel bρ.fst = ∫⁻ (x : β × Ω) in Set.univ ×ˢ t, f xρ

Alias of MeasureTheory.Measure.setLIntegral_condKernel_univ_left.

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)ρ.condKernel x) ρ.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, ω)ρ.condKernel bρ.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, ω)ρ.condKernel bρ.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, ω)ρ.condKernel bρ.fst = ∫ (x : β × Ω) in s ×ˢ t, f xρ

Alias of MeasureTheory.Measure.setIntegral_condKernel.

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, ω)ρ.condKernel bρ.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, ω)ρ.condKernel bρ.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, ω)ρ.condKernel bρ.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, ω)ρ.condKernel bρ.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 : α) ∂ρ.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