Theorem: Sieve.boundingSum_ge_log (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean)

State before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ s.selbergBoundingSum ≥ s.level.log / 2
Tactic:
trans (∑ m in Finset.Icc 1 (Nat.floor $ Real.sqrt s.level), 1 / (m:ℝ))
State after:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m ≥ s.level.log / 2

State before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m ≥ s.level.log / 2
Tactic:
trans (Real.log $ Real.sqrt s.level)
State after:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m ≥ (√s.level).log

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≥ s.level.log / 2

State before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m ≥ (√s.level).log

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≥ s.level.log / 2
Tactic:
rw [ge_iff_le]
State after:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≤ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≥ s.level.log / 2

State before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≤ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≥ s.level.log / 2
Tactic:
simp_rw[one_div]
State after:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≤ ∑ x ∈ Finset.Icc 1 ⌊√s.level⌋₊, (↑x)⁻¹

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≥ s.level.log / 2

State before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≤ ∑ x ∈ Finset.Icc 1 ⌊√s.level⌋₊, (↑x)⁻¹

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≥ s.level.log / 2
Tactic:
apply Aux.log_le_sum_inv (Real.sqrt s.level)
State after:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ 1 ≤ √s.level

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≥ s.level.log / 2

State before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ 1 ≤ √s.level

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≥ s.level.log / 2
Tactic:
rw [Real.le_sqrt] <;> linarith[s.one_le_level]
State after:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≥ s.level.log / 2

State before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≥ s.level.log / 2
Tactic:
apply ge_of_eq
State after:
case h
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log = s.level.log / 2

State before:
case h
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log = s.level.log / 2
Tactic:
refine Real.log_sqrt ?h.hx
State after:
case h.hx
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ 0 ≤ s.level

State before:
case h.hx
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ 0 ≤ s.level
Tactic:
linarith[s.one_le_level]
State after:
no goals

State before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m
Tactic:
exact boundingSum_ge_sum s hnu hP
State after:
no goals