Buthe2.eventually_Buthe_theta_eq_theta

lemma eventually_Buthe_theta_eq_theta (x : ℝ) (hx : 0 ≤ x) :    (fun y => Buthe_theta y) =ᶠ[𝓝[>] x] fun _ => θ x := by  filter_upwards [self_mem_nhdsWithin,    Ico_mem_nhdsGT_of_mem ⟨Nat.floor_le hx, Nat.lt_floor_add_one x⟩] with y hygt hyfloor  rw [Chebyshev.theta_eq_sum_Icc]  unfold Buthe_theta  have hfloor : ⌊y⌋₊ = ⌊x⌋₊ := Nat.floor_eq_on_Ico ⌊x⌋₊ y hyfloor  rw [hfloor]  refine Finset.sum_congr rfl ?_  intro p hp  have hpprime : p.Prime := (Finset.mem_filter.mp hp).2  have hp_pos : (0 : ℝ) < (p : ℝ) := by exact_mod_cast hpprime.pos  have hpy : (p : ℝ) < y := by    have hp_le_floor : p ≤ ⌊x⌋₊ := (Finset.mem_Icc.mp (Finset.mem_filter.mp hp).1).2    have hpx : (p : ℝ) ≤ x := le_trans (by exact_mod_cast hp_le_floor) (Nat.floor_le hx)    exact lt_of_le_of_lt hpx hygt  rw [Buthe_chiStarIcc_eq_one_of_pos_lt hp_pos hpy, one_mul]