tendsto_by_squeeze

lemma tendsto_by_squeeze (ε : ℝ) (hε : ε > 0) :    Tendsto (fun (x : ℝ) => (Nat.primeCounting ⌊(1 + ε) * x⌋₊ : ℝ) -      (Nat.primeCounting ⌊x⌋₊ : ℝ)) atTop atTop := by  obtain ⟨c, hc, pi_x_eq⟩ := pi_alt  rw [Asymptotics.isLittleO_iff_tendsto (by simp)] at hc  conv =>    arg 1    intro x    rw [pi_x_eq]    rw [pi_x_eq]  simp only [div_one] at hc   -- (1 + δ) * (( x / (Real.log (x)))) > (1 + f ( x)) * ( x / (Real.log (x)))   let d: ℝ := ε/(2*(2 + ε))  have hd: 0 < d := by positivity  have first_helper := smaller_terms hε c hc (d) hd  have second_helper := second_smaller_terms c hc d hd   apply Filter.tendsto_atTop_mono' (f₁ := fun x => (      ((1 - d) * ((1 + ε) * x / log ((1 + ε) * x)))      -      ((1 + d) * (x / log x)))    )  · rw [Filter.EventuallyLE]     simp only [eventually_atTop] at first_helper    simp only [gt_iff_lt, eventually_atTop] at second_helper     obtain ⟨a1, ha1⟩ := first_helper    obtain ⟨a2, ha2⟩ := second_helper     simp only [eventually_atTop]     use (max a1 a2)    intro b hb     have lt_compare: ∀ a b c d : ℝ, a < c ∧ b > d → a - b ≤ c - d := by      intro a b c d h_lt      obtain ⟨a_lt, b_gt⟩ := h_lt      linarith     apply lt_compare    simp only [ sup_le_iff] at hb    specialize ha1 b hb.1    specialize ha2 b hb.2    field_simp    field_simp at ha1 ha2    exact ⟨ha1, ha2⟩  · rw [← Filter.tendsto_comp_val_Ioi_atTop (a := 1)]    have log_split: ∀ x: Set.Ioi 1, x.val / log ((1 + ε) * x.val) =      x.val / (log (1 + ε) + log (x.val)) := by      intro x      have x_ge_one: 1 < x.val := Set.mem_Ioi.mp x.property      rw [Real.log_mul (by linarith) (by linarith)]     have log_factor: ∀ x: Set.Ioi 1, x.val / (log (1 + ε) + log (x.val)) =      x.val / ((1 + (log (1 + ε)/(log x.val))) * (log x.val)) := by      intro x      have : log (x.val) ≠ 0 := by        have pos := Real.log_pos x.property        linarith      field_simp      rw [add_comm]     conv at log_factor =>      intro x      rhs      rw [div_mul_eq_div_mul_one_div]     conv =>      arg 1      intro x      lhs      rw [mul_div_assoc]      rw [log_split x]     conv =>      arg 1      intro x      lhs      rw [log_factor]     suffices Tendsto (fun x : Set.Ioi (1 : ℝ) ↦ (1 - d) * ((1 + ε) * x) /      ((1 + log (1 + ε) / log x) * log x) - (1 + d) * x / log x) atTop atTop by      field_simp at this ⊢      exact this    conv =>      arg 1      intro x      rw [sub_eq_add_neg]      rw [← neg_div]      rw [div_add_div]      · skip      tactic =>        simp only [ne_eq, _root_.mul_eq_zero, log_eq_zero, not_or]        have x_pos := x.property        simp_rw [Set.Ioi, Set.mem_setOf_eq] at x_pos        refine ⟨?_, by linarith, by linarith, by linarith⟩        have log_num_pos: 0 < log (1 + ε) := by          exact Real.log_pos (by linarith)        have log_denom_pos: 0 < log x := by          exact Real.log_pos x.property        positivity      tactic =>        have pos := Real.log_pos (x.property)        linarith     conv =>      arg 1      intro x      equals ↑x * (log ↑x * ((1 + ε) * (1 - d)) -          (1 + log (1 + ε) / log ↑x) * ((1 + d) * log ↑x)) /        (log ↑x * ((1 + log (1 + ε) / log ↑x) * log ↑x)) =>        ring     simp only [mul_div_mul_comm]    conv =>      arg 1      intro x      rw [mul_comm]     apply Filter.Tendsto.pos_mul_atTop (C := (1 + ε) * (1 - d) - (1 + d))    · simp only [d, sub_pos]      field_simp      ring_nf      rw [add_assoc]      rw [add_lt_add_iff_left]      apply lt_of_sub_pos      ring_nf      positivity    · conv =>        arg 1        intro x        lhs        rhs        equals (log x.val) * ((1 + log (1 + ε) / log ↑x) * ((1 + d))) =>          ring       simp_rw [← mul_sub]      conv =>        arg 1        intro x        rhs        rw [mul_comm]       simp only [mul_div_mul_comm]      conv =>        arg 1        intro x        lhs        equals 1 =>          have log_pos := Real.log_pos x.property          field_simp       simp only [one_mul]      conv =>        arg 3        equals nhds (((1 + ε) * (1 - d) - (1 + d)) / 1) => simp       apply Filter.Tendsto.div      · apply Filter.Tendsto.sub        · simp        · conv =>            arg 3            equals nhds (1 * (1 + d)) => simp          apply Filter.Tendsto.mul          · conv =>              arg 3              equals nhds (1 + 0) => simp            apply Filter.Tendsto.add            · simp            · apply Filter.Tendsto.div_atTop (a := log (1 + ε))              · simp              · simp only [tendsto_comp_val_Ioi_atTop]                exact tendsto_log_atTop          · simp      · conv =>          arg 3          equals nhds (1 + 0) => simp        apply Filter.Tendsto.add        · simp        · apply Filter.Tendsto.div_atTop (a := log (1 + ε))          · simp          · simp only [tendsto_comp_val_Ioi_atTop]            exact tendsto_log_atTop      · simp    · let x_div_log (x: ℝ) := x / Real.log x      conv =>        arg 1        equals (fun (x : Set.Ioi 1) => x_div_log x.val) => rfl       rw [Filter.tendsto_comp_val_Ioi_atTop (a := 1)]      exact x_log_x_atTop