entropy_of_W_le

lemma entropy_of_W_le : H[W] ≤ (2*p.m - 1) * k + (p.m:ℝ)⁻¹ * ∑ i, H[X i] := by  have hm := p.hm  have : NeZero p.m := ⟨by lia⟩  calc    _ = H[∑ i, Q i] := by rw [Finset.sum_comm]    _ = H[Q 0 + ∑ i ∈ .Ioi 0, Q i] := by simp [Finset.add_sum_Ioi_eq_sum_Ici (f := Q)]    _ ≤ H[Q 0] + ∑ i ∈ .Ioi 0, (H[Q 0 + Q i] - H[Q 0]) := by      grw [← sub_le_iff_le_add', kvm_ineq_I (Y := Q)]      · simp      · fun_prop      let S : Fin p.m → Finset (Fin p.m × Fin p.m) := fun j ↦ {p|p.2=j}      let φ : (j:Fin p.m) → ((_: S j) → G) → G := fun j x ↦ ∑ i, x ⟨(i,j), by simp [S]⟩      convert iIndepFun.finsets_comp S _ h_indep (by fun_prop) φ (by fun_prop) with i ω      · simp [φ]      rw [Finset.pairwiseDisjoint_iff]; rintro _ _ _ _ ⟨⟨_, _⟩, hij⟩      simp [S] at hij; omega    _ ≤ k + (p.m:ℝ)⁻¹ * ∑ i, H[X i] + ∑ i ∈ .Ioi (0 : Fin p.m), 2 * k := by      gcongr with j hj      · exact le_of_eq (Q_ent _ h_mes h_indep hident _)      simp at hj      have : IdentDistrib (Q 0) (Q j) ℙ ℙ := Q_ident _ h_mes h_indep hident _ _      have hQj_mes : Measurable (-(Q j)) := Q_mes h_mes _      calc        _ = d[Q 0 # -(Q j)] := by          rw [IndepFun.rdist_eq _ (by fun_prop) hQj_mes, entropy_neg (by fun_prop),            ← this.entropy_congr, sub_neg_eq_add]          · linarith          exact Q_indep h_mes h_indep (by order)        _ ≤ _ := Q_dist _ h_mes h_indep hident _ _    _ = _ := by      have : (p.m-1:ℕ) = (p.m:ℝ)-(1:ℝ) := by norm_cast; grind      simp [this]; ring