awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this_1 : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
this : (Finset.Icc 1 (2 * n).sqrt).card = (2 * n).sqrt
x : ℕ
hx : x ∈ {x ∈ S | x ≤ (2 * n).sqrt}
h1 : x ∈ S
h2 : x ≤ (2 * n).sqrt
⊢ x ∈ Finset.Icc 1 (2 * n).sqrt

Tactic:
exact Finset.mem_Icc.mpr ⟨(Finset.mem_filter.1 h1).2.one_lt.le, h2⟩

Premises used: Iff.mpr, Nat.Prime.one_lt, Finset.mem_Icc, LT.lt.le, And.right, And.intro, Iff.mp, Finset.mem_filter
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
⊢ ∏ x ∈ S with ¬x ≤ (2 * n).sqrt, f x ≤ HPow.hPow (α := ℕ) 4 (2 * n / 3)

Tactic:
le_trans ?_ (primorial_le_four_pow (2 * n / 3))

Premises used: HMul.hMul, primorial_le_four_pow, HDiv.hDiv, OfNat.ofNat, le_trans
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
h₂ : ∏ x ∈ S with ¬x ≤ (2 * n).sqrt, f x ≤ primorial (2 * n / 3)
⊢ ∏ x ∈ S with ¬x ≤ (2 * n).sqrt, f x ≤ HPow.hPow (α := ℕ) 4 (2 * n / 3)

Tactic:
refine le_trans ?_ (primorial_le_four_pow (2 * n / 3))

Premises used: HMul.hMul, primorial_le_four_pow, HDiv.hDiv, OfNat.ofNat, le_trans
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
⊢ ∏ x ∈ S with ¬x ≤ (2 * n).sqrt, f x ≤ primorial (2 * n / 3)

