Measurability/integrability lemmas about kernels #
theorem
ProbabilityTheory.measurableSet_integrable_f_kernel_rnDeriv
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
{f : ℝ → ℝ}
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
(ξ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel ξ]
(hf : MeasureTheory.StronglyMeasurable f)
:
MeasurableSet {a : α | MeasureTheory.Integrable (fun (x : β) => f (κ.rnDeriv η a x).toReal) (ξ a)}
theorem
ProbabilityTheory.measurableSet_integrable_f_rnDeriv
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
{f : ℝ → ℝ}
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
:
MeasurableSet {a : α | MeasureTheory.Integrable (fun (x : β) => f ((κ a).rnDeriv (η a) x).toReal) (η a)}
theorem
ProbabilityTheory.measurable_integral_f_rnDeriv
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
{f : ℝ → ℝ}
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
:
Measurable fun (a : α) => ∫ (x : β), f ((κ a).rnDeriv (η a) x).toReal ∂η a
theorem
ProbabilityTheory.measurable_fDiv
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
{f : ℝ → ℝ}
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
:
Measurable fun (a : α) => ProbabilityTheory.fDiv f (κ a) (η a)