Mutual Information of kernels #
Main definitions #
mutualInfo
: Mutual information of a kernelκ
into a product space with respect to a measureμ
. This is denoted byIk[κ, μ]
and is equal toHk[fst κ, μ] + Hk[snd κ, μ] - Hk[κ, μ]
.
Main statements #
mutualInfo_nonneg
:Ik[κ, μ]
is nonnegativeentropy_condKernel_le_entropy_fst
andentropy_condKernel_le_entropy_snd
: conditioning reduces entropy.
Notations #
Ik[κ, μ] = Kernel.entropy κ μ
noncomputable def
ProbabilityTheory.Kernel.mutualInfo
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
(κ : ProbabilityTheory.Kernel T (S × U))
(μ : MeasureTheory.Measure T)
:
Mutual information of a kernel into a product space with respect to a measure.
Instances For
Mutual information of a kernel into a product space with respect to a measure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pretty printer defined by notation3
command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ProbabilityTheory.Kernel.mutualInfo_def
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
(κ : ProbabilityTheory.Kernel T (S × U))
(μ : MeasureTheory.Measure T)
:
@[simp]
theorem
ProbabilityTheory.Kernel.mutualInfo_zero_measure
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
(κ : ProbabilityTheory.Kernel T (S × U))
:
Ik[κ , 0] = 0
@[simp]
theorem
ProbabilityTheory.Kernel.mutualInfo_zero_kernel
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
(μ : MeasureTheory.Measure T)
:
Ik[0 , μ] = 0
theorem
ProbabilityTheory.Kernel.mutualInfo_congr
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
{κ η : ProbabilityTheory.Kernel T (S × U)}
{μ : MeasureTheory.Measure T}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
Ik[κ , μ] = Ik[η , μ]
theorem
ProbabilityTheory.Kernel.compProd_assoc
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
{V : Type u_5}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSpace V]
(ξ : ProbabilityTheory.Kernel T S)
[ProbabilityTheory.IsSFiniteKernel ξ]
(κ : ProbabilityTheory.Kernel (T × S) U)
[ProbabilityTheory.IsSFiniteKernel κ]
(η : ProbabilityTheory.Kernel (T × S × U) V)
[ProbabilityTheory.IsSFiniteKernel η]
:
((ξ.compProd κ).compProd η).map ⇑MeasurableEquiv.prodAssoc = ξ.compProd (κ.compProd (η.comap ⇑MeasurableEquiv.prodAssoc ⋯))
theorem
ProbabilityTheory.Kernel.Measure.compProd_compProd
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
(μ : MeasureTheory.Measure T)
(ξ : ProbabilityTheory.Kernel T S)
[ProbabilityTheory.IsSFiniteKernel ξ]
(κ : ProbabilityTheory.Kernel (T × S) U)
[ProbabilityTheory.IsSFiniteKernel κ]
:
μ.compProd (ξ.compProd κ) = MeasureTheory.Measure.map (⇑MeasurableEquiv.prodAssoc) ((μ.compProd ξ).compProd κ)
theorem
ProbabilityTheory.Kernel.Measure.compProd_compProd'
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
(μ : MeasureTheory.Measure T)
(ξ : ProbabilityTheory.Kernel T S)
[ProbabilityTheory.IsSFiniteKernel ξ]
(κ : ProbabilityTheory.Kernel (T × S) U)
[ProbabilityTheory.IsSFiniteKernel κ]
:
μ.compProd (ξ.compProd κ) = MeasureTheory.Measure.comap (⇑MeasurableEquiv.prodAssoc.symm) ((μ.compProd ξ).compProd κ)
theorem
ProbabilityTheory.Kernel.Measure.compProd_compProd''
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
(μ : MeasureTheory.Measure T)
(ξ : ProbabilityTheory.Kernel T S)
[ProbabilityTheory.IsSFiniteKernel ξ]
(κ : ProbabilityTheory.Kernel (T × S) U)
[ProbabilityTheory.IsSFiniteKernel κ]
:
(μ.compProd ξ).compProd κ = MeasureTheory.Measure.comap (⇑MeasurableEquiv.prodAssoc) (μ.compProd (ξ.compProd κ))
@[simp]
theorem
ProbabilityTheory.Kernel.mutualInfo_swapRight
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass U]
(κ : ProbabilityTheory.Kernel T (S × U))
(μ : MeasureTheory.Measure T)
:
Ik[κ.swapRight , μ] = Ik[κ , μ]
theorem
ProbabilityTheory.Kernel.mutualInfo_nonneg'
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass U]
[MeasurableSingletonClass T]
{κ : ProbabilityTheory.Kernel T (S × U)}
{μ : MeasureTheory.Measure T}
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : κ.FiniteKernelSupport)
:
0 ≤ Ik[κ , μ]
theorem
ProbabilityTheory.Kernel.mutualInfo_nonneg
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass U]
[MeasurableSingletonClass T]
[Countable T]
{κ : ProbabilityTheory.Kernel T (S × U)}
{μ : MeasureTheory.Measure T}
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : κ.AEFiniteKernelSupport μ)
:
0 ≤ Ik[κ , μ]
theorem
ProbabilityTheory.Kernel.mutualInfo_compProd
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass U]
[MeasurableSingletonClass T]
[Countable S]
[Countable T]
{κ : ProbabilityTheory.Kernel T S}
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
{η : ProbabilityTheory.Kernel (T × S) U}
[ProbabilityTheory.IsMarkovKernel η]
{μ : MeasureTheory.Measure T}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : κ.AEFiniteKernelSupport μ)
(hη : η.AEFiniteKernelSupport (μ.compProd κ))
:
theorem
ProbabilityTheory.Kernel.mutualInfo_eq_fst_sub
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass U]
[MeasurableSingletonClass T]
[Countable S]
[Countable T]
[Countable U]
[Nonempty S]
{κ : ProbabilityTheory.Kernel T (S × U)}
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
{μ : MeasureTheory.Measure T}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : κ.AEFiniteKernelSupport μ)
:
@[simp]
theorem
ProbabilityTheory.Kernel.mutualInfo_prod
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass U]
[MeasurableSingletonClass T]
[Countable S]
[Countable T]
[Countable U]
{κ : ProbabilityTheory.Kernel T S}
{η : ProbabilityTheory.Kernel T U}
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
[ProbabilityTheory.IsZeroOrMarkovKernel η]
(μ : MeasureTheory.Measure T)
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : κ.AEFiniteKernelSupport μ)
(hη : η.AEFiniteKernelSupport μ)
:
Ik[κ.prod η , μ] = 0
theorem
ProbabilityTheory.Kernel.mutualInfo_eq_snd_sub
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass U]
[MeasurableSingletonClass T]
[Countable S]
[Countable T]
[Countable U]
[Nonempty U]
{κ : ProbabilityTheory.Kernel T (S × U)}
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
{μ : MeasureTheory.Measure T}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : κ.AEFiniteKernelSupport μ)
:
theorem
ProbabilityTheory.Kernel.entropy_condKernel_le_entropy_fst
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass U]
[MeasurableSingletonClass T]
[Countable S]
[Countable T]
[Countable U]
[Nonempty S]
(κ : ProbabilityTheory.Kernel T (S × U))
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
(μ : MeasureTheory.Measure T)
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : κ.AEFiniteKernelSupport μ)
:
Hk[κ.swapRight.condKernel , μ.compProd κ.snd] ≤ Hk[κ.fst , μ]
theorem
ProbabilityTheory.Kernel.entropy_condKernel_le_entropy_snd
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass U]
[MeasurableSingletonClass T]
[Countable S]
[Countable T]
[Countable U]
[Nonempty U]
{κ : ProbabilityTheory.Kernel T (S × U)}
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
{μ : MeasureTheory.Measure T}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : κ.AEFiniteKernelSupport μ)
:
Hk[κ.condKernel , μ.compProd κ.fst] ≤ Hk[κ.snd , μ]
theorem
ProbabilityTheory.Kernel.entropy_snd_sub_mutualInfo_le_entropy_map_of_injective
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass U]
[MeasurableSingletonClass T]
[Countable S]
[Countable T]
[Countable U]
{V : Type u_6}
[Countable V]
[MeasurableSpace V]
[MeasurableSingletonClass V]
(κ : ProbabilityTheory.Kernel T (S × U))
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
(μ : MeasureTheory.Measure T)
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
(f : S × U → V)
(hfi : ∀ (x : S), Function.Injective fun (y : U) => f (x, y))
[ProbabilityTheory.FiniteSupport μ]
(hκ : κ.AEFiniteKernelSupport μ)
:
theorem
ProbabilityTheory.Kernel.entropy_reverse
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
{V : Type u_5}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSpace V]
[Countable S]
[MeasurableSingletonClass S]
[Countable T]
[MeasurableSingletonClass T]
[Countable U]
[MeasurableSingletonClass U]
[Countable V]
[MeasurableSingletonClass V]
{κ : ProbabilityTheory.Kernel T (S × U × V)}
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
{μ : MeasureTheory.Measure T}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : κ.AEFiniteKernelSupport μ)
:
Hk[κ.reverse , μ] = Hk[κ , μ]
instance
ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.compProd
{α : Type u_6}
{β : Type u_7}
{γ : Type u_8}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
(η : ProbabilityTheory.Kernel (α × β) γ)
[ProbabilityTheory.IsZeroOrMarkovKernel η]
:
ProbabilityTheory.IsZeroOrMarkovKernel (κ.compProd η)
Equations
- ⋯ = ⋯
instance
ProbabilityTheory.Kernel.IsZeroOrProbabilityMeasure.compProd
{α : Type u_6}
{β : Type u_7}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
:
MeasureTheory.IsZeroOrProbabilityMeasure (μ.compProd κ)
Equations
- ⋯ = ⋯
theorem
ProbabilityTheory.Kernel.entropy_condKernel_compProd_triple
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
{V : Type u_5}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSpace V]
[Countable S]
[MeasurableSingletonClass S]
[Countable T]
[MeasurableSingletonClass T]
[Countable U]
[MeasurableSingletonClass U]
[Countable V]
[MeasurableSingletonClass V]
[Nonempty V]
(ξ : ProbabilityTheory.Kernel T S)
[ProbabilityTheory.IsZeroOrMarkovKernel ξ]
(κ : ProbabilityTheory.Kernel (T × S) U)
[ProbabilityTheory.IsMarkovKernel κ]
(η : ProbabilityTheory.Kernel (T × S × U) V)
[ProbabilityTheory.IsMarkovKernel η]
(μ : MeasureTheory.Measure T)
[MeasureTheory.IsProbabilityMeasure μ]
:
Hk[((ξ.compProd κ).compProd η).condKernel , μ.compProd (ξ.compProd κ)] = Hk[η , μ.compProd (ξ.compProd κ)]
theorem
ProbabilityTheory.Kernel.entropy_submodular_compProd
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
{V : Type u_5}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSpace V]
[Countable S]
[MeasurableSingletonClass S]
[Countable T]
[MeasurableSingletonClass T]
[Countable U]
[MeasurableSingletonClass U]
[Countable V]
[MeasurableSingletonClass V]
{ξ : ProbabilityTheory.Kernel T S}
[ProbabilityTheory.IsZeroOrMarkovKernel ξ]
{κ : ProbabilityTheory.Kernel (T × S) U}
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
{η : ProbabilityTheory.Kernel (T × S × U) V}
[ProbabilityTheory.IsMarkovKernel η]
{μ : MeasureTheory.Measure T}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : κ.AEFiniteKernelSupport (μ.compProd ξ))
(hη : η.AEFiniteKernelSupport (μ.compProd (ξ.compProd κ)))
(hξ : ξ.AEFiniteKernelSupport μ)
:
Hk[η , μ.compProd (ξ.compProd κ)] ≤ Hk[(κ.compProd (η.comap ⇑MeasurableEquiv.prodAssoc ⋯)).snd , μ.compProd ξ]
theorem
ProbabilityTheory.Kernel.entropy_compProd_triple_add_entropy_le
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
{V : Type u_5}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSpace V]
[Countable S]
[MeasurableSingletonClass S]
[Countable T]
[MeasurableSingletonClass T]
[Countable U]
[MeasurableSingletonClass U]
[Countable V]
[MeasurableSingletonClass V]
{ξ : ProbabilityTheory.Kernel T S}
[ProbabilityTheory.IsZeroOrMarkovKernel ξ]
{κ : ProbabilityTheory.Kernel (T × S) U}
[ProbabilityTheory.IsMarkovKernel κ]
{η : ProbabilityTheory.Kernel (T × S × U) V}
[ProbabilityTheory.IsMarkovKernel η]
{μ : MeasureTheory.Measure T}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : κ.AEFiniteKernelSupport (μ.compProd ξ))
(hη : η.AEFiniteKernelSupport (μ.compProd (ξ.compProd κ)))
(hξ : ξ.AEFiniteKernelSupport μ)
:
theorem
ProbabilityTheory.Kernel.entropy_triple_add_entropy_le'
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
{V : Type u_5}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSpace V]
[Countable S]
[MeasurableSingletonClass S]
[Countable T]
[MeasurableSingletonClass T]
[Countable U]
[MeasurableSingletonClass U]
[Countable V]
[MeasurableSingletonClass V]
{κ : ProbabilityTheory.Kernel T (S × U × V)}
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
{μ : MeasureTheory.Measure T}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : κ.AEFiniteKernelSupport μ)
:
The submodularity inequality: $$ H[X,Y,Z] + H[X] \leq H[X,Z] + H[X,Y].$$
theorem
ProbabilityTheory.Kernel.entropy_triple_add_entropy_le
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
{V : Type u_5}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSpace V]
[Countable S]
[MeasurableSingletonClass S]
[Countable T]
[MeasurableSingletonClass T]
[Countable U]
[MeasurableSingletonClass U]
[Countable V]
[MeasurableSingletonClass V]
(κ : ProbabilityTheory.Kernel T (S × U × V))
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
(μ : MeasureTheory.Measure T)
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : κ.AEFiniteKernelSupport μ)
:
The submodularity inequality: $$ H[X,Y,Z] + H[Z] \leq H[X,Z] + H[Y,Z].$$