awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
hab : LT.lt (α := ℝ) 1 2
hab₁ : 1 < √x
⊢ IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log t) 2) volume 2 √x

Tactic:
apply intervalIntegrable_one_div_log_sq

Premises used: Chebyshev.intervalIntegrable_one_div_log_sq
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
hbc : 1 < √x
hbc₁ : 1 < x
⊢ IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log t) 2) volume (√x) x

Tactic:
apply intervalIntegrable_one_div_log_sq

Premises used: Chebyshev.intervalIntegrable_one_div_log_sq
-- Module: Mathlib.NumberTheory.Chebyshev
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
linarith₁ : x ≤ 1 → GT.gt (α := ℝ) 3 0
⊢ 1 < x

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
apply : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2 * √x) fun (x : ℝ) ↦ x
apply₁ : ∀ᶠ (x : ℝ) in atTop, HPow.hPow (β := ℕ) (log x) 2 ≠ 0
⊢ IsLittleO (F := ℝ) atTop Real.sqrt fun (x : ℝ) ↦ x / HPow.hPow (β := ℕ) (log x) 2

Tactic:
apply isLittleO_mul_iff_isLittleO_div _ |>.mp

Premises used: Iff.mp, Asymptotics.isLittleO_mul_iff_isLittleO_div
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
arg : fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2 * √x
| IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2 * √x) fun (x : ℝ) ↦ x

Tactic:
arg 2
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
h : ∀ (x : ℝ), HPow.hPow (β := ℕ) (log x) 2 * √x
| fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2 * √x

Tactic:
ext
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : √x * HPow.hPow (β := ℕ) (log x) 2
| HPow.hPow (β := ℕ) (log x) 2 * √x

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
h : ∀ (x : ℝ), √x * HPow.hPow (β := ℕ) (log x) 2
| IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2 * √x) fun (x : ℝ) ↦ x

Tactic:
arg 2; ext; rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
conv : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ √x * HPow.hPow (β := ℕ) (log x) 2) fun (x : ℝ) ↦ x
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2 * √x) fun (x : ℝ) ↦ x

Tactic:
conv => arg 2; ext; rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
apply : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2) fun (x : ℝ) ↦ x / √x
apply₁ : ∀ᶠ (x : ℝ) in atTop, √x ≠ 0
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ √x * HPow.hPow (β := ℕ) (log x) 2) fun (x : ℝ) ↦ x

Tactic:
apply isLittleO_mul_iff_isLittleO_div _ |>.mpr

Premises used: Iff.mpr, Asymptotics.isLittleO_mul_iff_isLittleO_div
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
simp_rw : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℝ) (log x) 2) fun (x : ℝ) ↦ x ^ (1 / 2)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2) fun (x : ℝ) ↦ x / √x

Tactic:
simp_rw [div_sqrt, sqrt_eq_rpow, ← rpow_two]

Premises used: Real.div_sqrt, Real.rpow_two, Real.sqrt_eq_rpow
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
⊢ 0 < 1 / 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℝ) (log x) 2) fun (x : ℝ) ↦ x ^ (1 / 2)

Tactic:
apply isLittleO_log_rpow_rpow_atTop _ (by norm_num)

Premises used: isLittleO_log_rpow_rpow_atTop
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 < x
⊢ √x ≠ 0

Tactic:
sqrt_ne_zero'.mpr hx

Premises used: Iff.mpr, Real.sqrt_ne_zero'
-- Module: Mathlib.NumberTheory.Chebyshev
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
h₁ h₂ : ∀ (x : ℝ) (hx : 0 < x), √x ≠ 0
⊢ ∀ᶠ (x : ℝ) in atTop, √x ≠ 0

Tactic:
filter_upwards [eventually_gt_atTop 0] with x hx using sqrt_ne_zero'.mpr hx

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 1 < x → HPow.hPow (β := ℕ) (log x) 2 ≠ 0
⊢ 1 < x → HPow.hPow (β := ℕ) (log x) 2 ≠ 0

Tactic:
_
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
h : ∀ (x : ℝ), 1 < x → HPow.hPow (β := ℕ) (log x) 2 ≠ 0
⊢ ∀ᶠ (x : ℝ) in atTop, HPow.hPow (β := ℕ) (log x) 2 ≠ 0

Tactic:
filter_upwards [eventually_gt_atTop 1] with x _

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 1 < x
apply : x ≠ 0
apply₁ : x ≠ 1
apply₂ : x ≠ -1
⊢ HPow.hPow (β := ℕ) (log x) 2 ≠ 0

