ProbabilityTheory.max_entropy_le_entropy_prod

@[to_additive /-- If `X₁, ..., Xₙ` are independent and `s ⊆ {1, ..., n}`, then for all `i ∈ s`,`H[Xᵢ] ≤ H[∑ j ∈ s, Xⱼ]`. -/]lemma max_entropy_le_entropy_prod {G : Type*} [Countable G] [hG : MeasurableSpace G]    [MeasurableSingletonClass G] [CommGroup G] [MeasurableMul₂ G]    {I : Type*} {s : Finset I} {i₀ : I} (hi₀ : i₀ ∈ s) {X : I → Ω → G} [∀ i, FiniteRange (X i)]    (hX : (i : I) → Measurable (X i)) (h_indep : iIndepFun X μ) :    H[X i₀ ; μ] ≤ H[∏ i ∈ s, X i ; μ] := by  have hs : s.Nonempty := ⟨i₀, hi₀⟩  induction hs using Finset.Nonempty.cons_induction with  | singleton i => simp_all  | cons j s Hnot _ Hind =>  rw [Finset.prod_cons]  rcases Finset.mem_cons.mp hi₀ with rfl | hi₀  · calc      _ ≤ max H[X i₀ ; μ] H[∏ i ∈ s, X i ; μ] := le_max_left _ _      _ ≤ H[X i₀ * ∏ i ∈ s, X i ; μ] := by        refine max_entropy_le_entropy_mul (hX i₀) (by fun_prop) ?_        exact iIndepFun.indepFun_finsetProd_of_notMem h_indep hX Hnot |>.symm  · calc      _ ≤ H[∏ i ∈ s, X i ; μ] := Hind hi₀      _ ≤ max H[X j ; μ] H[∏ i ∈ s, X i ; μ] := le_max_right _ _      _ ≤ H[X j * ∏ x ∈ s, X x ; μ] := by        refine max_entropy_le_entropy_mul (hX j) (by fun_prop) ?_        exact iIndepFun.indepFun_finsetProd_of_notMem h_indep hX Hnot |>.symm