Source indexedtheorem · leanprover/lean4:v4.32.0

BKLNW.prop_3_sub_3

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:326 to 339

Mathematical statement

Exact Lean statement

@[blueprint
  "bklnw-prop-3-sub-3"
  (title := "BKLNW Proposition 3, substep 3")
  (statement := /-- $f(2^n) = 1 + u_n$.-/)
  (proof := /-- Clear. -/)
  (latexEnv := "sublemma")
  (discussion := 633)]
theorem prop_3_sub_3 (n : ℕ) (hn : n ≥ 3) : f (2^n) = 1 + u n

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "bklnw-prop-3-sub-3"  (title := "BKLNW Proposition 3, substep 3")  (statement := /-- $f(2^n) = 1 + u_n$.-/)  (proof := /-- Clear. -/)  (latexEnv := "sublemma")  (discussion := 633)]theorem prop_3_sub_3 (n : ℕ) (hn : n ≥ 3) : f (2^n) = 1 + u n := by  have sum_bound : ⌊ (log (2 ^ n)) / (log 2) ⌋₊ = n := by norm_num  rw [f, u, sum_bound, ← add_sum_Ioc_eq_sum_Icc hn,    ← Icc_add_one_left_eq_Ioc, Nat.cast_ofNat, sub_self, rpow_zero]  congr with k  rw [← rpow_natCast _ n, ← rpow_mul (by norm_num)]  field_simp