Mutual Information of kernels #

Main definitions #

mutualInfo: Mutual information of a kernel κ into a product space with respect to a measure μ. This is denoted by Ik[κ, μ] and is equal to Hk[fst κ, μ] + Hk[snd κ, μ] - Hk[κ, μ].

Main statements #

mutualInfo_nonneg: Ik[κ, μ] is nonnegative
entropy_condKernel_le_entropy_fst and entropy_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] (κ : Kernel T (S × U)) (μ : MeasureTheory.Measure T) :

ℝ

Mutual information of a kernel into a product space with respect to a measure.

Equations

Ik[κ , μ] = Hk[κ.fst , μ] + Hk[κ.snd , μ] - Hk[κ , μ]

Instances For

source

def ProbabilityTheory.Kernel.«termIk[_,_]» :

Lean.ParserDescr

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

source

def ProbabilityTheory.Kernel.«termIk[_,_]».«delab_app.ProbabilityTheory.Kernel.mutualInfo» :

Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem ProbabilityTheory.Kernel.mutualInfo_def {S : Type u_2} {T : Type u_3} {U : Type u_4} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] (κ : Kernel T (S × U)) (μ : MeasureTheory.Measure T) :

Ik[κ , μ] = Hk[κ.fst , μ] + Hk[κ.snd , μ] - Hk[κ , μ]

source

@[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] (κ : Kernel T (S × U)) :

Ik[κ , 0] = 0

source

@[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

source

theorem ProbabilityTheory.Kernel.mutualInfo_congr {S : Type u_2} {T : Type u_3} {U : Type u_4} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] {κ η : Kernel T (S × U)} {μ : MeasureTheory.Measure T} (h : ⇑κ =ᵐ[μ] ⇑η) :

Ik[κ , μ] = Ik[η , μ]

source

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] (ξ : Kernel T S) [IsSFiniteKernel ξ] (κ : Kernel (T × S) U) [IsSFiniteKernel κ] (η : Kernel (T × S × U) V) [IsSFiniteKernel η] :

((ξ.compProd κ).compProd η).map ⇑MeasurableEquiv.prodAssoc = ξ.compProd (κ.compProd (η.comap ⇑MeasurableEquiv.prodAssoc ⋯))

source

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) (ξ : Kernel T S) [IsSFiniteKernel ξ] (κ : Kernel (T × S) U) [IsSFiniteKernel κ] :

μ.compProd (ξ.compProd κ) = MeasureTheory.Measure.map (⇑MeasurableEquiv.prodAssoc) ((μ.compProd ξ).compProd κ)

source

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) (ξ : Kernel T S) [IsSFiniteKernel ξ] (κ : Kernel (T × S) U) [IsSFiniteKernel κ] :

μ.compProd (ξ.compProd κ) = MeasureTheory.Measure.comap (⇑MeasurableEquiv.prodAssoc.symm) ((μ.compProd ξ).compProd κ)

source

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) (ξ : Kernel T S) [IsSFiniteKernel ξ] (κ : Kernel (T × S) U) [IsSFiniteKernel κ] :

(μ.compProd ξ).compProd κ = MeasureTheory.Measure.comap (⇑MeasurableEquiv.prodAssoc) (μ.compProd (ξ.compProd κ))

source

@[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] (κ : Kernel T (S × U)) (μ : MeasureTheory.Measure T) :

Ik[κ.swapRight , μ] = Ik[κ , μ]

source

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] {κ : Kernel T (S × U)} {μ : MeasureTheory.Measure T} [MeasureTheory.IsFiniteMeasure μ] [FiniteSupport μ] (hκ : κ.FiniteKernelSupport) :

0 ≤ Ik[κ , μ]

source

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] {κ : Kernel T (S × U)} {μ : MeasureTheory.Measure T} [MeasureTheory.IsFiniteMeasure μ] [FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) :

0 ≤ Ik[κ , μ]

source

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] {κ : Kernel T S} [IsZeroOrMarkovKernel κ] {η : Kernel (T × S) U} [IsMarkovKernel η] {μ : MeasureTheory.Measure T} [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) (hη : η.AEFiniteKernelSupport (μ.compProd κ)) :

Ik[κ.compProd η , μ] = Hk[κ , μ] + Hk[(κ.compProd η).snd , μ] - Hk[κ.compProd η , μ]

source

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] {κ : Kernel T (S × U)} [IsZeroOrMarkovKernel κ] {μ : MeasureTheory.Measure T} [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) :

Ik[κ , μ] = Hk[κ.fst , μ] - Hk[κ.swapRight.condKernel , μ.compProd κ.snd]

source

