Conditional f-divergence #
theorem
ProbabilityTheory.condFDiv_snd'_toReal_eq_ae
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{μ : MeasureTheory.Measure α}
{f : ℝ → ℝ}
[MeasurableSpace.CountableOrCountablyGenerated β γ]
{ξ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsFiniteKernel ξ]
{κ : ProbabilityTheory.Kernel (α × β) γ}
{η : ProbabilityTheory.Kernel (α × β) γ}
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
(h_ac : derivAtTop f = ⊤ → ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂ξ a, (κ (a, b)).AbsolutelyContinuous (η (a, b)))
(h_int : ∀ᵐ (a : α) ∂μ,
∀ᵐ (b : β) ∂ξ a, MeasureTheory.Integrable (fun (x : γ) => f ((κ (a, b)).rnDeriv (η (a, b)) x).toReal) (η (a, b)))
(h_int2 : ∀ᵐ (a : α) ∂μ,
MeasureTheory.Integrable (fun (b : β) => ∫ (x : γ), f ((κ (a, b)).rnDeriv (η (a, b)) x).toReal ∂η (a, b)) (ξ a))
:
∀ᵐ (a : α) ∂μ,
(ProbabilityTheory.condFDiv f (κ.snd' a) (η.snd' a) (ξ a)).toReal = ∫ (b : β), (ProbabilityTheory.fDiv f (κ (a, b)) (η (a, b))).toReal ∂ξ a
theorem
ProbabilityTheory.condFDiv_kernel_snd'_integrable_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{μ : MeasureTheory.Measure α}
{f : ℝ → ℝ}
[MeasurableSpace.CountableOrCountablyGenerated (α × β) γ]
[MeasureTheory.IsFiniteMeasure μ]
{ξ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsFiniteKernel ξ]
{κ : ProbabilityTheory.Kernel (α × β) γ}
{η : ProbabilityTheory.Kernel (α × β) γ}
[ProbabilityTheory.IsMarkovKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
(h_ac : derivAtTop f = ⊤ → ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂ξ a, (κ (a, b)).AbsolutelyContinuous (η (a, b)))
(h_int : ∀ᵐ (a : α) ∂μ,
∀ᵐ (b : β) ∂ξ a, MeasureTheory.Integrable (fun (x : γ) => f ((κ (a, b)).rnDeriv (η (a, b)) x).toReal) (η (a, b)))
(h_int2 : ∀ᵐ (a : α) ∂μ,
MeasureTheory.Integrable (fun (b : β) => ∫ (x : γ), f ((κ (a, b)).rnDeriv (η (a, b)) x).toReal ∂η (a, b)) (ξ a))
(hf_meas : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
(hf_one : f 1 = 0)
:
MeasureTheory.Integrable (fun (a : α) => (ProbabilityTheory.condFDiv f (κ.snd' a) (η.snd' a) (ξ a)).toReal) μ ↔ MeasureTheory.Integrable
(fun (a : α) => ∫ (b : β), |∫ (x : γ), f ((κ (a, b)).rnDeriv (η (a, b)) x).toReal ∂η (a, b)| ∂ξ a) μ
theorem
ProbabilityTheory.condFDiv_kernel_fst'_integrable_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{f : ℝ → ℝ}
[MeasurableSpace.CountableOrCountablyGenerated (α × β) γ]
{μ : MeasureTheory.Measure β}
[MeasureTheory.IsFiniteMeasure μ]
{ξ : ProbabilityTheory.Kernel β α}
[ProbabilityTheory.IsFiniteKernel ξ]
{κ : ProbabilityTheory.Kernel (α × β) γ}
{η : ProbabilityTheory.Kernel (α × β) γ}
[ProbabilityTheory.IsMarkovKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
(h_ac : derivAtTop f = ⊤ → ∀ᵐ (b : β) ∂μ, ∀ᵐ (a : α) ∂ξ b, (κ (a, b)).AbsolutelyContinuous (η (a, b)))
(h_int : ∀ᵐ (b : β) ∂μ,
∀ᵐ (a : α) ∂ξ b, MeasureTheory.Integrable (fun (x : γ) => f ((κ (a, b)).rnDeriv (η (a, b)) x).toReal) (η (a, b)))
(h_int2 : ∀ᵐ (b : β) ∂μ,
MeasureTheory.Integrable (fun (a : α) => ∫ (x : γ), f ((κ (a, b)).rnDeriv (η (a, b)) x).toReal ∂η (a, b)) (ξ b))
(hf_meas : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
(hf_one : f 1 = 0)
:
MeasureTheory.Integrable (fun (b : β) => (ProbabilityTheory.condFDiv f (κ.fst' b) (η.fst' b) (ξ b)).toReal) μ ↔ MeasureTheory.Integrable
(fun (b : β) => ∫ (a : α), |∫ (x : γ), f ((κ (a, b)).rnDeriv (η (a, b)) x).toReal ∂η (a, b)| ∂ξ b) μ
theorem
ProbabilityTheory.condFDiv_compProd_meas_eq_top
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{μ : MeasureTheory.Measure α}
{f : ℝ → ℝ}
[MeasurableSpace.CountableOrCountablyGenerated (α × β) γ]
[MeasureTheory.IsFiniteMeasure μ]
{ξ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsFiniteKernel ξ]
{κ : ProbabilityTheory.Kernel (α × β) γ}
{η : ProbabilityTheory.Kernel (α × β) γ}
[ProbabilityTheory.IsMarkovKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
(hf_meas : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
(hf_one : f 1 = 0)
:
ProbabilityTheory.condFDiv f κ η (μ.compProd ξ) = ⊤ ↔ (¬∀ᵐ (a : α) ∂μ, ProbabilityTheory.condFDiv f (κ.snd' a) (η.snd' a) (ξ a) ≠ ⊤) ∨ ¬MeasureTheory.Integrable (fun (x : α) => (ProbabilityTheory.condFDiv f (κ.snd' x) (η.snd' x) (ξ x)).toReal) μ
theorem
ProbabilityTheory.condFDiv_compProd_meas
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{μ : MeasureTheory.Measure α}
{f : ℝ → ℝ}
[MeasurableSpace.CountableOrCountablyGenerated (α × β) γ]
[MeasureTheory.IsFiniteMeasure μ]
{ξ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsFiniteKernel ξ]
{κ : ProbabilityTheory.Kernel (α × β) γ}
{η : ProbabilityTheory.Kernel (α × β) γ}
[ProbabilityTheory.IsMarkovKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
(hf_meas : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
(hf_one : f 1 = 0)
(h_top : ProbabilityTheory.condFDiv f κ η (μ.compProd ξ) ≠ ⊤)
:
ProbabilityTheory.condFDiv f κ η (μ.compProd ξ) = ↑(∫ (x : α), (ProbabilityTheory.condFDiv f (κ.snd' x) (η.snd' x) (ξ x)).toReal ∂μ)