Hellinger divergence

Main definitions

• FooBar

Main statements

• fooBar_unique

Notation

Implementation details

theorem ProbabilityTheory.integral_rpow_rnDeriv {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} (ha_pos : 0 < a) (ha : a ≠ 1) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] : ∫ (x : α), (μ.rnDeriv ν x).toReal ^ a ∂ν = ∫ (x : α), (ν.rnDeriv μ x).toReal ^ (1 - a) ∂μ

theorem ProbabilityTheory.integrable_rpow_rnDeriv_iff {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} [MeasureTheory.SigmaFinite ν] [MeasureTheory.SigmaFinite μ] (hμν : μ.AbsolutelyContinuous ν) (ha : 0 < a) : MeasureTheory.Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal ^ a) μ ↔ MeasureTheory.Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal ^ (1 + a)) ν

theorem ProbabilityTheory.integral_fun_rnDeriv_eq_zero_iff_mutuallySingular {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] {f : ENNReal → ℝ} (hf_nonneg : ∀ (x : ENNReal), 0 ≤ f x) (hf_zero : ∀ (x : ENNReal), f x = 0 ↔ x = 0 ∨ x = ⊤) (h_int : MeasureTheory.Integrable (f ∘ μ.rnDeriv ν) ν) : ∫ (x : α), f (μ.rnDeriv ν x) ∂ν = 0 ↔ μ.MutuallySingular ν

theorem ProbabilityTheory.integral_rpow_rnDeriv_eq_zero_iff_mutuallySingular {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (ha_zero : a ≠ 0) (h_int : MeasureTheory.Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal ^ a) ν) : ∫ (x : α), (μ.rnDeriv ν x).toReal ^ a ∂ν = 0 ↔ μ.MutuallySingular ν

theorem ProbabilityTheory.integral_rpow_rnDeriv_pos_iff_not_mutuallySingular {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (ha_zero : a ≠ 0) (h_int : MeasureTheory.Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal ^ a) ν) : 0 < ∫ (x : α), (μ.rnDeriv ν x).toReal ^ a ∂ν ↔ ¬μ.MutuallySingular ν

noncomputable def ProbabilityTheory.hellingerFun (a : ℝ) : ℝ → ℝ

Hellinger function, defined as x ↦ (a - 1)⁻¹ * (x ^ a - 1) for a ∈ (0, 1) ∪ (1, + ∞). At 0 the function is obtained by contiuity and is the indicator function of {0}. At 1 it is defined as x ↦ x * log x, because in this way we obtain that the Hellinger divergence at 1 conincides with the KL divergence, which is natural for continuity reasons.

Equations

• ProbabilityTheory.hellingerFun a = if a = 0 then fun (x : ℝ) => if x = 0 then 1 else 0 else if a = 1 then fun (x : ℝ) => x * Real.log x else fun (x : ℝ) => (a - 1)⁻¹ * (x ^ a - 1)

theorem ProbabilityTheory.hellingerFun_zero : ProbabilityTheory.hellingerFun 0 = fun (x : ℝ) => if x = 0 then 1 else 0

theorem ProbabilityTheory.hellingerFun_zero' : ProbabilityTheory.hellingerFun 0 = fun (x : ℝ) => 0 ^ x

theorem ProbabilityTheory.hellingerFun_zero'' : ProbabilityTheory.hellingerFun 0 = {0}.indicator 1

@[simp]

theorem ProbabilityTheory.hellingerFun_one : ProbabilityTheory.hellingerFun 1 = fun (x : ℝ) => x * Real.log x

theorem ProbabilityTheory.hellingerFun_of_ne_zero_of_ne_one {a : ℝ} (ha_zero : a ≠ 0) (ha_one : a ≠ 1) : ProbabilityTheory.hellingerFun a = fun (x : ℝ) => (a - 1)⁻¹ * (x ^ a - 1)

