Theorem: BrunTitchmarsh.boudingSum_ge (PrimeNumberTheoremAnd/BrunTitchmarsh.lean)

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
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

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
State after:
no goals

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
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

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]
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

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
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

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
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

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
State after:
no goals