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

rdist_add_const

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:375 to 393

Source documentation

Adding a constant to a random variable does not change the Rusza distance.

Exact Lean statement

lemma rdist_add_const [IsZeroOrProbabilityMeasure μ] [IsZeroOrProbabilityMeasure μ']
    (hX : Measurable X) (hY : Measurable Y) {c} :
    d[X ; μ # Y + fun _ ↦ c; μ'] = d[X ; μ # Y ; μ']

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma rdist_add_const [IsZeroOrProbabilityMeasure μ] [IsZeroOrProbabilityMeasure μ']    (hX : Measurable X) (hY : Measurable Y) {c} :    d[X ; μ # Y + fun _ ↦ c; μ'] = d[X ; μ # Y ; μ'] := by  rcases eq_zero_or_isProbabilityMeasure μ with rfl | hμ  · simp [rdist_def, entropy_add_const hY]  rcases eq_zero_or_isProbabilityMeasure μ' with rfl | hμ'  · simp [rdist_def]  obtain ⟨ν, X', Y', _, hX', hY', hind, hIdX, hIdY, -⟩ := independent_copies_finiteRange hX hY μ μ'  have A : IdentDistrib (Y' + fun _ ↦ c) (Y + fun _ ↦ c) ν μ' := by    change IdentDistrib (fun ω ↦ Y' ω + c) (fun ω ↦ Y ω + c) ν μ'    apply hIdY.comp (measurable_add_const c)  have B : IndepFun X' (Y' + fun _ ↦ c) ν := by    change IndepFun X' (fun ω ↦ Y' ω + c) ν    apply hind.comp measurable_id (measurable_add_const c)  have C : X' - (Y' + fun _ ↦ c) = (X' - Y') + (fun _ ↦ -c) := by    ext ω; simp; abel  rw [← hIdX.rdist_congr hIdY, ← hIdX.rdist_congr A, hind.rdist_eq hX' hY',    B.rdist_eq hX' (hY'.add_const _), entropy_add_const hY' c, C, entropy_add_const]  exact hX'.sub hY'