theorem ProbabilityTheory.continuous_rpow_const {a : ℝ} (ha_nonneg : 0 ≤ a) : Continuous fun (x : ℝ) => x ^ a

theorem ProbabilityTheory.continuous_hellingerFun {a : ℝ} (ha_pos : 0 < a) : Continuous (ProbabilityTheory.hellingerFun a)

theorem ProbabilityTheory.stronglyMeasurable_hellingerFun {a : ℝ} (ha_nonneg : 0 ≤ a) : MeasureTheory.StronglyMeasurable (ProbabilityTheory.hellingerFun a)

@[simp]

theorem ProbabilityTheory.hellingerFun_apply_one_eq_zero {a : ℝ} : ProbabilityTheory.hellingerFun a 1 = 0

theorem ProbabilityTheory.hellingerFun_apply_zero {a : ℝ} : ProbabilityTheory.hellingerFun a 0 = (1 - a)⁻¹

theorem ProbabilityTheory.convexOn_hellingerFun {a : ℝ} (ha_pos : 0 ≤ a) : ConvexOn ℝ (Set.Ici 0) (ProbabilityTheory.hellingerFun a)

theorem ProbabilityTheory.hasDerivAt_hellingerFun (a : ℝ) {x : ℝ} (hx : x ≠ 0) : HasDerivAt (ProbabilityTheory.hellingerFun a) (if a = 0 then 0 else if a = 1 then Real.log x + 1 else (a - 1)⁻¹ * a * x ^ (a - 1)) x

theorem ProbabilityTheory.rightDeriv_hellingerFun (a : ℝ) {x : ℝ} (hx : x ≠ 0) : rightDeriv (ProbabilityTheory.hellingerFun a) x = if a = 0 then 0 else if a = 1 then Real.log x + 1 else (a - 1)⁻¹ * a * x ^ (a - 1)

theorem ProbabilityTheory.tendsto_rightDeriv_hellingerFun_atTop_of_one_lt {a : ℝ} (ha : 1 < a) : Filter.Tendsto (rightDeriv (ProbabilityTheory.hellingerFun a)) Filter.atTop Filter.atTop

theorem ProbabilityTheory.tendsto_rightDeriv_hellingerFun_atTop_of_lt_one {a : ℝ} (ha : a < 1) : Filter.Tendsto (rightDeriv (ProbabilityTheory.hellingerFun a)) Filter.atTop (nhds 0)

theorem ProbabilityTheory.derivAtTop_hellingerFun_of_one_lt {a : ℝ} (ha : 1 < a) : derivAtTop (ProbabilityTheory.hellingerFun a) = ⊤

theorem ProbabilityTheory.derivAtTop_hellingerFun_of_one_le {a : ℝ} (ha : 1 ≤ a) : derivAtTop (ProbabilityTheory.hellingerFun a) = ⊤

theorem ProbabilityTheory.derivAtTop_hellingerFun_of_lt_one {a : ℝ} (ha : a < 1) : derivAtTop (ProbabilityTheory.hellingerFun a) = 0

theorem ProbabilityTheory.integrable_hellingerFun_iff_integrable_rpow {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} (ha_one : a ≠ 1) [MeasureTheory.IsFiniteMeasure ν] : MeasureTheory.Integrable (fun (x : α) => ProbabilityTheory.hellingerFun a (μ.rnDeriv ν x).toReal) ν ↔ MeasureTheory.Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal ^ a) ν

theorem ProbabilityTheory.integrable_hellingerFun_zero {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure ν] : MeasureTheory.Integrable (fun (x : α) => ProbabilityTheory.hellingerFun 0 (μ.rnDeriv ν x).toReal) ν

theorem ProbabilityTheory.integrable_hellingerFun_rnDeriv_of_lt_one {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} (ha_nonneg : 0 ≤ a) (ha : a < 1) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : MeasureTheory.Integrable (fun (x : α) => ProbabilityTheory.hellingerFun a (μ.rnDeriv ν x).toReal) ν

