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

diff_ent_le_rdist

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:258 to 268

Source documentation

|H[X] - H[Y]| ≤ 2 d[X ; Y].

Exact Lean statement

lemma diff_ent_le_rdist [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']
    (hX : Measurable X) (hY : Measurable Y) :
    |H[X ; μ] - H[Y ; μ']| ≤ 2 * d[X ; μ # Y ; μ']

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma diff_ent_le_rdist [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']    (hX : Measurable X) (hY : Measurable Y) :    |H[X ; μ] - H[Y ; μ']| ≤ 2 * d[X ; μ # Y ; μ'] := by  obtain ⟨ν, X', Y', _, hX', hY', hind, hIdX, hIdY, _, _⟩ :=    independent_copies_finiteRange hX hY μ μ'  rw [← hIdX.rdist_congr hIdY, hind.rdist_eq hX' hY', ← hIdX.entropy_congr, ← hIdY.entropy_congr,    abs_le]  have := max_entropy_le_entropy_sub hX' hY' hind  constructor  · linarith[le_max_right H[X'; ν] H[Y'; ν]]  · linarith[le_max_left H[X'; ν] H[Y'; ν]]