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

rdist_zero_eq_half_ent

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:224 to 233

Source documentation

d[X ; 0] = H[X] / 2.

Exact Lean statement

lemma rdist_zero_eq_half_ent [IsFiniteMeasure μ] [IsProbabilityMeasure μ'] :
    d[X ; μ # fun _ ↦ 0 ; μ'] = H[X ; μ]/2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma rdist_zero_eq_half_ent [IsFiniteMeasure μ] [IsProbabilityMeasure μ'] :    d[X ; μ # fun _ ↦ 0 ; μ'] = H[X ; μ]/2 := by  have aux : H[fun x => x.1 - x.2 ; (μ.map X).prod (dirac 0)]            = H[X ; μ] := by    have h : ((μ.map X).prod (dirac 0)).map (fun x => x.1 - x.2) = Measure.map X μ := by      rw [Measure.prod_dirac, Measure.map_map (by fun_prop) (by fun_prop)]      simp [Function.comp_def]    simp [entropy_def, h]  simp [rdist_def, entropy_const (0 : G), aux]  ring