f-Divergences

Main definitions

• FooBar

Main statements

• fooBar_unique

Notation

Implementation details

The most natural type for f is ℝ≥0∞ → EReal since we apply it to an ℝ≥0∞-valued RN derivative, and its value can be in general both positive or negative, and potentially +∞. However, we use ℝ → ℝ instead, for the following reasons:

• domain: convexity results like ConvexOn.map_average_le don't work for ℝ≥0∞ because they require a normed space with scalars in ℝ, but ℝ≥0∞ is a module over ℝ≥0. Also, the RN derivative is almost everywhere finite for σ-finite measures, so losing ∞ in the domain is not an issue.
• codomain: EReal is underdeveloped, and all functions we will actually use are finite anyway.

Most results will require these conditions on f: (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) (hf_one : f 1 = 0)

References

• [F. Bar, Quuxes][bibkey]

Tags

Foobars, barfoos

noncomputable def ProbabilityTheory.fDiv {α : Type u_1} {mα : MeasurableSpace α} (f : ℝ → ℝ) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) : EReal

f-Divergence of two measures.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.fDiv_of_not_integrable {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} (hf : ¬MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν) : ProbabilityTheory.fDiv f μ ν = ⊤

theorem ProbabilityTheory.fDiv_of_integrable {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} (hf : MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν) : ProbabilityTheory.fDiv f μ ν = ↑(∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν) + derivAtTop f * ↑((μ.singularPart ν) Set.univ)

theorem ProbabilityTheory.fDiv_ne_bot {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) : ProbabilityTheory.fDiv f μ ν ≠ ⊥

theorem ProbabilityTheory.fDiv_ne_bot_of_derivAtTop_nonneg {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} (hf : 0 ≤ derivAtTop f) : ProbabilityTheory.fDiv f μ ν ≠ ⊥

@[simp]

theorem ProbabilityTheory.fDiv_zero {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) : ProbabilityTheory.fDiv (fun (x : ℝ) => 0) μ ν = 0

@[simp]

theorem ProbabilityTheory.fDiv_zero_measure_left {α : Type u_1} {mα : MeasurableSpace α} {f : ℝ → ℝ} (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure ν] : ProbabilityTheory.fDiv f 0 ν = ↑(f 0) * ↑(ν Set.univ)

@[simp]

theorem ProbabilityTheory.fDiv_zero_measure_right {α : Type u_1} {mα : MeasurableSpace α} {f : ℝ → ℝ} (μ : MeasureTheory.Measure α) : ProbabilityTheory.fDiv f μ 0 = derivAtTop f * ↑(μ Set.univ)

@[simp]

theorem ProbabilityTheory.fDiv_const {α : Type u_1} {mα : MeasurableSpace α} (c : ℝ) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure ν] : ProbabilityTheory.fDiv (fun (x : ℝ) => c) μ ν = ↑(ν Set.univ) * ↑c

theorem ProbabilityTheory.fDiv_const' {α : Type u_1} {mα : MeasurableSpace α} {c : ℝ} (hc : 0 ≤ c) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) : ProbabilityTheory.fDiv (fun (x : ℝ) => c) μ ν = ↑(ν Set.univ) * ↑c

theorem ProbabilityTheory.fDiv_self {α : Type u_1} {mα : MeasurableSpace α} {f : ℝ → ℝ} (hf_one : f 1 = 0) (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : ProbabilityTheory.fDiv f μ μ = 0

@[simp]

theorem ProbabilityTheory.fDiv_id {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] : ProbabilityTheory.fDiv id μ ν = ↑(μ Set.univ)

@[simp]

theorem ProbabilityTheory.fDiv_id' {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] : ProbabilityTheory.fDiv (fun (x : ℝ) => x) μ ν = ↑(μ Set.univ)

theorem ProbabilityTheory.fDiv_congr' {α : Type u_1} {mα : MeasurableSpace α} {f : ℝ → ℝ} {g : ℝ → ℝ} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) (hfg : ∀ᵐ (x : ℝ) ∂MeasureTheory.Measure.map (fun (x : α) => (μ.rnDeriv ν x).toReal) ν, f x = g x) (hfg' : f =ᶠ[Filter.atTop] g) : ProbabilityTheory.fDiv f μ ν = ProbabilityTheory.fDiv g μ ν

theorem ProbabilityTheory.fDiv_congr {α : Type u_1} {mα : MeasurableSpace α} {f : ℝ → ℝ} {g : ℝ → ℝ} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) (h : ∀ x ≥ 0, f x = g x) : ProbabilityTheory.fDiv f μ ν = ProbabilityTheory.fDiv g μ ν

