Entropy of random variables #
Random variables carry the quantities of a measure through their laws: the entropy H[X ; μ] and
mutual information I[X : Y ; μ], and their expectations over the values of a third variable, the
conditional entropy H[X | Y ; μ] and conditional mutual information I[X : Y | Z ; μ]. On finite
types these obey the chain rule and vanish, for mutual
information, exactly on independent and
conditionally independent variables, so
conditioning leaves entropy unchanged only under independence.
Implementation notes #
[UPSTREAM] candidate: mathlib has no entropy of a random variable and no mutual information,
conditional or not.
References #
- [CT06], chapter 2.
- The PFR project,
PFR/ForMathlib/Entropy/Basic.lean.
noncomputable def
InformationTheory.entropy
{S : Type u_1}
[MeasurableSpace S]
{Ω : Type u_3}
[MeasurableSpace Ω]
(X : Ω → S)
(μ : MeasureTheory.Measure Ω)
:
ℝ
The entropy of a random variable is the entropy of its law.
Equations
- InformationTheory.entropy X μ = InformationTheory.measureEntropy (MeasureTheory.Measure.map X μ)
Instances For
The entropy of a random variable is the entropy of its law.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
InformationTheory.entropy_def
{S : Type u_1}
[MeasurableSpace S]
{Ω : Type u_3}
[MeasurableSpace Ω]
(X : Ω → S)
(μ : MeasureTheory.Measure Ω)
:
entropy X μ = measureEntropy (MeasureTheory.Measure.map X μ)
theorem
InformationTheory.entropy_nonneg
{S : Type u_1}
[MeasurableSpace S]
{Ω : Type u_3}
[MeasurableSpace Ω]
(X : Ω → S)
(μ : MeasureTheory.Measure Ω)
:
0 ≤ entropy X μ
@[simp]
theorem
InformationTheory.entropy_zero_measure
{S : Type u_1}
[MeasurableSpace S]
{Ω : Type u_3}
[MeasurableSpace Ω]
(X : Ω → S)
:
entropy X 0 = 0
theorem
InformationTheory.entropy_le_log_card
{S : Type u_1}
[MeasurableSpace S]
{Ω : Type u_3}
[MeasurableSpace Ω]
[Fintype S]
[MeasurableSingletonClass S]
(X : Ω → S)
(μ : MeasureTheory.Measure Ω)
:
entropy X μ ≤ Real.log ↑(Fintype.card S)
theorem
InformationTheory.entropy_eq_sum
{S : Type u_1}
[MeasurableSpace S]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
[Fintype S]
[MeasurableSingletonClass S]
(hX : Measurable X)
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
:
entropy X μ = ∑ s : S, (μ.real (X ⁻¹' {s})).negMulLog
theorem
InformationTheory.entropy_eq_sum_finset
{S : Type u_1}
[MeasurableSpace S]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
[MeasurableSingletonClass S]
(hX : Measurable X)
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
{A : Finset S}
(hA : ∀ (ω : Ω), X ω ∈ A)
:
entropy X μ = ∑ s ∈ A, (μ.real (X ⁻¹' {s})).negMulLog
The entropy of a random variable valued in a finite set is a sum over that set.
theorem
InformationTheory.entropy_of_subsingleton
{S : Type u_1}
[MeasurableSpace S]
{Ω : Type u_3}
[MeasurableSpace Ω]
[Fintype S]
[MeasurableSingletonClass S]
[Subsingleton S]
(X : Ω → S)
(μ : MeasureTheory.Measure Ω)
:
entropy X μ = 0
A random variable with at most one value has no entropy.
theorem
InformationTheory.entropy_const
{S : Type u_1}
[MeasurableSpace S]
{Ω : Type u_3}
[MeasurableSpace Ω]
[MeasurableSingletonClass S]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(x : S)
:
entropy (fun (x_1 : Ω) => x) μ = 0
A constant random variable has no entropy.
theorem
InformationTheory.entropy_eq_zero_iff
{S : Type u_1}
[MeasurableSpace S]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
[Fintype S]
[MeasurableSingletonClass S]
(hX : Measurable X)
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
:
entropy X μ = 0 ↔ ∃ (x : S), ∀ᵐ (ω : Ω) ∂μ, X ω = x
A random variable has zero entropy iff it is almost surely constant.
theorem
InformationTheory.entropy_comp_of_injective
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
(μ : MeasureTheory.Measure Ω)
(hX : Measurable X)
{f : S → T}
(hf : Measurable f)
(hinj : Function.Injective f)
:
Entropy is invariant under an injective recoding of the values.
theorem
InformationTheory.entropy_comm
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
{Y : Ω → T}
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
(μ : MeasureTheory.Measure Ω)
(hX : Measurable X)
(hY : Measurable Y)
:
theorem
ProbabilityTheory.IdentDistrib.entropy_eq
{S : Type u_1}
[MeasurableSpace S]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
{Ω' : Type u_4}
[MeasurableSpace Ω']
{μ : MeasureTheory.Measure Ω}
{ν : MeasureTheory.Measure Ω'}
{X' : Ω' → S}
(h : IdentDistrib X X' μ ν)
:
noncomputable def
InformationTheory.condEntropy
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
(X : Ω → S)
(Y : Ω → T)
(μ : MeasureTheory.Measure Ω)
:
ℝ
The conditional entropy of X given Y is the expectation, under the law of Y, of the
entropy of X conditioned on Y = y.
Equations
- InformationTheory.condEntropy X Y μ = ∫ (y : T), InformationTheory.entropy X μ[|Y ⁻¹' {y}] ∂MeasureTheory.Measure.map Y μ
Instances For
The conditional entropy of X given Y is the expectation, under the law of Y, of the
entropy of X conditioned on Y = y.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
InformationTheory.condEntropy_nonneg
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
(X : Ω → S)
(Y : Ω → T)
(μ : MeasureTheory.Measure Ω)
:
0 ≤ condEntropy X Y μ
theorem
InformationTheory.condEntropy_eq_sum
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{Y : Ω → T}
[Fintype T]
[MeasurableSingletonClass T]
(X : Ω → S)
(hY : Measurable Y)
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure μ]
:
condEntropy X Y μ = ∑ y : T, μ.real (Y ⁻¹' {y}) * entropy X μ[|Y ⁻¹' {y}]
theorem
InformationTheory.condEntropy_comp_of_injective
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
[MeasurableSingletonClass S]
{U : Type u_4}
[MeasurableSpace U]
[MeasurableSingletonClass U]
(Y : Ω → T)
(μ : MeasureTheory.Measure Ω)
(hX : Measurable X)
{f : S → U}
(hf : Measurable f)
(hinj : Function.Injective f)
:
condEntropy (f ∘ X) Y μ = condEntropy X Y μ
Recoding X injectively leaves its entropy given Y unchanged.
theorem
InformationTheory.condEntropy_comp_right_of_measurableEmbedding
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{Y : Ω → T}
{U : Type u_4}
[MeasurableSpace U]
(X : Ω → S)
(μ : MeasureTheory.Measure Ω)
(hY : Measurable Y)
{g : T → U}
(hg : MeasurableEmbedding g)
:
condEntropy X (g ∘ Y) μ = condEntropy X Y μ
Recoding Y by a measurable embedding leaves the entropy of X given Y unchanged.
noncomputable def
InformationTheory.mutualInfo
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
(X : Ω → S)
(Y : Ω → T)
(μ : MeasureTheory.Measure Ω)
:
ℝ
Mutual information of two random variables.
Equations
- InformationTheory.mutualInfo X Y μ = InformationTheory.entropy X μ + InformationTheory.entropy Y μ - InformationTheory.entropy (fun (ω : Ω) => (X ω, Y ω)) μ
Instances For
Mutual information of two random variables.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
InformationTheory.mutualInfo_def
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
(X : Ω → S)
(Y : Ω → T)
(μ : MeasureTheory.Measure Ω)
:
mutualInfo X Y μ = entropy X μ + entropy Y μ - entropy (fun (ω : Ω) => (X ω, Y ω)) μ
theorem
InformationTheory.mutualInfo_eq_measureMutualInfo
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
{Y : Ω → T}
(hX : Measurable X)
(hY : Measurable Y)
(μ : MeasureTheory.Measure Ω)
:
mutualInfo X Y μ = measureMutualInfo (MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, Y ω)) μ)
The mutual information of two random variables is that of their joint law.
theorem
InformationTheory.mutualInfo_comm
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
{Y : Ω → T}
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
(μ : MeasureTheory.Measure Ω)
(hX : Measurable X)
(hY : Measurable Y)
:
mutualInfo X Y μ = mutualInfo Y X μ
Mutual information is symmetric.
noncomputable def
InformationTheory.condMutualInfo
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{U : Type u_4}
[MeasurableSpace U]
(X : Ω → S)
(Y : Ω → T)
(Z : Ω → U)
(μ : MeasureTheory.Measure Ω)
:
ℝ
The conditional mutual information of X and Y given Z is the expectation, under the law of
Z, of the mutual information of X and Y conditioned on Z = z.
Equations
- InformationTheory.condMutualInfo X Y Z μ = ∫ (z : U), InformationTheory.mutualInfo X Y μ[|Z ⁻¹' {z}] ∂MeasureTheory.Measure.map Z μ
Instances For
The conditional mutual information of X and Y given Z is the expectation, under the law of
Z, of the mutual information of X and Y conditioned on Z = z.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
InformationTheory.mutualInfo_nonneg
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
{Y : Ω → T}
[Fintype S]
[Fintype T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(hX : Measurable X)
(hY : Measurable Y)
:
0 ≤ mutualInfo X Y μ
theorem
InformationTheory.entropy_pair_eq_add_condEntropy
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
{Y : Ω → T}
[Fintype S]
[Fintype T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(hX : Measurable X)
(hY : Measurable Y)
:
entropy (fun (ω : Ω) => (X ω, Y ω)) μ = entropy Y μ + condEntropy X Y μ
Chain rule. The entropy of a pair is H[X, Y] = H[Y] + H[X | Y].
theorem
InformationTheory.mutualInfo_eq_entropy_sub_condEntropy
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
{Y : Ω → T}
[Fintype S]
[Fintype T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(hX : Measurable X)
(hY : Measurable Y)
:
mutualInfo X Y μ = entropy X μ - condEntropy X Y μ
theorem
InformationTheory.condEntropy_le_entropy
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
{Y : Ω → T}
[Fintype S]
[Fintype T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(hX : Measurable X)
(hY : Measurable Y)
:
condEntropy X Y μ ≤ entropy X μ
Conditioning reduces entropy, H[X | Y] ≤ H[X].
theorem
InformationTheory.mutualInfo_eq_sum_log
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
{Y : Ω → T}
[Fintype S]
[Fintype T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(hX : Measurable X)
(hY : Measurable Y)
:
mutualInfo X Y μ = ∑ x : S,
∑ y : T,
μ.real (X ⁻¹' {x} ∩ Y ⁻¹' {y}) * Real.log (μ.real (X ⁻¹' {x} ∩ Y ⁻¹' {y}) / (μ.real (X ⁻¹' {x}) * μ.real (Y ⁻¹' {y})))
On finite types, mutual information is the expected logarithm of the ratio of the joint mass to the product of the marginal masses.
theorem
InformationTheory.mutualInfo_eq_zero_iff
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
{Y : Ω → T}
[Fintype S]
[Fintype T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(hX : Measurable X)
(hY : Measurable Y)
:
mutualInfo X Y μ = 0 ↔ ProbabilityTheory.IndepFun X Y μ
Mutual information vanishes exactly on independent random variables.
theorem
ProbabilityTheory.IndepFun.entropy_pair_eq_add
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
{Y : Ω → T}
[Fintype S]
[Fintype T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
(h : IndepFun X Y μ)
(hX : Measurable X)
(hY : Measurable Y)
:
InformationTheory.entropy (fun (ω : Ω) => (X ω, Y ω)) μ = InformationTheory.entropy X μ + InformationTheory.entropy Y μ
The entropy of a pair of independent random variables is the sum of their entropies.
theorem
InformationTheory.condEntropy_eq_entropy_iff
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
{Y : Ω → T}
[Fintype S]
[Fintype T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(hX : Measurable X)
(hY : Measurable Y)
:
condEntropy X Y μ = entropy X μ ↔ ProbabilityTheory.IndepFun X Y μ
Conditioning leaves the entropy of X unchanged exactly when Y is independent of X.
theorem
ProbabilityTheory.IndepFun.condEntropy_eq_entropy
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
{Y : Ω → T}
[Fintype S]
[Fintype T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
(h : IndepFun X Y μ)
(hX : Measurable X)
(hY : Measurable Y)
:
theorem
InformationTheory.condEntropy_prod_eq_of_indepFun
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
{Y : Ω → T}
[Fintype S]
[Fintype T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
{U : Type u_4}
[MeasurableSpace U]
[Fintype U]
[MeasurableSingletonClass U]
{Z : Ω → U}
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
(h : ProbabilityTheory.IndepFun (fun (ω : Ω) => (X ω, Y ω)) Z μ)
:
condEntropy X (fun (ω : Ω) => (Y ω, Z ω)) μ = condEntropy X Y μ
Conditioning also on a random variable independent of the pair (X, Y) leaves the entropy
of X given Y unchanged.
theorem
InformationTheory.condMutualInfo_eq_sum
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
{U : Type u_4}
[MeasurableSpace U]
[Fintype U]
[MeasurableSingletonClass U]
{Z : Ω → U}
(X : Ω → S)
(Y : Ω → T)
(hZ : Measurable Z)
:
condMutualInfo X Y Z μ = ∑ z : U, μ.real (Z ⁻¹' {z}) * mutualInfo X Y μ[|Z ⁻¹' {z}]
theorem
InformationTheory.condMutualInfo_eq_condEntropy_add_sub
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
{U : Type u_4}
[MeasurableSpace U]
[Fintype U]
[MeasurableSingletonClass U]
{Z : Ω → U}
(X : Ω → S)
(Y : Ω → T)
(hZ : Measurable Z)
:
condMutualInfo X Y Z μ = condEntropy X Z μ + condEntropy Y Z μ - condEntropy (fun (ω : Ω) => (X ω, Y ω)) Z μ
theorem
InformationTheory.condMutualInfo_eq_condEntropy_sub_condEntropy
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
{Y : Ω → T}
[Fintype S]
[Fintype T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
{U : Type u_4}
[MeasurableSpace U]
[Fintype U]
[MeasurableSingletonClass U]
{Z : Ω → U}
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
:
condMutualInfo X Y Z μ = condEntropy X Z μ - condEntropy X (fun (ω : Ω) => (Y ω, Z ω)) μ
theorem
InformationTheory.condMutualInfo_nonneg
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
{Y : Ω → T}
[Fintype S]
[Fintype T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
{U : Type u_4}
{Z : Ω → U}
[MeasurableSpace U]
(hX : Measurable X)
(hY : Measurable Y)
:
0 ≤ condMutualInfo X Y Z μ
theorem
InformationTheory.condMutualInfo_eq_zero_iff
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
{Y : Ω → T}
[Fintype S]
[Fintype T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
{U : Type u_4}
[MeasurableSpace U]
[Fintype U]
[MeasurableSingletonClass U]
{Z : Ω → U}
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
:
condMutualInfo X Y Z μ = 0 ↔ ∀ (z : U), ProbabilityTheory.IndepFun X Y μ[|Z ⁻¹' {z}]
Conditional mutual information vanishes exactly when X and Y are independent given each
value of Z.
theorem
InformationTheory.condMutualInfo_eq_sum_log
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
{Y : Ω → T}
[Fintype S]
[Fintype T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
{U : Type u_4}
[MeasurableSpace U]
[Fintype U]
[MeasurableSingletonClass U]
{Z : Ω → U}
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
:
condMutualInfo X Y Z μ = ∑ x : S,
∑ y : T,
∑ z : U,
μ.real (X ⁻¹' {x} ∩ Y ⁻¹' {y} ∩ Z ⁻¹' {z}) * Real.log
(μ[|Z ⁻¹' {z}].real (X ⁻¹' {x} ∩ Y ⁻¹' {y}) / (μ[|Z ⁻¹' {z}].real (X ⁻¹' {x}) * μ[|Z ⁻¹' {z}].real (Y ⁻¹' {y})))
On finite types, conditional mutual information is the expected logarithm of the ratio of the conditional joint mass to the product of the conditional marginal masses.
theorem
InformationTheory.condEntropy_le_condEntropy_comp
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
{Y : Ω → T}
[Fintype S]
[Fintype T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
{U : Type u_4}
[MeasurableSpace U]
[Fintype U]
[MeasurableSingletonClass U]
(hX : Measurable X)
(hY : Measurable Y)
(f : T → U)
:
condEntropy X Y μ ≤ condEntropy X (f ∘ Y) μ
Conditioning on a function of Y leaves at least the entropy that conditioning on Y
leaves.
theorem
InformationTheory.condEntropy_of_injective
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
{Y : Ω → T}
[Fintype S]
[Fintype T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
{U : Type u_4}
[MeasurableSpace U]
[Fintype U]
[MeasurableSingletonClass U]
(hX : Measurable X)
(hY : Measurable Y)
(f : T → S → U)
(hf : ∀ (t : T), Function.Injective (f t))
:
condEntropy (fun (ω : Ω) => f (Y ω) (X ω)) Y μ = condEntropy X Y μ
Recoding X injectively, in a way that may depend on Y, leaves the entropy of X given
Y unchanged.
theorem
InformationTheory.condEntropy_comp_self
{T : Type u_2}
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{Y : Ω → T}
[Fintype T]
[MeasurableSingletonClass T]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
{U : Type u_4}
[MeasurableSpace U]
[Fintype U]
[MeasurableSingletonClass U]
(hY : Measurable Y)
(f : T → U)
:
condEntropy (f ∘ Y) Y μ = 0
A function of Y has no entropy given Y.
theorem
InformationTheory.entropy_comp_le
{S : Type u_1}
[MeasurableSpace S]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
[Fintype S]
[MeasurableSingletonClass S]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
{U : Type u_4}
[MeasurableSpace U]
[Fintype U]
[MeasurableSingletonClass U]
(hX : Measurable X)
(f : S → U)
:
A function of a random variable has at most its entropy.
theorem
InformationTheory.entropy_le_measureEntropy
{S : Type u_1}
[MeasurableSpace S]
{Ω : Type u_3}
[MeasurableSpace Ω]
[Fintype S]
[MeasurableSingletonClass S]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
[Fintype Ω]
[MeasurableSingletonClass Ω]
(X : Ω → S)
:
entropy X μ ≤ measureEntropy μ
A random variable has at most the entropy of its sample-space measure.
theorem
ProbabilityTheory.IdentDistrib.condEntropy_eq
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
{Y : Ω → T}
[Fintype S]
[Fintype T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{Ω' : Type u_4}
[MeasurableSpace Ω']
{ν : MeasureTheory.Measure Ω'}
[MeasureTheory.IsProbabilityMeasure ν]
{X' : Ω' → S}
{Y' : Ω' → T}
(hX : Measurable X)
(hY : Measurable Y)
(hX' : Measurable X')
(hY' : Measurable Y')
(h : IdentDistrib (fun (ω : Ω) => (X ω, Y ω)) (fun (ω : Ω') => (X' ω, Y' ω)) μ ν)
:
InformationTheory.condEntropy X Y μ = InformationTheory.condEntropy X' Y' ν
Conditional entropy is determined by the joint law.
theorem
InformationTheory.condEntropy_eq_zero_iff
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
{Ω : Type u_3}
[MeasurableSpace Ω]
{X : Ω → S}
{Y : Ω → T}
[Fintype S]
[Fintype T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
[Nonempty S]
(hX : Measurable X)
(hY : Measurable Y)
:
condEntropy X Y μ = 0 ↔ ∃ (f : T → S), ∀ᵐ (ω : Ω) ∂μ, X ω = f (Y ω)
On finite types, conditional entropy vanishes exactly when X is almost surely a function
of Y.
theorem
InformationTheory.condEntropy_fst_snd
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
[Fintype S]
[Fintype T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
(ρ : MeasureTheory.Measure (S × T))
[MeasureTheory.IsProbabilityMeasure ρ]
:
condEntropy Prod.fst Prod.snd ρ = measureEntropy ρ.fst - measureMutualInfo ρ
On a joint law, the conditional entropy of the first coordinate given the second is the entropy of the first marginal less the mutual information.
theorem
InformationTheory.measureMutualInfo_le_measureEntropy_snd
{S : Type u_1}
{T : Type u_2}
[MeasurableSpace S]
[MeasurableSpace T]
[Fintype S]
[Fintype T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
(ρ : MeasureTheory.Measure (S × T))
[MeasureTheory.IsProbabilityMeasure ρ]
:
measureMutualInfo ρ ≤ measureEntropy ρ.snd
Mutual information is at most the entropy of the second marginal.