internlm/Lean-Github huggingface dataset:
Theorem: BrunTitchmarsh.IsBigO.nat_Top_of_atTop
Proof state before:
case intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|
Tactic:
let C := Finset.max' (insert c ((Finset.range N).image (fun n ↦ |f n| * |g n|⁻¹))) (by simp)
Proof state after:
case intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|
Theorem: BrunTitchmarsh.IsBigO.nat_Top_of_atTop
Proof state before:
case intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|
Tactic:
refine ⟨C, fun n ↦ ?_⟩
Proof state after:
case intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
⊢ |f n| ≤ C * |g n|
Theorem: BrunTitchmarsh.IsBigO.nat_Top_of_atTop
Proof state before:
case intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
⊢ |f n| ≤ C * |g n|
Tactic:
by_cases hn : N ≤ n
Proof state after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : N ≤ n
⊢ |f n| ≤ C * |g n|

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
⊢ |f n| ≤ C * |g n|
Theorem: BrunTitchmarsh.IsBigO.nat_Top_of_atTop
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
⊢ (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).Nonempty
Tactic:
simp
Proof state after:
no goals
Theorem: BrunTitchmarsh.IsBigO.nat_Top_of_atTop
Proof state before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : N ≤ n
⊢ |f n| ≤ C * |g n|
Tactic:
calc |f n| ≤ c * |g n| := hc n hn
  _ ≤ C * |g n| := by
    gcongr
    apply Finset.le_max'
    simp
Proof state after:
no goals
Theorem: BrunTitchmarsh.IsBigO.nat_Top_of_atTop
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : N ≤ n
⊢ c * |g n| ≤ C * |g n|
Tactic:
gcongr
Proof state after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : N ≤ n
⊢ c ≤ C
Theorem: BrunTitchmarsh.IsBigO.nat_Top_of_atTop
Proof state before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : N ≤ n
⊢ c ≤ C
Tactic:
apply Finset.le_max'
Proof state after:
case h.H2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : N ≤ n
⊢ c ∈ insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))
Theorem: BrunTitchmarsh.IsBigO.nat_Top_of_atTop
Proof state before:
case h.H2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : N ≤ n
⊢ c ∈ insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))
Tactic:
simp
Proof state after:
no goals
Theorem: BrunTitchmarsh.IsBigO.nat_Top_of_atTop
Proof state before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
⊢ |f n| ≤ C * |g n|
Tactic:
by_cases hg : g n = 0
Proof state after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : g n = 0
⊢ |f n| ≤ C * |g n|

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ |f n| ≤ C * |g n|
Theorem: BrunTitchmarsh.IsBigO.nat_Top_of_atTop
Proof state before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ |f n| ≤ C * |g n|
Tactic:
rw [← mul_inv_le_iff']
Proof state after:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ |f n| * |g n|⁻¹ ≤ C

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ 0 < |g n|
Theorem: BrunTitchmarsh.IsBigO.nat_Top_of_atTop
Proof state before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ |f n| * |g n|⁻¹ ≤ C

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ 0 < |g n|
Tactic:
apply Finset.le_max'
Proof state after:
case neg.H2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ |f n| * |g n|⁻¹ ∈ insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ 0 < |g n|
Theorem: BrunTitchmarsh.IsBigO.nat_Top_of_atTop
Proof state before:
case neg.H2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ |f n| * |g n|⁻¹ ∈ insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ 0 < |g n|
Tactic:
simp only [Finset.mem_insert, Finset.mem_image, Finset.mem_range]
Proof state after:
case neg.H2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ |f n| * |g n|⁻¹ = c ∨ ∃ a < N, |f a| * |g a|⁻¹ = |f n| * |g n|⁻¹

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ 0 < |g n|
Theorem: BrunTitchmarsh.IsBigO.nat_Top_of_atTop
Proof state before:
case neg.H2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ |f n| * |g n|⁻¹ = c ∨ ∃ a < N, |f a| * |g a|⁻¹ = |f n| * |g n|⁻¹

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ 0 < |g n|
Tactic:
exact .inr ⟨n, by omega, rfl⟩
Proof state after:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ 0 < |g n|
Theorem: BrunTitchmarsh.IsBigO.nat_Top_of_atTop
Proof state before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : g n = 0
⊢ |f n| ≤ C * |g n|
Tactic:
simp [hg, h0]
Proof state after:
no goals
Theorem: BrunTitchmarsh.IsBigO.nat_Top_of_atTop
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ n < N
Tactic:
omega
Proof state after:
no goals
Theorem: BrunTitchmarsh.IsBigO.nat_Top_of_atTop
Proof state before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ 0 < |g n|
Tactic:
simp [hg]
Proof state after:
no goals
Theorem: BrunTitchmarsh.pows_small_primes_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card ≤
    ↑(Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1)).card