theorem ProbabilityTheory.fDiv_congr_measure {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : ℝ → ℝ} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {μ' : MeasureTheory.Measure β} {ν' : MeasureTheory.Measure β} (h_int : MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν ↔ MeasureTheory.Integrable (fun (x : β) => f (μ'.rnDeriv ν' x).toReal) ν') (h_eq : MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν → MeasureTheory.Integrable (fun (x : β) => f (μ'.rnDeriv ν' x).toReal) ν' → ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν = ∫ (x : β), f (μ'.rnDeriv ν' x).toReal ∂ν') (h_sing : (μ.singularPart ν) Set.univ = (μ'.singularPart ν') Set.univ) : ProbabilityTheory.fDiv f μ ν = ProbabilityTheory.fDiv f μ' ν'

theorem ProbabilityTheory.fDiv_eq_zero_of_forall_nonneg {α : Type u_1} {mα : MeasurableSpace α} {f : ℝ → ℝ} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) (hf : ∀ x ≥ 0, f x = 0) : ProbabilityTheory.fDiv f μ ν = 0

theorem ProbabilityTheory.fDiv_mul {α : Type u_1} {mα : MeasurableSpace α} {f : ℝ → ℝ} {c : ℝ} (hc : 0 ≤ c) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) : ProbabilityTheory.fDiv (fun (x : ℝ) => c * f x) μ ν = ↑c * ProbabilityTheory.fDiv f μ ν

theorem ProbabilityTheory.fDiv_mul_of_ne_top {α : Type u_1} {mα : MeasurableSpace α} {f : ℝ → ℝ} (c : ℝ) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (h_top : derivAtTop f ≠ ⊤) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (h_int : MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν) : ProbabilityTheory.fDiv (fun (x : ℝ) => c * f x) μ ν = ↑c * ProbabilityTheory.fDiv f μ ν

theorem ProbabilityTheory.fDiv_add {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} {g : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν) (hg : MeasureTheory.Integrable (fun (x : α) => g (μ.rnDeriv ν x).toReal) ν) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hg_cvx : ConvexOn ℝ (Set.Ici 0) g) : ProbabilityTheory.fDiv (fun (x : ℝ) => f x + g x) μ ν = ProbabilityTheory.fDiv f μ ν + ProbabilityTheory.fDiv g μ ν

theorem ProbabilityTheory.fDiv_add_const {α : Type u_1} {mα : MeasurableSpace α} {f : ℝ → ℝ} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (c : ℝ) : ProbabilityTheory.fDiv (fun (x : ℝ) => f x + c) μ ν = ProbabilityTheory.fDiv f μ ν + ↑c * ↑(ν Set.univ)

theorem ProbabilityTheory.fDiv_sub_const {α : Type u_1} {mα : MeasurableSpace α} {f : ℝ → ℝ} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (c : ℝ) : ProbabilityTheory.fDiv (fun (x : ℝ) => f x - c) μ ν = ProbabilityTheory.fDiv f μ ν - ↑c * ↑(ν Set.univ)