@[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] {κ : Kernel T S} {η : Kernel T U} [IsZeroOrMarkovKernel κ] [IsZeroOrMarkovKernel η] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) (hη : η.AEFiniteKernelSupport μ) :

Ik[κ.prod η , μ] = 0

source

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] {κ : Kernel T (S × U)} [IsZeroOrMarkovKernel κ] {μ : MeasureTheory.Measure T} [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) :

Ik[κ , μ] = Hk[κ.snd , μ] - Hk[κ.condKernel , μ.compProd κ.fst]

source

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] (κ : Kernel T (S × U)) [IsZeroOrMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) :

Hk[κ.swapRight.condKernel , μ.compProd κ.snd] ≤ Hk[κ.fst , μ]

source

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] {κ : Kernel T (S × U)} [IsZeroOrMarkovKernel κ] {μ : MeasureTheory.Measure T} [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) :

Hk[κ.condKernel , μ.compProd κ.fst] ≤ Hk[κ.snd , μ]

source

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] (κ : Kernel T (S × U)) [IsZeroOrMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] (f : S × U → V) (hfi : ∀ (x : S), Function.Injective fun (y : U) => f (x, y)) [FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) :

Hk[κ.snd , μ] - Ik[κ , μ] ≤ Hk[κ.map f , μ]

source

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] {κ : Kernel T (S × U × V)} [IsZeroOrMarkovKernel κ] {μ : MeasureTheory.Measure T} [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) :

Hk[κ.reverse , μ] = Hk[κ , μ]

source

instance ProbabilityTheory.Kernel.IsZeroOrProbabilityMeasure.compProd {α : Type u_6} {β : Type u_7} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure α) [MeasureTheory.IsZeroOrProbabilityMeasure μ] (κ : Kernel α β) [IsZeroOrMarkovKernel κ] :

MeasureTheory.IsZeroOrProbabilityMeasure (μ.compProd κ)

source

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] (ξ : Kernel T S) [IsZeroOrMarkovKernel ξ] (κ : Kernel (T × S) U) [IsMarkovKernel κ] (η : Kernel (T × S × U) V) [IsMarkovKernel η] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] :

Hk[((ξ.compProd κ).compProd η).condKernel , μ.compProd (ξ.compProd κ)] = Hk[η , μ.compProd (ξ.compProd κ)]

source

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] {ξ : Kernel T S} [IsZeroOrMarkovKernel ξ] {κ : Kernel (T × S) U} [IsZeroOrMarkovKernel κ] {η : Kernel (T × S × U) V} [IsMarkovKernel η] {μ : MeasureTheory.Measure T} [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport (μ.compProd ξ)) (hη : η.AEFiniteKernelSupport (μ.compProd (ξ.compProd κ))) (hξ : ξ.AEFiniteKernelSupport μ) :

Hk[η , μ.compProd (ξ.compProd κ)] ≤ Hk[(κ.compProd (η.comap ⇑MeasurableEquiv.prodAssoc ⋯)).snd , μ.compProd ξ]

source

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] {ξ : Kernel T S} [IsZeroOrMarkovKernel ξ] {κ : Kernel (T × S) U} [IsMarkovKernel κ] {η : Kernel (T × S × U) V} [IsMarkovKernel η] {μ : MeasureTheory.Measure T} [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport (μ.compProd ξ)) (hη : η.AEFiniteKernelSupport (μ.compProd (ξ.compProd κ))) (hξ : ξ.AEFiniteKernelSupport μ) :

Hk[(ξ.compProd κ).compProd η , μ] + Hk[ξ , μ] ≤ Hk[ξ.compProd (κ.compProd (η.comap ⇑MeasurableEquiv.prodAssoc ⋯)).snd , μ] + Hk[ξ.compProd κ , μ]

source

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] {κ : Kernel T (S × U × V)} [IsZeroOrMarkovKernel κ] {μ : MeasureTheory.Measure T} [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) :

Hk[κ , μ] + Hk[κ.fst , μ] ≤ Hk[κ.deleteMiddle , μ] + Hk[κ.deleteRight , μ]

The submodularity inequality: $H [X, Y, Z] + H [X] \leq H [X, Z] + H [X, Y] .$

source

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] (κ : Kernel T (S × U × V)) [IsZeroOrMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) :

Hk[κ , μ] + Hk[κ.snd.snd , μ] ≤ Hk[κ.deleteMiddle , μ] + Hk[κ.snd , μ]

The submodularity inequality: $H [X, Y, Z] + H [Z] \leq H [X, Z] + H [Y, Z] .$

Documentation

PFR.ForMathlib.Entropy.Kernel.MutualInfo

Mutual Information of kernels #

Main definitions #

Main statements #

Notations #