lemma28_end

lemma lemma28_end (hε : 0 < ε) (hm : 1 ≤ m) (hk : 64 * m / ε ^ 2 ≤ k) :    (8 * m) ^ m * k ^ (m - 1) * #A ^ k * k * (2 * ‖f‖_[2 * m] : ℝ) ^ (2 * m) ≤      1 / 2 * ((k * ε) ^ (2 * m) * ∑ i : G, ‖f i‖ ^ (2 * m)) * #A ^ k := by  have hmeq : ((2 * m : ℕ) : ℝ≥0∞) = 2 * m := by rw [Nat.cast_mul, Nat.cast_two]  have hm' : 2 * m ≠ 0 := by    refine mul_ne_zero two_pos.ne' ?_    rw [← pos_iff_ne_zero, ← Nat.succ_le_iff]    exact hm  rw [mul_pow (2 : ℝ), ← hmeq, ← dLpNorm_pow_eq_sum_norm hm' f, ← mul_assoc, ← mul_assoc,    mul_right_comm _ (#A ^ k : ℝ), mul_right_comm _ (#A ^ k : ℝ),    mul_right_comm _ (#A ^ k : ℝ)]  rw [div_le_iff₀' (by positivity)] at hk  gcongr ?_ * _ * _  calc    (8 * m : ℝ) ^ m * k ^ (m - 1) * k * 2 ^ (2 * m)      = (8 * m) ^ m * 2 ^ (2 * m) * (k ^ (m - 1) * k) := by ring    _ = (64 * m * k / 2) ^ m := by rw [pow_sub_one_mul (by omega), pow_mul, ← mul_pow]; ring    _ ≤ (ε ^ 2 * k * k / 2) ^ m := by gcongr    -- FIXME: `ring` regression. See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/ring.20regression.20in.20v4.2E19.2E0-rc2/with/511226890    _ = (k * ε) ^ (2 * m) / 2 ^ m := by ring_nf; simp_rw [one_div]    _ ≤ (k * ε) ^ (2 * m) / 2 ^ 1 := by gcongr; norm_num    _ = 1 / 2 * (k * ε) ^ (2 * m) := by ring