theorem ProbabilityTheory.fDiv_linear {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {c : ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : ProbabilityTheory.fDiv (fun (x : ℝ) => c * (x - 1)) μ ν = ↑c * (↑(μ Set.univ).toReal - ↑(ν Set.univ).toReal)

theorem ProbabilityTheory.fDiv_add_linear' {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} {c : ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) : ProbabilityTheory.fDiv (fun (x : ℝ) => f x + c * (x - 1)) μ ν = ProbabilityTheory.fDiv f μ ν + ↑c * (↑(μ Set.univ).toReal - ↑(ν Set.univ).toReal)

theorem ProbabilityTheory.fDiv_add_linear {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} {c : ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (h_eq : μ Set.univ = ν Set.univ) : ProbabilityTheory.fDiv (fun (x : ℝ) => f x + c * (x - 1)) μ ν = ProbabilityTheory.fDiv f μ ν

theorem ProbabilityTheory.fDiv_eq_fDiv_centeredFunction {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) : ProbabilityTheory.fDiv f μ ν = ProbabilityTheory.fDiv (fun (x : ℝ) => f x - f 1 - rightDeriv f 1 * (x - 1)) μ ν + ↑(f 1) * ↑(ν Set.univ) + ↑(rightDeriv f 1) * (↑(μ Set.univ).toReal - ↑(ν Set.univ).toReal)

theorem ProbabilityTheory.fDiv_of_mutuallySingular {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.SigmaFinite μ] [MeasureTheory.IsFiniteMeasure ν] (h : μ.MutuallySingular ν) : ProbabilityTheory.fDiv f μ ν = ↑(f 0) * ↑(ν Set.univ) + derivAtTop f * ↑(μ Set.univ)

theorem ProbabilityTheory.fDiv_of_absolutelyContinuous {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [Decidable (MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν)] (h : μ.AbsolutelyContinuous ν) : ProbabilityTheory.fDiv f μ ν = if MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν then ↑(∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν) else ⊤

theorem ProbabilityTheory.fDiv_eq_add_withDensity_singularPart {α : Type u_1} {mα : MeasurableSpace α} {f : ℝ → ℝ} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) : ProbabilityTheory.fDiv f μ ν = ProbabilityTheory.fDiv f (ν.withDensity (μ.rnDeriv ν)) ν + ProbabilityTheory.fDiv f (μ.singularPart ν) ν - ↑(f 0) * ↑(ν Set.univ)

theorem ProbabilityTheory.fDiv_eq_add_withDensity_singularPart' {α : Type u_1} {mα : MeasurableSpace α} {f : ℝ → ℝ} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) : ProbabilityTheory.fDiv f μ ν = ProbabilityTheory.fDiv (fun (x : ℝ) => f x - f 0) (ν.withDensity (μ.rnDeriv ν)) ν + ProbabilityTheory.fDiv f (μ.singularPart ν) ν

theorem ProbabilityTheory.fDiv_eq_add_withDensity_singularPart'' {α : Type u_1} {mα : MeasurableSpace α} {f : ℝ → ℝ} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) : ProbabilityTheory.fDiv f μ ν = ProbabilityTheory.fDiv f (ν.withDensity (μ.rnDeriv ν)) ν + ProbabilityTheory.fDiv (fun (x : ℝ) => f x - f 0) (μ.singularPart ν) ν

theorem ProbabilityTheory.fDiv_eq_add_withDensity_derivAtTop {α : Type u_1} {mα : MeasurableSpace α} {f : ℝ → ℝ} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) : ProbabilityTheory.fDiv f μ ν = ProbabilityTheory.fDiv f (ν.withDensity (μ.rnDeriv ν)) ν + derivAtTop f * ↑((μ.singularPart ν) Set.univ)

theorem ProbabilityTheory.fDiv_absolutelyContinuous_add_mutuallySingular {α : Type u_1} {mα : MeasurableSpace α} {f : ℝ → ℝ} {μ₁ : MeasureTheory.Measure α} {μ₂ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ₁] [MeasureTheory.IsFiniteMeasure μ₂] [MeasureTheory.IsFiniteMeasure ν] (h₁ : μ₁.AbsolutelyContinuous ν) (h₂ : μ₂.MutuallySingular ν) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) : ProbabilityTheory.fDiv f (μ₁ + μ₂) ν = ProbabilityTheory.fDiv f μ₁ ν + derivAtTop f * ↑(μ₂ Set.univ)

theorem ProbabilityTheory.fDiv_add_measure_le_of_ac {α : Type u_1} {mα : MeasurableSpace α} {f : ℝ → ℝ} {μ₁ : MeasureTheory.Measure α} {μ₂ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ₁] [MeasureTheory.IsFiniteMeasure μ₂] [MeasureTheory.IsFiniteMeasure ν] (h₁ : μ₁.AbsolutelyContinuous ν) (h₂ : μ₂.AbsolutelyContinuous ν) (hf : MeasureTheory.StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) : ProbabilityTheory.fDiv f (μ₁ + μ₂) ν ≤ ProbabilityTheory.fDiv f μ₁ ν + derivAtTop f * ↑(μ₂ Set.univ)

Auxiliary lemma for fDiv_add_measure_le.

theorem ProbabilityTheory.fDiv_add_measure_le {α : Type u_1} {mα : MeasurableSpace α} {f : ℝ → ℝ} (μ₁ : MeasureTheory.Measure α) (μ₂ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ₁] [MeasureTheory.IsFiniteMeasure μ₂] [MeasureTheory.IsFiniteMeasure ν] (hf : MeasureTheory.StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) : ProbabilityTheory.fDiv f (μ₁ + μ₂) ν ≤ ProbabilityTheory.fDiv f μ₁ ν + derivAtTop f * ↑(μ₂ Set.univ)

theorem ProbabilityTheory.fDiv_le_zero_add_top_of_ac {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hμν : μ.AbsolutelyContinuous ν) (hf : MeasureTheory.StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) : ProbabilityTheory.fDiv f μ ν ≤ ↑(f 0) * ↑(ν Set.univ) + derivAtTop f * ↑(μ Set.univ)

Auxiliary lemma for fDiv_le_zero_add_top.

