AlmostPeriodicity.just_the_triangle_inequality

public lemma just_the_triangle_inequality {t : G} {a : Fin k → G} (ha : a ∈ l k m ε f A)    (ha' : (a + fun _ ↦ t) ∈ l k m ε f A) (hk : 0 < k) (hm : 1 ≤ m) :    ‖τ (-t) (mu A ∗ᵈ f) - mu A ∗ᵈ f‖_[2 * m] ≤ 2 * ε * ‖f‖_[2 * m] := by  let f₁ : G → ℂ := fun x ↦ ∑ i, f (x - a i)  let f₂ : G → ℂ := fun x ↦ ∑ i, f (x - a i - t)  have hp : (1 : ℝ≥0∞) ≤ 2 * m := by norm_cast; linarith  have h₁ : ‖f₁ - k • (mu A ∗ᵈ f)‖_[2 * m] ≤ k * ε * ‖f‖_[2 * m] := by    rw [l, Finset.mem_filter] at ha ; exact ha.2  have h₂ : ‖f₂ - k • (mu A ∗ᵈ f)‖_[2 * m] ≤ k * ε * ‖f‖_[2 * m] := by    rw [l, Finset.mem_filter, LProp] at ha'    refine ha'.2.trans_eq' ?_    congr with i : 1    simp [sub_sub, f₂]  have h₃ : f₂ = τ t f₁ := by    ext i : 1    rw [translate_apply]    refine Finset.sum_congr rfl fun j _ ↦ ?_    rw [sub_right_comm]  have h₄₁ : ‖τ t f₁ - k • (mu A ∗ᵈ f)‖_[2 * m] = ‖τ (-t) (τ t f₁ - k • (mu A ∗ᵈ f))‖_[2 * m] := by    rw [dLpNorm_translate]  have h₄ : ‖τ t f₁ - k • (mu A ∗ᵈ f)‖_[2 * m] = ‖f₁ - τ (-t) (k • (mu A ∗ᵈ f))‖_[2 * m] := by    rw [h₄₁, translate_sub_right, translate_translate]    simp  have h₅₁ : ‖τ (-t) (k • (mu A ∗ᵈ f)) - f₁‖_[2 * m] ≤ k * ε * ‖f‖_[2 * m] := by    rwa [dLpNorm_sub_comm, ← h₄, ← h₃]  have : (0 : ℝ) < k := by positivity  refine le_of_mul_le_mul_left ?_ this  rw [← nsmul_eq_mul, ← dLpNorm_nsmul _ (_ - mu A ∗ᵈ f), nsmul_sub, ←    translate_smul_right (-t) (mu A ∗ᵈ f) k, mul_assoc, mul_left_comm, two_mul ((k : ℝ) * _), ←    mul_assoc]  calc    ‖τ (-t) (k • (μ A ∗ᵈ f)) - k • (μ A ∗ᵈ f)‖_[2 * m]      ≤ ‖τ (-t) (k • (μ A ∗ᵈ f)) - f₁‖_[2 * m] + ‖f₁ - k • (μ A ∗ᵈ f)‖_[2 * m] :=      dLpNorm_sub_le_dLpNorm_sub_add_dLpNorm_sub (mod_cast hp)    _ ≤ k * ε * ‖f‖_[2 * m] + k * ε * ‖f‖_[2 * m] := by gcongr