internlm/Lean-Github huggingface dataset:
Theorem: BrunTitchmarsh.abs_rem_le
Proof state before:
case hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
this✝² : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
this✝¹ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃| ≤ |(↑d)⁻¹| + |(↑d)⁻¹ * C₃|
this✝ : |C₁ - C₂| ≤ |C₁| + |C₂|
this : |(↑d)⁻¹| ≤ 1
⊢ 1 ≤ d
Tactic:
omega
Proof state after:
no goals
Theorem: BrunTitchmarsh.abs_rem_le
Proof state before:
case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
⊢ 1 ≤ ⌈x⌉₊
Tactic:
simp [hx]
Proof state after:
no goals
Theorem: BrunTitchmarsh.boudingSum_ge
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (primeInterSieve x y z hz).selbergBoundingSum ≥ z.log / 2
Tactic:
apply boundingSum_ge_log
Proof state after:
case hnu
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (primeInterSieve x y z hz).nu = (↑ζ).pdiv ↑ArithmeticFunction.id

case hP
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (p : ℕ), p.Prime → ↑p ≤ (primeInterSieve x y z hz).level → p ∣ (primeInterSieve x y z hz).prodPrimes
Theorem: BrunTitchmarsh.boudingSum_ge
Proof state before:
case hnu
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (primeInterSieve x y z hz).nu = (↑ζ).pdiv ↑ArithmeticFunction.id
Tactic:
rfl
Proof state after:
no goals
Theorem: BrunTitchmarsh.boudingSum_ge
Proof state before:
case hP
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (p : ℕ), p.Prime → ↑p ≤ (primeInterSieve x y z hz).level → p ∣ (primeInterSieve x y z hz).prodPrimes
Tactic:
intro p hpp hp
Proof state after:
case hP
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hpp : p.Prime
hp : ↑p ≤ (primeInterSieve x y z hz).level
⊢ p ∣ (primeInterSieve x y z hz).prodPrimes
Theorem: BrunTitchmarsh.boudingSum_ge
Proof state before:
case hP
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hpp : p.Prime
hp : ↑p ≤ (primeInterSieve x y z hz).level
⊢ p ∣ (primeInterSieve x y z hz).prodPrimes
Tactic:
erw [prime_dvd_primorial_iff]
Proof state after:
case hP
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hpp : p.Prime
hp : ↑p ≤ (primeInterSieve x y z hz).level
⊢ p ≤ ⌊z⌋₊

case hP.hp
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hpp : p.Prime
hp : ↑p ≤ (primeInterSieve x y z hz).level
⊢ p.Prime
Theorem: BrunTitchmarsh.boudingSum_ge
Proof state before:
case hP
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hpp : p.Prime
hp : ↑p ≤ (primeInterSieve x y z hz).level
⊢ p ≤ ⌊z⌋₊

case hP.hp
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hpp : p.Prime
hp : ↑p ≤ (primeInterSieve x y z hz).level
⊢ p.Prime
Tactic:
apply Nat.le_floor
Proof state after:
case hP.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hpp : p.Prime
hp : ↑p ≤ (primeInterSieve x y z hz).level
⊢ ↑p ≤ z

case hP.hp
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hpp : p.Prime
hp : ↑p ≤ (primeInterSieve x y z hz).level
⊢ p.Prime
Theorem: BrunTitchmarsh.boudingSum_ge
Proof state before:
case hP.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hpp : p.Prime
hp : ↑p ≤ (primeInterSieve x y z hz).level
⊢ ↑p ≤ z

case hP.hp
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hpp : p.Prime
hp : ↑p ≤ (primeInterSieve x y z hz).level
⊢ p.Prime
Tactic:
exact hp
Proof state after:
case hP.hp
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hpp : p.Prime
hp : ↑p ≤ (primeInterSieve x y z hz).level
⊢ p.Prime
Theorem: BrunTitchmarsh.boudingSum_ge
Proof state before:
case hP.hp
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hpp : p.Prime
hp : ↑p ≤ (primeInterSieve x y z hz).level
⊢ p.Prime
Tactic:
exact hpp
Proof state after:
no goals
Theorem: BrunTitchmarsh.primeSieve_rem_sum_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (∑ d ∈ (primeInterSieve x y z hz).prodPrimes.divisors,
      if ↑d ≤ z then 3 ^ ω d * |(primeInterSieve x y z hz).rem d| else 0) ≤
    5 * z * (1 + z.log) ^ 3