theorem ProbabilityTheory.integrable_rpow_rnDeriv_of_lt_one {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} (ha_nonneg : 0 ≤ a) (ha : a < 1) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : MeasureTheory.Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal ^ a) ν

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

Hellinger divergence of order a. The cases a = 0 and a = 1 are defined separately inside the definition of the Hellinger function, so that in the case a = 0 we have hellingerDiv 0 μ ν = ν {x | (∂μ/∂ν) x = 0}, and in the case a = 1 the Hellinger divergence coincides with the KL divergence.

Equations

• ProbabilityTheory.hellingerDiv a μ ν = ProbabilityTheory.fDiv (ProbabilityTheory.hellingerFun a) μ ν

theorem ProbabilityTheory.hellingerDiv_zero {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) : ProbabilityTheory.hellingerDiv 0 μ ν = ↑(ν {x : α | (μ.rnDeriv ν x).toReal = 0})

theorem ProbabilityTheory.hellingerDiv_zero' {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : ProbabilityTheory.hellingerDiv 0 μ ν = ↑(ν {x : α | μ.rnDeriv ν x = 0})

theorem ProbabilityTheory.hellingerDiv_zero'' {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.IsFiniteMeasure ν] : ProbabilityTheory.hellingerDiv 0 μ ν = ↑(ν Set.univ) - ↑(ν {x : α | 0 < μ.rnDeriv ν x})

theorem ProbabilityTheory.hellingerDiv_zero_toReal {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.IsFiniteMeasure ν] : (ProbabilityTheory.hellingerDiv 0 μ ν).toReal = (ν Set.univ).toReal - (ν {x : α | 0 < μ.rnDeriv ν x}).toReal

theorem ProbabilityTheory.hellingerDiv_zero_ne_top {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure ν] : ProbabilityTheory.hellingerDiv 0 μ ν ≠ ⊤

@[simp]

theorem ProbabilityTheory.hellingerDiv_one {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] : ProbabilityTheory.hellingerDiv 1 μ ν = ProbabilityTheory.kl μ ν

@[simp]

theorem ProbabilityTheory.hellingerDiv_zero_measure_left {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure ν] : ProbabilityTheory.hellingerDiv a 0 ν = ↑(1 - a)⁻¹ * ↑(ν Set.univ)

@[simp]

theorem ProbabilityTheory.hellingerDiv_zero_measure_right_of_lt_one {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} (ha : a < 1) (μ : MeasureTheory.Measure α) : ProbabilityTheory.hellingerDiv a μ 0 = 0

@[simp]

theorem ProbabilityTheory.hellingerDiv_zero_measure_right_of_one_le {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} (ha : 1 ≤ a) (μ : MeasureTheory.Measure α) [hμ : NeZero μ] : ProbabilityTheory.hellingerDiv a μ 0 = ⊤

theorem ProbabilityTheory.hellingerDiv_eq_integral_of_integrable_of_ac {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} (h_int : MeasureTheory.Integrable (fun (x : α) => ProbabilityTheory.hellingerFun a (μ.rnDeriv ν x).toReal) ν) (h_ac : 1 ≤ a → μ.AbsolutelyContinuous ν) : ProbabilityTheory.hellingerDiv a μ ν = ↑(∫ (x : α), ProbabilityTheory.hellingerFun a (μ.rnDeriv ν x).toReal ∂ν)

If a ≤ 1 use hellingerDiv_eq_integral_of_integrable_of_le_one or hellingerDiv_eq_integral_of_le_one, as they have fewer hypotheses.

theorem ProbabilityTheory.hellingerDiv_eq_integral_of_integrable_of_lt_one {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} (ha : a < 1) (h_int : MeasureTheory.Integrable (fun (x : α) => ProbabilityTheory.hellingerFun a (μ.rnDeriv ν x).toReal) ν) : ProbabilityTheory.hellingerDiv a μ ν = ↑(∫ (x : α), ProbabilityTheory.hellingerFun a (μ.rnDeriv ν x).toReal ∂ν)

