Theorem: BrunTitchmarsh.Nat.log_eq_floor_logb (PrimeNumberTheoremAnd/BrunTitchmarsh.lean)

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
⊢ b.log n = ⌊(↑b).logb ↑n⌋₊
Tactic:
by_cases hn : n = 0
State after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : n = 0
⊢ b.log n = ⌊(↑b).logb ↑n⌋₊

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
⊢ b.log n = ⌊(↑b).logb ↑n⌋₊

State before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ b.log n = ⌊(↑b).logb ↑n⌋₊
Tactic:
apply le_antisymm
State after:
case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ b.log n ≤ ⌊(↑b).logb ↑n⌋₊

case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ ⌊(↑b).logb ↑n⌋₊ ≤ b.log n

State before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : n = 0
⊢ b.log n = ⌊(↑b).logb ↑n⌋₊
Tactic:
simp [hn]
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
⊢ 0 ≤ (↑b).logb ↑n
Tactic:
apply Real.logb_nonneg
State after:
case hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
⊢ 1 < ↑b

case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
⊢ 1 ≤ ↑n

State before:
case hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
⊢ 1 < ↑b
Tactic:
norm_cast
State after:
no goals

State before:
case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
⊢ 1 ≤ ↑n
Tactic:
norm_cast
State after:
case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
⊢ 1 ≤ n

State before:
case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
⊢ 1 ≤ n
Tactic:
exact Nat.one_le_iff_ne_zero.mpr hn
State after:
no goals

State before:
case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ b.log n ≤ ⌊(↑b).logb ↑n⌋₊
Tactic:
rw [Nat.le_floor_iff, Real.le_logb_iff_rpow_le]
State after:
case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ ↑b ^ ↑(b.log n) ≤ ↑n

case neg.a.hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 1 < ↑b

case neg.a.hy
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 < ↑n

case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 ≤ (↑b).logb ↑n

State before:
case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ ↑b ^ ↑(b.log n) ≤ ↑n

case neg.a.hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 1 < ↑b

case neg.a.hy
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 < ↑n

case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 ≤ (↑b).logb ↑n
Tactic:
norm_cast
State after:
case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ b ^ b.log n ≤ n

case neg.a.hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 1 < ↑b

case neg.a.hy
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 < ↑n

case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 ≤ (↑b).logb ↑n

State before:
case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ b ^ b.log n ≤ n

case neg.a.hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 1 < ↑b

case neg.a.hy
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 < ↑n

case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 ≤ (↑b).logb ↑n
Tactic:
apply Nat.pow_log_le_self
State after:
case neg.a.hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ n ≠ 0

case neg.a.hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 1 < ↑b

case neg.a.hy
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 < ↑n

case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 ≤ (↑b).logb ↑n

State before:
case neg.a.hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ n ≠ 0
Tactic:
exact hn
State after:
no goals

State before:
case neg.a.hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 1 < ↑b
Tactic:
norm_cast
State after:
no goals

State before:
case neg.a.hy
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 < ↑n
Tactic:
norm_cast
State after:
case neg.a.hy
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 < n

State before:
case neg.a.hy
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 < n
Tactic:
exact Nat.zero_lt_of_ne_zero hn
State after:
no goals

State before:
case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 0 ≤ (↑b).logb ↑n
Tactic:
exact hlogb_nonneg
State after:
no goals

State before:
case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ ⌊(↑b).logb ↑n⌋₊ ≤ b.log n
Tactic:
apply Nat.le_log_of_pow_le hb
State after:
case neg.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ b ^ ⌊(↑b).logb ↑n⌋₊ ≤ n

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ ↑b ^ ⌊(↑b).logb ↑n⌋₊ ≤ ↑b ^ (↑b).logb ↑n
Tactic:
rw [← Real.rpow_natCast]
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ ↑b ^ ↑⌊(↑b).logb ↑n⌋₊ ≤ ↑b ^ (↑b).logb ↑n

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ ↑b ^ ↑⌊(↑b).logb ↑n⌋₊ ≤ ↑b ^ (↑b).logb ↑n
Tactic:
gcongr
State after:
case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 1 ≤ ↑b

case hyz
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ ↑⌊(↑b).logb ↑n⌋₊ ≤ (↑b).logb ↑n

State before:
case hyz
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ ↑⌊(↑b).logb ↑n⌋₊ ≤ (↑b).logb ↑n
Tactic:
apply Nat.floor_le hlogb_nonneg
State after:
no goals

State before:
case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 1 ≤ ↑b
Tactic:
norm_cast
State after:
case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 1 ≤ b

State before:
case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 1 ≤ b
Tactic:
omega
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ ↑b ^ (↑b).logb ↑n = ↑n
Tactic:
rw [Real.rpow_logb] <;> norm_cast <;> omega
State after:
no goals