Tactic:
apply rem_sum_le_of_const (primeInterSieve x y z hz) 5 ?_
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ d > 0, |(primeInterSieve x y z hz).rem d| ≤ 5
Theorem: BrunTitchmarsh.primeSieve_rem_sum_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ d > 0, |(primeInterSieve x y z hz).rem d| ≤ 5
Tactic:
intro d hd
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d > 0
⊢ |(primeInterSieve x y z hz).rem d| ≤ 5
Theorem: BrunTitchmarsh.primeSieve_rem_sum_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d > 0
⊢ |(primeInterSieve x y z hz).rem d| ≤ 5
Tactic:
apply abs_rem_le <;> linarith
Proof state after:
no goals
Theorem: BrunTitchmarsh.siftedSum_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ (primeInterSieve x y z ⋯).siftedSum ≤ 2 * y / z.log + 5 * z * (1 + z.log) ^ 3
Tactic:
apply le_trans (SelbergSieve.selberg_bound_simple ..)
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ ((primeInterSieve x y z ⋯).totalMass / (primeInterSieve x y z ⋯).selbergBoundingSum +
      ∑ d ∈ (primeInterSieve x y z ⋯).prodPrimes.divisors,
        if ↑d ≤ (primeInterSieve x y z ⋯).level then 3 ^ ω d * |(primeInterSieve x y z ⋯).rem d| else 0) ≤
    2 * y / z.log + 5 * z * (1 + z.log) ^ 3
Theorem: BrunTitchmarsh.siftedSum_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ ((primeInterSieve x y z ⋯).totalMass / (primeInterSieve x y z ⋯).selbergBoundingSum +
      ∑ d ∈ (primeInterSieve x y z ⋯).prodPrimes.divisors,
        if ↑d ≤ (primeInterSieve x y z ⋯).level then 3 ^ ω d * |(primeInterSieve x y z ⋯).rem d| else 0) ≤
    2 * y / z.log + 5 * z * (1 + z.log) ^ 3
Tactic:
calc _ ≤ y / (Real.log z / 2) + 5 * z * (1+Real.log z)^3 := ?_
     _ = _ := by ring
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ ((primeInterSieve x y z ⋯).totalMass / (primeInterSieve x y z ⋯).selbergBoundingSum +
      ∑ d ∈ (primeInterSieve x y z ⋯).prodPrimes.divisors,
        if ↑d ≤ (primeInterSieve x y z ⋯).level then 3 ^ ω d * |(primeInterSieve x y z ⋯).rem d| else 0) ≤
    y / (z.log / 2) + 5 * z * (1 + z.log) ^ 3
Theorem: BrunTitchmarsh.siftedSum_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ ((primeInterSieve x y z ⋯).totalMass / (primeInterSieve x y z ⋯).selbergBoundingSum +
      ∑ d ∈ (primeInterSieve x y z ⋯).prodPrimes.divisors,
        if ↑d ≤ (primeInterSieve x y z ⋯).level then 3 ^ ω d * |(primeInterSieve x y z ⋯).rem d| else 0) ≤
    y / (z.log / 2) + 5 * z * (1 + z.log) ^ 3
Tactic:
gcongr
Proof state after:
case h₁.hd
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ 0 < z.log / 2

case h₁.hac
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ (primeInterSieve x y z ⋯).totalMass ≤ y

case h₁.hbd
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ z.log / 2 ≤ (primeInterSieve x y z ⋯).selbergBoundingSum

