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

ent_sub_zsmul_le

PFR.MoreRuzsaDist · PFR/MoreRuzsaDist.lean:686 to 708

Source documentation

Let X,Y,X' be independent G-valued random variables, with X' a copy of X, and let a be an integer. Then H[X - (a+1)Y] ≤ H[X - aY] + H[X - Y - X'] - H[X]

Exact Lean statement

lemma ent_sub_zsmul_le {Y : Ω → G} {X' : Ω → G} [FiniteRange X] [FiniteRange Y] [FiniteRange X']
    [IsProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (hX' : Measurable X')
    (h_indep : iIndepFun ![X, Y, X'] μ) (hident : IdentDistrib X X' μ μ) {a : ℤ} :
    H[X - (a+1) • Y; μ] ≤ H[X - a • Y; μ] + H[X - Y - X'; μ] - H[X; μ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ent_sub_zsmul_le {Y : Ω → G} {X' : Ω → G} [FiniteRange X] [FiniteRange Y] [FiniteRange X']    [IsProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (hX' : Measurable X')    (h_indep : iIndepFun ![X, Y, X'] μ) (hident : IdentDistrib X X' μ μ) {a : ℤ} :    H[X - (a+1) • Y; μ] ≤ H[X - a • Y; μ] + H[X - Y - X'; μ] - H[X; μ] := by  rw [add_smul, one_smul, add_comm, sub_add_eq_sub_sub]  have iX'Y : IndepFun X' Y μ := h_indep.indepFun (show 2 ≠ 1 by simp)  have iXY : IndepFun X Y μ := h_indep.indepFun (show 0 ≠ 1 by simp)  have hident' : IdentDistrib (X' - a • Y) (X - a • Y) μ μ := by    simp_rw [sub_eq_add_neg]    apply hident.symm.add (.refl (hY.const_smul a).neg.aemeasurable)    · exact iX'Y.comp measurable_id (.of_discrete (f := fun y ↦ -(a • y)))    · exact iXY.comp measurable_id (.of_discrete (f := fun y ↦ -(a • y)))  have iXY_X' : IndepFun (⟨X, Y⟩) X' μ :=    h_indep.indepFun_prodMk (fun i ↦ (by fin_cases i <;> assumption)) 0 1 2      (show 0 ≠ 2 by simp) (show 1 ≠ 2 by simp)  calc    _ ≤ H[X - Y - X' ; μ] + H[X' - a • Y ; μ] - H[X' ; μ] := by      refine ent_of_diff_le _ _ _ (hX.sub hY) (hY.const_smul a) hX' ?_      exact iXY_X'.comp (φ := fun (x, y) ↦ (x - y, a • y)) .of_discrete measurable_id    _ = _ := by      rw [hident.entropy_congr]      simp only [add_comm, sub_left_inj, _root_.add_left_inj]      exact hident'.entropy_congr