theorem ProbabilityTheory.hellingerDiv_eq_integral_of_lt_one {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} (ha_nonneg : 0 ≤ a) (ha : a < 1) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : ProbabilityTheory.hellingerDiv a μ ν = ↑(∫ (x : α), ProbabilityTheory.hellingerFun a (μ.rnDeriv ν x).toReal ∂ν)

theorem ProbabilityTheory.hellingerDiv_of_not_integrable {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} (h : ¬MeasureTheory.Integrable (fun (x : α) => ProbabilityTheory.hellingerFun a (μ.rnDeriv ν x).toReal) ν) : ProbabilityTheory.hellingerDiv a μ ν = ⊤

theorem ProbabilityTheory.hellingerDiv_of_one_lt_not_ac {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} (ha : 1 ≤ a) (h_ac : ¬μ.AbsolutelyContinuous ν) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] : ProbabilityTheory.hellingerDiv a μ ν = ⊤

theorem ProbabilityTheory.hellingerDiv_eq_top_iff {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] : ProbabilityTheory.hellingerDiv a μ ν = ⊤ ↔ ¬MeasureTheory.Integrable (fun (x : α) => ProbabilityTheory.hellingerFun a (μ.rnDeriv ν x).toReal) ν ∨ 1 ≤ a ∧ ¬μ.AbsolutelyContinuous ν

theorem ProbabilityTheory.hellingerDiv_ne_top_iff {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] : ProbabilityTheory.hellingerDiv a μ ν ≠ ⊤ ↔ MeasureTheory.Integrable (fun (x : α) => ProbabilityTheory.hellingerFun a (μ.rnDeriv ν x).toReal) ν ∧ (1 ≤ a → μ.AbsolutelyContinuous ν)

theorem ProbabilityTheory.hellingerDiv_eq_top_iff_of_one_le {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} (ha : 1 ≤ a) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] : ProbabilityTheory.hellingerDiv a μ ν = ⊤ ↔ ¬MeasureTheory.Integrable (fun (x : α) => ProbabilityTheory.hellingerFun a (μ.rnDeriv ν x).toReal) ν ∨ ¬μ.AbsolutelyContinuous ν

theorem ProbabilityTheory.hellingerDiv_ne_top_iff_of_one_le {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} (ha : 1 ≤ a) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] : ProbabilityTheory.hellingerDiv a μ ν ≠ ⊤ ↔ MeasureTheory.Integrable (fun (x : α) => ProbabilityTheory.hellingerFun a (μ.rnDeriv ν x).toReal) ν ∧ μ.AbsolutelyContinuous ν

theorem ProbabilityTheory.hellingerDiv_eq_top_iff_of_one_lt {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} (ha : 1 < a) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.IsFiniteMeasure ν] : ProbabilityTheory.hellingerDiv a μ ν = ⊤ ↔ ¬MeasureTheory.Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal ^ a) ν ∨ ¬μ.AbsolutelyContinuous ν

theorem ProbabilityTheory.hellingerDiv_ne_top_iff_of_one_lt {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} (ha : 1 < a) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.IsFiniteMeasure ν] : ProbabilityTheory.hellingerDiv a μ ν ≠ ⊤ ↔ MeasureTheory.Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal ^ a) ν ∧ μ.AbsolutelyContinuous ν

theorem ProbabilityTheory.hellingerDiv_eq_top_iff_of_lt_one {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} (ha : a < 1) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) : ProbabilityTheory.hellingerDiv a μ ν = ⊤ ↔ ¬MeasureTheory.Integrable (fun (x : α) => ProbabilityTheory.hellingerFun a (μ.rnDeriv ν x).toReal) ν