case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ (∑ d ∈ (primeInterSieve x y z ⋯).prodPrimes.divisors,
      if ↑d ≤ (primeInterSieve x y z ⋯).level then 3 ^ ω d * |(primeInterSieve x y z ⋯).rem d| else 0) ≤
    5 * z * (1 + z.log) ^ 3
Theorem: BrunTitchmarsh.siftedSum_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ y / (z.log / 2) + 5 * z * (1 + z.log) ^ 3 = 2 * y / z.log + 5 * z * (1 + z.log) ^ 3
Tactic:
ring
Proof state after:
no goals
Theorem: BrunTitchmarsh.siftedSum_le
Proof state before:
case h₁.hd
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ 0 < z.log / 2
Tactic:
linarith [Real.log_pos hz]
Proof state after:
no goals
Theorem: BrunTitchmarsh.siftedSum_le
Proof state before:
case h₁.hac
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ (primeInterSieve x y z ⋯).totalMass ≤ y
Tactic:
rfl
Proof state after:
no goals
Theorem: BrunTitchmarsh.siftedSum_le
Proof state before:
case h₁.hbd
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ z.log / 2 ≤ (primeInterSieve x y z ⋯).selbergBoundingSum
Tactic:
apply boudingSum_ge
Proof state after:
no goals
Theorem: BrunTitchmarsh.siftedSum_le
Proof state before:
case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ (∑ d ∈ (primeInterSieve x y z ⋯).prodPrimes.divisors,
      if ↑d ≤ (primeInterSieve x y z ⋯).level then 3 ^ ω d * |(primeInterSieve x y z ⋯).rem d| else 0) ≤
    5 * z * (1 + z.log) ^ 3
Tactic:
apply primeSieve_rem_sum_le x y z hx hy
Proof state after:
no goals
Theorem: BrunTitchmarsh.primesBetween_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
this : z ≤ z * (1 + z.log) ^ 3
⊢ ↑(primesBetween x (x + y)) ≤ 2 * y / z.log + 6 * z * (1 + z.log) ^ 3
Tactic:
linarith [siftedSum_le _ _ _ hx hy hz, primesBetween_le_siftedSum_add x y z hz.le]
Proof state after:
no goals
Theorem: BrunTitchmarsh.primesBetween_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ z ≤ z * (1 + z.log) ^ 3
Tactic:
apply le_mul_of_one_le_right
Proof state after:
case ha
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ 0 ≤ z

case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ 1 ≤ (1 + z.log) ^ 3
Theorem: BrunTitchmarsh.primesBetween_le
Proof state before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ 1 ≤ (1 + z.log) ^ 3
Tactic:
apply one_le_pow_of_one_le _ _
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ 1 ≤ 1 + z.log
Theorem: BrunTitchmarsh.primesBetween_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ 1 ≤ 1 + z.log
Tactic:
linarith [Real.log_nonneg (by linarith)]
Proof state after:
no goals
Theorem: BrunTitchmarsh.primesBetween_le
Proof state before:
case ha
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ 0 ≤ z
Tactic:
linarith
Proof state after:
no goals
Theorem: BrunTitchmarsh.primesBetween_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ 1 ≤ ?m.110225
Tactic:
linarith
Proof state after:
no goals
Theorem: BrunTitchmarsh.primesBetween_one
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n : ℕ
⊢ primesBetween 1 ↑n = (Finset.filter Nat.Prime (Finset.range (n + 1))).card
Tactic:
rw [primesBetween]
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n : ℕ
⊢ (Finset.filter Nat.Prime (Finset.Icc ⌈1⌉₊ ⌊↑n⌋₊)).card = (Finset.filter Nat.Prime (Finset.range (n + 1))).card
Theorem: BrunTitchmarsh.primesBetween_one
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n : ℕ
⊢ (Finset.filter Nat.Prime (Finset.Icc ⌈1⌉₊ ⌊↑n⌋₊)).card = (Finset.filter Nat.Prime (Finset.range (n + 1))).card
Tactic:
congr 1
Proof state after:
case e_s
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n : ℕ
⊢ Finset.filter Nat.Prime (Finset.Icc ⌈1⌉₊ ⌊↑n⌋₊) = Finset.filter Nat.Prime (Finset.range (n + 1))
Theorem: BrunTitchmarsh.primesBetween_one
Proof state before:
case e_s
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n : ℕ
⊢ Finset.filter Nat.Prime (Finset.Icc ⌈1⌉₊ ⌊↑n⌋₊) = Finset.filter Nat.Prime (Finset.range (n + 1))
Tactic:
ext p
Proof state after:
case e_s.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
⊢ p ∈ Finset.filter Nat.Prime (Finset.Icc ⌈1⌉₊ ⌊↑n⌋₊) ↔ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1))
Theorem: BrunTitchmarsh.primesBetween_one
Proof state before:
case e_s.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
⊢ p ∈ Finset.filter Nat.Prime (Finset.Icc ⌈1⌉₊ ⌊↑n⌋₊) ↔ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1))
Tactic:
simp only [Nat.ceil_one, Nat.floor_coe, Finset.mem_filter, Finset.mem_Icc, Finset.mem_range,
  and_congr_left_iff]
