f-Divergences #
Main definitions #
FooBar
Main statements #
fooBar_unique
Notation #
Implementation details #
theorem
ProbabilityTheory.fDiv_ae_ne_top_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
:
(∀ᵐ (a : α) ∂μ, ProbabilityTheory.fDiv f (κ a) (η a) ≠ ⊤) ↔ (∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (fun (x : β) => f ((κ a).rnDeriv (η a) x).toReal) (η a)) ∧ (derivAtTop f = ⊤ → ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
Equivalence between two possible versions of the first condition for the finiteness of the conditional f divergence, the second version is the preferred one.
theorem
ProbabilityTheory.integrable_fDiv_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 η]
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
(h_int : ∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (fun (x : β) => f ((κ a).rnDeriv (η a) x).toReal) (η a))
(h_ac : derivAtTop f = ⊤ → ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
:
MeasureTheory.Integrable (fun (x : α) => (ProbabilityTheory.fDiv f (κ x) (η x)).toReal) μ ↔ MeasureTheory.Integrable (fun (a : α) => ∫ (b : β), f ((κ a).rnDeriv (η a) b).toReal ∂η a) μ
Equivalence between two possible versions of the second condition for the finiteness of the conditional f divergence, the second version is the preferred one.
theorem
ProbabilityTheory.fDiv_toReal_eq_ae
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : ℝ → ℝ}
{γ : Type u_3}
[MeasurableSpace γ]
{ξ : ProbabilityTheory.Kernel α β}
{κ : ProbabilityTheory.Kernel (α × β) γ}
{η : ProbabilityTheory.Kernel (α × β) γ}
[ProbabilityTheory.IsFiniteKernel κ]
(hf_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)))
:
∀ᵐ (a : α) ∂μ,
∀ᵐ (b : β) ∂ξ a,
(ProbabilityTheory.fDiv f (κ (a, b)) (η (a, b))).toReal = ∫ (x : γ), f ((κ (a, b)).rnDeriv (η (a, b)) x).toReal ∂η (a, b) + (derivAtTop f).toReal * (((κ (a, b)).singularPart (η (a, b))) Set.univ).toReal
theorem
ProbabilityTheory.integral_f_rnDeriv_mul_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 : 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))
:
theorem
ProbabilityTheory.integral_f_rnDeriv_mul_withDensity_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 : 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 η))
:
theorem
ProbabilityTheory.integral_f_rnDeriv_le_integral_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.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_deriv : derivAtTop f = ⊤ → ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
:
theorem
ProbabilityTheory.le_fDiv_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))
:
ProbabilityTheory.fDiv f μ ν ≤ ProbabilityTheory.fDiv f (μ.compProd κ) (ν.compProd η)
theorem
ProbabilityTheory.fDiv_fst_le
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : ℝ → ℝ}
[Nonempty β]
[StandardBorelSpace β]
(μ : MeasureTheory.Measure (α × β))
(ν : MeasureTheory.Measure (α × β))
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hf : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
:
ProbabilityTheory.fDiv f μ.fst ν.fst ≤ ProbabilityTheory.fDiv f μ ν
theorem
ProbabilityTheory.fDiv_snd_le
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : ℝ → ℝ}
[Nonempty α]
[StandardBorelSpace α]
(μ : MeasureTheory.Measure (α × β))
(ν : MeasureTheory.Measure (α × β))
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hf : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
:
ProbabilityTheory.fDiv f μ.snd ν.snd ≤ ProbabilityTheory.fDiv f μ ν
theorem
ProbabilityTheory.fDiv_comp_le_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : ℝ → ℝ}
[Nonempty α]
[StandardBorelSpace α]
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
:
ProbabilityTheory.fDiv f (μ.bind ⇑κ) (ν.bind ⇑η) ≤ ProbabilityTheory.fDiv f (μ.compProd κ) (ν.compProd η)
theorem
ProbabilityTheory.fDiv_comp_right_le
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : ℝ → ℝ}
[Nonempty α]
[StandardBorelSpace α]
[MeasurableSpace.CountableOrCountablyGenerated α β]
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsMarkovKernel κ]
(hf : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
:
ProbabilityTheory.fDiv f (μ.bind ⇑κ) (ν.bind ⇑κ) ≤ ProbabilityTheory.fDiv f μ ν
The Data Processing Inequality for the f-divergence.