theorem
ProbabilityTheory.llr_self
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
[MeasureTheory.SigmaFinite μ]
:
MeasureTheory.llr μ μ =ᵐ[μ] 0
noncomputable def
ProbabilityTheory.kl
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
:
Kullback-Leibler divergence between two measures.
Equations
- ProbabilityTheory.kl μ ν = if μ.AbsolutelyContinuous ν ∧ MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ then ↑(∫ (x : α), MeasureTheory.llr μ ν x ∂μ) else ⊤
Instances For
theorem
ProbabilityTheory.kl_of_ac_of_integrable
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(h1 : μ.AbsolutelyContinuous ν)
(h2 : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ)
:
ProbabilityTheory.kl μ ν = ↑(∫ (x : α), MeasureTheory.llr μ ν x ∂μ)
@[simp]
theorem
ProbabilityTheory.kl_of_not_ac
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(h : ¬μ.AbsolutelyContinuous ν)
:
ProbabilityTheory.kl μ ν = ⊤
@[simp]
theorem
ProbabilityTheory.kl_of_not_integrable
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(h : ¬MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ)
:
ProbabilityTheory.kl μ ν = ⊤
theorem
ProbabilityTheory.kl_toReal_of_ac
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(h : μ.AbsolutelyContinuous ν)
:
(ProbabilityTheory.kl μ ν).toReal = ∫ (a : α), MeasureTheory.llr μ ν a ∂μ
If μ ≪ ν, then toReal of the Kullback-Leibler divergence is equal to an integral,
without any integrability condition. Not true in general without μ ≪ ν, as the integral might be
finite but non-zero.
@[simp]
theorem
ProbabilityTheory.kl_self
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
[MeasureTheory.SigmaFinite μ]
:
ProbabilityTheory.kl μ μ = 0
@[simp]
theorem
ProbabilityTheory.kl_zero_left
{α : Type u_1}
{mα : MeasurableSpace α}
{ν : MeasureTheory.Measure α}
:
ProbabilityTheory.kl 0 ν = 0
@[simp]
theorem
ProbabilityTheory.kl_zero_right
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NeZero μ]
:
ProbabilityTheory.kl μ 0 = ⊤
theorem
ProbabilityTheory.kl_eq_top_iff
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
:
ProbabilityTheory.kl μ ν = ⊤ ↔ μ.AbsolutelyContinuous ν → ¬MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ
theorem
ProbabilityTheory.kl_ne_top_iff
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
:
ProbabilityTheory.kl μ ν ≠ ⊤ ↔ μ.AbsolutelyContinuous ν ∧ MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ
theorem
ProbabilityTheory.kl_ne_top_iff'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
:
ProbabilityTheory.kl μ ν ≠ ⊤ ↔ ProbabilityTheory.kl μ ν = ↑(∫ (x : α), MeasureTheory.llr μ ν x ∂μ)
@[simp]
theorem
ProbabilityTheory.kl_ne_bot
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
:
ProbabilityTheory.kl μ ν ≠ ⊥
theorem
ProbabilityTheory.fDiv_mul_log_eq_top_iff
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.SigmaFinite ν]
:
ProbabilityTheory.fDiv (fun (x : ℝ) => x * Real.log x) μ ν = ⊤ ↔ μ.AbsolutelyContinuous ν → ¬MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ
theorem
ProbabilityTheory.kl_eq_fDiv
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
:
ProbabilityTheory.kl μ ν = ProbabilityTheory.fDiv (fun (x : ℝ) => x * Real.log x) μ ν
theorem
ProbabilityTheory.measurable_kl
{α : Type u_1}
{mα : MeasurableSpace α}
{β : Type u_2}
[MeasurableSpace β]
[MeasurableSpace.CountableOrCountablyGenerated α β]
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
:
Measurable fun (a : α) => ProbabilityTheory.kl (κ a) (η a)
theorem
ProbabilityTheory.kl_ge_mul_log'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsProbabilityMeasure ν]
(hμν : μ.AbsolutelyContinuous ν)
:
↑(μ Set.univ).toReal * ↑(Real.log (μ Set.univ).toReal) ≤ ProbabilityTheory.kl μ ν
theorem
ProbabilityTheory.kl_ge_mul_log
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
:
↑(μ Set.univ).toReal * ↑(Real.log ((μ Set.univ).toReal / (ν Set.univ).toReal)) ≤ ProbabilityTheory.kl μ ν
theorem
ProbabilityTheory.kl_nonneg'
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(h : μ Set.univ ≥ ν Set.univ)
:
0 ≤ ProbabilityTheory.kl μ ν
theorem
ProbabilityTheory.kl_nonneg
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsProbabilityMeasure μ]
[MeasureTheory.IsProbabilityMeasure ν]
:
0 ≤ ProbabilityTheory.kl μ ν
Gibbs' inequality: the Kullback-Leibler divergence between two probability distributions is nonnegative.
theorem
ProbabilityTheory.kl_eq_zero_iff
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(h_mass : μ Set.univ = ν Set.univ)
:
ProbabilityTheory.kl μ ν = 0 ↔ μ = ν
Converse Gibbs' inequality: the Kullback-Leibler divergence between two finite measures is zero if and only if the two distributions are equal.
theorem
ProbabilityTheory.kl_eq_zero_iff'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.IsProbabilityMeasure μ]
[MeasureTheory.IsProbabilityMeasure ν]
:
ProbabilityTheory.kl μ ν = 0 ↔ μ = ν
Converse Gibbs' inequality: the Kullback-Leibler divergence between two probability distributions is zero if and only if the two distributions are equal.
theorem
ProbabilityTheory.kl_comp_le_compProd
{α : Type u_1}
{mα : MeasurableSpace α}
{β : Type u_2}
{mβ : MeasurableSpace β}
[Nonempty α]
[StandardBorelSpace α]
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
:
ProbabilityTheory.kl (μ.bind ⇑κ) (ν.bind ⇑η) ≤ ProbabilityTheory.kl (μ.compProd κ) (ν.compProd η)
theorem
ProbabilityTheory.kl_comp_right_le
{α : Type u_1}
{mα : MeasurableSpace α}
{β : Type u_2}
{mβ : MeasurableSpace β}
[Nonempty α]
[StandardBorelSpace α]
[MeasurableSpace.CountableOrCountablyGenerated α β]
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsMarkovKernel κ]
:
ProbabilityTheory.kl (μ.bind ⇑κ) (ν.bind ⇑κ) ≤ ProbabilityTheory.kl μ ν
The Data Processing Inequality for the Kullback-Leibler divergence.