theorem ProbabilityTheory.hellingerDiv_ne_top_iff_of_lt_one {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} (ha : a < 1) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) : ProbabilityTheory.hellingerDiv a μ ν ≠ ⊤ ↔ MeasureTheory.Integrable (fun (x : α) => ProbabilityTheory.hellingerFun a (μ.rnDeriv ν x).toReal) ν

theorem ProbabilityTheory.hellingerDiv_ne_top_of_lt_one {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} (ha_nonneg : 0 ≤ a) (ha : a < 1) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : ProbabilityTheory.hellingerDiv a μ ν ≠ ⊤

theorem ProbabilityTheory.hellingerDiv_ne_bot {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} : ProbabilityTheory.hellingerDiv a μ ν ≠ ⊥

theorem ProbabilityTheory.hellingerDiv_eq_integral_of_ne_top {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.SigmaFinite ν] (h : ProbabilityTheory.hellingerDiv a μ ν ≠ ⊤) : ProbabilityTheory.hellingerDiv a μ ν = ↑(∫ (x : α), ProbabilityTheory.hellingerFun a (μ.rnDeriv ν x).toReal ∂ν)

theorem ProbabilityTheory.hellingerDiv_eq_integral_of_ne_top' {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} (ha_ne_zero : a ≠ 0) (ha_ne_one : a ≠ 1) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : ProbabilityTheory.hellingerDiv a μ ν ≠ ⊤) : ProbabilityTheory.hellingerDiv a μ ν = ↑(a - 1)⁻¹ * ↑(∫ (x : α), (μ.rnDeriv ν x).toReal ^ a ∂ν) - ↑(a - 1)⁻¹ * ↑(ν Set.univ)

theorem ProbabilityTheory.hellingerDiv_eq_integral_of_ne_top'' {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} (ha_ne_zero : a ≠ 0) (ha_ne_one : a ≠ 1) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (h : ProbabilityTheory.hellingerDiv a μ ν ≠ ⊤) : ProbabilityTheory.hellingerDiv a μ ν = ↑(a - 1)⁻¹ * ↑(∫ (x : α), (μ.rnDeriv ν x).toReal ^ a ∂ν) - ↑(a - 1)⁻¹

theorem ProbabilityTheory.hellingerDiv_eq_integral_of_lt_one' {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} (ha_pos : 0 < a) (ha : a < 1) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : ProbabilityTheory.hellingerDiv a μ ν = ↑(a - 1)⁻¹ * ↑(∫ (x : α), (μ.rnDeriv ν x).toReal ^ a ∂ν) - ↑(a - 1)⁻¹ * ↑(ν Set.univ)

theorem ProbabilityTheory.hellingerDiv_toReal_of_lt_one {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} (ha_pos : 0 < a) (ha : a < 1) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : (ProbabilityTheory.hellingerDiv a μ ν).toReal = (a - 1)⁻¹ * ∫ (x : α), (μ.rnDeriv ν x).toReal ^ a ∂ν - (a - 1)⁻¹ * (ν Set.univ).toReal

theorem ProbabilityTheory.hellingerDiv_of_mutuallySingular_of_one_le {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} (ha : 1 ≤ a) [NeZero μ] [MeasureTheory.SigmaFinite μ] [MeasureTheory.IsFiniteMeasure ν] (hμν : μ.MutuallySingular ν) : ProbabilityTheory.hellingerDiv a μ ν = ⊤

theorem ProbabilityTheory.hellingerDiv_of_mutuallySingular_of_lt_one {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} (ha : a < 1) [MeasureTheory.SigmaFinite μ] [MeasureTheory.IsFiniteMeasure ν] (hμν : μ.MutuallySingular ν) : ProbabilityTheory.hellingerDiv a μ ν = ↑(1 - a)⁻¹ * ↑(ν Set.univ)