Tactic:
(Finset.prod_le_prod' fun p hp => (?_ : f p ≤ p)).trans ?_

Premises used: Finset.prod_le_prod', LE.le.trans
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
h₂ : ∀ (p : ℕ) (hp : p ∈ {x ∈ S | ¬x ≤ (2 * n).sqrt}), f p ≤ p
h₃ : ∏ i ∈ S with ¬i ≤ (2 * n).sqrt, i ≤ primorial (2 * n / 3)
⊢ ∏ x ∈ S with ¬x ≤ (2 * n).sqrt, f x ≤ primorial (2 * n / 3)

Tactic:
refine (Finset.prod_le_prod' fun p hp => (?_ : f p ≤ p)).trans ?_

Premises used: Finset.prod_le_prod', LE.le.trans
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
p : ℕ
hp : p ∈ {x ∈ S | ¬x ≤ (2 * n).sqrt}
⊢ p ∈ S

Tactic:
obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hp

Premises used: Iff.mp, Finset.mem_filter
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
p : ℕ
hp : p ∈ {x ∈ S | ¬x ≤ (2 * n).sqrt}
h1 : p ∈ S
⊢ ¬p ≤ (2 * n).sqrt

Tactic:
obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hp

Premises used: Iff.mp, Finset.mem_filter
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
p : ℕ
hp : p ∈ {x ∈ S | ¬x ≤ (2 * n).sqrt}
h1 : p ∈ S
h2 : ¬p ≤ (2 * n).sqrt
⊢ f p ≤ p

Tactic:
(pow_right_mono₀ (Finset.mem_filter.1 h1).2.one_lt.le ?_).trans (pow_one p).le

Premises used: Nat.Prime.one_lt, LT.lt.le, Eq.le, And.right, pow_right_mono₀, pow_one, Iff.mp, Finset.mem_filter, LE.le.trans
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
p : ℕ
hp : p ∈ {x ∈ S | ¬x ≤ (2 * n).sqrt}
h1 : p ∈ S
h2 : ¬p ≤ (2 * n).sqrt
h₂ : LE.le (α := ℕ) ((n.centralBinom.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
⊢ f p ≤ p

Tactic:
refine (pow_right_mono₀ (Finset.mem_filter.1 h1).2.one_lt.le ?_).trans (pow_one p).le

Premises used: Nat.Prime.one_lt, LT.lt.le, Eq.le, And.right, pow_right_mono₀, pow_one, Iff.mp, Finset.mem_filter, LE.le.trans
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
p : ℕ
hp : p ∈ {x ∈ S | ¬x ≤ (2 * n).sqrt}
h1 : p ∈ S
h2 : ¬p ≤ (2 * n).sqrt
⊢ LE.le (α := ℕ) ((n.centralBinom.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)

Tactic:
Nat.factorization_choose_le_one (sqrt_lt'.mp <| not_le.1 h2)

Premises used: not_le, Nat.factorization_choose_le_one, Nat.centralBinom, Nat.sqrt_lt', Iff.mp
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
p : ℕ
hp : p ∈ {x ∈ S | ¬x ≤ (2 * n).sqrt}
h1 : p ∈ S
h2 : ¬p ≤ (2 * n).sqrt
⊢ LE.le (α := ℕ) ((n.centralBinom.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)

Tactic:
exact Nat.factorization_choose_le_one (sqrt_lt'.mp <| not_le.1 h2)

Premises used: not_le, Nat.factorization_choose_le_one, Nat.sqrt_lt', Iff.mp
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
⊢ ∏ i ∈ S with ¬i ≤ (2 * n).sqrt, i ≤ primorial (2 * n / 3)

Tactic:
Finset.prod_le_prod_of_subset_of_one_le' (Finset.filter_subset _ _) ?_

Premises used: Finset.filter_subset, Finset.prod_le_prod_of_subset_of_one_le', primorial
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
h₂ : ∀ i ∈ {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}, i ∉ {x ∈ S | ¬x ≤ (2 * n).sqrt} → 1 ≤ i
⊢ ∏ i ∈ S with ¬i ≤ (2 * n).sqrt, i ≤ primorial (2 * n / 3)

Tactic:
refine Finset.prod_le_prod_of_subset_of_one_le' (Finset.filter_subset _ _) ?_

Premises used: Finset.filter_subset, Finset.prod_le_prod_of_subset_of_one_le'
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
⊢ ∀ i ∈ {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}, i ∉ {x ∈ S | ¬x ≤ (2 * n).sqrt} → 1 ≤ i

Tactic:
fun p hp _ => (Finset.mem_filter.1 hp).2.one_lt.le

Premises used: Nat.Prime.one_lt, LT.lt.le, And.right, Iff.mp, Finset.mem_filter
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
⊢ ∀ i ∈ {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}, i ∉ {x ∈ S | ¬x ≤ (2 * n).sqrt} → 1 ≤ i

Tactic:
exact fun p hp _ => (Finset.mem_filter.1 hp).2.one_lt.le
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 512 ≤ n
⊢ LE.le (α := ℕ) 4 512

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 512 ≤ n
⊢ HPow.hPow (α := ℕ) 4 n < n * n.centralBinom

Tactic:
have no_prime : 4 ^ n < n * n.centralBinom :=
    Nat.four_pow_lt_mul_centralBinom n (le_trans (by norm_num1) n_large)
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 512 ≤ n
no_prime : HPow.hPow (α := ℕ) 4 n < n * n.centralBinom
contrapose! : ∀ (no_prime : ∀ (p : ℕ) (_ : Prime p) (_ : n < p), 2 * n < p), n * n.centralBinom ≤ HPow.hPow (α := ℕ) 4 n
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≤ 2 * n

Tactic:
contrapose! no_prime
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 512 ≤ n
no_prime : ∀ (p : ℕ) (_ : Prime p) (_ : n < p), 2 * n < p
⊢ LT.lt (α := ℕ) 2 512

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 512 ≤ n
no_prime : ∀ (p : ℕ) (_ : Prime p) (_ : n < p), 2 * n < p
⊢ n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3)

Tactic:
have : n.centralBinom ≤ (2 * n) ^ sqrt (2 * n) * 4 ^ (2 * n / 3) :=
    centralBinom_le_of_no_bertrand_prime n (lt_of_lt_of_le (by norm_num1) n_large) no_prime
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 512 ≤ n
no_prime : ∀ (p : ℕ) (_ : Prime p) (_ : n < p), 2 * n < p
this : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3)
grw : n * ((2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3)) ≤ HPow.hPow (α := ℕ) 4 n
grw₁ : n * (2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3) ≤ HPow.hPow (α := ℕ) 4 n
grw₂ grw₃ : HPow.hPow (α := ℕ) 4 n ≤ HPow.hPow (α := ℕ) 4 n
⊢ n * n.centralBinom ≤ HPow.hPow (α := ℕ) 4 n

Tactic:
grw [this, ← mul_assoc, bertrand_main_inequality n_large]

Premises used: mul_assoc, bertrand_main_inequality
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n q p : ℕ
prime_p : Prime p
covering : p ≤ 2 * q
H : n < q → ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≤ 2 * n
hn : n < p
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≤ 2 * n

Tactic:
grind
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
hn0 : n ≠ 0
inl : ∀ (h : 511 < n), ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≤ 2 * n
inr : ∀ (h : n ≤ 511), ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≤ 2 * n
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≤ 2 * n

Tactic:
rcases lt_or_ge 511 n with h | h

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
hn0 : n ≠ 0
h : 511 < n
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≤ 2 * n

Tactic:
exists_prime_lt_and_le_two_mul_eventually n h

Premises used: Nat.exists_prime_lt_and_le_two_mul_eventually
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
hn0 : n ≠ 0
h : 511 < n
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≤ 2 * n

Tactic:
exact exists_prime_lt_and_le_two_mul_eventually n h

Premises used: Nat.exists_prime_lt_and_le_two_mul_eventually
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
hn0 : n ≠ 0
h : n ≤ 511
⊢ LT.lt (α := ℕ) 511 521

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
hn0 : n ≠ 0
h : n ≤ 511
⊢ n < 521

Tactic:
replace h : n < 521 := h.trans_lt (by norm_num1)
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
hn0 : n ≠ 0
h : n < 521
inr : ∀ (h : n < 521), ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≤ 2 * n
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≤ 2 * n

Tactic:
revert h
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
x_1 : ℕ
h : x_1 ∈ Ioc 0 ⌊x⌋₊
⊢ LE.le (α := ℝ) (0 : ℝ) ((Λ : (a : ℕ) → ℝ) x_1 : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
x_1 : ℕ
h : x_1 ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}
⊢ LE.le (α := ℝ) 1 (↑x_1 : ℝ)

Tactic:
aesop
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hy : 2 ≤ x
⊢ 0 < θ x

Tactic:
sum_pos (fun n hn ↦ log_pos ?_) ⟨2, ?_⟩

Premises used: Finset.sum_pos, Real.log_pos, Chebyshev.theta, Exists.intro, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hy : 2 ≤ x
refine_1 : ∀ (n : ℕ) (hn : n ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}), LT.lt (α := ℝ) 1 (↑n : ℝ)
refine_2 : 2 ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}
⊢ 0 < θ x

Tactic:
refine sum_pos (fun n hn ↦ log_pos ?_) ⟨2, ?_⟩

Premises used: Finset.sum_pos, Real.log_pos, Exists.intro, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hy : 2 ≤ x
n : ℕ
hn : n ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}
⊢ n ∈ Ioc 0 ⌊x⌋₊ ∧ Nat.Prime n

Tactic:
simp only [mem_filter] at hn

Premises used: Finset.mem_filter
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hy : 2 ≤ x
n : ℕ
hn : n ∈ Ioc 0 ⌊x⌋₊ ∧ Nat.Prime n
⊢ LT.lt (α := ℝ) 1 (↑n : ℝ)

Tactic:
exact_mod_cast hn.2.one_lt

Premises used: Nat.Prime.one_lt, And.right
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hy : 2 ≤ x
⊢ 0 ≤ x

Tactic:
grind
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hy : 2 ≤ x
⊢ 0 ≤ x

Tactic:
have : 0 ≤ x := by grind
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hy : 2 ≤ x
this : 0 ≤ x
⊢ 2 ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}

Tactic:
simpa using ⟨(le_floor_iff this).2 hy, prime_two⟩
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
rw :
  ∑ n ∈ Ioc 0 ⌊x⌋₊, (Λ : (a : ℕ) → ℝ) n =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((Λ : (a : ℕ) → ℝ) 0 : ℝ) (∑ x ∈ Ioc 0 ⌊x⌋₊, (Λ : (a : ℕ) → ℝ) x : ℝ)
rw₁ : 0 ≤ ⌊x⌋₊
⊢ ψ x = ∑ n ∈ Icc 0 ⌊x⌋₊, (Λ : (a : ℕ) → ℝ) n

Tactic:
rw [psi, ← add_sum_Ioc_eq_sum_Icc]

Premises used: Finset.add_sum_Ioc_eq_sum_Icc, Chebyshev.psi
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
⊢ ∑ n ∈ Ioc 0 ⌊x⌋₊, (Λ : (a : ℕ) → ℝ) n =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((Λ : (a : ℕ) → ℝ) 0 : ℝ) (∑ x ∈ Ioc 0 ⌊x⌋₊, (Λ : (a : ℕ) → ℝ) x : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
⊢ 0 ≤ ⌊x⌋₊

Tactic:
simp
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
rw :
  (∑ a ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime a then log (↑a : ℝ) else 0) =
    (if Nat.Prime 0 then log (↑0 : ℝ) else 0) + ∑ x ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime x then log (↑x : ℝ) else 0
rw₁ : 0 ≤ ⌊x⌋₊
⊢ θ x = ∑ p ∈ Icc 0 ⌊x⌋₊ with Nat.Prime p, log (↑p : ℝ)

Tactic:
rw [theta, sum_filter, sum_filter, ← add_sum_Ioc_eq_sum_Icc]

Premises used: Finset.add_sum_Ioc_eq_sum_Icc, Chebyshev.theta, Finset.sum_filter
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
⊢ (∑ a ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime a then log (↑a : ℝ) else 0) =
    (if Nat.Prime 0 then log (↑0 : ℝ) else 0) + ∑ x ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime x then log (↑x : ℝ) else 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
⊢ θ x = ∑ p ∈ ⌊x⌋₊.primesLE, log (↑p : ℝ)

Tactic:
simp [theta_eq_sum_Icc, primesLE_eq_filter_Icc_zero]

Premises used: Nat.primesLE_eq_filter_Icc_zero, Chebyshev.theta_eq_sum_Icc
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ θ (↑n : ℝ) = ∑ p ∈ n.primesLE, log (↑p : ℝ)

Tactic:
simp [theta_eq_sum_primesLE]

Premises used: Chebyshev.theta_eq_sum_primesLE
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : x < 2
apply : ∀ (n : ℕ) (hn : n ∈ Ioc 0 ⌊x⌋₊), Eq (α := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ)
⊢ ψ x = 0

Tactic:
apply sum_eq_zero fun n hn ↦ ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : n ∈ Ioc 0 ⌊x⌋₊
⊢ 0 < n ∧ n ≤ ⌊x⌋₊

Tactic:
simp only [mem_Ioc] at hn

Premises used: Finset.mem_Ioc
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : 0 < n ∧ n ≤ ⌊x⌋₊
⊢ Eq (α := ℝ) ((Λ : (a : ℕ) → ℝ) 1 : ℝ) (0 : ℝ)

Tactic:
vonMangoldt_apply_one

Premises used: ArithmeticFunction.vonMangoldt_apply_one
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : 0 < n ∧ n ≤ ⌊x⌋₊
h : n = 1
⊢ Eq (α := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ)

Tactic:
convert! vonMangoldt_apply_one

Premises used: ArithmeticFunction.vonMangoldt_apply_one
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : 0 < n ∧ n ≤ ⌊x⌋₊
⊢ LT.lt (α := ℝ) (↑n : ℝ) 2

Tactic:
have := lt_of_le_of_lt (le_floor_iff' hn.1.ne' |>.mp hn.2) hx
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : 0 < n ∧ n ≤ ⌊x⌋₊
this : LT.lt (α := ℝ) (↑n : ℝ) 2
⊢ n < 2

Tactic:
norm_cast at this
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : 0 < n ∧ n ≤ ⌊x⌋₊
this : n < 2
linarith : n < 1 → -1 + (HAdd.hAdd (α := ℤ) 0 1 - (↑n : ℤ)) + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1) = 0
linarith₁ : 1 < n → -1 + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 2) + (HAdd.hAdd (α := ℤ) 1 1 - (↑n : ℤ)) = 0
⊢ n = 1

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
⊢ ψ 0 = 0

Tactic:
psi_eq_zero_of_lt_two zero_lt_two

Premises used: Chebyshev.psi_eq_zero_of_lt_two, zero_lt_two
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
⊢ ψ 1 = 0

Tactic:
psi_eq_zero_of_lt_two one_lt_two

Premises used: Chebyshev.psi_eq_zero_of_lt_two, one_lt_two
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : x < 2
apply : ∀ (n : ℕ) (hn : n ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}), log (↑n : ℝ) = 0
⊢ θ x = 0