Tactic:
norm_cast
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ (Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card ≤
    (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1)).card
Theorem: BrunTitchmarsh.pows_small_primes_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ (Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card ≤
    (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1)).card
Tactic:
exact Finset.card_image_le
Proof state after:
no goals
Theorem: BrunTitchmarsh.pows_small_primes_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1)).card ≤ ↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)
Tactic:
simp only [Finset.card_product, Nat.card_Ico, Finset.card_range, Nat.cast_mul, Nat.cast_add,
  Nat.cast_one]
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(⌈√↑N⌉₊ - 1) * (↑(Nat.log 2 N) + 1) ≤ ↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)
Theorem: BrunTitchmarsh.pows_small_primes_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(⌈√↑N⌉₊ - 1) * (↑(Nat.log 2 N) + 1) ≤ ↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)
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
⊢ ↑(⌈√↑N⌉₊ - 1) * (↑(Nat.log 2 N) + 1) ≤ ↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ ↑(⌈√↑N⌉₊ - 1) * (↑(Nat.log 2 N) + 1) ≤ ↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)
Theorem: BrunTitchmarsh.pows_small_primes_le
Proof state before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ ↑(⌈√↑N⌉₊ - 1) * (↑(Nat.log 2 N) + 1) ≤ ↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)
Tactic:
have : 1 ≤ Nat.ceil (Real.sqrt N) := by
  simp only [Nat.one_le_ceil_iff, Real.sqrt_pos, Nat.cast_pos]
  omega
Proof state after:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ ↑(⌈√↑N⌉₊ - 1) * (↑(Nat.log 2 N) + 1) ≤ ↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)
Theorem: BrunTitchmarsh.pows_small_primes_le
Proof state before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ ↑(⌈√↑N⌉₊ - 1) * (↑(Nat.log 2 N) + 1) ≤ ↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)
Tactic:
gcongr ?_ * ?_
Proof state after:
case neg.h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ ↑(⌈√↑N⌉₊ - 1) ≤ ↑N ^ (1 / 2)