Tactic:
apply pow_ne_zero _ <| log_ne_zero.mpr ⟨_, _, _⟩

Premises used: Iff.mpr, pow_ne_zero, And.intro, Real.log_ne_zero
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 1 < x
linarith : x = 0 → -1 + (1 - x) + (x - 0) = 0
⊢ x ≠ 0

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 1 < x
linarith : x = 1 → 1 - x + (x - 1) = 0
⊢ x ≠ 1

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 1 < x
linarith : x = -1 → HMul.hMul (α := ℝ) 2 (-1) + (1 - x) + (x - -1) = 0
linarith₁ : x = -1 → GT.gt (α := ℝ) 2 0
⊢ x ≠ -1

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
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
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
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2) fun (x : ℝ) ↦
    x / HPow.hPow (β := ℕ) (log x) 2

Tactic:
trans (fun x ↦ 4 * x / log x ^ 2 + √x / log 2 ^ 2)

Premises used: HMul.hMul, HDiv.hDiv, Real.log, HPow.hPow, HAdd.hAdd, Real.sqrt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
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‖
⊢ 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:
apply IsBigO.of_bound'

Premises used: Asymptotics.IsBigO.of_bound'
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
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‖
⊢ ∀ᶠ (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:
filter_upwards [eventually_ge_atTop 4] with x hx

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 4 ≤ x
linarith : x < 2 → HMul.hMul (α := ℝ) 2 (-1) + (4 - x) + (x - 2) = 0
linarith₁ : x < 2 → GT.gt (α := ℝ) 2 0
⊢ 2 ≤ x

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
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‖
⊢ 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 le_trans <| intervalIntegral.abs_integral_le_integral_abs (by linarith)

Premises used: intervalIntegral.abs_integral_le_integral_abs, le_trans
-- Module: Mathlib.NumberTheory.Chebyshev
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‖
h₁ :
  Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ |1 / HPow.hPow (β := ℕ) (log x) 2|) (fun (t : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log t) 2)
    (Set.uIcc 2 x)
⊢ ∫ (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))]

Premises used: intervalIntegral.integral_congr
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 4 ≤ x
h : 0 ≤ 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‖

Tactic:
grw [integral_one_div_log_sq_le_explicit hx, norm_of_nonneg]

Premises used: _private.0.Chebyshev.integral_one_div_log_sq_le_explicit, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 4 ≤ x
⊢ 0 ≤ 4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 4 ≤ x
t : ℝ
ht : t ∈ Set.uIcc 2 x
⊢ Eq (α := ℝ) ((fun (x : ℝ) ↦ |1 / HPow.hPow (β := ℕ) (log x) 2|) t)
    ((fun (t : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log t) 2) t)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Chebyshev
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

Tactic:
IsBigO.add ?_ ?_

Premises used: Asymptotics.IsBigO.add
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
refine_1 :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ 4 * x / HPow.hPow (β := ℕ) (log x) 2) fun (x : ℝ) ↦
    x / HPow.hPow (β := ℕ) (log x) 2
refine_2 :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ √x / HPow.hPow (β := ℕ) (log 2) 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

Tactic:
refine IsBigO.add ?_ ?_

Premises used: Asymptotics.IsBigO.add
-- Module: Mathlib.NumberTheory.Chebyshev
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) fun (x : ℝ) ↦
    x / HPow.hPow (β := ℕ) (log x) 2

Tactic:
simp_rw [mul_div_assoc]

Premises used: mul_div_assoc
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ 4 * (x / HPow.hPow (β := ℕ) (log x) 2)) fun (x : ℝ) ↦
    x / HPow.hPow (β := ℕ) (log x) 2

Tactic:
apply isBigO_const_mul_self

Premises used: Asymptotics.isBigO_const_mul_self
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
arg : fun (x : ℝ) ↦ √x / HPow.hPow (β := ℕ) (log 2) 2
| IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ √x / HPow.hPow (β := ℕ) (log 2) 2) fun (x : ℝ) ↦
    x / HPow.hPow (β := ℕ) (log x) 2

Tactic:
arg 2
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
h : ∀ (x : ℝ), √x / HPow.hPow (β := ℕ) (log 2) 2
| fun (x : ℝ) ↦ √x / HPow.hPow (β := ℕ) (log 2) 2