Tactic:
apply sum_eq_zero fun n hn ↦ ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : n ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}
⊢ log 1 = 0

Tactic:
log_one

Premises used: Real.log_one
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : n ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}
h : Eq (α := ℝ) (↑n : ℝ) 1
⊢ log (↑n : ℝ) = 0

Tactic:
convert! log_one

Premises used: Real.log_one
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : n ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}
⊢ (0 < n ∧ n ≤ ⌊x⌋₊) ∧ Nat.Prime n

Tactic:
simp only [mem_filter, mem_Ioc] at hn

Premises used: Finset.mem_filter, Finset.mem_Ioc
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : (0 < n ∧ n ≤ ⌊x⌋₊) ∧ Nat.Prime n
⊢ LT.lt (α := ℝ) (↑n : ℝ) 2

Tactic:
have := lt_of_le_of_lt (le_floor_iff' hn.1.1.ne' |>.mp hn.1.2) hx
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : (0 < n ∧ n ≤ ⌊x⌋₊) ∧ Nat.Prime n
this : LT.lt (α := ℝ) (↑n : ℝ) 2
h : ∀ (this : n < 2), n = 1
⊢ Eq (α := ℝ) (↑n : ℝ) 1

Tactic:
norm_cast at ⊢ this
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : (0 < n ∧ n ≤ ⌊x⌋₊) ∧ Nat.Prime n
this : n < 2
linarith : n < 1 → -1 + (HAdd.hAdd (α := ℤ) 0 1 - (↑n : ℤ)) + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1) = 0
linarith₁ : 1 < n → -1 + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 2) + (HAdd.hAdd (α := ℤ) 1 1 - (↑n : ℤ)) = 0
⊢ n = 1

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
⊢ θ 0 = 0