Proof state after:
case e_s.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
⊢ p.Prime → (1 ≤ p ∧ p ≤ n ↔ p < n + 1)
Theorem: BrunTitchmarsh.primesBetween_one
Proof state before:
case e_s.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
⊢ p.Prime → (1 ≤ p ∧ p ≤ n ↔ p < n + 1)
Tactic:
intro hp
Proof state after:
case e_s.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
hp : p.Prime
⊢ 1 ≤ p ∧ p ≤ n ↔ p < n + 1
Theorem: BrunTitchmarsh.primesBetween_one
Proof state before:
case e_s.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
hp : p.Prime
⊢ 1 ≤ p ∧ p ≤ n ↔ p < n + 1
Tactic:
refine ⟨?_, ?_⟩
Proof state after:
case e_s.a.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
hp : p.Prime
⊢ 1 ≤ p ∧ p ≤ n → p < n + 1

case e_s.a.refine_2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
hp : p.Prime
⊢ p < n + 1 → 1 ≤ p ∧ p ≤ n
Theorem: BrunTitchmarsh.primesBetween_one
Proof state before:
case e_s.a.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
hp : p.Prime
⊢ 1 ≤ p ∧ p ≤ n → p < n + 1
Tactic:
exact fun h => by omega
Proof state after:
no goals
Theorem: BrunTitchmarsh.primesBetween_one
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
hp : p.Prime
h : 1 ≤ p ∧ p ≤ n
⊢ p < n + 1
Tactic:
omega
Proof state after:
no goals
Theorem: BrunTitchmarsh.primesBetween_one
Proof state before:
case e_s.a.refine_2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
hp : p.Prime
⊢ p < n + 1 → 1 ≤ p ∧ p ≤ n
Tactic:
refine fun h => ⟨by have := hp.pos; omega, by omega⟩
Proof state after:
no goals
Theorem: BrunTitchmarsh.primesBetween_one
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
hp : p.Prime
h : p < n + 1
⊢ 1 ≤ p
Tactic:
have := hp.pos
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
hp : p.Prime
h : p < n + 1
this : 0 < p
⊢ 1 ≤ p
Theorem: BrunTitchmarsh.primesBetween_one
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
hp : p.Prime
h : p < n + 1
this : 0 < p
⊢ 1 ≤ p
Tactic:
omega
Proof state after:
no goals
Theorem: BrunTitchmarsh.primesBetween_one
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
hp : p.Prime
h : p < n + 1
⊢ p ≤ n
Tactic:
omega
Proof state after:
no goals
Theorem: BrunTitchmarsh.primesBetween_mono_right
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
⊢ primesBetween a b ≤ primesBetween a c
Tactic:
dsimp only [primesBetween]
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
⊢ (Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊b⌋₊)).card ≤ (Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊c⌋₊)).card
Theorem: BrunTitchmarsh.primesBetween_mono_right
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
⊢ (Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊b⌋₊)).card ≤ (Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊c⌋₊)).card
Tactic:
apply Finset.card_le_card
Proof state after:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
⊢ Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊b⌋₊) ⊆ Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊c⌋₊)
Theorem: BrunTitchmarsh.primesBetween_mono_right
Proof state before:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
⊢ Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊b⌋₊) ⊆ Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊c⌋₊)
Tactic:
intro p
Proof state after:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
p : ℕ
⊢ p ∈ Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊b⌋₊) → p ∈ Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊c⌋₊)
Theorem: BrunTitchmarsh.primesBetween_mono_right
Proof state before:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
p : ℕ
⊢ p ∈ Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊b⌋₊) → p ∈ Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊c⌋₊)
Tactic:
simp only [Finset.mem_filter, Finset.mem_Icc, Nat.ceil_le, and_imp]
Proof state after:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
p : ℕ
⊢ a ≤ ↑p → p ≤ ⌊b⌋₊ → p.Prime → (a ≤ ↑p ∧ p ≤ ⌊c⌋₊) ∧ p.Prime
Theorem: BrunTitchmarsh.primesBetween_mono_right
Proof state before:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
p : ℕ
⊢ a ≤ ↑p → p ≤ ⌊b⌋₊ → p.Prime → (a ≤ ↑p ∧ p ≤ ⌊c⌋₊) ∧ p.Prime
Tactic:
intro ha hb hp
Proof state after:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
p : ℕ
ha : a ≤ ↑p
hb : p ≤ ⌊b⌋₊
hp : p.Prime
⊢ (a ≤ ↑p ∧ p ≤ ⌊c⌋₊) ∧ p.Prime
Theorem: BrunTitchmarsh.primesBetween_mono_right
Proof state before:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
p : ℕ
ha : a ≤ ↑p
hb : p ≤ ⌊b⌋₊
hp : p.Prime
⊢ (a ≤ ↑p ∧ p ≤ ⌊c⌋₊) ∧ p.Prime
Tactic:
refine ⟨⟨ha, hb.trans (Nat.floor_mono hbc)⟩, hp⟩
Proof state after:
no goals
Theorem: BrunTitchmarsh.tmp
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.filter Nat.Prime (Finset.range N)).card ≤
    4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
