awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ ∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2 ≤
    4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2
have rw : HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 2..√x, 1 / HPow.hPow (β := ℕ) (log x) 2)
    (∫ (x : ℝ) in √x..x, 1 / HPow.hPow (β := ℕ) (log x) 2) ≤
  4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2
Tactic: rw [← intervalIntegral.integral_add_adjacent_intervals (b := x.sqrt)]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
rw :
  HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 2..√x, 1 / HPow.hPow (β := ℕ) (log x) 2)
      (∫ (x : ℝ) in √x..x, 1 / HPow.hPow (β := ℕ) (log x) 2) ≤
    4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2
⊢ ∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2 ≤
    4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2
have hab : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log t) 2) volume 2 √x
Tactic: rw [← intervalIntegral.integral_add_adjacent_intervals (b := x.sqrt)]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
rw :
  HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 2..√x, 1 / HPow.hPow (β := ℕ) (log x) 2)
      (∫ (x : ℝ) in √x..x, 1 / HPow.hPow (β := ℕ) (log x) 2) ≤
    4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2
hab : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log t) 2) volume 2 √x
⊢ ∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2 ≤
    4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2
have hbc : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log t) 2) volume (√x) x
Tactic: rw [← intervalIntegral.integral_add_adjacent_intervals (b := x.sqrt)]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ LT.lt (α := ℝ) 1 2
have linarith : LE.le (α := ℝ) 2 1 → -1 + HSub.hSub (α := ℝ) 2 1 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ 1 < √x
have linarith : √x ≤ 1 → -1 + (2 - √x) + (√x - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 2..√x, 1 / HPow.hPow (β := ℕ) (log x) 2)
      (∫ (x : ℝ) in √x..x, 1 / HPow.hPow (β := ℕ) (log x) 2) ≤
    4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2
have grw : (√x - 2) / HPow.hPow (β := ℕ) (log 2) 2 + (x - √x) / HPow.hPow (β := ℕ) (log √x) 2 ≤
  4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2
Tactic: grw [integral_1_div_log_sq_le two_le_sqrt (by linarith),
      integral_1_div_log_sq_le sqrt_le_x (by linarith)]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ 0 ≤ x