Tactic:
theta_eq_zero_of_lt_two zero_lt_two

Premises used: Chebyshev.theta_eq_zero_of_lt_two, zero_lt_two
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
⊢ θ 1 = 0

Tactic:
theta_eq_zero_of_lt_two one_lt_two

Premises used: Chebyshev.theta_eq_zero_of_lt_two, one_lt_two
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
rw rw₁ : Eq (α := ℝ) (∑ n ∈ Ioc 0 ⌊x⌋₊, (Λ : (a : ℕ) → ℝ) n) (∑ n ∈ Ioc 0 ⌊x⌋₊, (Λ : (a : ℕ) → ℝ) n)
⊢ Eq (α := ℝ) (∑ n ∈ Ioc 0 ⌊x⌋₊, (Λ : (a : ℕ) → ℝ) n) (∑ n ∈ Ioc 0 (floor (α := ℝ) (↑⌊x⌋₊ : ℝ)), (Λ : (a : ℕ) → ℝ) n)

Tactic:
rw [floor_natCast]

Premises used: Nat.floor_natCast
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
rw rw₁ : Eq (α := ℝ) (∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, log (↑p : ℝ)) (∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, log (↑p : ℝ))
⊢ Eq (α := ℝ) (∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, log (↑p : ℝ))
    (∑ p ∈ Ioc 0 (floor (α := ℝ) (↑⌊x⌋₊ : ℝ)) with Nat.Prime p, log (↑p : ℝ))