Tactic:
trans ↑((Finset.range (N+1)).filter Nat.Prime).card
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.filter Nat.Prime (Finset.range N)).card ≤ ↑(Finset.filter Nat.Prime (Finset.range (N + 1))).card

x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.filter Nat.Prime (Finset.range (N + 1))).card ≤
    4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
Theorem: BrunTitchmarsh.tmp
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.filter Nat.Prime (Finset.range (N + 1))).card ≤
    4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
Tactic:
rw [← primesBetween_one]
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
Theorem: BrunTitchmarsh.tmp
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
Tactic:
by_cases hN : N = 0
Proof state after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : N = 0
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
Theorem: BrunTitchmarsh.tmp
Proof state before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
Tactic:
by_cases hN : N = 1
Proof state after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : N = 1
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
Theorem: BrunTitchmarsh.tmp
Proof state before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
Tactic:
have h : primesBetween 1 (1 + N) ≤
    2 * (N / Real.log (N^(1/2:ℝ))) + 6 * (N ^ (1 / 2 : ℝ) * (1 + Real.log (N ^ (1 / 2 : ℝ))) ^ 3) := by
  convert (primesBetween_le 1 N (N ^ (1/2 : ℝ)) (by norm_num) (by norm_cast; omega)
    (Real.one_lt_rpow (by norm_cast; omega) (by norm_num))) using 1
  ring
Proof state after:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
h : ↑(primesBetween 1 (1 + ↑N)) ≤ 2 * (↑N / (↑N ^ (1 / 2)).log) + 6 * (↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3)
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
Theorem: BrunTitchmarsh.tmp
Proof state before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
h : ↑(primesBetween 1 (1 + ↑N)) ≤ 2 * (↑N / (↑N ^ (1 / 2)).log) + 6 * (↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3)
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
Tactic:
calc
  _ ≤ (primesBetween 1 (1+N):ℝ) := by
    norm_cast; apply primesBetween_mono_right; norm_cast; omega
  _ ≤ _ := by
    rw [Real.log_rpow (by norm_num; omega)] at h
    convert h using 2
    ring
