AlmostPeriodicity.T_bound

lemma T_bound (hK₂ : 2 ≤ K) (Lc Sc Ac ASc Tc : ℕ) (hk : k = ⌈(64 : ℝ) * m / (ε / 2) ^ 2⌉₊)    (h₁ : Lc * Sc ≤ ASc ^ k * Tc) (h₂ : (Ac : ℝ) ^ k / 2 ≤ Lc) (h₃ : (ASc : ℝ) ≤ K * Ac)    (hAc : 0 < Ac) (hε : 0 < ε) (hε' : ε ≤ 1) (hm : 1 ≤ m) :    K ^ (-512 * m / ε ^ 2 : ℝ) * Sc ≤ Tc := by  have hk' : k = ⌈(256 : ℝ) * m / ε ^ 2⌉₊ := by    rw [hk, div_pow, div_div_eq_mul_div, mul_right_comm]    congr 3    norm_num  have hK₀ : 0 < K := by positivity  have : (0 : ℝ) < Ac ^ k := by positivity  refine le_of_mul_le_mul_left ?_ this  rw [neg_mul, neg_div, Real.rpow_neg hK₀.le, mul_left_comm, inv_mul_le_iff₀ (by positivity)]  calc    (Ac ^ k * Sc : ℝ)      = 2 * (Ac ^ k / 2) * Sc := by ring    _ ≤ K * Lc * Sc := by gcongr    _ = K * ↑(Lc * Sc) := by push_cast; ring    _ ≤ K * ↑(ASc ^ k * Tc) := by gcongr    _ = K * ASc ^ k * Tc := by push_cast; ring    _ ≤ K * (K * Ac) ^ k * Tc := by gcongr    _ = K ^ (k + 1 : ℝ) * Ac ^ k * Tc := by norm_cast; push_cast; ring    _ ≤ K ^ (512 * m / ε ^ 2) * Ac ^ k * Tc := ?_    _ = K ^ (512 * m / ε ^ 2) * (Ac ^ k * Tc) := by ring  gcongr  · linarith  rw [← le_sub_iff_add_le, hk', mul_div_assoc, mul_div_assoc]  have h₄ := Nat.ceil_lt_add_one (a := 256 * (m / ε ^ 2)) (by positivity)  have h₅ : (1 : ℝ) ≤ 128 * (m / ε ^ 2) := by rw [div_eq_mul_one_div]; bound  linear_combination h₄ + 2 * h₅