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

ent_of_sub_smul'

PFR.MoreRuzsaDist · PFR/MoreRuzsaDist.lean:720 to 758

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_of_sub_smul' {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_of_sub_smul' {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 [sub_smul, one_smul, sub_eq_add_neg, neg_sub, add_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 hident'' : IdentDistrib (-(X + Y - X')) (X - Y - X') μ μ := by    simp_rw [neg_sub, ← sub_sub, sub_eq_add_neg, add_assoc]    refine hident.symm.add ?_ ?_ ?_    rotate_left    · rw [← neg_add]      apply IndepFun.comp _ measurable_id measurable_neg      refine h_indep.indepFun_add_right (fun i ↦ (by fin_cases i <;> assumption))        2 0 1 (by simp) (by simp)    · rw [← neg_add]      apply IndepFun.comp _ measurable_id measurable_neg      refine h_indep.indepFun_add_right (fun i ↦ (by fin_cases i <;> assumption))        0 1 2 (by simp) (by simp)    rw [add_comm, ← neg_add, ← neg_add]    exact (IdentDistrib.refl hY.aemeasurable).add hident iXY.symm iX'Y.symm |>.neg  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.add hY) (hY.const_smul a) hX' ?_      exact iXY_X'.comp (φ := fun (x, y) ↦ (x + y, a • y)) .of_discrete measurable_id    _ = H[- (X + Y - X') ; μ] + H[X - a • Y ; μ] - H[X ; μ] := by      rw [hident.entropy_congr]      simp only [hident'.entropy_congr, add_comm, sub_left_inj, _root_.add_right_inj]      exact entropy_neg (hX.add hY |>.sub hX') |>.symm    _ = _ := by      rw [add_comm, hident''.entropy_congr]