Proof state after:
no goals
Theorem: BrunTitchmarsh.tmp
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.filter Nat.Prime (Finset.range N)).card ≤ ↑(Finset.filter Nat.Prime (Finset.range (N + 1))).card
Tactic:
norm_cast
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ (Finset.filter Nat.Prime (Finset.range N)).card ≤ (Finset.filter Nat.Prime (Finset.range (N + 1))).card
Theorem: BrunTitchmarsh.tmp
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ (Finset.filter Nat.Prime (Finset.range N)).card ≤ (Finset.filter Nat.Prime (Finset.range (N + 1))).card
Tactic:
apply Finset.card_le_card
Proof state after:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ Finset.filter Nat.Prime (Finset.range N) ⊆ Finset.filter Nat.Prime (Finset.range (N + 1))
Theorem: BrunTitchmarsh.tmp
Proof state before:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ Finset.filter Nat.Prime (Finset.range N) ⊆ Finset.filter Nat.Prime (Finset.range (N + 1))
Tactic:
intro n
Proof state after:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
⊢ n ∈ Finset.filter Nat.Prime (Finset.range N) → n ∈ Finset.filter Nat.Prime (Finset.range (N + 1))
Theorem: BrunTitchmarsh.tmp
Proof state before:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
⊢ n ∈ Finset.filter Nat.Prime (Finset.range N) → n ∈ Finset.filter Nat.Prime (Finset.range (N + 1))
Tactic:
simp only [Finset.mem_filter, Finset.mem_range, and_imp]
Proof state after:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
⊢ n < N → n.Prime → n < N + 1 ∧ n.Prime
Theorem: BrunTitchmarsh.tmp
Proof state before:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
⊢ n < N → n.Prime → n < N + 1 ∧ n.Prime
Tactic:
refine fun hnN hp ↦ ⟨by omega, hp⟩
Proof state after:
no goals
Theorem: BrunTitchmarsh.tmp
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hp : n.Prime
⊢ n < N + 1
Tactic:
omega
Proof state after:
no goals
Theorem: BrunTitchmarsh.tmp
Proof state before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : N = 0
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
Tactic:
simp [hN, primesBetween]
Proof state after:
no goals
Theorem: BrunTitchmarsh.tmp
Proof state before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : N = 1
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
Tactic:
simp (config := {decide:=true}) [hN, primesBetween]
Proof state after:
no goals
Theorem: BrunTitchmarsh.tmp
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
⊢ ↑(primesBetween 1 (1 + ↑N)) ≤ 2 * (↑N / (↑N ^ (1 / 2)).log) + 6 * (↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3)
Tactic:
convert (primesBetween_le 1 N (N ^ (1/2 : ℝ)) (by norm_num) (by norm_cast; omega)
  (Real.one_lt_rpow (by norm_cast; omega) (by norm_num))) using 1
Proof state after:
case h.e'_4
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
⊢ 2 * (↑N / (↑N ^ (1 / 2)).log) + 6 * (↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3) =
    2 * ↑N / (↑N ^ (1 / 2)).log + 6 * ↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3
Theorem: BrunTitchmarsh.tmp
Proof state before:
case h.e'_4
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
⊢ 2 * (↑N / (↑N ^ (1 / 2)).log) + 6 * (↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3) =
    2 * ↑N / (↑N ^ (1 / 2)).log + 6 * ↑N ^ (1 / 2) * (1 + (↑N ^ (1 / 2)).log) ^ 3
Tactic:
ring
Proof state after:
no goals
Theorem: BrunTitchmarsh.tmp
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
⊢ 0 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: BrunTitchmarsh.tmp
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
⊢ 0 < ↑N
Tactic:
norm_cast
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN✝ : ¬N = 0
hN : ¬N = 1
⊢ 0 < N