AlmostPeriodicity.almost_periodicity

public lemma almost_periodicity (ε : ℝ) (hε : 0 < ε) (hε' : ε ≤ 1) (m : ℕ) (f : G → ℂ)    (hK₂ : 2 ≤ K) (hK : σ[A, S] ≤ K) :    ∃ T : Finset G,      K ^ (-512 * m / ε ^ 2 : ℝ) * #S ≤ #T ∧        ∀ t ∈ T, ‖τ t (mu A ∗ᵈ f) - mu A ∗ᵈ f‖_[2 * m] ≤ ε * ‖f‖_[2 * m] := by  obtain rfl | hm := m.eq_zero_or_pos  · exact ⟨S, by simp⟩  obtain rfl | hA := A.eq_empty_or_nonempty  · refine ⟨univ, ?_, fun t _ ↦ ?_⟩    · have : K ^ ((-512 : ℝ) * m / ε ^ 2) ≤ 1 := by        refine Real.rpow_le_one_of_one_le_of_nonpos (one_le_two.trans hK₂) ?_        rw [neg_mul, neg_div, Right.neg_nonpos_iff]        positivity      refine (mul_le_mul_of_nonneg_right this (Nat.cast_nonneg _)).trans ?_      rw [one_mul, Nat.cast_le]      exact card_le_univ _    simp only [mu_empty, zero_ddconv, translate_zero_right, sub_self, dLpNorm_zero]    positivity  let k := ⌈(64 : ℝ) * m / (ε / 2) ^ 2⌉₊  have hk : k ≠ 0 := by positivity  let L := l k m (ε / 2) f A  have : (#A : ℝ) ^ k / 2 ≤ #L := lemma28 (half_pos hε) hm (Nat.le_ceil _)  have hL : L.Nonempty := by    rw [← card_pos, ← @Nat.cast_pos ℝ]    exact this.trans_lt' (by positivity)  obtain ⟨a, ha, hL'⟩ := big_shifts S _ hk hL (filter_subset _ _)  refine ⟨({t | (a + fun _ ↦ -t) ∈ L} : Finset _), ?_, ?_⟩  · simp_rw [sub_eq_add_neg] at hL'    exact T_bound hK₂ #L #S #A #(A + S) _ rfl hL' this      (by rw [← cast_addConst_mul_card]; gcongr) hA.card_pos hε hε' hm  intro t ht  simp only [mem_filter, mem_univ, true_and] at ht  have := just_the_triangle_inequality ha ht hk.bot_lt hm  rwa [neg_neg, mul_div_cancel₀ _ (two_ne_zero' ℝ)] at this