AlmostPeriodicity.lemma28

public lemma lemma28 (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k) :    (#A ^ k : ℝ) / 2 ≤ #(l k m ε f A) := by  have : 0 < k := by    rw [← @Nat.cast_pos ℝ]    refine hk.trans_lt' ?_    refine div_pos (mul_pos (by norm_num1) ?_) (pow_pos hε _)    rw [Nat.cast_pos, ← Nat.succ_le_iff]    exact hm  rcases A.eq_empty_or_nonempty with (rfl | hA)  · simp [zero_pow this.ne']  refine lemma28_markov hε hm ?_  have hm' : 2 * m ≠ 0 := by linarith  have hmeq : ((2 * m : ℕ) : ℝ≥0∞) = 2 * m := by rw [Nat.cast_mul, Nat.cast_two]  rw [← hmeq, mul_pow]  simp only [dLpNorm_pow_eq_sum_norm hm']  rw [sum_comm]  have : ∀ x : G, ∑ a ∈ A ^^ k,      ‖∑ i, f (x - a i) - (k • (mu A ∗ᵈ f)) x‖ ^ (2 * m) ≤    (8 * m) ^ m * k ^ (m - 1) *      ∑ a ∈ A ^^ k, ∑ i, ‖f (x - a i) - (mu A ∗ᵈ f) x‖ ^ (2 * m) :=    lemma28_part_one hm  refine (sum_le_sum fun x _ ↦ this x).trans ?_  rw [← mul_sum]  simp only [@sum_comm _ _ G]  have (a : Fin k → G) (i : Fin k) :      ∑ x, ‖f (x - a i) - (mu A ∗ᵈ f) x‖ ^ (2 * m) = ‖τ (a i) f - mu A ∗ᵈ f‖_[2 * m] ^ (2 * m) := by    rw [← hmeq, dLpNorm_pow_eq_sum_norm hm']    simp only [Pi.sub_apply, translate_apply]  simp only [this]  have :    (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, (2 * ‖f‖_[2 * m]) ^ (2 * m) :=    lemma28_part_two hm hA  refine le_trans (mod_cast this) ?_  simpa [mul_assoc] using lemma28_end hε hm hk