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] (κ : ProbabilityTheory.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[κ , μ]

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.

def ProbabilityTheory.Kernel.«termIk[_,_]».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

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) : Ik[κ , μ] = Hk[κ.fst , μ] + Hk[κ.snd , μ] - Hk[κ , μ]

@[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)} {η : 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 κ)) : Ik[κ.compProd η , μ] = Hk[κ , μ] + Hk[(κ.compProd η).snd , μ] - Hk[κ.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 μ) : Ik[κ , μ] = Hk[κ.fst , μ] - Hk[κ.swapRight.condKernel , μ.compProd κ.snd]

@[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 μ) : Ik[κ , μ] = Hk[κ.snd , μ] - Hk[κ.condKernel , μ.compProd κ.fst]

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 μ) : Hk[κ.snd , μ] - Ik[κ , μ] ≤ Hk[κ.map f , μ]

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 μ) : Hk[(ξ.compProd κ).compProd η , μ] + Hk[ξ , μ] ≤ Hk[ξ.compProd (κ.compProd (η.comap ⇑MeasurableEquiv.prodAssoc ⋯)).snd , μ] + Hk[ξ.compProd κ , μ]

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 μ) : Hk[κ , μ] + Hk[κ.fst , μ] ≤ Hk[κ.deleteMiddle , μ] + Hk[κ.deleteRight , μ]

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 μ) : Hk[κ , μ] + Hk[κ.snd.snd , μ] ≤ Hk[κ.deleteMiddle , μ] + Hk[κ.snd , μ]

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