AlmostPeriodicity.lemma28_part_two

lemma lemma28_part_two (hm : 1 ≤ m) (hA : A.Nonempty) :    (8 * m) ^ m * k ^ (m - 1) * ∑ a ∈ A ^^ k, ∑ i, ‖τ (a i) f - mu A ∗ᵈ f‖_[2 * m] ^ (2 * m) ≤      (8 * m) ^ m * k ^ (m - 1) * ∑ _a ∈ A ^^ k, ∑ _i : Fin k, (2 * ‖f‖_[2 * m]) ^ (2 * m) := by  -- lots of the equalities about m can be automated but it's *way* slower  have hmeq : ((2 * m : ℕ) : ℝ≥0∞) = 2 * m := by rw [Nat.cast_mul, Nat.cast_two]  have hm' : 1 < 2 * m := (Nat.mul_le_mul_left 2 hm).trans_lt' <| by norm_num1  have hm'' : (1 : ℝ≥0∞) ≤ 2 * m := by rw [← hmeq, Nat.one_le_cast]; exact hm'.le  gcongr  refine (dLpNorm_sub_le hm'').trans ?_  rw [dLpNorm_translate, two_mul ‖f‖_[2 * m], add_le_add_iff_left]  have hmeq' : ((2 * m : ℝ≥0) : ℝ≥0∞) = 2 * m := by    rw [ENNReal.coe_mul, ENNReal.coe_two, ENNReal.coe_natCast]  have : (1 : ℝ≥0) < 2 * m := by    rw [← Nat.cast_two, ← Nat.cast_mul, Nat.one_lt_cast]    exact hm'  rw [← hmeq', ddconv_comm]  refine (dLpNorm_ddconv_le this.le _ _).trans ?_  rw [dL1Norm_mu hA, mul_one]