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

multiDist_nonneg_of_indep

PFR.MoreRuzsaDist · PFR/MoreRuzsaDist.lean:936 to 954

Mathematical statement

Exact Lean statement

lemma multiDist_nonneg_of_indep [Finite G] {m : ℕ} {Ω : Type*} (hΩ : MeasureSpace Ω)
    [IsProbabilityMeasure hΩ.volume] (X : Fin m → Ω → G) (hX : ∀ i, Measurable (X i))
    (h_indep : iIndepFun X ℙ) :
    0 ≤ D[X ; fun _ ↦ hΩ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma multiDist_nonneg_of_indep [Finite G] {m : ℕ} {Ω : Type*} (hΩ : MeasureSpace Ω)    [IsProbabilityMeasure hΩ.volume] (X : Fin m → Ω → G) (hX : ∀ i, Measurable (X i))    (h_indep : iIndepFun X ℙ) :    0 ≤ D[X ; fun _ ↦ hΩ] := by  rw [multiDist_indep hΩ hX h_indep]  have : IsProbabilityMeasure (ℙ : Measure Ω) := h_indep.isProbabilityMeasure  by_cases hm : m = 0  · subst hm    simp only [Finset.univ_eq_empty, Finset.sum_empty, CharP.cast_eq_zero, div_zero, sub_zero,      ge_iff_le]    erw [entropy_const]  norm_num  calc    (∑ i, H[X i]) / m ≤ (∑ i : Fin m, H[∑ i, X i]) / m:= by      gcongr with i      convert max_entropy_le_entropy_sum (Finset.mem_univ i) hX h_indep    _ = H[∑ i, X i] := by      simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]      field_simp