theorem
ProbabilityTheory.integrable_rnDeriv_mul_log_iff
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
(hμν : μ.AbsolutelyContinuous ν)
:
MeasureTheory.Integrable (fun (a : α) => (μ.rnDeriv ν a).toReal * Real.log (μ.rnDeriv ν a).toReal) ν ↔ MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ
theorem
ProbabilityTheory.integrable_llr_compProd_of_integrable_llr
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[ProbabilityTheory.IsMarkovKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(h_ac : (μ.compProd κ).AbsolutelyContinuous (ν.compProd η))
(hμν : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ)
(hκη_int : MeasureTheory.Integrable (fun (a : α) => ∫ (b : β), MeasureTheory.llr (κ a) (η a) b ∂κ a) μ)
(hκη_ae : ∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (MeasureTheory.llr (κ a) (η a)) (κ a))
:
MeasureTheory.Integrable (MeasureTheory.llr (μ.compProd κ) (ν.compProd η)) (μ.compProd κ)
theorem
ProbabilityTheory.integrable_llr_of_integrable_llr_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[ProbabilityTheory.IsMarkovKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(h_ac : (μ.compProd κ).AbsolutelyContinuous (ν.compProd η))
(h_int : MeasureTheory.Integrable (MeasureTheory.llr (μ.compProd κ) (ν.compProd η)) (μ.compProd κ))
:
theorem
ProbabilityTheory.ae_integrable_llr_of_integrable_llr_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[ProbabilityTheory.IsMarkovKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(h_ac : (μ.compProd κ).AbsolutelyContinuous (ν.compProd η))
(h_int : MeasureTheory.Integrable (MeasureTheory.llr (μ.compProd κ) (ν.compProd η)) (μ.compProd κ))
:
∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (MeasureTheory.llr (κ a) (η a)) (κ a)
theorem
ProbabilityTheory.integrable_integral_llr_of_integrable_llr_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[ProbabilityTheory.IsMarkovKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(h_ac : (μ.compProd κ).AbsolutelyContinuous (ν.compProd η))
(h_int : MeasureTheory.Integrable (MeasureTheory.llr (μ.compProd κ) (ν.compProd η)) (μ.compProd κ))
:
MeasureTheory.Integrable (fun (a : α) => ∫ (b : β), MeasureTheory.llr (κ a) (η a) b ∂κ a) μ
theorem
ProbabilityTheory.integrable_llr_compProd_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[ProbabilityTheory.IsMarkovKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(h_ac : (μ.compProd κ).AbsolutelyContinuous (ν.compProd η))
:
MeasureTheory.Integrable (MeasureTheory.llr (μ.compProd κ) (ν.compProd η)) (μ.compProd κ) ↔ (MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ ∧ MeasureTheory.Integrable (fun (a : α) => ∫ (b : β), MeasureTheory.llr (κ a) (η a) b ∂κ a) μ) ∧ ∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (MeasureTheory.llr (κ a) (η a)) (κ a)
theorem
ProbabilityTheory.Kernel.integrable_llr_compProd_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[MeasurableSpace.CountableOrCountablyGenerated β γ]
{κ₁ : ProbabilityTheory.Kernel α β}
{η₁ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsFiniteKernel κ₁]
[ProbabilityTheory.IsFiniteKernel η₁]
{κ₂ : ProbabilityTheory.Kernel (α × β) γ}
{η₂ : ProbabilityTheory.Kernel (α × β) γ}
[ProbabilityTheory.IsMarkovKernel κ₂]
[ProbabilityTheory.IsMarkovKernel η₂]
(a : α)
(h_ac : ((κ₁.compProd κ₂) a).AbsolutelyContinuous ((η₁.compProd η₂) a))
:
MeasureTheory.Integrable (MeasureTheory.llr ((κ₁.compProd κ₂) a) ((η₁.compProd η₂) a)) ((κ₁.compProd κ₂) a) ↔ MeasureTheory.Integrable (MeasureTheory.llr (κ₁ a) (η₁ a)) (κ₁ a) ∧ MeasureTheory.Integrable (fun (b : β) => ∫ (x : γ), MeasureTheory.llr (κ₂ (a, b)) (η₂ (a, b)) x ∂κ₂ (a, b)) (κ₁ a) ∧ ∀ᵐ (b : β) ∂κ₁ a, MeasureTheory.Integrable (MeasureTheory.llr (κ₂ (a, b)) (η₂ (a, b))) (κ₂ (a, b))
theorem
ProbabilityTheory.measurableSet_integrable_llr
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
:
MeasurableSet
{a : α |
MeasureTheory.Integrable (fun (b : β) => ((κ a).rnDeriv (η a) b).toReal * MeasureTheory.llr (κ a) (η a) b) (η a)}
theorem
ProbabilityTheory.ae_compProd_integrable_llr_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{μ : MeasureTheory.Measure α}
[MeasurableSpace.CountableOrCountablyGenerated (α × β) γ]
[MeasureTheory.SFinite μ]
{ξ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel ξ]
{κ : ProbabilityTheory.Kernel (α × β) γ}
{η : ProbabilityTheory.Kernel (α × β) γ}
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(h_ac : ∀ᵐ (x : α × β) ∂μ.compProd ξ, (κ x).AbsolutelyContinuous (η x))
:
(∀ᵐ (x : α × β) ∂μ.compProd ξ, MeasureTheory.Integrable (MeasureTheory.llr (κ x) (η x)) (κ x)) ↔ ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂ξ a, MeasureTheory.Integrable (MeasureTheory.llr (κ (a, b)) (η (a, b))) (κ (a, b))