Source indexedlemma · leanprover/lean4:v4.33.0-rc1

ProbabilityTheory.condMutualInfo_of_inj

PFR.ForMathlib.Entropy.Basic · PFR/ForMathlib/Entropy/Basic.lean:975 to 984

Mathematical statement

Exact Lean statement

lemma condMutualInfo_of_inj [Countable U]
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] [FiniteRange Z]
    {V : Type*} [MeasurableSpace V] [MeasurableSingletonClass V] [Countable V]
    {f : U → V} (hf : Function.Injective f) :
    I[X : Y | f ∘ Z; μ] = I[X : Y | Z; μ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma condMutualInfo_of_inj [Countable U]    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)    (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] [FiniteRange Z]    {V : Type*} [MeasurableSpace V] [MeasurableSingletonClass V] [Countable V]    {f : U → V} (hf : Function.Injective f) :    I[X : Y | f ∘ Z; μ] = I[X : Y | Z; μ] := by  have hfZ : Measurable (f ∘ Z) := by fun_prop  rw [condMutualInfo_eq hX hY hZ, condMutualInfo_eq hX hY hfZ,    condEntropy_of_injective' _ hX hZ _ hf hfZ, condEntropy_of_injective' _ hY hZ _ hf hfZ,    condEntropy_of_injective' _ (hX.prodMk hY) hZ _ hf hfZ]