f-Divergences of composition products: infinite values #
We determine when fDiv f (μ ⊗ₘ κ) (ν ⊗ₘ κ) is infinite, with special attention given to the
case ν = μ, which is linked to the conditional divergence.
Every measure and kernel are supposed finite.
Recall fDiv_ne_top_iff':
fDiv f μ ν ≠ ⊤ ↔ derivAtTop f = ⊤ → (Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν ∧ μ ≪ ν)
If derivAtTop f ≠ ⊤ then fDiv f μ ν ≠ ⊤.
If derivAtTop f = ⊤, then fDiv f (μ ⊗ₘ κ) (ν ⊗ₘ κ) = ⊤ unless
μ ⊗ₘ κ ≪ ν ⊗ₘ κ. That's equivalent toμ ≪ νandμ ⊗ₘ κ ≪ μ ⊗ₘ κ.Integrable (fun x ↦ f ((∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ κ)) x).toReal) (ν ⊗ₘ κ). TODO
@[simp]
theorem
ProbabilityTheory.fDiv_compProd_right
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : ℝ → ℝ}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsMarkovKernel κ]
(hf : MeasureTheory.StronglyMeasurable f)
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
ProbabilityTheory.fDiv f (μ.compProd κ) (ν.compProd κ) = ProbabilityTheory.fDiv f μ ν
theorem
ProbabilityTheory.fDiv_compProd_ne_top_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 κ]
[∀ (a : α), NeZero (κ a)]
[ProbabilityTheory.IsFiniteKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
ProbabilityTheory.fDiv f (μ.compProd κ) (ν.compProd η) ≠ ⊤ ↔ derivAtTop f = ⊤ →
(∀ᵐ (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)
ν ∧ (μ.compProd κ).AbsolutelyContinuous (ν.compProd η)
theorem
ProbabilityTheory.fDiv_compProd_ne_top_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 κ]
[∀ (a : α), NeZero (κ a)]
[ProbabilityTheory.IsFiniteKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
ProbabilityTheory.fDiv f (μ.compProd κ) (ν.compProd η) ≠ ⊤ ↔ derivAtTop f = ⊤ →
(∀ᵐ (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) ν ∧ (μ.compProd κ).AbsolutelyContinuous (ν.compProd η)
theorem
ProbabilityTheory.fDiv_compProd_eq_top_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 κ]
[∀ (a : α), NeZero (κ a)]
[ProbabilityTheory.IsFiniteKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
ProbabilityTheory.fDiv f (μ.compProd κ) (ν.compProd η) = ⊤ ↔ derivAtTop f = ⊤ ∧ ((∀ᵐ (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)
ν →
μ.AbsolutelyContinuous ν → ¬(μ.compProd κ).AbsolutelyContinuous (μ.compProd η))
theorem
ProbabilityTheory.fDiv_compProd_eq_top_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 κ]
[∀ (a : α), NeZero (κ a)]
[ProbabilityTheory.IsFiniteKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
ProbabilityTheory.fDiv f (μ.compProd κ) (ν.compProd η) = ⊤ ↔ derivAtTop f = ⊤ ∧ ((∀ᵐ (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) ν →
μ.AbsolutelyContinuous ν → ¬(μ.compProd κ).AbsolutelyContinuous (μ.compProd η))
theorem
ProbabilityTheory.fDiv_compProd_right_ne_top_iff'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
[∀ (a : α), NeZero (κ a)]
[ProbabilityTheory.IsFiniteKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
ProbabilityTheory.fDiv f (μ.compProd κ) (μ.compProd η) ≠ ⊤ ↔ derivAtTop f = ⊤ →
(∀ᵐ (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)
μ ∧ (μ.compProd κ).AbsolutelyContinuous (μ.compProd η)
theorem
ProbabilityTheory.fDiv_compProd_right_eq_top_iff'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
[∀ (a : α), NeZero (κ a)]
[ProbabilityTheory.IsFiniteKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
ProbabilityTheory.fDiv f (μ.compProd κ) (μ.compProd η) = ⊤ ↔ derivAtTop f = ⊤ ∧ ((∀ᵐ (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)
μ →
¬(μ.compProd κ).AbsolutelyContinuous (μ.compProd η))
theorem
ProbabilityTheory.fDiv_compProd_left_ne_top_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)
:
ProbabilityTheory.fDiv f (μ.compProd κ) (ν.compProd κ) ≠ ⊤ ↔ derivAtTop f = ⊤ → MeasureTheory.Integrable (fun (a : α) => f (μ.rnDeriv ν a).toReal) ν ∧ μ.AbsolutelyContinuous ν
theorem
ProbabilityTheory.fDiv_compProd_left_eq_top_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)
:
ProbabilityTheory.fDiv f (μ.compProd κ) (ν.compProd κ) = ⊤ ↔ derivAtTop f = ⊤ ∧ (MeasureTheory.Integrable (fun (a : α) => f (μ.rnDeriv ν a).toReal) ν → ¬μ.AbsolutelyContinuous ν)
theorem
ProbabilityTheory.fDiv_compProd_ne_top_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 κ]
[∀ (a : α), NeZero (κ a)]
[ProbabilityTheory.IsFiniteKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
ProbabilityTheory.fDiv f (μ.compProd κ) (ν.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) ν ∧ (derivAtTop f = ⊤ → μ.AbsolutelyContinuous ν ∧ ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
theorem
ProbabilityTheory.fDiv_compProd_eq_top_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 κ]
[∀ (a : α), NeZero (κ a)]
[ProbabilityTheory.IsFiniteKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
ProbabilityTheory.fDiv f (μ.compProd κ) (ν.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) ν →
derivAtTop f = ⊤ ∧ (μ.AbsolutelyContinuous ν → ¬∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
theorem
ProbabilityTheory.fDiv_compProd_right_ne_top_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
[∀ (a : α), NeZero (κ a)]
[ProbabilityTheory.IsFiniteKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
ProbabilityTheory.fDiv f (μ.compProd κ) (μ.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) μ ∧ (derivAtTop f = ⊤ → ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
theorem
ProbabilityTheory.fDiv_compProd_right_eq_top_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
[∀ (a : α), NeZero (κ a)]
[ProbabilityTheory.IsFiniteKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
ProbabilityTheory.fDiv f (μ.compProd κ) (μ.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) μ →
derivAtTop f = ⊤ ∧ ¬∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a)
theorem
ProbabilityTheory.f_rnDeriv_ae_le_integral
{α : 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.IsMarkovKernel η]
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
(h_int : MeasureTheory.Integrable (fun (p : α × β) => f ((μ.compProd κ).rnDeriv (ν.compProd η) p).toReal) (ν.compProd η))
(hκη : ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
:
theorem
ProbabilityTheory.integrable_f_rnDeriv_mul_kernel
{α : 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.IsMarkovKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
(h_int : MeasureTheory.Integrable (fun (p : α × β) => f ((μ.compProd κ).rnDeriv (ν.compProd η) p).toReal) (ν.compProd η))
(hκη : ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
:
MeasureTheory.Integrable (fun (a : α) => f (μ.rnDeriv ν a * (κ a) Set.univ).toReal) ν
theorem
ProbabilityTheory.integrable_f_rnDeriv_mul_withDensity
{α : 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.IsMarkovKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
(h_int : MeasureTheory.Integrable (fun (p : α × β) => f ((μ.compProd κ).rnDeriv (ν.compProd η) p).toReal) (ν.compProd η))
:
MeasureTheory.Integrable (fun (a : α) => f (μ.rnDeriv ν a * ((η.withDensity (κ.rnDeriv η)) a) Set.univ).toReal) ν
theorem
ProbabilityTheory.f_rnDeriv_le_add
{α : 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.IsMarkovKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(h_deriv : derivAtTop f = ⊤ → ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
:
theorem
ProbabilityTheory.integrable_f_rnDeriv_of_integrable_compProd'
{α : 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.IsMarkovKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
(hf_int : MeasureTheory.Integrable (fun (p : α × β) => f ((μ.compProd κ).rnDeriv (ν.compProd η) p).toReal) (ν.compProd η))
(h_deriv : derivAtTop f = ⊤ → ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
:
MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν
theorem
ProbabilityTheory.fDiv_ne_top_of_fDiv_compProd_ne_top
{α : 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.IsMarkovKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
(h_ne_top : ProbabilityTheory.fDiv f (μ.compProd κ) (ν.compProd η) ≠ ⊤)
:
ProbabilityTheory.fDiv f μ ν ≠ ⊤