have linarith : x < 0 → HMul.hMul (α := ℝ) 4 (-1) + (4 - x) + (x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
linarith : x < 0 → HMul.hMul (α := ℝ) 4 (-1) + (4 - x) + (x - 0) = 0
⊢ 0 ≤ x
have linarith₁ : x < 0 → GT.gt (α := ℝ) 4 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ (√x - 2) / HPow.hPow (β := ℕ) (log 2) 2 + (x - √x) / HPow.hPow (β := ℕ) (log √x) 2 ≤
    4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2
have rw : HPow.hPow (α := ℝ) (β := ℕ) 2 2 * ((x - √x) / HPow.hPow (β := ℕ) (log x) 2) + (√x - 2) / HPow.hPow (β := ℕ) (log 2) 2 ≤
  4 * (x / HPow.hPow (β := ℕ) (log x) 2) + √x / HPow.hPow (β := ℕ) (log 2) 2
Tactic: rw [log_sqrt (by linarith), add_comm, div_pow, ← div_mul, mul_comm, mul_div_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 2 * ((x - √x) / HPow.hPow (β := ℕ) (log x) 2) +
      (√x - 2) / HPow.hPow (β := ℕ) (log 2) 2 ≤
    4 * (x / HPow.hPow (β := ℕ) (log x) 2) + √x / HPow.hPow (β := ℕ) (log 2) 2
have norm_num : 4 * ((x - √x) / HPow.hPow (β := ℕ) (log x) 2) + (√x - 2) / HPow.hPow (β := ℕ) (log 2) 2 ≤
  4 * (x / HPow.hPow (β := ℕ) (log x) 2) + √x / HPow.hPow (β := ℕ) (log 2) 2
Tactic: norm_num
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ 4 * ((x - √x) / HPow.hPow (β := ℕ) (log x) 2) + (√x - 2) / HPow.hPow (β := ℕ) (log 2) 2 ≤
    4 * (x / HPow.hPow (β := ℕ) (log x) 2) + √x / HPow.hPow (β := ℕ) (log 2) 2
have h₁ : x - √x ≤ x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
h₁ : x - √x ≤ x
⊢ 4 * ((x - √x) / HPow.hPow (β := ℕ) (log x) 2) + (√x - 2) / HPow.hPow (β := ℕ) (log 2) 2 ≤
    4 * (x / HPow.hPow (β := ℕ) (log x) 2) + √x / HPow.hPow (β := ℕ) (log 2) 2
have h₂ : √x - 2 ≤ √x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ x - √x ≤ x
have linarith : x < x - √x → HMul.hMul (α := ℝ) 2 (-1) + (2 - √x) + (x - (x - √x)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
linarith : x < x - √x → HMul.hMul (α := ℝ) 2 (-1) + (2 - √x) + (x - (x - √x)) = 0
⊢ x - √x ≤ x
have linarith₁ : x < x - √x → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ √x - 2 ≤ √x
have linarith : √x < √x - 2 → HMul.hMul (α := ℝ) 2 (-1) + (√x - (√x - 2)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
linarith : √x < √x - 2 → HMul.hMul (α := ℝ) 2 (-1) + (√x - (√x - 2)) = 0
⊢ √x - 2 ≤ √x
have linarith₁ : √x < √x - 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log t) 2) volume 2 √x
have hab : LT.lt (α := ℝ) 1 2
Tactic: apply intervalIntegrable_one_div_log_sq
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
hab : LT.lt (α := ℝ) 1 2
⊢ IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log t) 2) volume 2 √x
have hab₁ : 1 < √x
Tactic: apply intervalIntegrable_one_div_log_sq
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log t) 2) volume (√x) x
have hbc : 1 < √x
Tactic: apply intervalIntegrable_one_div_log_sq
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
hbc : 1 < √x
⊢ IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log t) 2) volume (√x) x
have hbc₁ : 1 < x
Tactic: apply intervalIntegrable_one_div_log_sq
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ 1 < x
have linarith : x ≤ 1 → HMul.hMul (α := ℝ) 3 (-1) + (4 - x) + (x - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
linarith : x ≤ 1 → HMul.hMul (α := ℝ) 3 (-1) + (4 - x) + (x - 1) = 0
⊢ 1 < x
have linarith₁ : x ≤ 1 → GT.gt (α := ℝ) 3 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
⊢ IsLittleO (F := ℝ) atTop Real.sqrt fun (x : ℝ) ↦ x / HPow.hPow (β := ℕ) (log x) 2
have apply : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2 * √x) fun (x : ℝ) ↦ x
Tactic: apply isLittleO_mul_iff_isLittleO_div _ |>.mp
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
apply : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2 * √x) fun (x : ℝ) ↦ x
⊢ IsLittleO (F := ℝ) atTop Real.sqrt fun (x : ℝ) ↦ x / HPow.hPow (β := ℕ) (log x) 2
have apply₁ : ∀ᶠ (x : ℝ) in atTop, HPow.hPow (β := ℕ) (log x) 2 ≠ 0
Tactic: apply isLittleO_mul_iff_isLittleO_div _ |>.mp
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
| IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2 * √x) fun (x : ℝ) ↦ x
have arg : fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2 * √x
Tactic: arg 2
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
| fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2 * √x
have h : ∀ (x : ℝ), HPow.hPow (β := ℕ) (log x) 2 * √x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
| HPow.hPow (β := ℕ) (log x) 2 * √x
have h : √x * HPow.hPow (β := ℕ) (log x) 2
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
| IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2 * √x) fun (x : ℝ) ↦ x
have h : ∀ (x : ℝ), √x * HPow.hPow (β := ℕ) (log x) 2
Tactic: arg 2; ext; rw [mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2 * √x) fun (x : ℝ) ↦ x
have conv : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ √x * HPow.hPow (β := ℕ) (log x) 2) fun (x : ℝ) ↦ x
Tactic: conv => arg 2; ext; rw [mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ √x * HPow.hPow (β := ℕ) (log x) 2) fun (x : ℝ) ↦ x
have apply : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2) fun (x : ℝ) ↦ x / √x
Tactic: apply isLittleO_mul_iff_isLittleO_div _ |>.mpr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
apply : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2) fun (x : ℝ) ↦ x / √x
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ √x * HPow.hPow (β := ℕ) (log x) 2) fun (x : ℝ) ↦ x
have apply₁ : ∀ᶠ (x : ℝ) in atTop, √x ≠ 0
Tactic: apply isLittleO_mul_iff_isLittleO_div _ |>.mpr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2) fun (x : ℝ) ↦ x / √x
have simp_rw : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℝ) (log x) 2) fun (x : ℝ) ↦ x ^ (1 / 2)
Tactic: simp_rw [div_sqrt, sqrt_eq_rpow, ← rpow_two]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
⊢ ∀ᶠ (x : ℝ) in atTop, √x ≠ 0
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 0 < x) x} x →
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ √x ≠ 0) x} x}
    a
