f-Divergences on sub-sigma-algebras #
Main statements #
fDiv_map_le: data processing inequality for f-divergences and measurable functionsfDiv_trim_le: data processing inequality for f-divergences and sub-sigma-algebras
theorem
ProbabilityTheory.fDiv_map_le_of_map_le_of_ac
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{ν : MeasureTheory.Measure α}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure ν]
(hf : MeasureTheory.StronglyMeasurable f)
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
{g : α → β}
(hg : Measurable g)
(h : ∀ (μ : MeasureTheory.Measure α),
MeasureTheory.IsFiniteMeasure μ →
μ.AbsolutelyContinuous ν →
ProbabilityTheory.fDiv f (MeasureTheory.Measure.map g μ) (MeasureTheory.Measure.map g ν) ≤ ProbabilityTheory.fDiv f μ ν)
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
:
ProbabilityTheory.fDiv f (MeasureTheory.Measure.map g μ) (MeasureTheory.Measure.map g ν) ≤ ProbabilityTheory.fDiv f μ ν
To prove the DPI for an f-divergence, for the map by a function, it suffices to prove it under an absolute continuity hypothesis.
theorem
ProbabilityTheory.f_rnDeriv_map_le
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hμν : μ.AbsolutelyContinuous ν)
{g : α → β}
(hg : Measurable g)
(hf : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
(h_int : MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν)
:
(fun (x : α) => f ((MeasureTheory.Measure.map g μ).rnDeriv (MeasureTheory.Measure.map g ν) (g x)).toReal) ≤ᵐ[ν] MeasureTheory.condexp (MeasurableSpace.comap g mβ) ν fun (x : α) => f (μ.rnDeriv ν x).toReal
theorem
ProbabilityTheory.integrable_f_rnDeriv_map
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hμν : μ.AbsolutelyContinuous ν)
{g : α → β}
(hg : Measurable g)
(hf : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
(h_int : MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν)
:
MeasureTheory.Integrable
(fun (x : β) => f ((MeasureTheory.Measure.map g μ).rnDeriv (MeasureTheory.Measure.map g ν) x).toReal)
(MeasureTheory.Measure.map g ν)
theorem
ProbabilityTheory.fDiv_map_of_ac
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hμν : μ.AbsolutelyContinuous ν)
{g : α → β}
(hg : Measurable g)
(hf : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
(h_int : MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν)
:
ProbabilityTheory.fDiv f (MeasureTheory.Measure.map g μ) (MeasureTheory.Measure.map g ν) = ↑(∫ (x : α), f (MeasureTheory.condexp (MeasurableSpace.comap g mβ) ν (fun (x : α) => (μ.rnDeriv ν x).toReal) x) ∂ν)
theorem
ProbabilityTheory.fDiv_trim_of_ac
{α : Type u_1}
{m : MeasurableSpace α}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hm : m ≤ mα)
(hμν : μ.AbsolutelyContinuous ν)
(hf : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
(h_int : MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν)
:
ProbabilityTheory.fDiv f (μ.trim hm) (ν.trim hm) = ↑(∫ (x : α), f (MeasureTheory.condexp m ν (fun (x : α) => (μ.rnDeriv ν x).toReal) x) ∂ν)
theorem
ProbabilityTheory.f_rnDeriv_trim_le
{α : Type u_1}
{m : MeasurableSpace α}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hm : m ≤ mα)
(hμν : μ.AbsolutelyContinuous ν)
(hf : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
(h_int : MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν)
:
(fun (x : α) => f ((μ.trim hm).rnDeriv (ν.trim hm) x).toReal) ≤ᵐ[ν.trim hm] MeasureTheory.condexp m ν fun (x : α) => f (μ.rnDeriv ν x).toReal
theorem
ProbabilityTheory.integrable_f_rnDeriv_trim
{α : Type u_1}
{m : MeasurableSpace α}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hm : m ≤ mα)
(hμν : μ.AbsolutelyContinuous ν)
(hf : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
(h_int : MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν)
:
MeasureTheory.Integrable (fun (x : α) => f ((μ.trim hm).rnDeriv (ν.trim hm) x).toReal) (ν.trim hm)
theorem
ProbabilityTheory.integrable_f_condexp_rnDeriv
{α : Type u_1}
{m : MeasurableSpace α}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hm : m ≤ mα)
(hμν : μ.AbsolutelyContinuous ν)
(hf : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
(h_int : MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν)
:
MeasureTheory.Integrable (fun (x : α) => f (MeasureTheory.condexp m ν (fun (x : α) => (μ.rnDeriv ν x).toReal) x)) ν
theorem
ProbabilityTheory.fDiv_map_le
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
{g : α → β}
(hg : Measurable g)
(hf : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
:
ProbabilityTheory.fDiv f (MeasureTheory.Measure.map g μ) (MeasureTheory.Measure.map g ν) ≤ ProbabilityTheory.fDiv f μ ν
Data processing inequality for f-divergences and measurable functions.
theorem
ProbabilityTheory.fDiv_trim_le
{α : Type u_1}
{m : MeasurableSpace α}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hm : m ≤ mα)
(hf : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
:
ProbabilityTheory.fDiv f (μ.trim hm) (ν.trim hm) ≤ ProbabilityTheory.fDiv f μ ν
Data processing inequality for f-divergences and sub-sigma-algebras.
theorem
ProbabilityTheory.fDiv_trim_comap_rnDeriv_of_ac
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hμν : μ.AbsolutelyContinuous ν)
(hf : MeasureTheory.StronglyMeasurable f)
:
ProbabilityTheory.fDiv f (μ.trim ⋯) (ν.trim ⋯) = ProbabilityTheory.fDiv f μ ν
The f-divergence of two measures restricted to the sigma-algebras generated by their Radon-Nikodym derivative is the f-divergence of the unrestricted measures. The restriction to that sigma-algebra is useful because it is countably generated.