Hₛ le log d

theorem Hₛ_le_log_d (d : ProbDistribution α) : Hₛ d ≤ Real.log (Fintype.card α) := by  --Thanks Aristotle  by_cases h : Fintype.card α = 0  · simp_all [Hₛ, Fintype.card_eq_zero_iff.mp h]  -- Since the sum of the probabilities is 1, we can apply Jensen's inequality for the convex function -x log x.  have h_jensen {p : α → ℝ} (hsum : ∑ i, p i = 1) (hp : ∀ i, 0 ≤ p i ∧ p i ≤ 1) :      -∑ i, p i * (p i).log ≤ Real.log (Fintype.card α) := by    have h_jensen : (∑ i, (Fintype.card α : ℝ)⁻¹ * p i) * (∑ i, (Fintype.card α : ℝ)⁻¹ * p i).log ≤          (∑ i, (Fintype.card α : ℝ)⁻¹ * (p i * (p i).log)) := by      have h_convex : ConvexOn ℝ (Set.Icc 0 1) (fun x ↦ x * Real.log x) :=        Real.convexOn_mul_log.subset Set.Icc_subset_Ici_self (convex_Icc 0 1)      convert h_convex.map_sum_le _ _ _ <;> aesop    simp_rw [← Finset.mul_sum, hsum, mul_one, Real.log_inv] at h_jensen    have : 0 < (Fintype.card α : ℝ)⁻¹ := by positivity    have := mul_inv_cancel₀ <| show (Fintype.card α : ℝ) ≠ 0 by positivity    nlinarith  simpa [Hₛ, H₁, Real.negMulLog] using h_jensen d.2 (by grind)