theorem ProbabilityTheory.hellingerDiv_le_of_lt_one {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} (ha_nonneg : 0 ≤ a) (ha : a < 1) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : ProbabilityTheory.hellingerDiv a μ ν ≤ ↑(1 - a)⁻¹ * ↑(ν Set.univ)

theorem ProbabilityTheory.hellingerDiv_symm' {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} (ha_pos : 0 < a) (ha : a < 1) (h_eq : μ Set.univ = ν Set.univ) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : (1 - ↑a) * ProbabilityTheory.hellingerDiv a μ ν = ↑a * ProbabilityTheory.hellingerDiv (1 - a) ν μ

theorem ProbabilityTheory.hellingerDiv_symm {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} (ha_pos : 0 < a) (ha : a < 1) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : (1 - ↑a) * ProbabilityTheory.hellingerDiv a μ ν = ↑a * ProbabilityTheory.hellingerDiv (1 - a) ν μ

theorem ProbabilityTheory.hellingerDiv_zero_nonneg {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) : 0 ≤ ProbabilityTheory.hellingerDiv 0 μ ν

theorem ProbabilityTheory.hellingerDiv_nonneg {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} (ha_pos : 0 ≤ a) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : 0 ≤ ProbabilityTheory.hellingerDiv a μ ν

In this section there are results about the expression ν(α) + (a - 1) * Hₐ(μ, ν), which appears in the definition of the Renyi divergence.

theorem ProbabilityTheory.meas_univ_add_mul_hellingerDiv_eq {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} (ha_ne_zero : a ≠ 0) (ha_ne_one : a ≠ 1) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : ProbabilityTheory.hellingerDiv a μ ν ≠ ⊤) : ↑(ν Set.univ) + (↑a - 1) * ProbabilityTheory.hellingerDiv a μ ν = ↑(∫ (x : α), (μ.rnDeriv ν x).toReal ^ a ∂ν)

theorem ProbabilityTheory.meas_univ_add_mul_hellingerDiv_zero_eq {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} (ha : a = 0) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : ↑(ν Set.univ) + (↑a - 1) * ProbabilityTheory.hellingerDiv a μ ν = ↑(ν {x : α | 0 < μ.rnDeriv ν x})

theorem ProbabilityTheory.meas_univ_add_mul_hellingerDiv_nonneg_of_le_one {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} (ha_nonneg : 0 ≤ a) (ha : a ≤ 1) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : 0 ≤ ↑(ν Set.univ) + (↑a - 1) * ProbabilityTheory.hellingerDiv a μ ν

theorem ProbabilityTheory.meas_univ_add_mul_hellingerDiv_nonneg_of_one_lt {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} (ha : 1 < a) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : 0 ≤ ↑(ν Set.univ) + (↑a - 1) * ProbabilityTheory.hellingerDiv a μ ν

theorem ProbabilityTheory.meas_univ_add_mul_hellingerDiv_nonneg {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} (ha_nonneg : 0 ≤ a) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : 0 ≤ ↑(ν Set.univ) + (↑a - 1) * ProbabilityTheory.hellingerDiv a μ ν

theorem ProbabilityTheory.meas_univ_add_mul_hellingerDiv_eq_zero_iff {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} (ha_ne_one : a ≠ 1) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : ↑(ν Set.univ) + (↑a - 1) * ProbabilityTheory.hellingerDiv a μ ν = 0 ↔ μ.MutuallySingular ν ∧ ProbabilityTheory.hellingerDiv a μ ν ≠ ⊤

theorem ProbabilityTheory.meas_univ_add_mul_hellingerDiv_eq_zero_iff_of_lt_one {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} (ha : a < 1) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : ↑(ν Set.univ) + (↑a - 1) * ProbabilityTheory.hellingerDiv a μ ν = 0 ↔ μ.MutuallySingular ν