Tactic: filter_upwards [eventually_gt_atTop 0] with x hx using sqrt_ne_zero'.mpr hx
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 0 < x) x} x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ √x ≠ 0) x} x}
      a
⊢ ∀ᶠ (x : ℝ) in atTop, √x ≠ 0
have h₁ : ∀ (a : ℝ), 0 < a → √a ≠ 0
Tactic: filter_upwards [eventually_gt_atTop 0] with x hx using sqrt_ne_zero'.mpr hx
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
⊢ ∀ᶠ (x : ℝ) in atTop, HPow.hPow (β := ℕ) (log x) 2 ≠ 0
have h : ∀ (x : ℝ), 1 < x → HPow.hPow (β := ℕ) (log x) 2 ≠ 0
Tactic: filter_upwards [eventually_gt_atTop 1] with x _
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 1 < x
⊢ HPow.hPow (β := ℕ) (log x) 2 ≠ 0
have apply : x ≠ 0
Tactic: apply pow_ne_zero _ <| log_ne_zero.mpr ⟨_, _, _⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 1 < x
apply : x ≠ 0
⊢ HPow.hPow (β := ℕ) (log x) 2 ≠ 0
have apply₁ : x ≠ 1
Tactic: apply pow_ne_zero _ <| log_ne_zero.mpr ⟨_, _, _⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 1 < x
apply : x ≠ 0
apply₁ : x ≠ 1
⊢ HPow.hPow (β := ℕ) (log x) 2 ≠ 0
have apply₂ : x ≠ -1
Tactic: apply pow_ne_zero _ <| log_ne_zero.mpr ⟨_, _, _⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 1 < x
⊢ x ≠ 0
have linarith : x = 0 → -1 + (1 - x) + (x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 1 < x
⊢ x ≠ 1
have linarith : x = 1 → 1 - x + (x - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 1 < x
⊢ x ≠ -1
have linarith : x = -1 → HMul.hMul (α := ℝ) 2 (-1) + (1 - x) + (x - -1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 1 < x
linarith : x = -1 → HMul.hMul (α := ℝ) 2 (-1) + (1 - x) + (x - -1) = 0
⊢ x ≠ -1
have linarith₁ : x = -1 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2) fun (x : ℝ) ↦
    x / HPow.hPow (β := ℕ) (log x) 2
have trans : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2) fun (x : ℝ) ↦
  4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2
Tactic: trans (fun x ↦ 4 * x / log x ^ 2 + √x / log 2 ^ 2)
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
trans :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2) fun (x : ℝ) ↦
    4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2) fun (x : ℝ) ↦
    x / HPow.hPow (β := ℕ) (log x) 2
have trans₁ : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ 4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2)
  fun (x : ℝ) ↦ x / HPow.hPow (β := ℕ) (log x) 2
Tactic: trans (fun x ↦ 4 * x / log x ^ 2 + √x / log 2 ^ 2)
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2) fun (x : ℝ) ↦
    4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2
have h : ∀ᶠ (x : ℝ) in atTop,
  Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2) ≤
    ‖4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2‖