Tactic:
rw [floor_natCast]

Premises used: Nat.floor_natCast
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x y : ℝ
hxy : x ≤ y
h : Ioc 0 ⌊x⌋₊ ⊆ Ioc 0 ⌊y⌋₊
hf : ∀ i ∈ Ioc 0 ⌊y⌋₊, i ∉ Ioc 0 ⌊x⌋₊ → LE.le (α := ℝ) (0 : ℝ) ((Λ : (a : ℕ) → ℝ) i : ℝ)
⊢ ψ x ≤ ψ y

Tactic:
apply sum_le_sum_of_subset_of_nonneg

Premises used: Finset.sum_le_sum_of_subset_of_nonneg
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x y : ℝ
hxy : x ≤ y
⊢ LE.le (α := ℕ) 0 0

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x y : ℝ
hxy : x ≤ y
⊢ ⌊x⌋₊ ≤ ⌊y⌋₊

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x y : ℝ
hxy : x ≤ y
⊢ Ioc 0 ⌊x⌋₊ ⊆ Ioc 0 ⌊y⌋₊

Tactic:
exact Ioc_subset_Ioc (by rfl) (by gcongr)

Premises used: Finset.Ioc_subset_Ioc
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x y : ℝ
hxy : x ≤ y
⊢ ∀ i ∈ Ioc 0 ⌊y⌋₊, i ∉ Ioc 0 ⌊x⌋₊ → LE.le (α := ℝ) (0 : ℝ) ((Λ : (a : ℕ) → ℝ) i : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x y : ℝ
hxy : x ≤ y
h : {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p} ⊆ {p ∈ Ioc 0 ⌊y⌋₊ | Nat.Prime p}
hf : ∀ i ∈ {p ∈ Ioc 0 ⌊y⌋₊ | Nat.Prime p}, i ∉ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p} → 0 ≤ log (↑i : ℝ)
⊢ θ x ≤ θ y

