TODO #
theorem
ProbabilityTheory.singularPart_compProd_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
:
(μ.compProd κ).singularPart (ν.compProd κ) = (μ.singularPart ν).compProd κ
theorem
ProbabilityTheory.singularPart_compProd''
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
:
theorem
ProbabilityTheory.singularPart_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
:
theorem
ProbabilityTheory.singularPart_compProd'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
:
theorem
ProbabilityTheory.singularPart_compProd_right
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
:
(μ.compProd κ).singularPart (μ.compProd η) = μ.compProd (κ.singularPart η)
theorem
MeasureTheory.Integrable.compProd_mk_left_ae'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{E : Type u_4}
[NormedAddCommGroup E]
[MeasureTheory.SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
⦃f : α × β → E⦄
(hf : MeasureTheory.Integrable f (μ.compProd κ))
:
∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (y : β) => f (x, y)) (κ x)
theorem
MeasureTheory.Integrable.integral_norm_compProd'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{E : Type u_4}
[NormedAddCommGroup E]
[MeasureTheory.SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
⦃f : α × β → E⦄
(hf : MeasureTheory.Integrable f (μ.compProd κ))
:
MeasureTheory.Integrable (fun (x : α) => ∫ (y : β), ‖f (x, y)‖ ∂κ x) μ
theorem
MeasureTheory.Integrable.integral_compProd'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{E : Type u_4}
[NormedAddCommGroup E]
[MeasureTheory.SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
⦃f : α × β → E⦄
[NormedSpace ℝ E]
(hf : MeasureTheory.Integrable f (μ.compProd κ))
:
MeasureTheory.Integrable (fun (x : α) => ∫ (y : β), f (x, y) ∂κ x) μ
theorem
ProbabilityTheory.integrable_f_rnDeriv_compProd_iff_of_nonneg'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure ν]
[ProbabilityTheory.IsFiniteKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(h_nonneg : ∀ (x : ℝ), 0 ≤ x → 0 ≤ f x)
:
MeasureTheory.Integrable (fun (x : α × β) => f ((μ.compProd κ).rnDeriv (ν.compProd η) x).toReal) (ν.compProd η) ↔ (∀ᵐ (a : α) ∂ν,
MeasureTheory.Integrable (fun (x : β) => f ((μ.compProd κ).rnDeriv (ν.compProd η) (a, x)).toReal) (η a)) ∧ MeasureTheory.Integrable (fun (a : α) => ∫ (b : β), f ((μ.compProd κ).rnDeriv (ν.compProd η) (a, b)).toReal ∂η a) ν
theorem
ProbabilityTheory.integrable_add_affine_iff
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(f : ℝ → ℝ)
(a : ℝ)
(b : ℝ)
:
MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal + a * (μ.rnDeriv ν x).toReal + b) ν ↔ MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν
theorem
ProbabilityTheory.integrable_sub_affine_iff
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(f : ℝ → ℝ)
(a : ℝ)
(b : ℝ)
:
MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal - (a * (μ.rnDeriv ν x).toReal + b)) ν ↔ MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν
theorem
ProbabilityTheory.integrable_f_rnDeriv_compProd_iff'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
MeasureTheory.Integrable (fun (x : α × β) => f ((μ.compProd κ).rnDeriv (ν.compProd η) x).toReal) (ν.compProd η) ↔ (∀ᵐ (a : α) ∂ν,
MeasureTheory.Integrable (fun (x : β) => f ((μ.compProd κ).rnDeriv (ν.compProd η) (a, x)).toReal) (η a)) ∧ MeasureTheory.Integrable (fun (a : α) => ∫ (b : β), f ((μ.compProd κ).rnDeriv (ν.compProd η) (a, b)).toReal ∂η a) ν
theorem
ProbabilityTheory.integrable_f_rnDeriv_compProd_iff'_of_ac
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(h_ac : (μ.compProd κ).AbsolutelyContinuous (μ.compProd η))
(hf : MeasureTheory.StronglyMeasurable f)
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
MeasureTheory.Integrable (fun (x : α × β) => f ((μ.compProd κ).rnDeriv (ν.compProd η) x).toReal) (ν.compProd η) ↔ (∀ᵐ (a : α) ∂ν,
MeasureTheory.Integrable (fun (x : β) => f (μ.rnDeriv ν a * (μ.compProd κ).rnDeriv (μ.compProd η) (a, x)).toReal)
(η a)) ∧ MeasureTheory.Integrable
(fun (a : α) => ∫ (b : β), f (μ.rnDeriv ν a * (μ.compProd κ).rnDeriv (μ.compProd η) (a, b)).toReal ∂η a) ν
theorem
ProbabilityTheory.f_compProd_congr_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : ℝ → ℝ}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
:
theorem
ProbabilityTheory.integral_f_compProd_left_congr
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : ℝ → ℝ}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
:
theorem
ProbabilityTheory.integrable_f_rnDeriv_compProd_left_iff'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
[ProbabilityTheory.IsFiniteKernel κ]
(hf : MeasureTheory.StronglyMeasurable f)
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
MeasureTheory.Integrable (fun (x : α × β) => f ((μ.compProd κ).rnDeriv (ν.compProd κ) x).toReal) (ν.compProd κ) ↔ MeasureTheory.Integrable (fun (a : α) => ((κ a) Set.univ).toReal * f (μ.rnDeriv ν a).toReal) ν
theorem
ProbabilityTheory.integrable_f_rnDeriv_compProd_left_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
[ProbabilityTheory.IsMarkovKernel κ]
(hf : MeasureTheory.StronglyMeasurable f)
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
MeasureTheory.Integrable (fun (x : α × β) => f ((μ.compProd κ).rnDeriv (ν.compProd κ) x).toReal) (ν.compProd κ) ↔ MeasureTheory.Integrable (fun (a : α) => f (μ.rnDeriv ν a).toReal) ν
theorem
ProbabilityTheory.f_compProd_congr
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : ℝ → ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
:
theorem
ProbabilityTheory.integral_f_compProd_congr
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : ℝ → ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
:
theorem
ProbabilityTheory.integral_f_compProd_right_congr
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : ℝ → ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
:
theorem
ProbabilityTheory.integrable_f_rnDeriv_of_integrable_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(hf_int : MeasureTheory.Integrable (fun (x : α × β) => f ((μ.compProd κ).rnDeriv (μ.compProd η) x).toReal) (μ.compProd η))
:
∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (fun (x : β) => f ((κ a).rnDeriv (η a) x).toReal) (η a)
theorem
ProbabilityTheory.integrable_f_rnDeriv_compProd_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
MeasureTheory.Integrable (fun (x : α × β) => f ((μ.compProd κ).rnDeriv (ν.compProd η) x).toReal) (ν.compProd η) ↔ (∀ᵐ (a : α) ∂ν, MeasureTheory.Integrable (fun (x : β) => f (μ.rnDeriv ν a * (κ a).rnDeriv (η a) x).toReal) (η a)) ∧ MeasureTheory.Integrable (fun (a : α) => ∫ (b : β), f (μ.rnDeriv ν a * (κ a).rnDeriv (η a) b).toReal ∂η a) ν
theorem
ProbabilityTheory.integrable_f_rnDeriv_compProd_right_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
MeasureTheory.Integrable (fun (x : α × β) => f ((μ.compProd κ).rnDeriv (μ.compProd η) x).toReal) (μ.compProd η) ↔ (∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (fun (x : β) => f ((κ a).rnDeriv (η a) x).toReal) (η a)) ∧ MeasureTheory.Integrable (fun (a : α) => ∫ (b : β), f ((κ a).rnDeriv (η a) b).toReal ∂η a) μ