theorem
ProbabilityTheory.kl_ae_ne_top_iff
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
:
(∀ᵐ (a : α) ∂μ, ProbabilityTheory.kl (κ a) (η a) ≠ ⊤) ↔ (∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a)) ∧ ∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (MeasureTheory.llr (κ a) (η a)) (κ a)
Equivalence between two possible versions of the first condition for the finiteness of the conditional KL divergence, the second version is the preferred one.
theorem
ProbabilityTheory.integrable_kl_iff
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
(h_ac : ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
:
MeasureTheory.Integrable (fun (a : α) => (ProbabilityTheory.kl (κ a) (η a)).toReal) μ ↔ MeasureTheory.Integrable (fun (a : α) => ∫ (x : β), MeasureTheory.llr (κ a) (η a) x ∂κ a) μ
Equivalence between two possible versions of the second condition for the finiteness of the conditional KL divergence, the first version is the preferred one.
noncomputable def
ProbabilityTheory.condKL
{α : Type u_1}
{mα : MeasurableSpace α}
{β : Type u_2}
{mβ : MeasurableSpace β}
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
(μ : MeasureTheory.Measure α)
:
Kullback-Leibler divergence between two kernels κ and η conditional to a measure μ. It is defined as KL(κ, η | μ) := ∫ x, KL(κ x, η x) dμ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ProbabilityTheory.condKL_of_ae_ne_top_of_integrable
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
(h1 : ∀ᵐ (a : α) ∂μ, ProbabilityTheory.kl (κ a) (η a) ≠ ⊤)
(h2 : MeasureTheory.Integrable (fun (a : α) => (ProbabilityTheory.kl (κ a) (η a)).toReal) μ)
:
ProbabilityTheory.condKL κ η μ = ↑(∫ (x : α), (fun (a : α) => (ProbabilityTheory.kl (κ a) (η a)).toReal) x ∂μ)
theorem
ProbabilityTheory.condKL_of_ae_ac_of_ae_integrable_of_integrable
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
(h_ac : ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
(h_ae_int : ∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (MeasureTheory.llr (κ a) (η a)) (κ a))
(h_int : MeasureTheory.Integrable (fun (a : α) => (ProbabilityTheory.kl (κ a) (η a)).toReal) μ)
:
ProbabilityTheory.condKL κ η μ = ↑(∫ (x : α), (fun (a : α) => (ProbabilityTheory.kl (κ a) (η a)).toReal) x ∂μ)
theorem
ProbabilityTheory.condKL_of_ae_ac_of_ae_integrable_of_integrable'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
(h_ac : ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
(h_ae_int : ∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (MeasureTheory.llr (κ a) (η a)) (κ a))
(h_int : MeasureTheory.Integrable (fun (a : α) => (ProbabilityTheory.kl (κ a) (η a)).toReal) μ)
:
ProbabilityTheory.condKL κ η μ = ↑(∫ (x : α), (fun (a : α) => ∫ (x : β), MeasureTheory.llr (κ a) (η a) x ∂κ a) x ∂μ)
@[simp]
theorem
ProbabilityTheory.condKL_of_not_ae_ne_top
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
(h : ¬∀ᵐ (a : α) ∂μ, ProbabilityTheory.kl (κ a) (η a) ≠ ⊤)
:
ProbabilityTheory.condKL κ η μ = ⊤
@[simp]
theorem
ProbabilityTheory.condKL_of_not_ae_ac
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
(h : ¬∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
:
ProbabilityTheory.condKL κ η μ = ⊤
@[simp]
theorem
ProbabilityTheory.condKL_of_not_ae_integrable
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
(h : ¬∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (MeasureTheory.llr (κ a) (η a)) (κ a))
:
ProbabilityTheory.condKL κ η μ = ⊤
@[simp]
theorem
ProbabilityTheory.condKL_of_not_integrable
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
(h : ¬MeasureTheory.Integrable (fun (a : α) => (ProbabilityTheory.kl (κ a) (η a)).toReal) μ)
:
ProbabilityTheory.condKL κ η μ = ⊤
@[simp]
theorem
ProbabilityTheory.condKL_of_not_integrable'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
(h : ¬MeasureTheory.Integrable (fun (a : α) => ∫ (x : β), MeasureTheory.llr (κ a) (η a) x ∂κ a) μ)
:
ProbabilityTheory.condKL κ η μ = ⊤
theorem
ProbabilityTheory.condKL_toReal_of_ae_ac_of_ae_integrable
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
(h_ac : ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
(h_ae_int : ∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (MeasureTheory.llr (κ a) (η a)) (κ a))
:
(ProbabilityTheory.condKL κ η μ).toReal = ∫ (x : α), (fun (a : α) => (ProbabilityTheory.kl (κ a) (η a)).toReal) x ∂μ
theorem
ProbabilityTheory.condKL_eq_top_iff
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
:
ProbabilityTheory.condKL κ η μ = ⊤ ↔ (¬∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a)) ∨ (¬∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (MeasureTheory.llr (κ a) (η a)) (κ a)) ∨ ¬MeasureTheory.Integrable (fun (a : α) => (ProbabilityTheory.kl (κ a) (η a)).toReal) μ
theorem
ProbabilityTheory.condKL_ne_top_iff
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
:
ProbabilityTheory.condKL κ η μ ≠ ⊤ ↔ (∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a)) ∧ (∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (MeasureTheory.llr (κ a) (η a)) (κ a)) ∧ MeasureTheory.Integrable (fun (a : α) => (ProbabilityTheory.kl (κ a) (η a)).toReal) μ
theorem
ProbabilityTheory.condKL_ne_top_iff'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
:
ProbabilityTheory.condKL κ η μ ≠ ⊤ ↔ ProbabilityTheory.condKL κ η μ = ↑(∫ (x : α), (fun (a : α) => (ProbabilityTheory.kl (κ a) (η a)).toReal) x ∂μ)
theorem
ProbabilityTheory.condKL_eq_condFDiv
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
:
ProbabilityTheory.condKL κ η μ = ProbabilityTheory.condFDiv (fun (x : ℝ) => x * Real.log x) κ η μ
@[simp]
theorem
ProbabilityTheory.condKL_self
{α : Type u_1}
{mα : MeasurableSpace α}
{β : Type u_2}
{mβ : MeasurableSpace β}
(κ : ProbabilityTheory.Kernel α β)
(μ : MeasureTheory.Measure α)
[ProbabilityTheory.IsFiniteKernel κ]
:
ProbabilityTheory.condKL κ κ μ = 0
@[simp]
theorem
ProbabilityTheory.condKL_zero_left
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{η : ProbabilityTheory.Kernel α β}
:
ProbabilityTheory.condKL 0 η μ = 0
@[simp]
theorem
ProbabilityTheory.condKL_zero_right
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
(h : ∃ᵐ (a : α) ∂μ, κ a ≠ 0)
:
ProbabilityTheory.condKL κ 0 μ = ⊤
@[simp]
theorem
ProbabilityTheory.condKL_zero_measure
{α : Type u_1}
{mα : MeasurableSpace α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
:
ProbabilityTheory.condKL κ η 0 = 0
@[simp]
theorem
ProbabilityTheory.condKL_isEmpty_left
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
[IsEmpty α]
:
ProbabilityTheory.condKL κ η μ = 0
theorem
ProbabilityTheory.condKL_ne_bot
{α : Type u_1}
{mα : MeasurableSpace α}
{β : Type u_2}
{mβ : MeasurableSpace β}
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
(μ : MeasureTheory.Measure α)
:
ProbabilityTheory.condKL κ η μ ≠ ⊥
theorem
ProbabilityTheory.condKL_nonneg
{α : Type u_1}
{mα : MeasurableSpace α}
{β : Type u_2}
{mβ : MeasurableSpace β}
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsMarkovKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
(μ : MeasureTheory.Measure α)
:
0 ≤ ProbabilityTheory.condKL κ η μ
@[simp]
theorem
ProbabilityTheory.condKL_const
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{ξ : MeasureTheory.Measure β}
[MeasureTheory.IsFiniteMeasure ξ]
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
:
ProbabilityTheory.condKL (ProbabilityTheory.Kernel.const β μ) (ProbabilityTheory.Kernel.const β ν) ξ = ProbabilityTheory.kl μ ν * ↑(ξ Set.univ)
theorem
ProbabilityTheory.kl_fst_le
{α : Type u_1}
{mα : MeasurableSpace α}
{β : Type u_2}
{mβ : MeasurableSpace β}
[Nonempty β]
[StandardBorelSpace β]
(μ : MeasureTheory.Measure (α × β))
(ν : MeasureTheory.Measure (α × β))
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
:
ProbabilityTheory.kl μ.fst ν.fst ≤ ProbabilityTheory.kl μ ν
theorem
ProbabilityTheory.kl_snd_le
{α : Type u_1}
{mα : MeasurableSpace α}
{β : Type u_2}
{mβ : MeasurableSpace β}
[Nonempty α]
[StandardBorelSpace α]
(μ : MeasureTheory.Measure (α × β))
(ν : MeasureTheory.Measure (α × β))
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
:
ProbabilityTheory.kl μ.snd ν.snd ≤ ProbabilityTheory.kl μ ν
theorem
ProbabilityTheory.le_kl_compProd
{α : Type u_1}
{mα : MeasurableSpace α}
{β : Type u_2}
{mβ : MeasurableSpace β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsMarkovKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
:
ProbabilityTheory.kl μ ν ≤ ProbabilityTheory.kl (μ.compProd κ) (ν.compProd η)
theorem
ProbabilityTheory.condKL_compProd_meas_eq_top
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{γ : Type u_3}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[MeasurableSpace.CountableOrCountablyGenerated (α × β) γ]
[MeasureTheory.SFinite μ]
{ξ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel ξ]
{κ : ProbabilityTheory.Kernel (α × β) γ}
{η : ProbabilityTheory.Kernel (α × β) γ}
[ProbabilityTheory.IsMarkovKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
:
ProbabilityTheory.condKL κ η (μ.compProd ξ) = ⊤ ↔ (¬∀ᵐ (a : α) ∂μ, ProbabilityTheory.condKL (κ.snd' a) (η.snd' a) (ξ a) ≠ ⊤) ∨ ¬MeasureTheory.Integrable (fun (x : α) => (ProbabilityTheory.condKL (κ.snd' x) (η.snd' x) (ξ x)).toReal) μ
This is to handle the case in condKL_compProd_meas when the lhs is ⊤, in this case the rhs is
'morally' also ⊤, so the equality holds, but actually in Lean the equality is not true, because of
how we handle the infinities in the integrals, so we have to make a separate lemma for this case.
theorem
ProbabilityTheory.condKL_compProd_meas
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{γ : Type u_3}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[MeasurableSpace.CountableOrCountablyGenerated (α × β) γ]
[MeasureTheory.SFinite μ]
{ξ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel ξ]
{κ : ProbabilityTheory.Kernel (α × β) γ}
{η : ProbabilityTheory.Kernel (α × β) γ}
[ProbabilityTheory.IsMarkovKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
(h : ProbabilityTheory.condKL κ η (μ.compProd ξ) ≠ ⊤)
:
ProbabilityTheory.condKL κ η (μ.compProd ξ) = ↑(∫ (x : α), (ProbabilityTheory.condKL (κ.snd' x) (η.snd' x) (ξ x)).toReal ∂μ)
theorem
ProbabilityTheory.kl_compProd_left
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
[∀ (x : α), NeZero (κ x)]
[ProbabilityTheory.IsFiniteKernel η]
:
ProbabilityTheory.kl (μ.compProd κ) (μ.compProd η) = ProbabilityTheory.condKL κ η μ
theorem
ProbabilityTheory.kl_compProd_right
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
(κ : ProbabilityTheory.Kernel α β)
[MeasurableSpace.CountableOrCountablyGenerated α β]
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
[ProbabilityTheory.IsMarkovKernel κ]
:
ProbabilityTheory.kl (μ.compProd κ) (ν.compProd κ) = ProbabilityTheory.kl μ ν
theorem
ProbabilityTheory.kl_compProd
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[ProbabilityTheory.IsMarkovKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
:
ProbabilityTheory.kl (μ.compProd κ) (ν.compProd η) = ProbabilityTheory.kl μ ν + ProbabilityTheory.condKL κ η μ
The chain rule for the KL divergence.
theorem
ProbabilityTheory.kl_fst_add_condKL
{α : Type u_1}
{mα : MeasurableSpace α}
{β : Type u_2}
{mβ : MeasurableSpace β}
[StandardBorelSpace β]
[Nonempty β]
{μ : MeasureTheory.Measure (α × β)}
{ν : MeasureTheory.Measure (α × β)}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
:
ProbabilityTheory.kl μ.fst ν.fst + ProbabilityTheory.condKL μ.condKernel ν.condKernel μ.fst = ProbabilityTheory.kl μ ν
The chain rule for the KL divergence.
theorem
ProbabilityTheory.Kernel.integrable_llr_compProd_iff'
{α : Type u_1}
{mα : MeasurableSpace α}
{β : Type u_2}
{γ : Type u_3}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[MeasurableSpace.CountableOrCountablyGenerated β γ]
{κ₁ : ProbabilityTheory.Kernel α β}
{η₁ : ProbabilityTheory.Kernel α β}
{κ₂ : ProbabilityTheory.Kernel (α × β) γ}
{η₂ : ProbabilityTheory.Kernel (α × β) γ}
[ProbabilityTheory.IsFiniteKernel κ₁]
[ProbabilityTheory.IsFiniteKernel η₁]
[ProbabilityTheory.IsMarkovKernel κ₂]
[ProbabilityTheory.IsMarkovKernel η₂]
(a : α)
(h_ac : ((κ₁.compProd κ₂) a).AbsolutelyContinuous ((η₁.compProd η₂) a))
:
MeasureTheory.Integrable (MeasureTheory.llr ((κ₁.compProd κ₂) a) ((η₁.compProd η₂) a)) ((κ₁.compProd κ₂) a) ↔ MeasureTheory.Integrable (MeasureTheory.llr (κ₁ a) (η₁ a)) (κ₁ a) ∧ MeasureTheory.Integrable (fun (b : β) => (ProbabilityTheory.kl (κ₂ (a, b)) (η₂ (a, b))).toReal) (κ₁ a) ∧ ∀ᵐ (b : β) ∂κ₁ a, MeasureTheory.Integrable (MeasureTheory.llr (κ₂ (a, b)) (η₂ (a, b))) (κ₂ (a, b))
theorem
ProbabilityTheory.kl_compProd_kernel_of_ae_ac_of_ae_integrable
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{γ : Type u_3}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[MeasurableSpace.CountableOrCountablyGenerated β γ]
{κ₁ : ProbabilityTheory.Kernel α β}
{η₁ : ProbabilityTheory.Kernel α β}
{κ₂ : ProbabilityTheory.Kernel (α × β) γ}
{η₂ : ProbabilityTheory.Kernel (α × β) γ}
[ProbabilityTheory.IsFiniteKernel κ₁]
[ProbabilityTheory.IsFiniteKernel η₁]
[ProbabilityTheory.IsMarkovKernel κ₂]
[ProbabilityTheory.IsMarkovKernel η₂]
(h_ac : ∀ᵐ (a : α) ∂μ, ((κ₁.compProd κ₂) a).AbsolutelyContinuous ((η₁.compProd η₂) a))
(h_ae_int : ∀ᵐ (a : α) ∂μ,
MeasureTheory.Integrable (MeasureTheory.llr ((κ₁.compProd κ₂) a) ((η₁.compProd η₂) a)) ((κ₁.compProd κ₂) a))
:
∀ᵐ (a : α) ∂μ,
(ProbabilityTheory.kl ((κ₁.compProd κ₂) a) ((η₁.compProd η₂) a)).toReal = (ProbabilityTheory.kl (κ₁ a) (η₁ a)).toReal + ∫ (b : β), (ProbabilityTheory.kl (κ₂ (a, b)) (η₂ (a, b))).toReal ∂κ₁ a
theorem
ProbabilityTheory.condKL_compProd_kernel_eq_top
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{γ : Type u_3}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[MeasurableSpace.CountableOrCountablyGenerated (α × β) γ]
{κ₁ : ProbabilityTheory.Kernel α β}
{η₁ : ProbabilityTheory.Kernel α β}
{κ₂ : ProbabilityTheory.Kernel (α × β) γ}
{η₂ : ProbabilityTheory.Kernel (α × β) γ}
[ProbabilityTheory.IsMarkovKernel κ₁]
[ProbabilityTheory.IsMarkovKernel η₁]
[ProbabilityTheory.IsMarkovKernel κ₂]
[ProbabilityTheory.IsMarkovKernel η₂]
[MeasureTheory.SFinite μ]
:
ProbabilityTheory.condKL (κ₁.compProd κ₂) (η₁.compProd η₂) μ = ⊤ ↔ ProbabilityTheory.condKL κ₁ η₁ μ = ⊤ ∨ ProbabilityTheory.condKL κ₂ η₂ (μ.compProd κ₁) = ⊤
theorem
ProbabilityTheory.condKL_compProd_kernel
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{γ : Type u_3}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[MeasurableSpace.CountableOrCountablyGenerated (α × β) γ]
{κ₁ : ProbabilityTheory.Kernel α β}
{η₁ : ProbabilityTheory.Kernel α β}
{κ₂ : ProbabilityTheory.Kernel (α × β) γ}
{η₂ : ProbabilityTheory.Kernel (α × β) γ}
[ProbabilityTheory.IsMarkovKernel κ₁]
[ProbabilityTheory.IsMarkovKernel η₁]
[ProbabilityTheory.IsMarkovKernel κ₂]
[ProbabilityTheory.IsMarkovKernel η₂]
[MeasureTheory.SFinite μ]
:
ProbabilityTheory.condKL (κ₁.compProd κ₂) (η₁.compProd η₂) μ = ProbabilityTheory.condKL κ₁ η₁ μ + ProbabilityTheory.condKL κ₂ η₂ (μ.compProd κ₁)
theorem
ProbabilityTheory.kl_prod_two'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
{ξ : MeasureTheory.Measure β}
{ψ : MeasureTheory.Measure β}
[MeasureTheory.IsProbabilityMeasure ξ]
[MeasureTheory.IsProbabilityMeasure ψ]
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
:
ProbabilityTheory.kl (μ.prod ξ) (ν.prod ψ) = ProbabilityTheory.kl μ ν + ProbabilityTheory.kl ξ ψ * ↑(μ Set.univ)
theorem
ProbabilityTheory.kl_prod_two
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
{ξ : MeasureTheory.Measure β}
{ψ : MeasureTheory.Measure β}
[MeasureTheory.IsProbabilityMeasure ξ]
[MeasureTheory.IsProbabilityMeasure ψ]
[MeasureTheory.IsProbabilityMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
:
ProbabilityTheory.kl (μ.prod ξ) (ν.prod ψ) = ProbabilityTheory.kl μ ν + ProbabilityTheory.kl ξ ψ
Tensorization property for KL divergence
theorem
ProbabilityTheory.MeasurableEquiv.piCongrLeft_apply_apply
{ι : Type u_3}
{ι' : Type u_4}
(e : ι ≃ ι')
{β : ι' → Type u_5}
[(i' : ι') → MeasurableSpace (β i')]
(x : (i : ι) → β (e i))
(i : ι)
:
(MeasurableEquiv.piCongrLeft (fun (i' : ι') => β i') e) x (e i) = x i
theorem
ProbabilityTheory.Measure.pi_map_piCongrLeft
{ι : Type u_3}
{ι' : Type u_4}
[hι : Fintype ι]
[hι' : Fintype ι']
(e : ι ≃ ι')
{β : ι' → Type u_5}
[(i : ι') → MeasurableSpace (β i)]
(μ : (i : ι') → MeasureTheory.Measure (β i))
[∀ (i : ι'), MeasureTheory.SigmaFinite (μ i)]
:
MeasureTheory.Measure.map (⇑(MeasurableEquiv.piCongrLeft (fun (i : ι') => β i) e))
(MeasureTheory.Measure.pi fun (i : ι) => μ (e i)) = MeasureTheory.Measure.pi μ
theorem
ProbabilityTheory.kl_pi
{ι : Type u_3}
[hι : Fintype ι]
{β : ι → Type u_4}
[(i : ι) → MeasurableSpace (β i)]
[∀ (i : ι), MeasurableSpace.CountablyGenerated (β i)]
{μ : (i : ι) → MeasureTheory.Measure (β i)}
{ν : (i : ι) → MeasureTheory.Measure (β i)}
[∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)]
[∀ (i : ι), MeasureTheory.IsProbabilityMeasure (ν i)]
:
ProbabilityTheory.kl (MeasureTheory.Measure.pi μ) (MeasureTheory.Measure.pi ν) = ∑ i : ι, ProbabilityTheory.kl (μ i) (ν i)
theorem
ProbabilityTheory.kl_pi_const
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{ι : Type u_3}
[hι : Fintype ι]
[MeasurableSpace.CountablyGenerated α]
[MeasureTheory.IsProbabilityMeasure μ]
[MeasureTheory.IsProbabilityMeasure ν]
:
ProbabilityTheory.kl (MeasureTheory.Measure.pi fun (x : ι) => μ) (MeasureTheory.Measure.pi fun (x : ι) => ν) = ↑(Fintype.card ι) * ProbabilityTheory.kl μ ν
theorem
ProbabilityTheory.kl_comp_left_le
{α : Type u_1}
{mα : MeasurableSpace α}
{β : Type u_2}
{mβ : MeasurableSpace β}
[Nonempty α]
[StandardBorelSpace α]
[MeasurableSpace.CountableOrCountablyGenerated α β]
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
[∀ (a : α), NeZero (κ a)]
[ProbabilityTheory.IsFiniteKernel η]
:
ProbabilityTheory.kl (μ.bind ⇑κ) (μ.bind ⇑η) ≤ ProbabilityTheory.condKL κ η μ