Tactic:
ext
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 1 / HPow.hPow (β := ℕ) (log 2) 2 * √x
| √x / HPow.hPow (β := ℕ) (log 2) 2

Tactic:
rw [← mul_one_div, mul_comm]

Premises used: mul_one_div, mul_comm
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
h : ∀ (x : ℝ), 1 / HPow.hPow (β := ℕ) (log 2) 2 * √x
| IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ √x / HPow.hPow (β := ℕ) (log 2) 2) fun (x : ℝ) ↦
    x / HPow.hPow (β := ℕ) (log x) 2

Tactic:
arg 2; ext; rw [← mul_one_div, mul_comm]

Premises used: mul_one_div, mul_comm
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
refine_2 :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log 2) 2 * √x) fun (x : ℝ) ↦
    x / HPow.hPow (β := ℕ) (log x) 2
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ √x / HPow.hPow (β := ℕ) (log 2) 2) fun (x : ℝ) ↦
    x / HPow.hPow (β := ℕ) (log x) 2

Tactic:
conv => arg 2; ext; rw [← mul_one_div, mul_comm]

Premises used: mul_one_div, mul_comm
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log 2) 2 * √x) fun (x : ℝ) ↦
    x / HPow.hPow (β := ℕ) (log x) 2

Tactic:
apply IsBigO.const_mul_left sqrt_isLittleO.isBigO

Premises used: Asymptotics.IsBigO.const_mul_left, _private.0.Chebyshev.sqrt_isLittleO, Asymptotics.IsLittleO.isBigO
-- Module: Mathlib.NumberTheory.Chebyshev
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

Tactic:
(IsBigO.of_bound (log 4) ?_).trans integral_one_div_log_sq_isBigO

Premises used: Chebyshev.integral_one_div_log_sq_isBigO, Real.log, Asymptotics.IsBigO.trans, Asymptotics.IsBigO.of_bound, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
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)
⊢ 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

Tactic:
refine (IsBigO.of_bound (log 4) ?_).trans integral_one_div_log_sq_isBigO

Premises used: Chebyshev.integral_one_div_log_sq_isBigO, Real.log, Asymptotics.IsBigO.trans, Asymptotics.IsBigO.of_bound, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h :
  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)
⊢ 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:
_
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
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)
⊢ ∀ᶠ (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:
filter_upwards [eventually_ge_atTop 4] with x _

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 4 ≤ x
linarith : x < 2 → HMul.hMul (α := ℝ) 2 (-1) + (4 - x) + (x - 2) = 0
linarith₁ : x < 2 → GT.gt (α := ℝ) 2 0
⊢ 2 ≤ x

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 4 ≤ x
rw : LE.le (α := ℝ) 0 (∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2)
⊢ ∫ (x : ℝ) in 2..x, log 4 * (1 / HPow.hPow (β := ℕ) (log x) 2) =
    log 4 * |∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2|

Tactic:
rw [intervalIntegral.integral_const_mul, abs_of_nonneg]

Premises used: abs_of_nonneg, intervalIntegral.integral_const_mul
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 4 ≤ x
u : ℝ
h_1 : u ∈ Set.Icc 2 x
⊢ 0 ≤ 1 / HPow.hPow (β := ℕ) (log u) 2

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 4 ≤ x
⊢ LE.le (α := ℝ) 0 (∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2)

Tactic:
exact intervalIntegral.integral_nonneg (by linarith) fun u _ ↦ by positivity

Premises used: intervalIntegral.integral_nonneg
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 4 ≤ x
calc : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ |θ x / (x * HPow.hPow (β := ℕ) (log x) 2)|) volume 2 x
calc₁ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log 4 * (1 / HPow.hPow (β := ℕ) (log x) 2)) volume 2 x
calc₂ :
  ∀ t ∈ Set.Icc 2 x,
    ∀ (ht : 2 ≤ t), t ≤ x → |θ t / (t * HPow.hPow (β := ℕ) (log t) 2)| ≤ log 4 * (1 / HPow.hPow (β := ℕ) (log t) 2)
⊢ |∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)| ≤
    log 4 * |∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2|

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

Premises used: HMul.hMul, intervalIntegral.integral_mono_on, HDiv.hDiv, Real.log, intervalIntegral.abs_integral_le_integral_abs, Chebyshev.theta, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 4 ≤ x
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ |θ x / (x * HPow.hPow (β := ℕ) (log x) 2)|) volume 2 x