case neg.h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ ↑(Nat.log 2 N) + 1 ≤ 1 + (↑N).log / Real.log 2
Theorem: BrunTitchmarsh.pows_small_primes_le
Proof state before:
case neg.h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ ↑(Nat.log 2 N) + 1 ≤ 1 + (↑N).log / Real.log 2
Tactic:
rw [Nat.log_eq_floor_logb _ _ (by norm_num), Real.log_div_log, Nat.cast_two]
Proof state after:
case neg.h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ ↑⌊Real.logb 2 ↑N⌋₊ + 1 ≤ 1 + Real.logb 2 ↑N
Theorem: BrunTitchmarsh.pows_small_primes_le
Proof state before:
case neg.h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
hlogb_nonneg : 0 ≤ Real.logb 2 ↑N
⊢ ↑⌊Real.logb 2 ↑N⌋₊ + 1 ≤ 1 + Real.logb 2 ↑N
Tactic:
linarith [Nat.floor_le hlogb_nonneg]
Proof state after:
no goals
Theorem: BrunTitchmarsh.pows_small_primes_le
Proof state before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : N = 0
⊢ ↑(⌈√↑N⌉₊ - 1) * (↑(Nat.log 2 N) + 1) ≤ ↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)
Tactic:
simp [hN]
Proof state after:
no goals
Theorem: BrunTitchmarsh.pows_small_primes_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ 1 ≤ ⌈√↑N⌉₊
Tactic:
simp only [Nat.one_le_ceil_iff, Real.sqrt_pos, Nat.cast_pos]
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ 0 < N
Theorem: BrunTitchmarsh.pows_small_primes_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ 0 < N
Tactic:
omega
Proof state after:
no goals
Theorem: BrunTitchmarsh.pows_small_primes_le
Proof state before:
case neg.h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ ↑(⌈√↑N⌉₊ - 1) ≤ ↑N ^ (1 / 2)
Tactic:
rw [← Real.sqrt_eq_rpow, Nat.cast_sub this, Nat.cast_one]
Proof state after:
case neg.h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ ↑⌈√↑N⌉₊ - 1 ≤ √↑N
Theorem: BrunTitchmarsh.pows_small_primes_le
Proof state before:
case neg.h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ ↑⌈√↑N⌉₊ - 1 ≤ √↑N
Tactic:
have := Nat.ceil_lt_add_one (show 0 ≤ Real.sqrt N by positivity)
Proof state after:
case neg.h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this✝ : 1 ≤ ⌈√↑N⌉₊
this : ↑⌈√↑N⌉₊ < √↑N + 1
⊢ ↑⌈√↑N⌉₊ - 1 ≤ √↑N
Theorem: BrunTitchmarsh.pows_small_primes_le
Proof state before:
case neg.h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this✝ : 1 ≤ ⌈√↑N⌉₊
this : ↑⌈√↑N⌉₊ < √↑N + 1
⊢ ↑⌈√↑N⌉₊ - 1 ≤ √↑N
Tactic:
linarith
Proof state after:
no goals
Theorem: BrunTitchmarsh.pows_small_primes_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ 0 ≤ √↑N
Tactic:
positivity
Proof state after:
no goals
Theorem: BrunTitchmarsh.pows_small_primes_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ 1 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: BrunTitchmarsh.pows_small_primes_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ 0 ≤ Real.logb 2 ↑N
Tactic:
apply Real.logb_nonneg
Proof state after:
case hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ 1 < 2

case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ 1 ≤ ↑N
Theorem: BrunTitchmarsh.pows_small_primes_le
Proof state before:
case hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ 1 < 2
Tactic:
norm_cast
Proof state after:
no goals
Theorem: BrunTitchmarsh.pows_small_primes_le
Proof state before:
case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ 1 ≤ ↑N
Tactic:
norm_cast
Proof state after:
case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ 1 ≤ N
Theorem: BrunTitchmarsh.pows_small_primes_le
Proof state before:
case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ 1 ≤ N
Tactic:
omega
Proof state after:
no goals
Theorem: BrunTitchmarsh.one_add_log_div_log_two_isBigO
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => 1 + N.log / Real.log 2) =O[atTop] fun N => N.log
Tactic:
refine IsBigO.add ?h₁ ?h₂
Proof state after:
case h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => 1) =O[atTop] fun N => N.log