Tactic: apply IsBigO.of_bound'
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
⊢ ∀ᶠ (x : ℝ) in atTop,
    Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2) ≤
      ‖4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2‖
have h : ∀ (x : ℝ) (hx : 4 ≤ x),
  Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2) ≤
    ‖4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2‖
Tactic: filter_upwards [eventually_ge_atTop 4] with x hx
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
⊢ 2 ≤ x
have linarith : x < 2 → HMul.hMul (α := ℝ) 2 (-1) + (4 - x) + (x - 2) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
linarith : x < 2 → HMul.hMul (α := ℝ) 2 (-1) + (4 - x) + (x - 2) = 0
⊢ 2 ≤ x
have linarith₁ : x < 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
⊢ Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2) ≤
    ‖4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2‖
have h : ∫ (x : ℝ) in 2..x, |1 / HPow.hPow (β := ℕ) (log x) 2| ≤
  ‖4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2‖
Tactic: apply le_trans <| intervalIntegral.abs_integral_le_integral_abs (by linarith)
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
⊢ ∫ (x : ℝ) in 2..x, |1 / HPow.hPow (β := ℕ) (log x) 2| ≤
    ‖4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2‖
have h : ∫ (x : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log x) 2 ≤
  ‖4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2‖
Tactic: rw [intervalIntegral.integral_congr (g := (fun t ↦ 1 / log t ^ 2))]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
h :
  ∫ (x : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log x) 2 ≤
    ‖4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2‖
⊢ ∫ (x : ℝ) in 2..x, |1 / HPow.hPow (β := ℕ) (log x) 2| ≤
    ‖4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2‖
have h₁ : Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ |1 / HPow.hPow (β := ℕ) (log x) 2|) (fun (t : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log t) 2)
  (Set.uIcc 2 x)
Tactic: rw [intervalIntegral.integral_congr (g := (fun t ↦ 1 / log t ^ 2))]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
⊢ ∫ (x : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log x) 2 ≤
    ‖4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2‖
have h : 0 ≤ 4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2
Tactic: grw [integral_one_div_log_sq_le_explicit hx, norm_of_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
⊢ IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (x : ℝ) ↦ 4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2) fun (x : ℝ) ↦
    x / HPow.hPow (β := ℕ) (log x) 2
have refine_1 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ 4 * x / HPow.hPow (β := ℕ) (log x) 2) fun (x : ℝ) ↦
  x / HPow.hPow (β := ℕ) (log x) 2
Tactic: refine IsBigO.add ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
refine_1 :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ 4 * x / HPow.hPow (β := ℕ) (log x) 2) fun (x : ℝ) ↦
    x / HPow.hPow (β := ℕ) (log x) 2
⊢ IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (x : ℝ) ↦ 4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2) fun (x : ℝ) ↦
    x / HPow.hPow (β := ℕ) (log x) 2
have refine_2 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ √x / HPow.hPow (β := ℕ) (log 2) 2) fun (x : ℝ) ↦
  x / HPow.hPow (β := ℕ) (log x) 2
Tactic: refine IsBigO.add ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ 4 * x / HPow.hPow (β := ℕ) (log x) 2) fun (x : ℝ) ↦
    x / HPow.hPow (β := ℕ) (log x) 2
have refine_1 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ 4 * (x / HPow.hPow (β := ℕ) (log x) 2)) fun (x : ℝ) ↦
  x / HPow.hPow (β := ℕ) (log x) 2
Tactic: simp_rw [mul_div_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
| IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ √x / HPow.hPow (β := ℕ) (log 2) 2) fun (x : ℝ) ↦
    x / HPow.hPow (β := ℕ) (log x) 2
have arg : fun (x : ℝ) ↦ √x / HPow.hPow (β := ℕ) (log 2) 2
Tactic: arg 2
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
| fun (x : ℝ) ↦ √x / HPow.hPow (β := ℕ) (log 2) 2
have h : ∀ (x : ℝ), √x / HPow.hPow (β := ℕ) (log 2) 2
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
| √x / HPow.hPow (β := ℕ) (log 2) 2
have h : 1 / HPow.hPow (β := ℕ) (log 2) 2 * √x
Tactic: rw [← mul_one_div, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
| IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ √x / HPow.hPow (β := ℕ) (log 2) 2) fun (x : ℝ) ↦
    x / HPow.hPow (β := ℕ) (log x) 2