Tactic:
(intervalIntegrable_iff.mpr ?_).abs

Premises used: Iff.mpr, intervalIntegrable_iff, IntervalIntegrable.abs
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 4 ≤ x
refine :
  IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ θ x / (x * HPow.hPow (β := ℕ) (log x) 2)) (Set.uIoc 2 x)
    volume
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ |θ x / (x * HPow.hPow (β := ℕ) (log x) 2)|) volume 2 x

Tactic:
refine (intervalIntegrable_iff.mpr ?_).abs

Premises used: Iff.mpr, intervalIntegrable_iff, IntervalIntegrable.abs
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 4 ≤ x
rw :
  IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ θ x / (x * HPow.hPow (β := ℕ) (log x) 2)) (Set.Icc 2 x)
    volume
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ θ x / (x * HPow.hPow (β := ℕ) (log x) 2)) (Set.uIoc 2 x)
    volume

Tactic:
rw [Set.uIoc_of_le (by linarith), ← integrableOn_Icc_iff_integrableOn_Ioc]

Premises used: integrableOn_Icc_iff_integrableOn_Ioc, Set.uIoc_of_le
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 4 ≤ x
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ θ x / (x * HPow.hPow (β := ℕ) (log x) 2)) (Set.Icc 2 x)
    volume

Tactic:
integrableOn_theta_div_id_mul_log_sq x

Premises used: Chebyshev.integrableOn_theta_div_id_mul_log_sq
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 4 ≤ x
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ θ x / (x * HPow.hPow (β := ℕ) (log x) 2)) (Set.Icc 2 x)
    volume

Tactic:
exact integrableOn_theta_div_id_mul_log_sq x

Premises used: Chebyshev.integrableOn_theta_div_id_mul_log_sq
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 4 ≤ x
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ |θ x / (x * HPow.hPow (β := ℕ) (log x) 2)|) volume 2 x

Tactic:
case hf =>
    refine (intervalIntegrable_iff.mpr ?_).abs
    rw [Set.uIoc_of_le (by linarith), ← integrableOn_Icc_iff_integrableOn_Ioc]
    exact integrableOn_theta_div_id_mul_log_sq x

Premises used: Iff.mpr, intervalIntegrable_iff, Chebyshev.integrableOn_theta_div_id_mul_log_sq, IntervalIntegrable.abs, integrableOn_Icc_iff_integrableOn_Ioc, Set.uIoc_of_le
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 4 ≤ x
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log 4 * (1 / HPow.hPow (β := ℕ) (log x) 2)) volume 2 x

Tactic:
(intervalIntegrable_one_div_log_sq ?_ ?_).const_mul _

Premises used: Chebyshev.intervalIntegrable_one_div_log_sq, IntervalIntegrable.const_mul
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 4 ≤ x
refine_1 : LT.lt (α := ℝ) 1 2
refine_2 : 1 < x
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log 4 * (1 / HPow.hPow (β := ℕ) (log x) 2)) volume 2 x

Tactic:
refine (intervalIntegrable_one_div_log_sq ?_ ?_).const_mul _

Premises used: Chebyshev.intervalIntegrable_one_div_log_sq, IntervalIntegrable.const_mul
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 4 ≤ x
linarith : LE.le (α := ℝ) 2 1 → -1 + HSub.hSub (α := ℝ) 2 1 = 0
⊢ LT.lt (α := ℝ) 1 2

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 4 ≤ x
linarith : x ≤ 1 → HMul.hMul (α := ℝ) 3 (-1) + (4 - x) + (x - 1) = 0
linarith₁ : x ≤ 1 → GT.gt (α := ℝ) 3 0
⊢ 1 < x

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 4 ≤ x
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log 4 * (1 / HPow.hPow (β := ℕ) (log x) 2)) volume 2 x

Tactic:
case hg =>
    refine (intervalIntegrable_one_div_log_sq ?_ ?_).const_mul _ <;> linarith

Premises used: Chebyshev.intervalIntegrable_one_div_log_sq, IntervalIntegrable.const_mul
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 4 ≤ x
t : ℝ
h_1 : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right : t ≤ x
positivity positivity₁ positivity₂ positivity₃ : 0 ≤ θ t → 0 ≤ θ t / (t * HPow.hPow (β := ℕ) (log t) 2)
⊢ 0 ≤ θ t / (t * HPow.hPow (β := ℕ) (log t) 2)