case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => N.log / Real.log 2) =O[atTop] fun N => N.log
Theorem: BrunTitchmarsh.one_add_log_div_log_two_isBigO
Proof state before:
case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => N.log / Real.log 2) =O[atTop] fun N => N.log
Tactic:
simp_rw [div_eq_inv_mul]
Proof state after:
case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => (Real.log 2)⁻¹ * N.log) =O[atTop] fun N => N.log
Theorem: BrunTitchmarsh.one_add_log_div_log_two_isBigO
Proof state before:
case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => (Real.log 2)⁻¹ * N.log) =O[atTop] fun N => N.log
Tactic:
apply IsBigO.const_mul_left
Proof state after:
case h₂.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => x.log) =O[atTop] fun N => N.log
Theorem: BrunTitchmarsh.one_add_log_div_log_two_isBigO
Proof state before:
case h₂.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => x.log) =O[atTop] fun N => N.log
Tactic:
apply isBigO_refl
Proof state after:
no goals
Theorem: BrunTitchmarsh.one_add_log_div_log_two_isBigO
Proof state before:
case h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => 1) =O[atTop] fun N => N.log
Tactic:
convert Real.isLittleO_const_log_atTop.isBigO
Proof state after:
no goals
Theorem: BrunTitchmarsh.pow_half_mul_one_add_log_div_isBigO
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => N ^ (1 / 2) * (1 + N.log / Real.log 2)) =O[atTop] fun N => N ^ (1 / 2) * N.log
Tactic:
apply IsBigO.mul
Proof state after:
case h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => x ^ (1 / 2)) =O[atTop] fun x => x ^ (1 / 2)

case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => 1 + x.log / Real.log 2) =O[atTop] fun x => x.log
Theorem: BrunTitchmarsh.pow_half_mul_one_add_log_div_isBigO
Proof state before:
case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => 1 + x.log / Real.log 2) =O[atTop] fun x => x.log
Tactic:
apply one_add_log_div_log_two_isBigO
Proof state after:
no goals
Theorem: BrunTitchmarsh.pow_half_mul_one_add_log_div_isBigO
Proof state before:
case h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => x ^ (1 / 2)) =O[atTop] fun x => x ^ (1 / 2)
Tactic:
apply isBigO_refl
Proof state after:
no goals
Theorem: BrunTitchmarsh.pow_half_mul_one_add_log_div_isBigO
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => N ^ (1 / 2) * N.log) =O[atTop] fun N => N / N.log
Tactic:
convert rpow_mul_rpow_log_isBigO_id_div_log 1 (show 1/2 < (1:ℝ) by norm_num) using 1
Proof state after:
case h.e'_7
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => N ^ (1 / 2) * N.log) = fun x => x ^ (1 / 2) * x.log ^ 1
Theorem: BrunTitchmarsh.pow_half_mul_one_add_log_div_isBigO
Proof state before:
case h.e'_7
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => N ^ (1 / 2) * N.log) = fun x => x ^ (1 / 2) * x.log ^ 1
Tactic:
simp
Proof state after:
no goals
Theorem: BrunTitchmarsh.pow_half_mul_one_add_log_div_isBigO
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ 1 / 2 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: BrunTitchmarsh.card_pows_aux
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card) =O[atTop]
    fun N => ↑N / (↑N).log
Tactic:
apply IsBigO.trans ?_ pow_half_mul_one_add_log_div_isBigO.natCast
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card) =O[atTop]
    fun n => ↑n ^ (1 / 2) * (1 + (↑n).log / Real.log 2)
Theorem: BrunTitchmarsh.card_pows_aux
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card) =O[atTop]
    fun n => ↑n ^ (1 / 2) * (1 + (↑n).log / Real.log 2)
Tactic:
apply isBigO_of_le
Proof state after:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (x : ℕ),
    ‖↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card‖ ≤
      ‖↑x ^ (1 / 2) * (1 + (↑x).log / Real.log 2)‖
Theorem: BrunTitchmarsh.card_pows_aux
Proof state before:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (x : ℕ),
    ‖↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card‖ ≤
      ‖↑x ^ (1 / 2) * (1 + (↑x).log / Real.log 2)‖
Tactic:
intro N
Proof state after:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ‖↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card‖ ≤
    ‖↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)‖
Theorem: BrunTitchmarsh.card_pows_aux
Proof state before:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ‖↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card‖ ≤
    ‖↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)‖
Tactic:
simp only [RCLike.norm_natCast, one_div, norm_mul, Real.norm_eq_abs]
Proof state after:
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card ≤
    |↑N ^ 2⁻¹| * |1 + (↑N).log / Real.log 2|