theorem ProbabilityTheory.fDiv_le_zero_add_top {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hf : MeasureTheory.StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) : ProbabilityTheory.fDiv f μ ν ≤ ↑(f 0) * ↑(ν Set.univ) + derivAtTop f * ↑(μ Set.univ)

theorem ProbabilityTheory.fDiv_lt_top_of_ac {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} (h : μ.AbsolutelyContinuous ν) (h_int : MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν) : ProbabilityTheory.fDiv f μ ν < ⊤

theorem ProbabilityTheory.fDiv_of_not_ac {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hf : derivAtTop f = ⊤) (hμν : ¬μ.AbsolutelyContinuous ν) : ProbabilityTheory.fDiv f μ ν = ⊤

theorem ProbabilityTheory.fDiv_lt_top_iff_ac {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hf : derivAtTop f = ⊤) (h_int : MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν) : ProbabilityTheory.fDiv f μ ν < ⊤ ↔ μ.AbsolutelyContinuous ν

theorem ProbabilityTheory.fDiv_ne_top_iff_ac {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hf : derivAtTop f = ⊤) (h_int : MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν) : ProbabilityTheory.fDiv f μ ν ≠ ⊤ ↔ μ.AbsolutelyContinuous ν

theorem ProbabilityTheory.fDiv_eq_top_iff_not_ac {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hf : derivAtTop f = ⊤) (h_int : MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν) : ProbabilityTheory.fDiv f μ ν = ⊤ ↔ ¬μ.AbsolutelyContinuous ν

theorem ProbabilityTheory.fDiv_of_derivAtTop_eq_top {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hf : derivAtTop f = ⊤) [Decidable (MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν ∧ μ.AbsolutelyContinuous ν)] : ProbabilityTheory.fDiv f μ ν = if MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν ∧ μ.AbsolutelyContinuous ν then ↑(∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν) else ⊤

theorem ProbabilityTheory.fDiv_lt_top_of_derivAtTop_ne_top {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hf : derivAtTop f ≠ ⊤) (h_int : MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν) : ProbabilityTheory.fDiv f μ ν < ⊤

theorem ProbabilityTheory.fDiv_lt_top_of_derivAtTop_ne_top' {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h_top : derivAtTop f ≠ ⊤) (hf : MeasureTheory.StronglyMeasurable f) (h_cvx : ConvexOn ℝ (Set.Ici 0) f) : ProbabilityTheory.fDiv f μ ν < ⊤

theorem ProbabilityTheory.fDiv_lt_top_iff_of_derivAtTop_ne_top {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hf : derivAtTop f ≠ ⊤) : ProbabilityTheory.fDiv f μ ν < ⊤ ↔ MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν

theorem ProbabilityTheory.fDiv_ne_top_of_derivAtTop_ne_top {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h_top : derivAtTop f ≠ ⊤) (hf : MeasureTheory.StronglyMeasurable f) (h_cvx : ConvexOn ℝ (Set.Ici 0) f) : ProbabilityTheory.fDiv f μ ν ≠ ⊤

theorem ProbabilityTheory.fDiv_ne_top_iff_of_derivAtTop_ne_top {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hf : derivAtTop f ≠ ⊤) : ProbabilityTheory.fDiv f μ ν ≠ ⊤ ↔ MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν

theorem ProbabilityTheory.fDiv_eq_top_iff_of_derivAtTop_ne_top {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hf : derivAtTop f ≠ ⊤) : ProbabilityTheory.fDiv f μ ν = ⊤ ↔ ¬MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν

theorem ProbabilityTheory.fDiv_eq_top_iff {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.SigmaFinite ν] : ProbabilityTheory.fDiv f μ ν = ⊤ ↔ ¬MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν ∨ derivAtTop f = ⊤ ∧ ¬μ.AbsolutelyContinuous ν

theorem ProbabilityTheory.fDiv_eq_top_iff' {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hf : MeasureTheory.StronglyMeasurable f) (h_cvx : ConvexOn ℝ (Set.Ici 0) f) : ProbabilityTheory.fDiv f μ ν = ⊤ ↔ derivAtTop f = ⊤ ∧ (¬MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν ∨ ¬μ.AbsolutelyContinuous ν)

theorem ProbabilityTheory.fDiv_ne_top_iff {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.SigmaFinite ν] : ProbabilityTheory.fDiv f μ ν ≠ ⊤ ↔ MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν ∧ (derivAtTop f = ⊤ → μ.AbsolutelyContinuous ν)

