Rényi divergence #
Main definitions #
FooBar
Main statements #
fooBar_unique
Notation #
Implementation details #
theorem
ProbabilityTheory.exp_mul_llr
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
(hνμ : ν.AbsolutelyContinuous μ)
:
theorem
ProbabilityTheory.exp_mul_llr'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
(hμν : μ.AbsolutelyContinuous ν)
:
noncomputable def
ProbabilityTheory.renyiDiv
{α : Type u_1}
{mα : MeasurableSpace α}
(a : ℝ)
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
:
Rényi divergence of order a. If a = 1, it is defined as kl μ ν, otherwise as
(a - 1)⁻¹ * log (ν(α) + (a - 1) * Hₐ(μ, ν)).
If ν is a probability measure then this becomes the more usual definition
(a - 1)⁻¹ * log (1 + (a - 1) * Hₐ(μ, ν)), but this definition maintains some useful properties
also for a general finite measure ν, in particular the integral form
Rₐ(μ, ν) = (a - 1)⁻¹ * log (∫ x, ((∂μ/∂ν) x) ^ a ∂ν).
We use ENNReal.log instead of Real.log, because it is monotone on ℝ≥0∞, while the real log is
monotone only on (0, ∞) (Real.log 0 = 0). This allows us to transfer inequalities from the
Hellinger divergence to the Rényi divergence.
Equations
- ProbabilityTheory.renyiDiv a μ ν = if a = 1 then ProbabilityTheory.kl μ ν else ↑(a - 1)⁻¹ * (↑(ν Set.univ) + (↑a - 1) * ProbabilityTheory.hellingerDiv a μ ν).toENNReal.log
Instances For
@[simp]
theorem
ProbabilityTheory.renyiDiv_zero
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.IsFiniteMeasure ν]
:
ProbabilityTheory.renyiDiv 0 μ ν = -(ν {x : α | 0 < μ.rnDeriv ν x}).log
@[simp]
theorem
ProbabilityTheory.renyiDiv_one
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
:
ProbabilityTheory.renyiDiv 1 μ ν = ProbabilityTheory.kl μ ν
theorem
ProbabilityTheory.renyiDiv_of_ne_one
{α : Type u_1}
{mα : MeasurableSpace α}
{a : ℝ}
(ha_ne_one : a ≠ 1)
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
:
ProbabilityTheory.renyiDiv a μ ν = ↑(a - 1)⁻¹ * (↑(ν Set.univ) + (↑a - 1) * ProbabilityTheory.hellingerDiv a μ ν).toENNReal.log
@[simp]
theorem
ProbabilityTheory.renyiDiv_zero_measure_left
{α : Type u_1}
{mα : MeasurableSpace α}
{a : ℝ}
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure ν]
:
ProbabilityTheory.renyiDiv a 0 ν = ↑(a - 1).sign * ⊥
@[simp]
theorem
ProbabilityTheory.renyiDiv_zero_measure_right
{α : Type u_1}
{mα : MeasurableSpace α}
{a : ℝ}
(μ : MeasureTheory.Measure α)
[NeZero μ]
:
ProbabilityTheory.renyiDiv a μ 0 = ⊤
theorem
ProbabilityTheory.renyiDiv_eq_top_of_hellingerDiv_eq_top'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
(ha_ne_one : a ≠ 1)
(h : ProbabilityTheory.hellingerDiv a μ ν = ⊤)
:
ProbabilityTheory.renyiDiv a μ ν = ⊤
theorem
ProbabilityTheory.renyiDiv_eq_top_of_hellingerDiv_eq_top
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
(h : ProbabilityTheory.hellingerDiv a μ ν = ⊤)
:
ProbabilityTheory.renyiDiv a μ ν = ⊤
theorem
ProbabilityTheory.renyiDiv_eq_top_iff_hellingerDiv_eq_top_of_one_lt
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
(ha : 1 < a)
[MeasureTheory.IsFiniteMeasure ν]
:
ProbabilityTheory.renyiDiv a μ ν = ⊤ ↔ ProbabilityTheory.hellingerDiv a μ ν = ⊤
theorem
ProbabilityTheory.renyiDiv_eq_top_iff_hellingerDiv_eq_top_of_one_le
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
(ha : 1 ≤ a)
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.IsFiniteMeasure ν]
:
ProbabilityTheory.renyiDiv a μ ν = ⊤ ↔ ProbabilityTheory.hellingerDiv a μ ν = ⊤
theorem
ProbabilityTheory.renyiDiv_eq_top_iff_of_one_lt
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
(ha : 1 < a)
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.IsFiniteMeasure ν]
:
ProbabilityTheory.renyiDiv a μ ν = ⊤ ↔ ¬MeasureTheory.Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal ^ a) ν ∨ ¬μ.AbsolutelyContinuous ν
theorem
ProbabilityTheory.renyiDiv_ne_top_iff_of_one_lt
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
(ha : 1 < a)
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.IsFiniteMeasure ν]
:
ProbabilityTheory.renyiDiv a μ ν ≠ ⊤ ↔ MeasureTheory.Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal ^ a) ν ∧ μ.AbsolutelyContinuous ν
theorem
ProbabilityTheory.renyiDiv_eq_top_iff_mutuallySingular_of_lt_one
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
(ha_nonneg : 0 ≤ a)
(ha : a < 1)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
:
ProbabilityTheory.renyiDiv a μ ν = ⊤ ↔ μ.MutuallySingular ν
theorem
ProbabilityTheory.renyiDiv_ne_bot_of_le_one
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
(ha : a ≤ 1)
[MeasureTheory.IsFiniteMeasure ν]
:
ProbabilityTheory.renyiDiv a μ ν ≠ ⊥
theorem
ProbabilityTheory.renyiDiv_eq_bot_iff_of_one_lt
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
(ha : 1 < a)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
:
ProbabilityTheory.renyiDiv a μ ν = ⊥ ↔ μ = 0
theorem
ProbabilityTheory.renyiDiv_ne_bot
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
[hμ : NeZero μ]
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
:
ProbabilityTheory.renyiDiv a μ ν ≠ ⊥
theorem
ProbabilityTheory.renyiDiv_of_mutuallySingular
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
(ha_nonneg : 0 ≤ a)
[NeZero μ]
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hμν : μ.MutuallySingular ν)
:
ProbabilityTheory.renyiDiv a μ ν = ⊤
theorem
ProbabilityTheory.renyiDiv_of_one_lt_of_not_integrable
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
(ha : 1 < a)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(h_int : ¬MeasureTheory.Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal ^ a) ν)
:
ProbabilityTheory.renyiDiv a μ ν = ⊤
theorem
ProbabilityTheory.renyiDiv_of_one_le_of_not_ac
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
(ha : 1 ≤ a)
(h_ac : ¬μ.AbsolutelyContinuous ν)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
:
ProbabilityTheory.renyiDiv a μ ν = ⊤
theorem
ProbabilityTheory.forall_renyiDiv_eq_top_of_eq_top_of_lt_one
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
(ha_nonneg : 0 ≤ a)
(ha : a < 1)
[NeZero μ]
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(h : ProbabilityTheory.renyiDiv a μ ν = ⊤)
(a' : ℝ)
:
0 ≤ a' → ProbabilityTheory.renyiDiv a' μ ν = ⊤
theorem
ProbabilityTheory.renyiDiv_eq_log_integral_of_lt_one
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
(ha_pos : 0 < a)
(ha : a < 1)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
:
ProbabilityTheory.renyiDiv a μ ν = ↑(a - 1)⁻¹ * (ENNReal.ofReal (∫ (x : α), (μ.rnDeriv ν x).toReal ^ a ∂ν)).log
The Rényi divergence renyiDiv a μ ν can be written as the log of an integral
with respect to ν.
theorem
ProbabilityTheory.renyiDiv_eq_log_integral
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
(ha_pos : 0 < a)
(ha_ne_one : a ≠ 1)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(h_int : MeasureTheory.Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal ^ a) ν)
(h_ac : μ.AbsolutelyContinuous ν)
:
ProbabilityTheory.renyiDiv a μ ν = ↑(a - 1)⁻¹ * (ENNReal.ofReal (∫ (x : α), (μ.rnDeriv ν x).toReal ^ a ∂ν)).log
The Rényi divergence renyiDiv a μ ν can be written as the log of an integral
with respect to ν.
If a < 1, use renyiDiv_eq_log_integral_of_lt_one instead.
theorem
ProbabilityTheory.renyiDiv_eq_log_integral_of_lt_one'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
(ha_pos : 0 < a)
(ha : a < 1)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(h_ac : μ.AbsolutelyContinuous ν)
:
ProbabilityTheory.renyiDiv a μ ν = ↑(a - 1)⁻¹ * (ENNReal.ofReal (∫ (x : α), (μ.rnDeriv ν x).toReal ^ (a - 1) ∂μ)).log
If μ ≪ ν, the Rényi divergence renyiDiv a μ ν can be written as the log of an integral
with respect to μ.
theorem
ProbabilityTheory.renyiDiv_eq_log_integral'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
(ha_pos : 0 < a)
(ha : a ≠ 1)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(h_int : MeasureTheory.Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal ^ a) ν)
(h_ac : μ.AbsolutelyContinuous ν)
:
ProbabilityTheory.renyiDiv a μ ν = ↑(a - 1)⁻¹ * (ENNReal.ofReal (∫ (x : α), (μ.rnDeriv ν x).toReal ^ (a - 1) ∂μ)).log
If μ ≪ ν, the Rényi divergence renyiDiv a μ ν can be written as the log of an integral
with respect to μ.
If a < 1, use renyiDiv_eq_log_integral_of_lt_one' instead.
theorem
ProbabilityTheory.renyiDiv_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.renyiDiv a μ ν = ↑a * ProbabilityTheory.renyiDiv (1 - a) ν μ
theorem
ProbabilityTheory.renyiDiv_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.renyiDiv a μ ν = ↑a * ProbabilityTheory.renyiDiv (1 - a) ν μ
theorem
ProbabilityTheory.coe_cgf_llr_of_lt_one
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
(ha_pos : 0 < a)
(ha : a < 1)
[hν : NeZero ν]
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hνμ : ν.AbsolutelyContinuous μ)
:
↑(ProbabilityTheory.cgf (MeasureTheory.llr μ ν) ν a) = (↑a - 1) * ProbabilityTheory.renyiDiv a μ ν
theorem
ProbabilityTheory.cgf_llr_of_lt_one
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
(ha_pos : 0 < a)
(ha : a < 1)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hνμ : ν.AbsolutelyContinuous μ)
:
ProbabilityTheory.cgf (MeasureTheory.llr μ ν) ν a = (a - 1) * (ProbabilityTheory.renyiDiv a μ ν).toReal
theorem
ProbabilityTheory.coe_cgf_llr'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
(ha_pos : 0 < a)
[hν : NeZero μ]
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(h_int : MeasureTheory.Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal ^ (1 + a)) ν)
(hμν : μ.AbsolutelyContinuous ν)
:
↑(ProbabilityTheory.cgf (MeasureTheory.llr μ ν) μ a) = ↑a * ProbabilityTheory.renyiDiv (1 + a) μ ν
theorem
ProbabilityTheory.cgf_llr'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{a : ℝ}
(ha_pos : 0 < a)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(h_int : MeasureTheory.Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal ^ (1 + a)) ν)
(hμν : μ.AbsolutelyContinuous ν)
:
ProbabilityTheory.cgf (MeasureTheory.llr μ ν) μ a = a * (ProbabilityTheory.renyiDiv (1 + a) μ ν).toReal
noncomputable def
ProbabilityTheory.renyiDensity
{α : Type u_1}
{mα : MeasurableSpace α}
(a : ℝ)
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
(x : α)
:
Density of the Rényi measure renyiMeasure a μ ν with respect to μ + ν.
Equations
- ProbabilityTheory.renyiDensity a μ ν x = μ.rnDeriv (μ + ν) x ^ a * ν.rnDeriv (μ + ν) x ^ (1 - a) * ENNReal.ofReal (Real.exp (-(a - 1) * (ProbabilityTheory.renyiDiv a μ ν).toReal))
Instances For
noncomputable def
ProbabilityTheory.renyiMeasure
{α : Type u_1}
{mα : MeasurableSpace α}
(a : ℝ)
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
:
Tilted measure of μ with respect to ν parametrized by a.
Equations
- ProbabilityTheory.renyiMeasure a μ ν = (μ + ν).withDensity (ProbabilityTheory.renyiDensity a μ ν)
Instances For
theorem
ProbabilityTheory.le_renyiDiv_of_le_hellingerDiv
{α : Type u_1}
{mα : MeasurableSpace α}
{β : Type u_3}
{mβ : MeasurableSpace β}
{a : ℝ}
{μ₁ : MeasureTheory.Measure α}
{ν₁ : MeasureTheory.Measure α}
{μ₂ : MeasureTheory.Measure β}
{ν₂ : MeasureTheory.Measure β}
[MeasureTheory.SigmaFinite μ₁]
[MeasureTheory.SigmaFinite ν₁]
[MeasureTheory.SigmaFinite μ₂]
[MeasureTheory.SigmaFinite ν₂]
(h_eq : ν₁ Set.univ = ν₂ Set.univ)
(h_le : ProbabilityTheory.hellingerDiv a μ₁ ν₁ ≤ ProbabilityTheory.hellingerDiv a μ₂ ν₂)
:
ProbabilityTheory.renyiDiv a μ₁ ν₁ ≤ ProbabilityTheory.renyiDiv a μ₂ ν₂
theorem
ProbabilityTheory.le_renyiDiv_compProd
{α : Type u_1}
{mα : MeasurableSpace α}
{a : ℝ}
{β : Type u_3}
{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.renyiDiv a μ ν ≤ ProbabilityTheory.renyiDiv a (μ.compProd κ) (ν.compProd η)
theorem
ProbabilityTheory.renyiDiv_fst_le
{α : Type u_1}
{mα : MeasurableSpace α}
{a : ℝ}
{β : Type u_3}
{mβ : MeasurableSpace β}
[Nonempty β]
[StandardBorelSpace β]
(ha_pos : 0 < a)
(μ : MeasureTheory.Measure (α × β))
(ν : MeasureTheory.Measure (α × β))
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
:
ProbabilityTheory.renyiDiv a μ.fst ν.fst ≤ ProbabilityTheory.renyiDiv a μ ν
theorem
ProbabilityTheory.renyiDiv_snd_le
{α : Type u_1}
{mα : MeasurableSpace α}
{a : ℝ}
{β : Type u_3}
{mβ : MeasurableSpace β}
[Nonempty α]
[StandardBorelSpace α]
(ha_pos : 0 < a)
(μ : MeasureTheory.Measure (α × β))
(ν : MeasureTheory.Measure (α × β))
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
:
ProbabilityTheory.renyiDiv a μ.snd ν.snd ≤ ProbabilityTheory.renyiDiv a μ ν
theorem
ProbabilityTheory.renyiDiv_comp_le_compProd
{α : Type u_1}
{mα : MeasurableSpace α}
{a : ℝ}
{β : Type u_3}
{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.renyiDiv a (μ.bind ⇑κ) (ν.bind ⇑η) ≤ ProbabilityTheory.renyiDiv a (μ.compProd κ) (ν.compProd η)
theorem
ProbabilityTheory.renyiDiv_comp_right_le
{α : Type u_1}
{mα : MeasurableSpace α}
{a : ℝ}
{β : Type u_3}
{mβ : MeasurableSpace β}
[Nonempty α]
[StandardBorelSpace α]
(ha_pos : 0 < a)
[MeasurableSpace.CountableOrCountablyGenerated α β]
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsMarkovKernel κ]
:
ProbabilityTheory.renyiDiv a (μ.bind ⇑κ) (ν.bind ⇑κ) ≤ ProbabilityTheory.renyiDiv a μ ν
The Data Processing Inequality for the Renyi divergence.