Tactic:
apply sum_le_sum_of_subset_of_nonneg

Premises used: Finset.sum_le_sum_of_subset_of_nonneg
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x y : ℝ
hxy : x ≤ y
⊢ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p} ⊆ {p ∈ Ioc 0 ⌊y⌋₊ | Nat.Prime p}

Tactic:
exact filter_subset_filter _ <| Ioc_subset_Ioc_right (by gcongr)

Premises used: Finset.filter_subset_filter, Finset.Ioc_subset_Ioc_right
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x y : ℝ
hxy : x ≤ y
⊢ ∀ i ∈ {p ∈ Ioc 0 ⌊y⌋₊ | Nat.Prime p}, i ∉ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p} → 0 ≤ log (↑i : ℝ)

Tactic:
fun p _ _ ↦ log_natCast_nonneg p

Premises used: Real.log_natCast_nonneg
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x y : ℝ
hxy : x ≤ y
⊢ ∀ i ∈ {p ∈ Ioc 0 ⌊y⌋₊ | Nat.Prime p}, i ∉ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p} → 0 ≤ log (↑i : ℝ)

Tactic:
exact fun p _ _ ↦ log_natCast_nonneg p

Premises used: Real.log_natCast_nonneg
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
rw :
  Eq (α := ℝ) (∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, log (↑p : ℝ)) (∑ i ∈ range (⌊x⌋₊ + 1) with Nat.Prime i, log (↑i : ℝ))
⊢ ∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, log (↑p : ℝ) = log (↑(∏ p ∈ range (⌊x⌋₊ + 1) with Nat.Prime p, p) : ℝ)

Tactic:
rw [cast_prod, log_prod (fun p hp ↦ mod_cast (mem_filter.mp hp).2.pos.ne')]

Premises used: Real.log_prod, Nat.cast_prod
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
e_s : ∀ (p : ℕ), p ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p} ↔ p ∈ {p ∈ range (⌊x⌋₊ + 1) | Nat.Prime p}
⊢ Eq (α := ℝ) (∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, log (↑p : ℝ)) (∑ i ∈ range (⌊x⌋₊ + 1) with Nat.Prime i, log (↑i : ℝ))

Tactic:
congr 1 with p
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
p : ℕ
⊢ p ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p} ↔ p ∈ {p ∈ range (⌊x⌋₊ + 1) | Nat.Prime p}

Tactic:
simp_all [Prime.pos]

Premises used: Nat.Prime.pos
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 ≤ x
rw : log (↑(primorial ⌊x⌋₊) : ℝ) ≤ log 4 * x
⊢ θ x ≤ log 4 * x

Tactic:
rw [theta_eq_log_primorial]

Premises used: Chebyshev.theta_eq_log_primorial