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

ProbabilityTheory.condEntropy_of_injective

PFR.ForMathlib.Entropy.Basic · PFR/ForMathlib/Entropy/Basic.lean:506 to 523

Source documentation

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].

Exact Lean statement

lemma condEntropy_of_injective
    [MeasurableSingletonClass U] (μ : Measure Ω) [IsFiniteMeasure μ] (hX : Measurable X)
    (hY : Measurable Y) (f : T → S → U) (hf : ∀ t, Injective (f t)) [FiniteRange Y] :
    H[(fun ω ↦ f (Y ω) (X ω)) | Y ; μ] = H[X | Y ; μ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma condEntropy_of_injective    [MeasurableSingletonClass U] (μ : Measure Ω) [IsFiniteMeasure μ] (hX : Measurable X)    (hY : Measurable Y) (f : T → S → U) (hf : ∀ t, Injective (f t)) [FiniteRange Y] :    H[(fun ω ↦ f (Y ω) (X ω)) | Y ; μ] = H[X | Y ; μ] := by  rw [condEntropy_eq_sum _ _ _ hY, condEntropy_eq_sum _ _ _ hY]  have : ∀ y, H[fun ω ↦ f (Y ω) (X ω)|Y← y; μ] = H[(f y ∘ X) | Y ← y ; μ] := by    intro y    refine entropy_congr ?_    have : ∀ᵐ ω ∂μ[|Y ← y], Y ω = y := by      rw [ae_iff, cond_apply (hY (.singleton _))]      have : {a | ¬Y a = y} = (Y ⁻¹' {y})ᶜ := by ext; simp      rw [this, Set.inter_compl_self, measure_empty, mul_zero]    filter_upwards [this] with ω hω    rw [hω]    simp  simp_rw [this]  congr with y  rw [entropy_comp_of_injective _ hX (f y) (hf y)]