theorem ProbabilityTheory.fDiv_ne_top_iff' {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hf : MeasureTheory.StronglyMeasurable f) (h_cvx : ConvexOn ℝ (Set.Ici 0) f) : ProbabilityTheory.fDiv f μ ν ≠ ⊤ ↔ derivAtTop f = ⊤ → MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν ∧ μ.AbsolutelyContinuous ν

theorem ProbabilityTheory.integrable_of_fDiv_ne_top {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} (h : ProbabilityTheory.fDiv f μ ν ≠ ⊤) : MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν

theorem ProbabilityTheory.fDiv_of_ne_top {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} (h : ProbabilityTheory.fDiv f μ ν ≠ ⊤) : ProbabilityTheory.fDiv f μ ν = ↑(∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν) + derivAtTop f * ↑((μ.singularPart ν) Set.univ)

theorem ProbabilityTheory.toReal_fDiv_of_integrable {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_int : MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν) (h_deriv : derivAtTop f = ⊤ → μ.AbsolutelyContinuous ν) : (ProbabilityTheory.fDiv f μ ν).toReal = ∫ (y : α), f (μ.rnDeriv ν y).toReal ∂ν + (derivAtTop f * ↑((μ.singularPart ν) Set.univ)).toReal

theorem ProbabilityTheory.le_fDiv_of_ac {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) (hμν : μ.AbsolutelyContinuous ν) : ↑(f (μ Set.univ).toReal) ≤ ProbabilityTheory.fDiv f μ ν

theorem ProbabilityTheory.f_measure_univ_le_add {α : Type u_1} {mα : MeasurableSpace α} {f : ℝ → ℝ} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) : ↑(f (μ Set.univ).toReal) ≤ ↑(f ((ν.withDensity (μ.rnDeriv ν)) Set.univ).toReal) + derivAtTop f * ↑((μ.singularPart ν) Set.univ)

theorem ProbabilityTheory.le_fDiv {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) : ↑(f (μ Set.univ).toReal) ≤ ProbabilityTheory.fDiv f μ ν

theorem ProbabilityTheory.fDiv_nonneg {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) (hf_one : f 1 = 0) : 0 ≤ ProbabilityTheory.fDiv f μ ν

theorem ProbabilityTheory.fDiv_mono'' {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} {g : ℝ → ℝ} (hf_int : MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν) (hfg : f ≤ᵐ[MeasureTheory.Measure.map (fun (x : α) => (μ.rnDeriv ν x).toReal) ν] g) (hfg' : derivAtTop f ≤ derivAtTop g) : ProbabilityTheory.fDiv f μ ν ≤ ProbabilityTheory.fDiv g μ ν

theorem ProbabilityTheory.fDiv_mono' {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} {g : ℝ → ℝ} (hf_int : MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν) (hfg : f ≤ g) (hfg' : derivAtTop f ≤ derivAtTop g) : ProbabilityTheory.fDiv f μ ν ≤ ProbabilityTheory.fDiv g μ ν

theorem ProbabilityTheory.fDiv_nonneg_of_nonneg {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} (hf : 0 ≤ f) (hf' : 0 ≤ derivAtTop f) : 0 ≤ ProbabilityTheory.fDiv f μ ν

theorem ProbabilityTheory.fDiv_eq_zero_iff {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h_mass : μ Set.univ = ν Set.univ) (hf_deriv : derivAtTop f = ⊤) (hf_cvx : StrictConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) (hf_one : f 1 = 0) : ProbabilityTheory.fDiv f μ ν = 0 ↔ μ = ν

theorem ProbabilityTheory.fDiv_eq_zero_iff' {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hf_deriv : derivAtTop f = ⊤) (hf_cvx : StrictConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) (hf_one : f 1 = 0) : ProbabilityTheory.fDiv f μ ν = 0 ↔ μ = ν

theorem ProbabilityTheory.fDiv_map_measurableEmbedding {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {g : α → β} (hg : MeasurableEmbedding g) : ProbabilityTheory.fDiv f (MeasureTheory.Measure.map g μ) (MeasureTheory.Measure.map g ν) = ProbabilityTheory.fDiv f μ ν

theorem ProbabilityTheory.fDiv_restrict_of_integrable {α : Type u_1} {mα : MeasurableSpace α} {f : ℝ → ℝ} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {s : Set α} (hs : MeasurableSet s) (h_int : MeasureTheory.IntegrableOn (fun (x : α) => f (μ.rnDeriv ν x).toReal) s ν) : ProbabilityTheory.fDiv f (μ.restrict s) ν = ↑(∫ (x : α) in s, f (μ.rnDeriv ν x).toReal ∂ν) + ↑(f 0) * ↑(ν sᶜ) + derivAtTop f * ↑((μ.singularPart ν) s)