entropy_of_Z_two_le

lemma entropy_of_Z_two_le : H[Z2] ≤ (8 * p.m^2 - 16 * p.m + 1) * k + (p.m:ℝ)⁻¹ * ∑ i, H[X i] := by  have hm := p.hm  let zero : Fin p.m := ⟨0, by linarith [hm]⟩  let one : Fin p.m := ⟨1, by linarith [hm]⟩  let Y' : Fin p.m → Ω' → G := fun i ω ↦ i.val • Q i ω  have : Y' one = Q one := by ext; simp [one, Y']  calc    _ = H[ Q one + ∑ i ∈ .Ioi one, i.val • (Q i)] := by      congr      calc        _ = ∑ j ∈ Finset.univ.erase zero, j.val • Q j  := Z2_eq        _ = _ := by          symm; rw [add_comm, ←this]          convert! Finset.sum_erase_add _ _ _ using 3 <;> try infer_instance          · ext ⟨_, _⟩; simp [zero, one]; omega          simp [one, zero]    _ ≤ H[Q one] + ∑ i ∈ .Ioi one, (H[Q one + i.val • (Q i)] - H[Q one]) := by      rw [←sub_le_iff_le_add']      simp_rw [←this]      convert! kvm_ineq_I (s := .Ioi one) _ _ _ using 1 <;> try infer_instance      · 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 ↦ j.val • ∑ i, x ⟨(i,j), by simp [S]⟩      convert iIndepFun.finsets_comp S _ h_indep (by fun_prop) φ (by fun_prop) with i ω      · simp [φ, Y']      rw [Finset.pairwiseDisjoint_iff]; rintro _ _ _ _ ⟨⟨_, _⟩, hij⟩      simp [S] at hij; omega    _ ≤ H[Q one] + ∑ i ∈ .Ioi one, 4 * p.m * (2 * k) := by      gcongr with i hi      have hQi_mes : Measurable (-(Q i)) := Q_mes h_mes _      calc        _ = H[Q one - (i.val:ℤ) • -(Q i)] - H[Q one]:= by simp        _ ≤ 4 * |(i.val:ℤ)| * d[Q one # -(Q i)] := by          convert ent_sub_zsmul_sub_ent_le _ _ _ <;> try infer_instance          all_goals try fun_prop          simp at hi; exact Q_indep h_mes h_indep (by order)        _ ≤ _ := by          gcongr          · exact rdist_nonneg (by fun_prop) (by fun_prop)          · simp          exact Q_dist _ h_mes h_indep hident _ _    _ ≤ k + (p.m:ℝ)⁻¹ * ∑ i, H[X i] + ∑ i ∈ .Ioi one, 4 * p.m * (2 * k) := by      gcongr; exact le_of_eq (Q_ent _ h_mes h_indep hident _)    _ = _ := by      have : ↑(p.m - 1 - 1) = (p.m - 1 - 1 : ℝ) := by        norm_cast; rw [Int.subNatNat_of_le (by omega)]; omega      simp [one, this]; ring