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

ProbabilityTheory.entropy_submodular

PFR.ForMathlib.Entropy.Basic · PFR/ForMathlib/Entropy/Basic.lean:1080 to 1091

Source documentation

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

Exact Lean statement

lemma entropy_submodular (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    [FiniteRange X] [FiniteRange Y] [FiniteRange Z] :
    H[X | ⟨Y, Z⟩ ; μ] ≤ H[X | Z ; μ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma entropy_submodular (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)    [FiniteRange X] [FiniteRange Y] [FiniteRange Z] :    H[X | ⟨Y, Z⟩ ; μ] ≤ H[X | Z ; μ] := by  rcases eq_zero_or_isProbabilityMeasure μ with rfl | hμ  · simp  have : Nonempty S := Nonempty.map X (μ.nonempty_of_neZero)  have : Nonempty T := Nonempty.map Y (μ.nonempty_of_neZero)  rw [condEntropy_eq_kernel_entropy hX hZ, condEntropy_two_eq_kernel_entropy hX hY hZ]  refine (Kernel.entropy_condKernel_le_entropy_snd ?_).trans_eq ?_  · apply Kernel.aefiniteKernelSupport_condDistrib    all_goals fun_prop  exact Kernel.entropy_congr (condDistrib_snd_ae_eq hY hX hZ _)