Tactic:
positivity [theta_nonneg t]

Premises used: Chebyshev.theta_nonneg
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 4 ≤ x
t : ℝ
h_1 : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right : t ≤ x
linarith : t < 0 → HMul.hMul (α := ℝ) 2 (-1) + (2 - t) + (t - 0) = 0
linarith₁ : t < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ t

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 4 ≤ x
t : ℝ
h_1 : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right : t ≤ x
h₁ : 0 ≤ t * HPow.hPow (β := ℕ) (log t) 2
grw grw₁ : log 4 * t / (t * HPow.hPow (β := ℕ) (log t) 2) ≤ log 4 * t / (t * HPow.hPow (β := ℕ) (log t) 2)
⊢ θ t / (t * HPow.hPow (β := ℕ) (log t) 2) ≤ log 4 * t / (t * HPow.hPow (β := ℕ) (log t) 2)

Tactic:
grw [theta_le_log4_mul_x (by linarith)]

Premises used: Chebyshev.theta_le_log4_mul_x
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 4 ≤ x
t : ℝ
h_1 : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right : t ≤ x
⊢ log 4 * t / (t * HPow.hPow (β := ℕ) (log t) 2) = log 4 * (1 / HPow.hPow (β := ℕ) (log t) 2)

Tactic:
field
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 4 ≤ x
t : ℝ
h_1 : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right : t ≤ x
calc : θ t / (t * HPow.hPow (β := ℕ) (log t) 2) ≤ log 4 * t / (t * HPow.hPow (β := ℕ) (log t) 2)
calc₁ : log 4 * t / (t * HPow.hPow (β := ℕ) (log t) 2) = log 4 * (1 / HPow.hPow (β := ℕ) (log t) 2)
⊢ |θ t / (t * HPow.hPow (β := ℕ) (log t) 2)| ≤ log 4 * (1 / HPow.hPow (β := ℕ) (log t) 2)

Tactic:
calc |θ t / (t * log t ^ 2)|
    _ = θ t / (t * log t ^ 2) := abs_of_nonneg (by positivity [theta_nonneg t])
    _ ≤ log 4 * t / (t * log t ^ 2) := by grw [theta_le_log4_mul_x (by linarith)]
    _ = log 4 * (1 / log t ^ 2) := by field

Premises used: HMul.hMul, HDiv.hDiv, Real.log, Chebyshev.theta, HPow.hPow, abs_of_nonneg, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 4 ≤ x
t : ℝ
h_1 : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right : t ≤ x
case : θ t / (t * HPow.hPow (β := ℕ) (log t) 2) ≤ log 4 * t / (t * HPow.hPow (β := ℕ) (log t) 2)
case₁ : log 4 * t / (t * HPow.hPow (β := ℕ) (log t) 2) = log 4 * (1 / HPow.hPow (β := ℕ) (log t) 2)
⊢ |θ t / (t * HPow.hPow (β := ℕ) (log t) 2)| ≤ log 4 * (1 / HPow.hPow (β := ℕ) (log t) 2)

Tactic:
case hh =>
    calc |θ t / (t * log t ^ 2)|
    _ = θ t / (t * log t ^ 2) := abs_of_nonneg (by positivity [theta_nonneg t])
    _ ≤ log 4 * t / (t * log t ^ 2) := by grw [theta_le_log4_mul_x (by linarith)]
    _ = log 4 * (1 / log t ^ 2) := by field

Premises used: HMul.hMul, HDiv.hDiv, Real.log, Chebyshev.theta, HPow.hPow, abs_of_nonneg, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2))
    fun (x : ℝ) ↦ x / log x

Tactic:
integral_theta_div_log_sq_isBigO.trans_isLittleO ?_

Premises used: Chebyshev.integral_theta_div_log_sq_isBigO, Asymptotics.IsBigO.trans_isLittleO
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
refine : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x / HPow.hPow (β := ℕ) (log x) 2) fun (x : ℝ) ↦ x / log x
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2))
    fun (x : ℝ) ↦ x / log x

Tactic:
refine integral_theta_div_log_sq_isBigO.trans_isLittleO ?_

Premises used: Chebyshev.integral_theta_div_log_sq_isBigO, Asymptotics.IsBigO.trans_isLittleO
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
⊢ ∀ᶠ (x : ℝ) in atTop, x / log x = 0 → x / HPow.hPow (β := ℕ) (log x) 2 = 0

Tactic:
simp