theorem ProbabilityTheory.meas_univ_add_mul_hellingerDiv_eq_zero_iff_of_one_lt {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} (ha : 1 < a) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : ↑(ν Set.univ) + (↑a - 1) * ProbabilityTheory.hellingerDiv a μ ν = 0 ↔ μ = 0

theorem ProbabilityTheory.toENNReal_meas_univ_add_mul_hellingerDiv_eq_zero_iff_of_lt_one {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} (ha_nonneg : 0 ≤ a) (ha : a < 1) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : (↑(ν Set.univ) + (↑a - 1) * ProbabilityTheory.hellingerDiv a μ ν).toENNReal = 0 ↔ μ.MutuallySingular ν

theorem ProbabilityTheory.toENNReal_meas_univ_add_mul_hellingerDiv_eq_zero_iff_of_one_lt {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} (ha : 1 < a) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : (↑(ν Set.univ) + (↑a - 1) * ProbabilityTheory.hellingerDiv a μ ν).toENNReal = 0 ↔ μ = 0

theorem ProbabilityTheory.meas_univ_add_mul_hellingerDiv_ne_top_of_lt_one {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} (ha : a < 1) [MeasureTheory.IsFiniteMeasure ν] : ↑(ν Set.univ) + (↑a - 1) * ProbabilityTheory.hellingerDiv a μ ν ≠ ⊤

theorem ProbabilityTheory.meas_univ_add_mul_hellingerDiv_eq_top_iff_of_one_lt {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {a : ℝ} (ha : 1 < a) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : ↑(ν Set.univ) + (↑a - 1) * ProbabilityTheory.hellingerDiv a μ ν = ⊤ ↔ ¬MeasureTheory.Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal ^ a) ν ∨ ¬μ.AbsolutelyContinuous ν

theorem ProbabilityTheory.le_hellingerDiv_compProd {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} {β : Type u_2} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (ha_pos : 0 < a) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η] : ProbabilityTheory.hellingerDiv a μ ν ≤ ProbabilityTheory.hellingerDiv a (μ.compProd κ) (ν.compProd η)

theorem ProbabilityTheory.hellingerDiv_fst_le {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} {β : Type u_2} {mβ : MeasurableSpace β} [Nonempty β] [StandardBorelSpace β] (ha_pos : 0 < a) (μ : MeasureTheory.Measure (α × β)) (ν : MeasureTheory.Measure (α × β)) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : ProbabilityTheory.hellingerDiv a μ.fst ν.fst ≤ ProbabilityTheory.hellingerDiv a μ ν

theorem ProbabilityTheory.hellingerDiv_snd_le {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} {β : Type u_2} {mβ : MeasurableSpace β} [Nonempty α] [StandardBorelSpace α] (ha_pos : 0 < a) (μ : MeasureTheory.Measure (α × β)) (ν : MeasureTheory.Measure (α × β)) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : ProbabilityTheory.hellingerDiv a μ.snd ν.snd ≤ ProbabilityTheory.hellingerDiv a μ ν

theorem ProbabilityTheory.hellingerDiv_comp_le_compProd {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} {β : Type u_2} {mβ : MeasurableSpace β} [Nonempty α] [StandardBorelSpace α] (ha_pos : 0 < a) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.hellingerDiv a (μ.bind ⇑κ) (ν.bind ⇑η) ≤ ProbabilityTheory.hellingerDiv a (μ.compProd κ) (ν.compProd η)

theorem ProbabilityTheory.hellingerDiv_comp_right_le {α : Type u_1} {mα : MeasurableSpace α} {a : ℝ} {β : Type u_2} {mβ : MeasurableSpace β} [Nonempty α] [StandardBorelSpace α] (ha_pos : 0 < a) [MeasurableSpace.CountableOrCountablyGenerated α β] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel κ] : ProbabilityTheory.hellingerDiv a (μ.bind ⇑κ) (ν.bind ⇑κ) ≤ ProbabilityTheory.hellingerDiv a μ ν

The Data Processing Inequality for the Hellinger divergence.