Entropy #
This file imports the entropy definitions and basic API from PFR.ForMathlib.Entropy.Basic.
The main definitions live in the ProbabilityTheory namespace:
It also provides notations such as H[X], H[X ; μ], H[X | Y], and I[X : Y].
theorem
ProbabilityTheory.entropy_le_log_of_card_le
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
[Fintype S]
[Nonempty S]
[MeasurableSingletonClass S]
(X : Ω → S)
(μ : MeasureTheory.Measure Ω)
{N : ℕ}
(hcard : Fintype.card S ≤ N)
:
Entropy is bounded by the logarithm of any natural-number upper bound on the alphabet size.
theorem
ProbabilityTheory.entropy_le_nat_mul_log_two_of_card_le_two_pow
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
[Fintype S]
[Nonempty S]
[MeasurableSingletonClass S]
(X : Ω → S)
(μ : MeasureTheory.Measure Ω)
{c : ℕ}
(hcard : Fintype.card S ≤ 2 ^ c)
:
Entropy is bounded by c * log 2 when the alphabet has size at most 2 ^ c.
theorem
ProbabilityTheory.mutualInfo_le_entropy_left
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
[MeasurableSpace T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[Countable S]
[Countable T]
{X : Ω → S}
{Y : Ω → T}
{μ : MeasureTheory.Measure Ω}
(hX : Measurable X)
(hY : Measurable Y)
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
:
Mutual information is bounded by the entropy of the left variable.
theorem
ProbabilityTheory.mutualInfo_le_entropy_right
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
[MeasurableSpace T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[Countable S]
[Countable T]
{X : Ω → S}
{Y : Ω → T}
{μ : MeasureTheory.Measure Ω}
(hX : Measurable X)
(hY : Measurable Y)
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
:
Mutual information is bounded by the entropy of the right variable.
theorem
ProbabilityTheory.mutualInfo_congr_ae
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
[MeasurableSpace T]
{X : Ω → S}
{Y : Ω → T}
{μ : MeasureTheory.Measure Ω}
{X' : Ω → S}
{Y' : Ω → T}
(hX : Measurable X)
(hY : Measurable Y)
(hXae : X =ᵐ[μ] X')
(hYae : Y =ᵐ[μ] Y')
:
theorem
ProbabilityTheory.mutualInfo_comp_right_of_injective
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
[MeasurableSpace T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[Countable S]
[Countable T]
{X : Ω → S}
{Y : Ω → T}
{μ : MeasureTheory.Measure Ω}
{V : Type u_5}
[MeasurableSpace V]
[MeasurableSingletonClass V]
[Countable V]
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
(hX : Measurable X)
(hY : Measurable Y)
(f : T → V)
(hf : Measurable f)
(hfinj : Function.Injective f)
:
Mutual information is unchanged by an injective recoding of the right variable.
theorem
ProbabilityTheory.mutualInfo_eq_zero_of_ae_eq_const_left
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
[MeasurableSpace T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
{X : Ω → S}
{Y : Ω → T}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
(hX : Measurable X)
(hY : Measurable Y)
(c : S)
(hconst : X =ᵐ[μ] fun (x : Ω) => c)
:
If the left variable is almost surely constant, its mutual information with any finite variable is zero.
theorem
ProbabilityTheory.mutualInfo_eq_zero_of_ae_eq_const_right
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
[MeasurableSpace T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[Countable S]
[Countable T]
{X : Ω → S}
{Y : Ω → T}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
(hX : Measurable X)
(hY : Measurable Y)
(c : T)
(hconst : Y =ᵐ[μ] fun (x : Ω) => c)
:
If the right variable is almost surely constant, its mutual information with any finite variable is zero.
theorem
ProbabilityTheory.condMutualInfo_eq_zero_of_ae_eq_const_left
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[MeasurableSingletonClass U]
[Countable U]
{X : Ω → S}
{Y : Ω → T}
{Z : Ω → U}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
[FiniteRange Z]
(hX : Measurable X)
(hY : Measurable Y)
(c : S)
(hconst : X =ᵐ[μ] fun (x : Ω) => c)
:
If the left variable is almost surely constant, its conditional mutual information with any finite variable is zero.
theorem
ProbabilityTheory.condMutualInfo_eq_zero_of_ae_eq_const_right
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[MeasurableSingletonClass U]
[Countable S]
[Countable T]
[Countable U]
{X : Ω → S}
{Y : Ω → T}
{Z : Ω → U}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
[FiniteRange Z]
(hX : Measurable X)
(hY : Measurable Y)
(c : T)
(hconst : Y =ᵐ[μ] fun (x : Ω) => c)
:
If the right variable is almost surely constant, its conditional mutual information with any finite variable is zero.
theorem
ProbabilityTheory.indepFun_of_measureReal_inter_preimage_singleton_eq_mul
{Ω : Type u_5}
{S : Type u_6}
{T : Type u_7}
[MeasurableSpace Ω]
[MeasurableSpace S]
[MeasurableSpace T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[Finite S]
[Finite T]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure μ]
(X : Ω → S)
(Y : Ω → T)
(hX : Measurable X)
(hY : Measurable Y)
(h : ∀ (x : S) (y : T), μ.real (X ⁻¹' {x} ∩ Y ⁻¹' {y}) = μ.real (X ⁻¹' {x}) * μ.real (Y ⁻¹' {y}))
:
IndepFun X Y μ
For finite alphabets, independence of two random variables follows from factorization on singleton fibers.
theorem
ProbabilityTheory.condMutualInfo_le_condEntropy_left
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[MeasurableSingletonClass U]
[Countable S]
[Countable T]
[Countable U]
{X : Ω → S}
{Y : Ω → T}
{Z : Ω → U}
{μ : MeasureTheory.Measure Ω}
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
[FiniteRange Z]
:
Conditional mutual information is bounded by the left conditional entropy.
theorem
ProbabilityTheory.condMutualInfo_le_condEntropy_right
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[MeasurableSingletonClass U]
[Countable S]
[Countable T]
[Countable U]
{X : Ω → S}
{Y : Ω → T}
{Z : Ω → U}
{μ : MeasureTheory.Measure Ω}
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
[FiniteRange Z]
:
Conditional mutual information is bounded by the right conditional entropy.
theorem
ProbabilityTheory.condMutualInfo_le_entropy_left
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[MeasurableSingletonClass U]
[Countable S]
[Countable T]
[Countable U]
{X : Ω → S}
{Y : Ω → T}
{Z : Ω → U}
{μ : MeasureTheory.Measure Ω}
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
[FiniteRange Z]
:
Conditional mutual information is bounded by the entropy of the left variable.
theorem
ProbabilityTheory.condMutualInfo_le_entropy_right
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[MeasurableSingletonClass U]
[Countable S]
[Countable T]
[Countable U]
{X : Ω → S}
{Y : Ω → T}
{Z : Ω → U}
{μ : MeasureTheory.Measure Ω}
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
[FiniteRange Z]
:
Conditional mutual information is bounded by the entropy of the right variable.
theorem
ProbabilityTheory.condMutualInfo_comp_left_le_of_comp_conditioning
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[MeasurableSingletonClass U]
[Countable S]
[Countable T]
[Countable U]
{X : Ω → S}
{Y : Ω → T}
{Z : Ω → U}
{μ : MeasureTheory.Measure Ω}
{V : Type u_5}
[MeasurableSpace V]
[MeasurableSingletonClass V]
[Countable V]
[MeasureTheory.IsProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
[FiniteRange Z]
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
(f : U → S → V)
:
Conditional data processing where the left-side postprocessing may depend on the conditioning value.
theorem
ProbabilityTheory.condMutualInfo_comp_right_le_of_comp_conditioning
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[MeasurableSingletonClass U]
[Countable S]
[Countable T]
[Countable U]
{X : Ω → S}
{Y : Ω → T}
{Z : Ω → U}
{μ : MeasureTheory.Measure Ω}
{V : Type u_5}
[MeasurableSpace V]
[MeasurableSingletonClass V]
[Countable V]
[MeasureTheory.IsProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
[FiniteRange Z]
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
(f : U → T → V)
(hf : Measurable (Function.uncurry f))
:
Conditional data processing where the right-side postprocessing may depend on the conditioning value.
theorem
ProbabilityTheory.condMutualInfo_conditioning_prod_function_eq
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[MeasurableSingletonClass U]
[Countable S]
[Countable T]
[Countable U]
{X : Ω → S}
{Y : Ω → T}
{Z : Ω → U}
{μ : MeasureTheory.Measure Ω}
{V : Type u_5}
[MeasurableSpace V]
[MeasurableSingletonClass V]
[Countable V]
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
[FiniteRange Z]
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
(f : U → V)
:
Adding a deterministic function of the conditioning variable to the conditioning variable does not change conditional mutual information.
theorem
ProbabilityTheory.condMutualInfo_conditioning_prod_left_function_le
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[MeasurableSingletonClass U]
[Countable S]
[Countable T]
[Countable U]
{X : Ω → S}
{Y : Ω → T}
{Z : Ω → U}
{μ : MeasureTheory.Measure Ω}
{V : Type u_5}
[MeasurableSpace V]
[MeasurableSingletonClass V]
[Countable V]
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
[FiniteRange Z]
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
(f : U → S → V)
(hf : Measurable (Function.uncurry f))
:
Conditioning additionally on a deterministic function of the left variable and the existing conditioning data cannot increase conditional mutual information.
theorem
ProbabilityTheory.condMutualInfo_conditioning_prod_right_function_le
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[MeasurableSingletonClass U]
[Countable S]
[Countable T]
[Countable U]
{X : Ω → S}
{Y : Ω → T}
{Z : Ω → U}
{μ : MeasureTheory.Measure Ω}
{V : Type u_5}
[MeasurableSpace V]
[MeasurableSingletonClass V]
[Countable V]
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
[FiniteRange Z]
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
(f : U → T → V)
(hf : Measurable (Function.uncurry f))
:
Conditioning additionally on a deterministic function of the right variable and the existing conditioning data cannot increase conditional mutual information.
theorem
ProbabilityTheory.condMutualInfo_comp_conditioning_le_of_condMutualInfo_eq_zero
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[MeasurableSingletonClass U]
[Countable S]
[Countable T]
[Countable U]
{X : Ω → S}
{Y : Ω → T}
{μ : MeasureTheory.Measure Ω}
{V : Type u_5}
[MeasurableSpace V]
[MeasurableSingletonClass V]
[Countable V]
{W : Ω → V}
(f : V → U)
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
[FiniteRange W]
(hX : Measurable X)
(hY : Measurable Y)
(hW : Measurable W)
(hf : Measurable f)
(hzero : I[X : W|f ∘ W;μ] = 0)
:
If a coarse conditioning variable is a deterministic function of a finer one, and the finer
conditioning variable carries no conditional information about X beyond the coarse variable,
then the finer conditioning can only increase I[X : Y | -].
theorem
ProbabilityTheory.condMutualInfo_prod_left_eq_add
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[MeasurableSingletonClass U]
[Countable S]
[Countable T]
[Countable U]
{X : Ω → S}
{Y : Ω → T}
{Z : Ω → U}
{μ : MeasureTheory.Measure Ω}
{V : Type u_5}
[MeasurableSpace V]
[MeasurableSingletonClass V]
[Countable V]
{W : Ω → V}
(hX : Measurable X)
(hW : Measurable W)
(hY : Measurable Y)
(hZ : Measurable Z)
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange W]
[FiniteRange Y]
[FiniteRange Z]
:
Chain rule for conditional mutual information, splitting a pair on the left.
theorem
ProbabilityTheory.condMutualInfo_prod_right_eq_add
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[MeasurableSingletonClass U]
[Countable S]
[Countable T]
[Countable U]
{X : Ω → S}
{Y : Ω → T}
{Z : Ω → U}
{μ : MeasureTheory.Measure Ω}
{V : Type u_5}
[MeasurableSpace V]
[MeasurableSingletonClass V]
[Countable V]
{W : Ω → V}
(hX : Measurable X)
(hY : Measurable Y)
(hW : Measurable W)
(hZ : Measurable Z)
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
[FiniteRange W]
[FiniteRange Z]
:
Chain rule for conditional mutual information, splitting a pair on the right.
theorem
ProbabilityTheory.condMutualInfo_le_prod_right_snd
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[MeasurableSingletonClass U]
[Countable S]
[Countable T]
{X : Ω → S}
{Y : Ω → T}
{Z : Ω → U}
{μ : MeasureTheory.Measure Ω}
{V : Type u_5}
[MeasurableSpace V]
[MeasurableSingletonClass V]
[Countable V]
{W : Ω → V}
(hX : Measurable X)
(hY : Measurable Y)
(hW : Measurable W)
(hZ : Measurable Z)
[MeasureTheory.IsProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
[FiniteRange W]
[FiniteRange Z]
:
Adding an extra right-side variable cannot decrease conditional mutual information.
theorem
ProbabilityTheory.condMutualInfo_boolVector_eq_sum_strictPrefix
{Ω : Type u_6}
{T : Type u_7}
{U : Type u_8}
[MeasurableSpace Ω]
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass T]
[MeasurableSingletonClass U]
[Countable T]
[Countable U]
{m : ℕ}
{Y : Ω → T}
{Z : Ω → U}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[FiniteRange Y]
[FiniteRange Z]
(X : Ω → Fin m → Bool)
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
:
Chain rule for conditional mutual information against a finite boolean vector, exposing coordinates from left to right.
theorem
ProbabilityTheory.cond_cond_eq_cond_of_subset
{Ω₀ : Type u_6}
[MeasurableSpace Ω₀]
(μ : MeasureTheory.Measure Ω₀)
[MeasureTheory.IsFiniteMeasure μ]
{A F : Set Ω₀}
(hA : MeasurableSet A)
(hF : MeasurableSet F)
(hFA : F ⊆ A)
:
Conditioning on a larger event and then on a smaller event is the same as conditioning directly on the smaller event.
theorem
ProbabilityTheory.measureReal_mul_cond_real_eq_measureReal_of_subset
{Ω₀ : Type u_6}
[MeasurableSpace Ω₀]
(μ : MeasureTheory.Measure Ω₀)
[MeasureTheory.IsFiniteMeasure μ]
{A F : Set Ω₀}
(hA : MeasurableSet A)
(hFA : F ⊆ A)
:
Real masses obey the same reweighting identity for nested conditioning events.
theorem
ProbabilityTheory.condMutualInfo_prod_conditioning_eq_sum
{Ω₀ : Type u_6}
{S₀ : Type u_7}
{T₀ : Type u_8}
{A : Type u_9}
{U₀ : Type u_10}
[MeasurableSpace Ω₀]
[MeasurableSpace S₀]
[MeasurableSpace T₀]
[MeasurableSpace A]
[MeasurableSpace U₀]
[MeasurableSingletonClass S₀]
[MeasurableSingletonClass T₀]
[MeasurableSingletonClass A]
[MeasurableSingletonClass U₀]
[Countable S₀]
[Countable T₀]
[Fintype A]
[Finite U₀]
{X : Ω₀ → S₀}
{Y : Ω₀ → T₀}
{K : Ω₀ → A}
{Z : Ω₀ → U₀}
{μ : MeasureTheory.Measure Ω₀}
[MeasureTheory.IsFiniteMeasure μ]
(hK : Measurable K)
(hZ : Measurable Z)
[FiniteRange X]
[FiniteRange Y]
:
If the conditioning variable is a pair (K, Z), conditional mutual information is the
average over the fibers of K of the conditional mutual information given Z.
theorem
ProbabilityTheory.measureReal_mul_cond_condMutualInfo_le_condMutualInfo_of_event_eq_preimage
{Ω₀ : Type u_6}
{S₀ : Type u_7}
{T₀ : Type u_8}
{U₀ : Type u_9}
[MeasurableSpace Ω₀]
[MeasurableSpace S₀]
[MeasurableSpace T₀]
[MeasurableSpace U₀]
[MeasurableSingletonClass S₀]
[MeasurableSingletonClass T₀]
[MeasurableSingletonClass U₀]
[Countable S₀]
[Countable T₀]
[Countable U₀]
(μ : MeasureTheory.Measure Ω₀)
[MeasureTheory.IsProbabilityMeasure μ]
(X : Ω₀ → S₀)
(Y : Ω₀ → T₀)
(Z : Ω₀ → U₀)
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
[FiniteRange X]
[FiniteRange Y]
[FiniteRange Z]
{A : Set Ω₀}
{B : Set U₀}
(hB : MeasurableSet B)
(hA : A = Z ⁻¹' B)
:
If an event is determined by the conditioning variable, then the contribution of the conditional mutual information on that event is bounded by the original conditional mutual information. This is the information-theoretic reweighting used in Claim 6.21.
theorem
ProbabilityTheory.mutualInfo_prod_right_eq_add
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
[MeasurableSpace T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[Countable S]
[Countable T]
{X : Ω → S}
{Y : Ω → T}
{μ : MeasureTheory.Measure Ω}
{V : Type u_5}
[MeasurableSpace V]
[MeasurableSingletonClass V]
[Countable V]
{W : Ω → V}
(hX : Measurable X)
(hY : Measurable Y)
(hW : Measurable W)
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
[FiniteRange W]
:
Chain rule for mutual information, splitting a pair on the right.
theorem
ProbabilityTheory.condMutualInfo_le_mutualInfo_of_condDependence_le
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
[MeasurableSpace T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[Countable S]
[Countable T]
{X : Ω → S}
{Y : Ω → T}
{μ : MeasureTheory.Measure Ω}
{V : Type u_5}
[MeasurableSpace V]
[MeasurableSingletonClass V]
[Countable V]
{W : Ω → V}
(hX : Measurable X)
(hY : Measurable Y)
(hW : Measurable W)
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
[FiniteRange W]
(hdep : I[X : W|Y;μ] ≤ I[X : W ; μ])
:
Chain-rule rearrangement: if conditioning on Y does not increase the dependence between
X and W, then conditioning on W cannot increase the information that Y has about X
beyond the unconditioned I[X : Y].
theorem
ProbabilityTheory.condEntropy_congr_ae
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
[MeasurableSpace T]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[Countable S]
[Countable T]
{X : Ω → S}
{Y : Ω → T}
{μ : MeasureTheory.Measure Ω}
{X' : Ω → S}
{Y' : Ω → T}
[MeasureTheory.IsProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
[FiniteRange X']
[FiniteRange Y']
(hX : Measurable X)
(hY : Measurable Y)
(hX' : Measurable X')
(hY' : Measurable Y')
(hXae : X =ᵐ[μ] X')
(hYae : Y =ᵐ[μ] Y')
:
Conditional entropy is unchanged when both variables are replaced by almost-everywhere equal variables.
theorem
ProbabilityTheory.condMutualInfo_congr_ae_left_right
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[MeasurableSingletonClass U]
[Countable S]
[Countable T]
[Countable U]
{X : Ω → S}
{Y : Ω → T}
{Z : Ω → U}
{μ : MeasureTheory.Measure Ω}
{X' : Ω → S}
{Y' : Ω → T}
[MeasureTheory.IsProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
[FiniteRange X']
[FiniteRange Y']
[FiniteRange Z]
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
(hX' : Measurable X')
(hY' : Measurable Y')
(hXae : X =ᵐ[μ] X')
(hYae : Y =ᵐ[μ] Y')
:
Conditional mutual information is unchanged when the two measured variables are replaced by almost-everywhere equal variables and the conditioning variable is unchanged.
theorem
ProbabilityTheory.condMutualInfo_congr_ae
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[MeasurableSingletonClass U]
[Countable S]
[Countable T]
[Countable U]
{X : Ω → S}
{Y : Ω → T}
{Z : Ω → U}
{μ : MeasureTheory.Measure Ω}
{X' : Ω → S}
{Y' : Ω → T}
{Z' : Ω → U}
[MeasureTheory.IsProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
[FiniteRange Z]
[FiniteRange X']
[FiniteRange Y']
[FiniteRange Z']
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
(hX' : Measurable X')
(hY' : Measurable Y')
(hZ' : Measurable Z')
(hXae : X =ᵐ[μ] X')
(hYae : Y =ᵐ[μ] Y')
(hZae : Z =ᵐ[μ] Z')
:
Conditional mutual information is unchanged when all three variables are replaced by almost-everywhere equal variables.
theorem
ProbabilityTheory.IdentDistrib.condMutualInfo_eq
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[MeasurableSingletonClass U]
[Countable S]
[Countable T]
[Countable U]
{X : Ω → S}
{Y : Ω → T}
{Z : Ω → U}
{μ : MeasureTheory.Measure Ω}
{Ω' : Type u_6}
[MeasurableSpace Ω']
{μ' : MeasureTheory.Measure Ω'}
{X' : Ω' → S}
{Y' : Ω' → T}
{Z' : Ω' → U}
[MeasureTheory.IsProbabilityMeasure μ]
[MeasureTheory.IsProbabilityMeasure μ']
[FiniteRange X]
[FiniteRange Y]
[FiniteRange Z]
[FiniteRange X']
[FiniteRange Y']
[FiniteRange Z']
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
(hX' : Measurable X')
(hY' : Measurable Y')
(hZ' : Measurable Z')
(h : IdentDistrib (fun (ω : Ω) => (X ω, Y ω, Z ω)) (fun (ω : Ω') => (X' ω, Y' ω, Z' ω)) μ μ')
:
Conditional mutual information is determined by the joint law of (X, Y, Z).
theorem
ProbabilityTheory.condMutualInfo_comp_right_conditioning_of_injective
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace S]
{T : Type u_3}
{U : Type u_4}
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSingletonClass S]
[MeasurableSingletonClass T]
[MeasurableSingletonClass U]
[Countable S]
[Countable T]
[Countable U]
{X : Ω → S}
{Y : Ω → T}
{Z : Ω → U}
{μ : MeasureTheory.Measure Ω}
{V : Type u_6}
{W : Type u_7}
[MeasurableSpace V]
[MeasurableSpace W]
[MeasurableSingletonClass V]
[MeasurableSingletonClass W]
[Countable V]
[Countable W]
{f : T → V}
{g : U → W}
[MeasureTheory.IsProbabilityMeasure μ]
[FiniteRange X]
[FiniteRange Y]
[FiniteRange Z]
(hX : Measurable X)
(hY : Measurable Y)
(hZ : Measurable Z)
(hfmeas : Measurable f)
(hgmeas : Measurable g)
(hfinj : Function.Injective f)
(hginj : Function.Injective g)
:
Conditional mutual information is unchanged by injective recodings of the right variable and the conditioning variable.
theorem
ProbabilityTheory.IdentDistrib.cond_of_pair
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{A : Type u_6}
{B : Type u_7}
[MeasurableSpace A]
[MeasurableSpace B]
{Ω' : Type u_8}
[MeasurableSpace Ω']
{μ' : MeasureTheory.Measure Ω'}
{X : Ω → A}
{Y : Ω → B}
{X' : Ω' → A}
{Y' : Ω' → B}
{s : Set B}
(hs : MeasurableSet s)
(hY : Measurable Y)
(hY' : Measurable Y')
(h : IdentDistrib (fun (ω : Ω) => (X ω, Y ω)) (fun (ω : Ω') => (X' ω, Y' ω)) μ μ')
:
If (X, Y) and (X', Y') have the same joint law, then conditioning on the same measurable
event in the Y/Y' coordinate preserves the law of X/X'. This is the heterogeneous-codomain
version of ProbabilityTheory.IdentDistrib.cond.