Entropy and conditional entropy

Main definitions

• entropy: entropy of a random variable, defined as measureEntropy (volume.map X)
• condEntropy: conditional entropy of a random variable X w.r.t. another one Y
• mutualInfo: mutual information of two random variables

Main statements

• chain_rule: $H[⟨X, Y⟩] = H[Y] + H[X | Y]$
• entropy_cond_le_entropy: $H[X | Y] ≤ H[X]$. (Chain rule another way.)
• entropy_triple_add_entropy_le: $H[X, Y, Z] + H[Z] ≤ H[X, Z] + H[Y, Z]$. (Submodularity of entropy.)

Notations

• H[X] = entropy X
• H[X | Y ← y] = Hm[(ℙ[|Y ← y]).map X]
• H[X | Y] = condEntropy X Y, such that H[X | Y] = (volume.map Y)[fun y ↦ H[X | Y ← y]]
• I[X : Y] = mutualInfo X Y

All notations have variants where we can specify the measure (which is otherwise supposed to be volume). For example H[X ; μ] and I[X : Y ; μ] instead of H[X] and I[X : Y] respectively.

noncomputable def ProbabilityTheory.entropy {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] (X : Ω → S) (μ : MeasureTheory.Measure Ω := by volume_tac) : ℝ

Entropy of a random variable with values in a finite measurable space.

Equations

• H[X ; μ] = Hm[MeasureTheory.Measure.map X μ]

def ProbabilityTheory.«termH[_;_]» : Lean.ParserDescr

Entropy of a random variable with values in a finite measurable space.

Equations

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

def ProbabilityTheory.«termH[_]» : Lean.ParserDescr

Entropy of a random variable with values in a finite measurable space.

Equations

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

def ProbabilityTheory.«termH[_|_←_;_]» : Lean.ParserDescr

Entropy of a random variable with values in a finite measurable space.

Equations

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

def ProbabilityTheory.«termH[_|_←_]» : Lean.ParserDescr

Entropy of a random variable with values in a finite measurable space.

Equations

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

theorem ProbabilityTheory.entropy_def {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] (X : Ω → S) (μ : MeasureTheory.Measure Ω) : H[X ; μ] = Hm[MeasureTheory.Measure.map X μ]

Entropy of a random variable agrees with entropy of its distribution.

theorem ProbabilityTheory.entropy_eq_kernel_entropy {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] (X : Ω → S) (μ : MeasureTheory.Measure Ω) : H[X ; μ] = Hk[Kernel.const Unit (MeasureTheory.Measure.map X μ) , MeasureTheory.Measure.dirac ()]

Entropy of a random variable is also the kernel entropy of the distribution over a Dirac mass.

@[simp]

theorem ProbabilityTheory.entropy_zero_measure {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] (X : Ω → S) : H[X ; 0] = 0

Any variable on a zero measure space has zero entropy.