have h : ∀ (x : ℝ), 1 / HPow.hPow (β := ℕ) (log 2) 2 * √x
Tactic: arg 2; ext; rw [← mul_one_div, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ √x / HPow.hPow (β := ℕ) (log 2) 2) fun (x : ℝ) ↦
    x / HPow.hPow (β := ℕ) (log x) 2
have refine_2 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log 2) 2 * √x) fun (x : ℝ) ↦
  x / HPow.hPow (β := ℕ) (log x) 2
Tactic: conv => arg 2; ext; rw [← mul_one_div, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2))
    fun (x : ℝ) ↦ x / HPow.hPow (β := ℕ) (log x) 2
have refine : ∀ᶠ (x : ℝ) in atTop,
  Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤
    log 4 * Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2)
Tactic: refine (IsBigO.of_bound (log 4) ?_).trans integral_one_div_log_sq_isBigO
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
⊢ ∀ᶠ (x : ℝ) in atTop,
    Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤
      log 4 * Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2)
have h : ∀ (x : ℝ),
  4 ≤ x →
    Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤
      log 4 * Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2)
Tactic: filter_upwards [eventually_ge_atTop 4] with x _
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 4 ≤ x
⊢ 2 ≤ x
have linarith : x < 2 → HMul.hMul (α := ℝ) 2 (-1) + (4 - x) + (x - 2) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 4 ≤ x
linarith : x < 2 → HMul.hMul (α := ℝ) 2 (-1) + (4 - x) + (x - 2) = 0
⊢ 2 ≤ x
have linarith₁ : x < 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 4 ≤ x
⊢ ∫ (x : ℝ) in 2..x, log 4 * (1 / HPow.hPow (β := ℕ) (log x) 2) =
    log 4 * |∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2|
have rw : LE.le (α := ℝ) 0 (∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2)
Tactic: rw [intervalIntegral.integral_const_mul, abs_of_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 4 ≤ x
⊢ |∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)| ≤
    log 4 * |∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2|
have calc : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ |θ x / (x * HPow.hPow (β := ℕ) (log x) 2)|) volume 2 x
Tactic: calc |∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)|
    _ ≤ ∫ (x : ℝ) in 2..x, |θ x / (x * log x ^ 2)| :=
        intervalIntegral.abs_integral_le_integral_abs (by linarith)
    _ ≤ ∫ (x : ℝ) in 2..x, log 4 * (1 / log x ^ 2) :=
        intervalIntegral.integral_mono_on (by linarith) ?hf ?hg fun t ⟨ht, _⟩ ↦ ?hh
    _ = log 4 * |∫ (t : ℝ) in 2..x, 1 / log t ^ 2| := by
        rw [intervalIntegral.integral_const_mul, abs_of_nonneg]
        exact intervalIntegral.integral_nonneg (by linarith) fun u _ ↦ by positivity
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 4 ≤ x
calc : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ |θ x / (x * HPow.hPow (β := ℕ) (log x) 2)|) volume 2 x
⊢ |∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)| ≤
    log 4 * |∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2|
have calc₁ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log 4 * (1 / HPow.hPow (β := ℕ) (log x) 2)) volume 2 x
Tactic: calc |∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)|
    _ ≤ ∫ (x : ℝ) in 2..x, |θ x / (x * log x ^ 2)| :=
        intervalIntegral.abs_integral_le_integral_abs (by linarith)
    _ ≤ ∫ (x : ℝ) in 2..x, log 4 * (1 / log x ^ 2) :=
        intervalIntegral.integral_mono_on (by linarith) ?hf ?hg fun t ⟨ht, _⟩ ↦ ?hh
    _ = log 4 * |∫ (t : ℝ) in 2..x, 1 / log t ^ 2| := by
        rw [intervalIntegral.integral_const_mul, abs_of_nonneg]
        exact intervalIntegral.integral_nonneg (by linarith) fun u _ ↦ by positivity