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_fstandentropy_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[ProbabilityTheory.kernel.fst κ , μ] + Hk[ProbabilityTheory.kernel.snd κ , μ] - Hk[κ , μ]
Instances For
Pretty printer defined by notation3 command.
Equations
- One or more equations did not get rendered due to their size.
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
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[ProbabilityTheory.kernel.fst κ , μ] + Hk[ProbabilityTheory.kernel.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 : μ.ae.EventuallyEq ⇑κ ⇑η)
:
Ik[κ , μ] = Ik[η , μ]
theorem
ProbabilityTheory.kernel.mutualInfo_compProd
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[Nonempty S]
[Countable S]
[MeasurableSpace S]
[MeasurableSingletonClass S]
[Countable T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Nonempty U]
[MeasurableSpace U]
[MeasurableSingletonClass U]
{κ : ↥(ProbabilityTheory.kernel T S)}
[ProbabilityTheory.IsMarkovKernel κ]
{η : ↥(ProbabilityTheory.kernel (T × S) U)}
[ProbabilityTheory.IsMarkovKernel η]
{μ : MeasureTheory.Measure T}
[MeasureTheory.IsProbabilityMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ)
(hη : ProbabilityTheory.kernel.AEFiniteKernelSupport η (μ.compProd κ))
:
Ik[ProbabilityTheory.kernel.compProd κ η , μ] = Hk[κ , μ] + Hk[ProbabilityTheory.kernel.snd (ProbabilityTheory.kernel.compProd κ η) , μ] - Hk[ProbabilityTheory.kernel.compProd κ η , μ]
theorem
ProbabilityTheory.kernel.mutualInfo_eq_snd_sub
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[Nonempty S]
[Countable S]
[MeasurableSpace S]
[MeasurableSingletonClass S]
[Countable T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Nonempty U]
[Countable U]
[MeasurableSpace U]
[MeasurableSingletonClass U]
{κ : ↥(ProbabilityTheory.kernel T (S × U))}
[ProbabilityTheory.IsMarkovKernel κ]
{μ : MeasureTheory.Measure T}
[MeasureTheory.IsProbabilityMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ)
:
Ik[κ , μ] = Hk[ProbabilityTheory.kernel.snd κ , μ] - Hk[ProbabilityTheory.kernel.condKernel κ , μ.compProd (ProbabilityTheory.kernel.fst κ)]
theorem
ProbabilityTheory.kernel.mutualInfo_eq_fst_sub
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[Nonempty S]
[Countable S]
[MeasurableSpace S]
[MeasurableSingletonClass S]
[Countable T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Nonempty U]
[Countable U]
[MeasurableSpace U]
[MeasurableSingletonClass U]
{κ : ↥(ProbabilityTheory.kernel T (S × U))}
[ProbabilityTheory.IsMarkovKernel κ]
{μ : MeasureTheory.Measure T}
[MeasureTheory.IsProbabilityMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ)
:
Ik[κ , μ] = Hk[ProbabilityTheory.kernel.fst κ , μ] - Hk[ProbabilityTheory.kernel.condKernel (ProbabilityTheory.kernel.swapRight κ) ,
μ.compProd (ProbabilityTheory.kernel.snd κ)]
@[simp]
theorem
ProbabilityTheory.kernel.mutualInfo_prod
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[Nonempty S]
[Countable S]
[MeasurableSpace S]
[MeasurableSingletonClass S]
[Countable T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Nonempty U]
[Countable U]
[MeasurableSpace U]
[MeasurableSingletonClass U]
{κ : ↥(ProbabilityTheory.kernel T S)}
{η : ↥(ProbabilityTheory.kernel T U)}
[ProbabilityTheory.IsMarkovKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
(μ : MeasureTheory.Measure T)
[MeasureTheory.IsProbabilityMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ)
(hη : ProbabilityTheory.kernel.AEFiniteKernelSupport η μ)
:
Ik[ProbabilityTheory.kernel.prod κ η , μ] = 0
@[simp]
theorem
ProbabilityTheory.kernel.mutualInfo_swapRight
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace S]
[MeasurableSingletonClass S]
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass U]
(κ : ↥(ProbabilityTheory.kernel T (S × U)))
(μ : MeasureTheory.Measure T)
:
Ik[ProbabilityTheory.kernel.swapRight κ , μ] = Ik[κ , μ]
theorem
ProbabilityTheory.kernel.mutualInfo_nonneg'
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace S]
[MeasurableSingletonClass S]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[MeasurableSpace U]
[MeasurableSingletonClass U]
{κ : ↥(ProbabilityTheory.kernel T (S × U))}
{μ : MeasureTheory.Measure T}
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : ProbabilityTheory.kernel.FiniteKernelSupport κ)
:
0 ≤ Ik[κ , μ]
theorem
ProbabilityTheory.kernel.mutualInfo_nonneg
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[Nonempty S]
[MeasurableSpace S]
[MeasurableSingletonClass S]
[Countable T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Nonempty U]
[MeasurableSpace U]
[MeasurableSingletonClass U]
{κ : ↥(ProbabilityTheory.kernel T (S × U))}
{μ : MeasureTheory.Measure T}
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ)
:
0 ≤ Ik[κ , μ]
theorem
ProbabilityTheory.kernel.entropy_condKernel_le_entropy_fst
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[Nonempty S]
[Countable S]
[MeasurableSpace S]
[MeasurableSingletonClass S]
[Countable T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Nonempty U]
[Countable U]
[MeasurableSpace U]
[MeasurableSingletonClass U]
(κ : ↥(ProbabilityTheory.kernel T (S × U)))
[ProbabilityTheory.IsMarkovKernel κ]
(μ : MeasureTheory.Measure T)
[MeasureTheory.IsProbabilityMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ)
:
Hk[ProbabilityTheory.kernel.condKernel (ProbabilityTheory.kernel.swapRight κ) ,
μ.compProd (ProbabilityTheory.kernel.snd κ)] ≤ Hk[ProbabilityTheory.kernel.fst κ , μ]
theorem
ProbabilityTheory.kernel.entropy_condKernel_le_entropy_snd
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[Nonempty S]
[Countable S]
[MeasurableSpace S]
[MeasurableSingletonClass S]
[Countable T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Nonempty U]
[Countable U]
[MeasurableSpace U]
[MeasurableSingletonClass U]
{κ : ↥(ProbabilityTheory.kernel T (S × U))}
[ProbabilityTheory.IsMarkovKernel κ]
{μ : MeasureTheory.Measure T}
[MeasureTheory.IsProbabilityMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ)
:
Hk[ProbabilityTheory.kernel.condKernel κ , μ.compProd (ProbabilityTheory.kernel.fst κ)] ≤ Hk[ProbabilityTheory.kernel.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}
[Nonempty S]
[Countable S]
[MeasurableSpace S]
[MeasurableSingletonClass S]
[Nonempty T]
[Countable T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Nonempty U]
[Countable U]
[MeasurableSpace U]
[MeasurableSingletonClass U]
{V : Type u_5}
[Nonempty V]
[Countable V]
[MeasurableSpace V]
[MeasurableSingletonClass V]
(κ : ↥(ProbabilityTheory.kernel T (S × U)))
[ProbabilityTheory.IsMarkovKernel κ]
(μ : MeasureTheory.Measure T)
[MeasureTheory.IsProbabilityMeasure μ]
(f : S × U → V)
(hfi : ∀ (x : S), Function.Injective fun (y : U) => f (x, y))
[ProbabilityTheory.FiniteSupport μ]
(hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ)
:
Hk[ProbabilityTheory.kernel.snd κ , μ] - Ik[κ , μ] ≤ Hk[ProbabilityTheory.kernel.map κ f ⋯ , μ]
theorem
ProbabilityTheory.kernel.compProd_assoc
{V : Type u_5}
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSpace V]
(ξ : ↥(ProbabilityTheory.kernel T S))
[ProbabilityTheory.IsMarkovKernel ξ]
(κ : ↥(ProbabilityTheory.kernel (T × S) U))
[ProbabilityTheory.IsMarkovKernel κ]
(η : ↥(ProbabilityTheory.kernel (T × S × U) V))
[ProbabilityTheory.IsMarkovKernel η]
:
ProbabilityTheory.kernel.map (ProbabilityTheory.kernel.compProd (ProbabilityTheory.kernel.compProd ξ κ) η)
⇑MeasurableEquiv.prodAssoc ⋯ = ProbabilityTheory.kernel.compProd ξ
(ProbabilityTheory.kernel.compProd κ (ProbabilityTheory.kernel.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)
[MeasureTheory.IsProbabilityMeasure μ]
(ξ : ↥(ProbabilityTheory.kernel T S))
[ProbabilityTheory.IsMarkovKernel ξ]
(κ : ↥(ProbabilityTheory.kernel (T × S) U))
[ProbabilityTheory.IsMarkovKernel κ]
:
μ.compProd (ProbabilityTheory.kernel.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)
[MeasureTheory.IsProbabilityMeasure μ]
(ξ : ↥(ProbabilityTheory.kernel T S))
[ProbabilityTheory.IsMarkovKernel ξ]
(κ : ↥(ProbabilityTheory.kernel (T × S) U))
[ProbabilityTheory.IsMarkovKernel κ]
:
μ.compProd (ProbabilityTheory.kernel.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)
[MeasureTheory.IsProbabilityMeasure μ]
(ξ : ↥(ProbabilityTheory.kernel T S))
[ProbabilityTheory.IsMarkovKernel ξ]
(κ : ↥(ProbabilityTheory.kernel (T × S) U))
[ProbabilityTheory.IsMarkovKernel κ]
:
(μ.compProd ξ).compProd κ = MeasureTheory.Measure.comap (⇑MeasurableEquiv.prodAssoc) (μ.compProd (ProbabilityTheory.kernel.compProd ξ κ))
theorem
ProbabilityTheory.kernel.entropy_submodular_compProd
{V : Type u_5}
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[Nonempty S]
[Countable S]
[MeasurableSpace S]
[MeasurableSingletonClass S]
[Countable T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Nonempty U]
[Countable U]
[MeasurableSpace U]
[MeasurableSingletonClass U]
[Nonempty V]
[Countable V]
[MeasurableSpace V]
[MeasurableSingletonClass V]
{ξ : ↥(ProbabilityTheory.kernel T S)}
[ProbabilityTheory.IsMarkovKernel ξ]
{κ : ↥(ProbabilityTheory.kernel (T × S) U)}
[ProbabilityTheory.IsMarkovKernel κ]
{η : ↥(ProbabilityTheory.kernel (T × S × U) V)}
[ProbabilityTheory.IsMarkovKernel η]
{μ : MeasureTheory.Measure T}
[MeasureTheory.IsProbabilityMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ (μ.compProd ξ))
(hη : ProbabilityTheory.kernel.AEFiniteKernelSupport η (μ.compProd (ProbabilityTheory.kernel.compProd ξ κ)))
(hξ : ProbabilityTheory.kernel.AEFiniteKernelSupport ξ μ)
:
Hk[η , μ.compProd (ProbabilityTheory.kernel.compProd ξ κ)] ≤ Hk[ProbabilityTheory.kernel.snd
(ProbabilityTheory.kernel.compProd κ (ProbabilityTheory.kernel.comap η ⇑MeasurableEquiv.prodAssoc ⋯)) ,
μ.compProd ξ]
theorem
ProbabilityTheory.kernel.entropy_condKernel_compProd_triple
{V : Type u_5}
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[Countable S]
[MeasurableSpace S]
[MeasurableSingletonClass S]
[Countable T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Countable U]
[MeasurableSpace U]
[MeasurableSingletonClass U]
[Nonempty V]
[Countable V]
[MeasurableSpace V]
[MeasurableSingletonClass V]
(ξ : ↥(ProbabilityTheory.kernel T S))
[ProbabilityTheory.IsMarkovKernel ξ]
(κ : ↥(ProbabilityTheory.kernel (T × S) U))
[ProbabilityTheory.IsMarkovKernel κ]
(η : ↥(ProbabilityTheory.kernel (T × S × U) V))
[ProbabilityTheory.IsMarkovKernel η]
(μ : MeasureTheory.Measure T)
[MeasureTheory.IsProbabilityMeasure μ]
:
Hk[ProbabilityTheory.kernel.condKernel (ProbabilityTheory.kernel.compProd (ProbabilityTheory.kernel.compProd ξ κ) η) ,
μ.compProd (ProbabilityTheory.kernel.compProd ξ κ)] = Hk[η , μ.compProd (ProbabilityTheory.kernel.compProd ξ κ)]
theorem
ProbabilityTheory.kernel.entropy_compProd_triple_add_entropy_le
{V : Type u_5}
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[Nonempty S]
[Countable S]
[MeasurableSpace S]
[MeasurableSingletonClass S]
[Countable T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Nonempty U]
[Countable U]
[MeasurableSpace U]
[MeasurableSingletonClass U]
[Nonempty V]
[Countable V]
[MeasurableSpace V]
[MeasurableSingletonClass V]
{ξ : ↥(ProbabilityTheory.kernel T S)}
[ProbabilityTheory.IsMarkovKernel ξ]
{κ : ↥(ProbabilityTheory.kernel (T × S) U)}
[ProbabilityTheory.IsMarkovKernel κ]
{η : ↥(ProbabilityTheory.kernel (T × S × U) V)}
[ProbabilityTheory.IsMarkovKernel η]
{μ : MeasureTheory.Measure T}
[MeasureTheory.IsProbabilityMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ (μ.compProd ξ))
(hη : ProbabilityTheory.kernel.AEFiniteKernelSupport η (μ.compProd (ProbabilityTheory.kernel.compProd ξ κ)))
(hξ : ProbabilityTheory.kernel.AEFiniteKernelSupport ξ μ)
:
Hk[ProbabilityTheory.kernel.compProd (ProbabilityTheory.kernel.compProd ξ κ) η , μ] + Hk[ξ , μ] ≤ Hk[ProbabilityTheory.kernel.compProd ξ
(ProbabilityTheory.kernel.snd
(ProbabilityTheory.kernel.compProd κ (ProbabilityTheory.kernel.comap η ⇑MeasurableEquiv.prodAssoc ⋯))) ,
μ] + Hk[ProbabilityTheory.kernel.compProd ξ κ , μ]
theorem
ProbabilityTheory.kernel.entropy_triple_add_entropy_le'
{V : Type u_5}
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[Nonempty S]
[Countable S]
[MeasurableSpace S]
[MeasurableSingletonClass S]
[Countable T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Nonempty U]
[Countable U]
[MeasurableSpace U]
[MeasurableSingletonClass U]
[Nonempty V]
[Countable V]
[MeasurableSpace V]
[MeasurableSingletonClass V]
{κ : ↥(ProbabilityTheory.kernel T (S × U × V))}
[ProbabilityTheory.IsMarkovKernel κ]
{μ : MeasureTheory.Measure T}
[MeasureTheory.IsProbabilityMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ)
:
Hk[κ , μ] + Hk[ProbabilityTheory.kernel.fst κ , μ] ≤ Hk[ProbabilityTheory.kernel.deleteMiddle κ , μ] + Hk[ProbabilityTheory.kernel.deleteRight κ , μ]
The submodularity inequality: $$ H[X,Y,Z] + H[X] \leq H[X,Z] + H[X,Y].$$
theorem
ProbabilityTheory.kernel.entropy_reverse
{V : Type u_5}
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[Nonempty S]
[Countable S]
[MeasurableSpace S]
[MeasurableSingletonClass S]
[Countable T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Nonempty U]
[Countable U]
[MeasurableSpace U]
[MeasurableSingletonClass U]
[Nonempty V]
[Countable V]
[MeasurableSpace V]
[MeasurableSingletonClass V]
{κ : ↥(ProbabilityTheory.kernel T (S × U × V))}
[ProbabilityTheory.IsMarkovKernel κ]
{μ : MeasureTheory.Measure T}
[MeasureTheory.IsProbabilityMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ)
:
Hk[ProbabilityTheory.kernel.reverse κ , μ] = Hk[κ , μ]
theorem
ProbabilityTheory.kernel.entropy_triple_add_entropy_le
{V : Type u_5}
{S : Type u_2}
{T : Type u_3}
{U : Type u_4}
[Nonempty S]
[Countable S]
[MeasurableSpace S]
[MeasurableSingletonClass S]
[Countable T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Nonempty U]
[Countable U]
[MeasurableSpace U]
[MeasurableSingletonClass U]
[Nonempty V]
[Countable V]
[MeasurableSpace V]
[MeasurableSingletonClass V]
(κ : ↥(ProbabilityTheory.kernel T (S × U × V)))
[ProbabilityTheory.IsMarkovKernel κ]
(μ : MeasureTheory.Measure T)
[MeasureTheory.IsProbabilityMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ)
:
Hk[κ , μ] + Hk[ProbabilityTheory.kernel.snd (ProbabilityTheory.kernel.snd κ) , μ] ≤ Hk[ProbabilityTheory.kernel.deleteMiddle κ , μ] + Hk[ProbabilityTheory.kernel.snd κ , μ]
The submodularity inequality: $$ H[X,Y,Z] + H[Z] \leq H[X,Z] + H[Y,Z].$$