theorem ProbabilityTheory.entropy_congr {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {μ : MeasureTheory.Measure Ω} {X X' : Ω → S} (h : X =ᵐ[μ] X') : H[X ; μ] = H[X' ; μ]

Two variables that agree almost everywhere, have the same entropy.

theorem ProbabilityTheory.entropy_nonneg {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] (X : Ω → S) (μ : MeasureTheory.Measure Ω) : 0 ≤ H[X ; μ]

Entropy is always non-negative.

theorem ProbabilityTheory.IdentDistrib.entropy_congr {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {μ : MeasureTheory.Measure Ω} {Ω' : Type u_6} [MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} {X' : Ω' → S} (h : IdentDistrib X X' μ μ') : H[X ; μ] = H[X' ; μ']

Two variables that have the same distribution, have the same entropy.

theorem ProbabilityTheory.entropy_le_log_card {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [Fintype S] [MeasurableSingletonClass S] (X : Ω → S) (μ : MeasureTheory.Measure Ω) : H[X ; μ] ≤ Real.log ↑(Fintype.card S)

Entropy is at most the logarithm of the cardinality of the range.

theorem ProbabilityTheory.entropy_le_log_card_of_mem {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [DiscreteMeasurableSpace S] {A : Finset S} {μ : MeasureTheory.Measure Ω} {X : Ω → S} (hX : Measurable X) (h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ A) : H[X ; μ] ≤ Real.log ↑A.card

Entropy is at most the logarithm of the cardinality of a set in which X almost surely takes values in.

theorem ProbabilityTheory.entropy_le_log_card_of_mem_finite {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [DiscreteMeasurableSpace S] {A : Set S} {μ : MeasureTheory.Measure Ω} {X : Ω → S} (hA : A.Finite) (hX : Measurable X) (h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ A) : H[X ; μ] ≤ Real.log ↑(Nat.card ↑A)

Entropy is at most the logarithm of the cardinality of a set in which X almost surely takes values in.

theorem ProbabilityTheory.entropy_eq_sum {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsZeroOrProbabilityMeasure μ] : H[X ; μ] = ∑' (x : S), ((MeasureTheory.Measure.map X μ).real {x}).negMulLog

H[X] = ∑ₛ P[X=s] log 1 / P[X=s].

theorem ProbabilityTheory.entropy_eq_sum' {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsZeroOrProbabilityMeasure μ] : H[X ; μ] = ∑' (x : S), ((MeasureTheory.Measure.map X μ).real {x}).negMulLog

theorem ProbabilityTheory.entropy_eq_sum_finset {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsZeroOrProbabilityMeasure μ] {A : Finset S} (hA : (MeasureTheory.Measure.map X μ) (↑A)ᶜ = 0) : H[X ; μ] = ∑ x ∈ A, ((MeasureTheory.Measure.map X μ).real {x}).negMulLog

theorem ProbabilityTheory.entropy_eq_sum_finset' {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsZeroOrProbabilityMeasure μ] {A : Finset S} (hA : (MeasureTheory.Measure.map X μ) (↑A)ᶜ = 0) : H[X ; μ] = ∑ x ∈ A, ((MeasureTheory.Measure.map X μ).real {x}).negMulLog

theorem ProbabilityTheory.entropy_eq_sum_finiteRange {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} [MeasurableSingletonClass S] (hX : Measurable X) {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteRange X] : H[X ; μ] = ∑ x ∈ FiniteRange.toFinset X, ((MeasureTheory.Measure.map X μ).real {x}).negMulLog

theorem ProbabilityTheory.entropy_eq_sum_finiteRange' {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} [MeasurableSingletonClass S] (hX : Measurable X) {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteRange X] : H[X ; μ] = ∑ x ∈ FiniteRange.toFinset X, ((MeasureTheory.Measure.map X μ).real {x}).negMulLog

theorem ProbabilityTheory.entropy_cond_eq_sum {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {Y : Ω → T} (μ : MeasureTheory.Measure Ω) (y : T) : H[X | Y ← y ; μ] = ∑' (x : S), ((MeasureTheory.Measure.map X μ[|Y ⁻¹' {y}]).real {x}).negMulLog

H[X | Y=y] = ∑_s P[X=s | Y=y] log 1/(P[X=s | Y=y]).

theorem ProbabilityTheory.entropy_cond_eq_sum_finiteRange {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {Y : Ω → T} [MeasurableSingletonClass S] (hX : Measurable X) (μ : MeasureTheory.Measure Ω) (y : T) [FiniteRange X] : H[X | Y ← y ; μ] = ∑ x ∈ FiniteRange.toFinset X, ((MeasureTheory.Measure.map X μ[|Y ⁻¹' {y}]).real {x}).negMulLog

theorem ProbabilityTheory.entropy_comp_of_injective {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} [MeasurableSpace T] [Countable S] [MeasurableSingletonClass S] [MeasurableSingletonClass T] (μ : MeasureTheory.Measure Ω) (hX : Measurable X) (f : S → T) (hf : Function.Injective f) : H[f ∘ X ; μ] = H[X ; μ]

If X, Y are S-valued and T-valued random variables, and Y = f(X) for some injection f : S \to T, then H[Y] = H[X]. One can also use entropy_of_comp_eq_of_comp as an alternative if verifying injectivity is fiddly. For the upper bound only, see entropy_comp_le.

@[simp]

theorem ProbabilityTheory.entropy_const {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {μ : MeasureTheory.Measure Ω} [MeasurableSingletonClass S] [MeasureTheory.IsZeroOrProbabilityMeasure μ] (c : S) : H[fun (x : Ω) => c ; μ] = 0

The entropy of any constant is zero.

theorem ProbabilityTheory.IsUniform.entropy_eq {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [DiscreteMeasurableSpace S] {H : Finset S} {X : Ω → S} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hX : IsUniform (↑H) X μ) (hX' : Measurable X) : H[X ; μ] = Real.log ↑(Nat.card ↥H)

If X is uniformly distributed on H, then H[X] = log |H|.

theorem ProbabilityTheory.IsUniform.entropy_eq' {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [DiscreteMeasurableSpace S] {A : Set S} (hA : A.Finite) {X : Ω → S} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hX : IsUniform A X μ) (hX' : Measurable X) : H[X ; μ] = Real.log ↑A.ncard

Variant of IsUniform.entropy_congr where H is a finite Set rather than Finset.

theorem ProbabilityTheory.entropy_eq_log_card {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} [Fintype S] [MeasurableSingletonClass S] (hX : Measurable X) (μ : MeasureTheory.Measure Ω) [hμ : NeZero μ] [MeasureTheory.IsFiniteMeasure μ] : H[X ; μ] = Real.log ↑(Fintype.card S) ↔ ∀ (s : S), (MeasureTheory.Measure.map X μ) {s} = μ Set.univ / ↑(Fintype.card S)

If X is S-valued random variable, then H[X] = log |S| if and only if X is uniformly distributed.

theorem ProbabilityTheory.prob_ge_exp_neg_entropy {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSingletonClass S] (X : Ω → S) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (hX : Measurable X) [hX' : FiniteRange X] : ∃ (s : S), μ Set.univ * ↑(Real.exp (-H[X ; μ])).toNNReal ≤ (MeasureTheory.Measure.map X μ) {s}

If X is an S-valued random variable, then there exists s ∈ S such that P[X = s] ≥ \exp(- H[X]).

TODO: remove the probability measure hypothesis, which is unnecessary here.

theorem ProbabilityTheory.prob_ge_exp_neg_entropy' {S : Type u_2} [MeasurableSpace S] [MeasurableSingletonClass S] {Ω : Type u_6} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : Ω → S) (hX : Measurable X) [FiniteRange X] : ∃ (s : S), Real.exp (-H[X ; μ]) ≤ μ.real (X ⁻¹' {s})

If X is an S-valued random variable, then there exists s ∈ S such that P[X=s] ≥ \exp(-H[X]).

theorem ProbabilityTheory.const_of_nonpos_entropy {S : Type u_2} [MeasurableSpace S] [MeasurableSingletonClass S] {Ω : Type u_6} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → S} (hX : Measurable X) [FiniteRange X] (hent : H[X ; μ] ≤ 0) : ∃ (s : S), μ.real (X ⁻¹' {s}) = 1

If X is an S-valued random variable of non-positive entropy, then X is almost surely constant.

@[simp]

theorem ProbabilityTheory.entropy_prod_comp {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} [Countable S] [MeasurableSingletonClass S] [MeasurableSpace T] [MeasurableSingletonClass T] (hX : Measurable X) (μ : MeasureTheory.Measure Ω) (f : S → T) : H[⟨X, f ∘ X⟩ ; μ] = H[X ; μ]

H[X, f(X)] = H[X].

theorem ProbabilityTheory.entropy_comm {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {Y : Ω → T} [Countable S] [MeasurableSingletonClass S] [MeasurableSpace T] [MeasurableSingletonClass T] [Countable T] (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : H[⟨X, Y⟩ ; μ] = H[⟨Y, X⟩ ; μ]

H[X, Y] = H[Y, X].

theorem ProbabilityTheory.entropy_assoc {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} [Countable S] [MeasurableSingletonClass S] [MeasurableSpace T] [MeasurableSingletonClass T] [Countable U] [MeasurableSingletonClass U] [Countable T] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (μ : MeasureTheory.Measure Ω) : H[⟨X, ⟨Y, Z⟩⟩ ; μ] = H[⟨⟨X, Y⟩, Z⟩ ; μ]

H[(X, Y), Z] = H[X, (Y, Z)].

noncomputable def ProbabilityTheory.condEntropy {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace T] (X : Ω → S) (Y : Ω → T) (μ : MeasureTheory.Measure Ω := by volume_tac) : ℝ

Conditional entropy of a random variable w.r.t. another. This is the expectation under the law of Y of the entropy of the law of X conditioned on the event Y = y.

Equations

• H[X | Y ; μ] = ∫ (x : T), (fun (y : T) => H[X | Y ← y ; μ]) x ∂MeasureTheory.Measure.map Y μ

theorem ProbabilityTheory.condEntropy_def {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace T] (X : Ω → S) (Y : Ω → T) (μ : MeasureTheory.Measure Ω) : H[X | Y ; μ] = ∫ (x : T), (fun (y : T) => H[X | Y ← y ; μ]) x ∂MeasureTheory.Measure.map Y μ

def ProbabilityTheory.«termH[_|_;_]» : Lean.ParserDescr

Conditional entropy of a random variable w.r.t. another. This is the expectation under the law of Y of the entropy of the law of X conditioned on the event Y = y.

Equations

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

def ProbabilityTheory.«termH[_|_]» : Lean.ParserDescr

Conditional entropy of a random variable w.r.t. another. This is the expectation under the law of Y of the entropy of the law of X conditioned on the event Y = y.

Equations

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

theorem ProbabilityTheory.condEntropy_eq_zero {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace T] {X : Ω → S} {Y : Ω → T} [MeasurableSingletonClass T] (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (t : T) (ht : (MeasureTheory.Measure.map Y μ).real {t} = 0) : H[X | Y ← t ; μ] = 0

theorem ProbabilityTheory.condEntropy_eq_kernel_entropy {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace T] {X : Ω → S} {Y : Ω → T} [MeasurableSingletonClass T] [Nonempty S] [Countable S] [MeasurableSingletonClass S] (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [FiniteRange Y] : H[X | Y ; μ] = Hk[condDistrib X Y μ , MeasureTheory.Measure.map Y μ]

Conditional entropy of a random variable is equal to the entropy of its conditional kernel.

theorem ProbabilityTheory.condEntropy_two_eq_kernel_entropy {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {Z : Ω → U} [MeasurableSpace T] {X : Ω → S} {Y : Ω → T} [MeasurableSingletonClass T] [Countable T] [Nonempty T] [Nonempty S] [MeasurableSingletonClass S] [Countable S] [Countable U] [MeasurableSingletonClass U] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] [FiniteRange Y] [FiniteRange Z] : H[X | ⟨Y, Z⟩ ; μ] = Hk[(condDistrib (fun (a : Ω) => (Y a, X a)) Z μ).condKernel , (MeasureTheory.Measure.map Z μ).compProd (condDistrib (fun (a : Ω) => (Y a, X a)) Z μ).fst]

@[simp]

theorem ProbabilityTheory.condEntropy_zero_measure {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace T] (X : Ω → S) (Y : Ω → T) : H[X | Y ; 0] = 0

Any random variable on a zero measure space has zero conditional entropy.

theorem ProbabilityTheory.condEntropy_nonneg {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace T] (X : Ω → S) (Y : Ω → T) (μ : MeasureTheory.Measure Ω) : 0 ≤ H[X | Y ; μ]

Conditional entropy is non-negative.

theorem ProbabilityTheory.condEntropy_le_log_card {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass S] [Fintype S] (X : Ω → S) (Y : Ω → T) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : H[X | Y ; μ] ≤ Real.log ↑(Fintype.card S)

Conditional entropy is at most the logarithm of the cardinality of the range.

theorem ProbabilityTheory.condEntropy_eq_sum {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass T] (X : Ω → S) (Y : Ω → T) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (hY : Measurable Y) [FiniteRange Y] : H[X | Y ; μ] = ∑ y ∈ FiniteRange.toFinset Y, (MeasureTheory.Measure.map Y μ).real {y} * H[X | Y ← y ; μ]

H[X|Y] = ∑_y P[Y=y] H[X|Y=y].

theorem ProbabilityTheory.condEntropy_eq_sum_fintype {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass T] (X : Ω → S) (Y : Ω → T) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (hY : Measurable Y) [Fintype T] : H[X | Y ; μ] = ∑ y : T, μ.real (Y ⁻¹' {y}) * H[X | Y ← y ; μ]

H[X|Y] = ∑_y P[Y=y] H[X|Y=y]$.

theorem ProbabilityTheory.condEntropy_prod_eq_sum {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {T' : Type u_5} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass T] {X : Ω → S} {Y : Ω → T} {Z : Ω → T'} [MeasurableSpace T'] [MeasurableSingletonClass T'] (μ : MeasureTheory.Measure Ω) (hY : Measurable Y) (hZ : Measurable Z) [MeasureTheory.IsFiniteMeasure μ] [Fintype T] [Fintype T'] : H[X | ⟨Y, Z⟩ ; μ] = ∑ z : T', μ.real (Z ⁻¹' {z}) * H[X | Y ; μ[|Z ⁻¹' {z}]]

theorem ProbabilityTheory.condEntropy_eq_sum_sum {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace T] {X : Ω → S} [MeasurableSingletonClass T] [MeasurableSingletonClass S] (hX : Measurable X) {Y : Ω → T} (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] : H[X | Y ; μ] = ∑ y ∈ FiniteRange.toFinset Y, ∑ x ∈ FiniteRange.toFinset X, (MeasureTheory.Measure.map Y μ).real {y} * ((MeasureTheory.Measure.map X μ[|Y ⁻¹' {y}]).real {x}).negMulLog

H[X|Y] = ∑_y ∑_x P[Y=y] P[X=x|Y=y] log ⧸(P[X=x|Y=y])$.

theorem ProbabilityTheory.condEntropy_eq_sum_sum_fintype {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace T] {X : Ω → S} [MeasurableSingletonClass T] {Y : Ω → T} (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] [Fintype S] [Fintype T] : H[X | Y ; μ] = ∑ y : T, ∑ x : S, (MeasureTheory.Measure.map Y μ).real {y} * ((MeasureTheory.Measure.map X μ[|Y ⁻¹' {y}]).real {x}).negMulLog

H[X|Y] = ∑_y ∑_x P[Y=y] P[X=x|Y=y] log ⧸(P[X=x|Y=y])$.

theorem ProbabilityTheory.condEntropy_eq_sum_prod {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace T] {X : Ω → S} [MeasurableSingletonClass T] [MeasurableSingletonClass S] (hX : Measurable X) {Y : Ω → T} (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] : H[X | Y ; μ] = ∑ p ∈ FiniteRange.toFinset X ×ˢ FiniteRange.toFinset Y, (MeasureTheory.Measure.map Y μ).real {p.2} * ((MeasureTheory.Measure.map X μ[|Y ⁻¹' {p.2}]).real {p.1}).negMulLog

Same as previous lemma, but with a sum over a product space rather than a double sum.

theorem ProbabilityTheory.condEntropy_of_injective {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] [MeasurableSpace T] {X : Ω → S} {Y : Ω → T} [MeasurableSingletonClass T] [MeasurableSingletonClass S] [Countable S] [MeasurableSingletonClass U] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (hX : Measurable X) (hY : Measurable Y) (f : T → S → U) (hf : ∀ (t : T), Function.Injective (f t)) [FiniteRange Y] : H[fun (ω : Ω) => f (Y ω) (X ω) | Y ; μ] = H[X | Y ; μ]

If X : Ω → S, Y : Ω → T are random variables, and f : T × S → U is injective for each fixed t ∈ T, then H[f(Y, X) | Y] = H[X | Y]. Thus for instance H[X-Y|Y] = H[X|Y].

theorem ProbabilityTheory.condEntropy_comp_of_injective {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] [MeasurableSpace T] {X : Ω → S} [MeasurableSingletonClass T] [MeasurableSingletonClass S] [Countable S] {Y : Ω → U} (μ : MeasureTheory.Measure Ω) (hX : Measurable X) (f : S → T) (hf : Function.Injective f) : H[f ∘ X | Y ; μ] = H[X | Y ; μ]

A weaker version of the above lemma in which f is independent of Y.

theorem ProbabilityTheory.condEntropy_comm {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] [MeasurableSpace T] {X : Ω → S} {Y : Ω → T} [MeasurableSingletonClass T] [MeasurableSingletonClass S] [Countable S] [Countable T] {Z : Ω → U} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : H[⟨X, Y⟩ | Z ; μ] = H[⟨Y, X⟩ | Z ; μ]

H[X, Y| Z] = H[Y, X| Z].

theorem ProbabilityTheory.chain_rule' {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {Y : Ω → T} [MeasurableSpace T] [Countable S] [MeasurableSingletonClass S] [Countable T] [MeasurableSingletonClass T] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) [FiniteRange X] [FiniteRange Y] : H[⟨X, Y⟩ ; μ] = H[X ; μ] + H[Y | X ; μ]

One form of the chain rule : H[X, Y] = H[X] + H[Y | X].

theorem ProbabilityTheory.chain_rule {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {Y : Ω → T} [MeasurableSpace T] [Countable S] [MeasurableSingletonClass S] [Countable T] [MeasurableSingletonClass T] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) [FiniteRange X] [FiniteRange Y] : H[⟨X, Y⟩ ; μ] = H[Y ; μ] + H[X | Y ; μ]

Another form of the chain rule : H[X, Y] = H[Y] + H[X | Y].

theorem ProbabilityTheory.chain_rule'' {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {Y : Ω → T} [MeasurableSpace T] [Countable S] [MeasurableSingletonClass S] [Countable T] [MeasurableSingletonClass T] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) [FiniteRange X] [FiniteRange Y] : H[X | Y ; μ] = H[⟨X, Y⟩ ; μ] - H[Y ; μ]

Another form of the chain rule : H[X | Y] = H[X, Y] - H[Y].

theorem ProbabilityTheory.IdentDistrib.condEntropy_eq {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {μ : MeasureTheory.Measure Ω} [MeasurableSpace T] [Countable S] [MeasurableSingletonClass S] [Countable T] [MeasurableSingletonClass T] {Ω' : Type u_6} [MeasurableSpace Ω'] {X : Ω → S} {Y : Ω → T} {μ' : MeasureTheory.Measure Ω'} {X' : Ω' → S} {Y' : Ω' → T} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] (hX : Measurable X) (hY : Measurable Y) (hX' : Measurable X') (hY' : Measurable Y') (h : IdentDistrib (⟨X, Y⟩) (⟨X', Y'⟩) μ μ') [FiniteRange X] [FiniteRange Y] [FiniteRange X'] [FiniteRange Y'] : H[X | Y ; μ] = H[X' | Y' ; μ']

Two pairs of variables that have the same joint distribution, have the same conditional entropy.

theorem ProbabilityTheory.condEntropy_of_injective' {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {X : Ω → S} {Y : Ω → T} [MeasurableSpace T] [Countable S] [MeasurableSingletonClass S] [Countable T] [MeasurableSingletonClass T] [Countable U] [MeasurableSingletonClass U] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (f : T → U) (hf : Function.Injective f) (hfY : Measurable (f ∘ Y)) [FiniteRange X] [FiniteRange Y] : H[X | f ∘ Y ; μ] = H[X | Y ; μ]

If X : Ω → S and Y : Ω → T are random variables, and f : T → U is an injection then H[X | f(Y)] = H[X | Y].

theorem ProbabilityTheory.condEntropy_comp_self {Ω : Type u_1} {S : Type u_2} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {X : Ω → S} {μ : MeasureTheory.Measure Ω} [Countable S] [MeasurableSingletonClass S] [Countable U] [MeasurableSingletonClass U] [MeasureTheory.IsProbabilityMeasure μ] (hX : Measurable X) {f : S → U} (hf : Measurable f) [FiniteRange X] : H[X | f ∘ X ; μ] = H[X ; μ] - H[f ∘ X ; μ]

H[X | f(X)] = H[X] - H[f(X)].

theorem ProbabilityTheory.cond_chain_rule' {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} [MeasurableSpace T] [Countable S] [MeasurableSingletonClass S] [Countable T] [MeasurableSingletonClass T] [Countable U] [MeasurableSingletonClass U] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) [FiniteRange X] [FiniteRange Y] [FiniteRange Z] : H[⟨X, Y⟩ | Z ; μ] = H[X | Z ; μ] + H[Y | ⟨X, Z⟩ ; μ]

If X : Ω → S, Y : Ω → T, Z : Ω → U are random variables, then H[X, Y | Z] = H[X | Z] + H[Y|X, Z].

theorem ProbabilityTheory.cond_chain_rule {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} [MeasurableSpace T] [Countable S] [MeasurableSingletonClass S] [Countable T] [MeasurableSingletonClass T] [Countable U] [MeasurableSingletonClass U] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) [FiniteRange X] [FiniteRange Y] [FiniteRange Z] : H[⟨X, Y⟩ | Z ; μ] = H[Y | Z ; μ] + H[X | ⟨Y, Z⟩ ; μ]

H[X, Y | Z] = H[Y | Z] + H[X | Y, Z].

theorem ProbabilityTheory.entropy_comp_le {Ω : Type u_1} {S : Type u_2} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {X : Ω → S} [Countable S] [MeasurableSingletonClass S] [Countable U] [MeasurableSingletonClass U] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : Measurable X) (f : S → U) [FiniteRange X] : H[f ∘ X ; μ] ≤ H[X ; μ]

Data-processing inequality for the entropy: H[f(X)] ≤ H[X]. To upgrade this to equality, see entropy_of_comp_eq_of_comp or entropy_comp_of_injective.

theorem ProbabilityTheory.entropy_of_comp_eq_of_comp {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {Y : Ω → T} [MeasurableSpace T] [Countable S] [MeasurableSingletonClass S] [Countable T] [MeasurableSingletonClass T] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (f : S → T) (g : T → S) (h1 : Y = f ∘ X) (h2 : X = g ∘ Y) [FiniteRange X] [FiniteRange Y] : H[X ; μ] = H[Y ; μ]

A Schroder-Bernstein type theorem for entropy : if two random variables are functions of each other, then they have the same entropy. Can be used as a substitute for entropy_comp_of_injective if one doesn't want to establish the injectivity.

noncomputable def ProbabilityTheory.mutualInfo {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace T] (X : Ω → S) (Y : Ω → T) (μ : MeasureTheory.Measure Ω := by volume_tac) : ℝ

The mutual information I[X : Y] of two random variables is defined to be H[X] + H[Y] - H[X ; Y].

Equations

• I[X : Y ; μ] = H[X ; μ] + H[Y ; μ] - H[⟨X, Y⟩ ; μ]

def ProbabilityTheory.«termI[_:_;_]» : Lean.ParserDescr

The mutual information I[X : Y] of two random variables is defined to be H[X] + H[Y] - H[X ; Y].

Equations

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

def ProbabilityTheory.«termI[_:_]» : Lean.ParserDescr

The mutual information I[X : Y] of two random variables is defined to be H[X] + H[Y] - H[X ; Y].

Equations

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

theorem ProbabilityTheory.mutualInfo_def {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace T] (X : Ω → S) (Y : Ω → T) (μ : MeasureTheory.Measure Ω) : I[X : Y ; μ] = H[X ; μ] + H[Y ; μ] - H[⟨X, Y⟩ ; μ]

theorem ProbabilityTheory.entropy_add_entropy_sub_mutualInfo {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace T] (X : Ω → S) (Y : Ω → T) (μ : MeasureTheory.Measure Ω) : H[X ; μ] + H[Y ; μ] - I[X : Y ; μ] = H[⟨X, Y⟩ ; μ]

theorem ProbabilityTheory.IdentDistrib.mutualInfo_eq {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {Y : Ω → T} {μ : MeasureTheory.Measure Ω} [MeasurableSpace T] {Ω' : Type u_6} [MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} {X' : Ω' → S} {Y' : Ω' → T} (hXY : IdentDistrib (⟨X, Y⟩) (⟨X', Y'⟩) μ μ') : I[X : Y ; μ] = I[X' : Y' ; μ']

Substituting variables for ones with the same distributions doesn't change the mutual information.

noncomputable def ProbabilityTheory.condMutualInfo {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] [MeasurableSpace T] (X : Ω → S) (Y : Ω → T) (Z : Ω → U) (μ : MeasureTheory.Measure Ω := by volume_tac) : ℝ

The conditional mutual information I[X : Y| Z] is the mutual information of X| Z=z and Y| Z=z, integrated over z.

Equations

• I[X : Y|Z;μ] = ∫ (x : U), (fun (z : U) => H[X | Z ← z ; μ] + H[Y | Z ← z ; μ] - H[⟨X, Y⟩ | Z ← z ; μ]) x ∂MeasureTheory.Measure.map Z μ

theorem ProbabilityTheory.condMutualInfo_def {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] [MeasurableSpace T] (X : Ω → S) (Y : Ω → T) (Z : Ω → U) (μ : MeasureTheory.Measure Ω) : I[X : Y|Z;μ] = ∫ (x : U), (fun (z : U) => H[X | Z ← z ; μ] + H[Y | Z ← z ; μ] - H[⟨X, Y⟩ | Z ← z ; μ]) x ∂MeasureTheory.Measure.map Z μ

def ProbabilityTheory.«termI[_:_|_;_]» : Lean.ParserDescr

The conditional mutual information I[X : Y| Z] is the mutual information of X| Z=z and Y| Z=z, integrated over z.

Equations

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

def ProbabilityTheory.«termI[_:_|_]» : Lean.ParserDescr

The conditional mutual information I[X : Y| Z] is the mutual information of X| Z=z and Y| Z=z, integrated over z.

Equations

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

theorem ProbabilityTheory.condMutualInfo_eq_integral_mutualInfo {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} {μ : MeasureTheory.Measure Ω} [MeasurableSpace T] : I[X : Y|Z;μ] = ∫ (x : U), (fun (z : U) => I[X : Y ; μ[|Z ⁻¹' {z}]]) x ∂MeasureTheory.Measure.map Z μ

@[simp]

theorem ProbabilityTheory.condMutualInfo_zero_measure {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} [MeasurableSpace T] : I[X : Y|Z;0] = 0

theorem ProbabilityTheory.mutualInfo_nonneg {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {Y : Ω → T} [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [FiniteRange X] [FiniteRange Y] : 0 ≤ I[X : Y ; μ]

Mutual information is non-negative.

theorem ProbabilityTheory.entropy_pair_le_add {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {Y : Ω → T} [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [FiniteRange X] [FiniteRange Y] : H[⟨X, Y⟩ ; μ] ≤ H[X ; μ] + H[Y ; μ]

Subadditivity of entropy.

theorem ProbabilityTheory.mutualInfo_eq_zero {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {Y : Ω → T} [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] (hX : Measurable X) (hY : Measurable Y) {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] : I[X : Y ; μ] = 0 ↔ IndepFun X Y μ

I[X : Y] = 0 iff X, Y are independent.

theorem ProbabilityTheory.IndepFun.mutualInfo_eq_zero {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {Y : Ω → T} [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] (hX : Measurable X) (hY : Measurable Y) {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] : IndepFun X Y μ → I[X : Y ; μ] = 0

Alias of the reverse direction of ProbabilityTheory.mutualInfo_eq_zero.

---

I[X : Y] = 0 iff X, Y are independent.

theorem ProbabilityTheory.mutualInfo_const {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] (hX : Measurable X) (c : T) {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteRange X] : I[X : fun (x : Ω) => c ; μ] = 0

The mutual information with a constant is always zero.

theorem ProbabilityTheory.entropy_pair_eq_add {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {Y : Ω → T} [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] (hX : Measurable X) (hY : Measurable Y) {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] : H[⟨X, Y⟩ ; μ] = H[X ; μ] + H[Y ; μ] ↔ IndepFun X Y μ

H[X, Y] = H[X] + H[Y] if and only if X, Y are independent.

theorem ProbabilityTheory.IndepFun.entropy_pair_eq_add {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {Y : Ω → T} [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] (hX : Measurable X) (hY : Measurable Y) {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] : IndepFun X Y μ → H[⟨X, Y⟩ ; μ] = H[X ; μ] + H[Y ; μ]

If X, Y are independent, then H[X, Y] = H[X] + H[Y].

theorem ProbabilityTheory.iIndepFun.entropy_eq_add {Ω : Type u_6} {S : Type u_7} [hΩ : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {m : ℕ} [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype S] {X : Fin m → Ω → S} (hX : ∀ (i : Fin m), Measurable (X i)) (h_indep : iIndepFun X MeasureTheory.volume) : H[fun (ω : Ω) (i : Fin m) => X i ω] = ∑ i : Fin m, H[X i]

theorem ProbabilityTheory.mutualInfo_comm {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {Y : Ω → T} [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable S] [Countable T] (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : I[X : Y ; μ] = I[Y : X ; μ]

I[X : Y] = I[Y : X].

theorem ProbabilityTheory.mutualInfo_eq_entropy_sub_condEntropy {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {Y : Ω → T} [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable S] [Countable T] (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] : I[X : Y ; μ] = H[X ; μ] - H[X | Y ; μ]

I[X : Y] = H[X] - H[X|Y].

theorem ProbabilityTheory.mutualInfo_eq_entropy_sub_condEntropy' {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {Y : Ω → T} [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable S] [Countable T] (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] : I[X : Y ; μ] = H[Y ; μ] - H[Y | X ; μ]

I[X : Y] = H[Y] - H[Y | X].

theorem ProbabilityTheory.entropy_sub_mutualInfo_eq_condEntropy {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {Y : Ω → T} [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable S] [Countable T] (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] : H[X ; μ] - I[X : Y ; μ] = H[X | Y ; μ]

H[X] - I[X : Y] = H[X | Y].

theorem ProbabilityTheory.entropy_sub_mutualInfo_eq_condEntropy' {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {Y : Ω → T} [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable S] [Countable T] (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] : H[Y ; μ] - I[X : Y ; μ] = H[Y | X ; μ]

H[Y] - I[X : Y] = H[Y | X].

theorem ProbabilityTheory.IndepFun.condEntropy_eq_entropy {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {Y : Ω → T} [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable S] [Countable T] {μ : MeasureTheory.Measure Ω} (h : IndepFun X Y μ) (hX : Measurable X) (hY : Measurable Y) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] : H[X | Y ; μ] = H[X ; μ]

theorem ProbabilityTheory.condMutualInfo_eq_kernel_mutualInfo {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable S] [Countable T] [Countable U] [MeasurableSingletonClass U] [Nonempty S] [Nonempty T] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteRange Z] : I[X : Y|Z;μ] = Ik[condDistrib (⟨X, Y⟩) Z μ , MeasureTheory.Measure.map Z μ]

The conditional mutual information agrees with the information of the conditional kernel.

theorem ProbabilityTheory.condMutualInfo_eq_sum {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} {μ : MeasureTheory.Measure Ω} [MeasurableSpace T] [MeasurableSingletonClass U] [MeasureTheory.IsFiniteMeasure μ] (hZ : Measurable Z) [FiniteRange Z] : I[X : Y|Z;μ] = ∑ z ∈ FiniteRange.toFinset Z, μ.real (Z ⁻¹' {z}) * I[X : Y ; μ[|Z ⁻¹' {z}]]

theorem ProbabilityTheory.condMutualInfo_eq_sum' {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} {μ : MeasureTheory.Measure Ω} [MeasurableSpace T] [MeasurableSingletonClass U] [MeasureTheory.IsFiniteMeasure μ] (hZ : Measurable Z) [Fintype U] : I[X : Y|Z;μ] = ∑ z : U, μ.real (Z ⁻¹' {z}) * I[X : Y ; μ[|Z ⁻¹' {z}]]

A variant of condMutualInfo_eq_sum when Z has finite codomain.

theorem ProbabilityTheory.condMutualInfo_nonneg {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {X : Ω → S} {Y : Ω → T} [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] (hX : Measurable X) (hY : Measurable Y) {Z : Ω → U} {μ : MeasureTheory.Measure Ω} [FiniteRange X] [FiniteRange Y] : 0 ≤ I[X : Y|Z;μ]

Conditional information is non-nonegative.

theorem ProbabilityTheory.condMutualInfo_comm {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {X : Ω → S} {Y : Ω → T} [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable S] [Countable T] (hX : Measurable X) (hY : Measurable Y) (Z : Ω → U) (μ : MeasureTheory.Measure Ω) : I[X : Y|Z;μ] = I[Y : X|Z;μ]

I[X : Y | Z] = I[Y : X | Z].

theorem ProbabilityTheory.condMutualInfo_eq {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable S] [Countable T] [MeasurableSingletonClass U] [Countable U] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteRange Z] : I[X : Y|Z;μ] = H[X | Z ; μ] + H[Y | Z ; μ] - H[⟨X, Y⟩ | Z ; μ]

I[X : Y| Z] = H[X| Z] + H[Y| Z] - H[X, Y| Z].

theorem ProbabilityTheory.condMutualInfo_eq' {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable S] [Countable T] [MeasurableSingletonClass U] [Countable U] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] [FiniteRange Z] : I[X : Y|Z;μ] = H[X | Z ; μ] - H[X | ⟨Y, Z⟩ ; μ]

I[X : Y| Z] = H[X| Z] - H[X|Y, Z].

theorem ProbabilityTheory.condMutualInfo_of_inj_map {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} {μ : MeasureTheory.Measure Ω} [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable S] [Countable T] [MeasurableSingletonClass U] [Countable U] [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) {V : Type u_6} [MeasurableSpace V] [MeasurableSingletonClass V] [Countable V] (f : U → S → V) (hf : ∀ (t : U), Function.Injective (f t)) [FiniteRange Z] : I[fun (ω : Ω) => f (Z ω) (X ω) : Y|Z;μ] = I[X : Y|Z;μ]

If f(Z, X) is injective for each fixed Z, then I[f(Z, X) : Y| Z] = I[X : Y| Z].

theorem ProbabilityTheory.condMutualInfo_of_inj {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable S] [Countable T] [MeasurableSingletonClass U] [Countable U] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] [FiniteRange Z] {V : Type u_6} [MeasurableSpace V] [MeasurableSingletonClass V] [Countable V] {f : U → V} (hf : Function.Injective f) : I[X : Y|f ∘ Z;μ] = I[X : Y|Z;μ]

theorem ProbabilityTheory.condMutualInfo_of_inj' {S : Type u_6} {T : Type u_7} {U : Type u_8} {S' : Type u_9} {T' : Type u_10} {U' : Type u_11} {Ω : Type u_12} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSingletonClass S] [Countable S] [MeasurableSpace T] [MeasurableSingletonClass T] [Countable T] [MeasurableSpace U] [MeasurableSingletonClass U] [Countable U] [MeasurableSpace S'] [MeasurableSingletonClass S'] [Countable S'] [MeasurableSpace T'] [MeasurableSingletonClass T'] [Countable T'] [MeasurableSpace U'] [MeasurableSingletonClass U'] [Countable U'] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] [FiniteRange Z] {f : S → S'} (hf : Function.Injective f) {g : T → T'} (hg : Function.Injective g) {h : U → U'} (hh : Function.Injective h) : I[f ∘ X : g ∘ Y|h ∘ Z;μ] = I[X : Y|Z;μ]

theorem ProbabilityTheory.condEntropy_prod_eq_of_indepFun {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} {μ : MeasureTheory.Measure Ω} [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable S] [Countable T] [MeasurableSingletonClass U] [Fintype T] [Fintype U] [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) [FiniteRange X] (h : IndepFun (⟨X, Y⟩) Z μ) : H[X | ⟨Y, Z⟩ ; μ] = H[X | Y ; μ]

theorem ProbabilityTheory.condMutualInfo_eq_zero {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} {μ : MeasureTheory.Measure Ω} [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable U] [MeasurableSingletonClass U] (hX : Measurable X) (hY : Measurable Y) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] [FiniteRange Z] : I[X : Y|Z;μ] = 0 ↔ CondIndepFun X Y Z μ

I[X : Y| Z]=0 iff X, Y are conditionally independent over Z.

theorem ProbabilityTheory.ent_of_cond_indep {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} (μ : MeasureTheory.Measure Ω) [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable U] [MeasurableSingletonClass U] [Countable S] [Countable T] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (h : CondIndepFun X Y Z μ) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] [FiniteRange Z] : H[⟨X, ⟨Y, Z⟩⟩ ; μ] = H[⟨X, Z⟩ ; μ] + H[⟨Y, Z⟩ ; μ] - H[Z ; μ]

If X, Y are conditionally independent over Z, then H[X, Y, Z] = H[X, Z] + H[Y, Z] - H[Z].

theorem ProbabilityTheory.entropy_sub_condEntropy {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {Y : Ω → T} (μ : MeasureTheory.Measure Ω) [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable S] [Countable T] [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) [FiniteRange X] [FiniteRange Y] : H[X ; μ] - H[X | Y ; μ] = I[X : Y ; μ]

H[X] - H[X|Y] = I[X : Y]

theorem ProbabilityTheory.condEntropy_le_entropy {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] {X : Ω → S} {Y : Ω → T} (μ : MeasureTheory.Measure Ω) [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable S] [Countable T] [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) [FiniteRange X] [FiniteRange Y] : H[X | Y ; μ] ≤ H[X ; μ]

H[X | Y] ≤ H[X].

theorem ProbabilityTheory.entropy_submodular {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} (μ : MeasureTheory.Measure Ω) [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable U] [MeasurableSingletonClass U] [Countable S] [Countable T] [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) [FiniteRange X] [FiniteRange Y] [FiniteRange Z] : H[X | ⟨Y, Z⟩ ; μ] ≤ H[X | Z ; μ]

H[X | Y, Z] ≤ H[X | Z].

theorem ProbabilityTheory.condEntropy_comp_ge {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {X : Ω → S} {Y : Ω → T} [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable U] [MeasurableSingletonClass U] [Countable S] [Countable T] [FiniteRange X] [FiniteRange Y] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (f : S → U) : H[Y | f ∘ X ; μ] ≥ H[Y | X ; μ]

Data-processing inequality for the conditional entropy: H[Y|f(X)] ≥ H[Y|X] To upgrade this to equality, see condEntropy_of_injective'

theorem ProbabilityTheory.entropy_triple_add_entropy_le {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} (μ : MeasureTheory.Measure Ω) [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable U] [MeasurableSingletonClass U] [Countable S] [Countable T] [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) [FiniteRange X] [FiniteRange Y] [FiniteRange Z] : H[⟨X, ⟨Y, Z⟩⟩ ; μ] + H[Z ; μ] ≤ H[⟨X, Z⟩ ; μ] + H[⟨Y, Z⟩ ; μ]

The submodularity inequality: H[X, Y, Z] + H[Z] ≤ H[X, Z] + H[Y, Z].

theorem ProbabilityTheory.mutual_comp_le {Ω : Type uΩ} {S : Type uS} {T : Type uT} {U : Type uU} [mΩ : MeasurableSpace Ω] [Countable S] [Countable T] [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [MeasurableSingletonClass U] {X : Ω → S} {Y : Ω → T} [Countable U] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (f : S → U) [FiniteRange X] [FiniteRange Y] : I[f ∘ X : Y ; μ] ≤ I[X : Y ; μ]

Let X, Ybe random variables. For any function f, g on the range of X, we have I[f(X) : Y] ≤ I[X : Y].

theorem ProbabilityTheory.mutual_comp_comp_le {Ω : Type uΩ} {S : Type uS} {T : Type uT} {U : Type uU} {V : Type uV} [mΩ : MeasurableSpace Ω] [Countable S] [Countable T] [Countable V] [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSpace V] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [MeasurableSingletonClass U] [MeasurableSingletonClass V] {X : Ω → S} {Y : Ω → T} [Countable U] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (f : S → U) (g : T → V) (hg : Measurable g) [FiniteRange X] [FiniteRange Y] : I[f ∘ X : g ∘ Y ; μ] ≤ I[X : Y ; μ]

Let X, Y be random variables. For any functions f, g on the ranges of X, Y respectively, we have I[f ∘ X : g ∘ Y ; μ] ≤ I[X : Y ; μ].

theorem ProbabilityTheory.condMutual_comp_comp_le {Ω : Type uΩ} {S : Type uS} {T : Type uT} {U : Type uU} {V : Type uV} {W : Type uW} [mΩ : MeasurableSpace Ω] [Countable S] [Countable T] [Countable V] [Countable W] [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSpace V] [MeasurableSpace W] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [MeasurableSingletonClass U] [MeasurableSingletonClass V] [MeasurableSingletonClass W] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (f : S → V) (g : T → W) (hg : Measurable g) [FiniteRange X] [FiniteRange Y] [FiniteRange Z] : I[f ∘ X : g ∘ Y|Z;μ] ≤ I[X : Y|Z;μ]

Let X, Y, Z. For any functions f, g on the ranges of X, Y respectively, we have I[f ∘ X : g ∘ Y | Z ; μ] ≤ I[X : Y | Z ; μ].