internlm/Lean-Github huggingface dataset:
Theorem: vonMangoldt_cheby
Proof state before:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ ∀ i < n, IsPrimePow i → (↑i).log ≤ (↑n).log
Tactic:
intro i hi hi_p
Proof state after:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n i : ℕ
hi : i < n
hi_p : IsPrimePow i
⊢ (↑i).log ≤ (↑n).log
Theorem: vonMangoldt_cheby
Proof state before:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n i : ℕ
hi : i < n
hi_p : IsPrimePow i
⊢ (↑i).log ≤ (↑n).log
Tactic:
have := hi_p.pos
Proof state after:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n i : ℕ
hi : i < n
hi_p : IsPrimePow i
this : 0 < i
⊢ (↑i).log ≤ (↑n).log
Theorem: vonMangoldt_cheby
Proof state before:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n i : ℕ
hi : i < n
hi_p : IsPrimePow i
this : 0 < i
⊢ (↑i).log ≤ (↑n).log
Tactic:
gcongr
Proof state after:
no goals
Theorem: vonMangoldt_cheby
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ ∑ _i ∈ Finset.filter IsPrimePow (Finset.range n), (↑n).log ≤ C * (↑n / (↑n).log) * (↑n).log
Tactic:
simp
Proof state after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ ↑(Finset.filter IsPrimePow (Finset.range n)).card * (↑n).log ≤ C * (↑n / (↑n).log) * (↑n).log
Theorem: vonMangoldt_cheby
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ ↑(Finset.filter IsPrimePow (Finset.range n)).card * (↑n).log ≤ C * (↑n / (↑n).log) * (↑n).log
Tactic:
gcongr
Proof state after:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ ↑(Finset.filter IsPrimePow (Finset.range n)).card ≤ C * (↑n / (↑n).log)
Theorem: vonMangoldt_cheby
Proof state before:
case h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ ↑(Finset.filter IsPrimePow (Finset.range n)).card ≤ C * (↑n / (↑n).log)
Tactic:
apply hC
Proof state after:
no goals
Theorem: vonMangoldt_cheby
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ C * (↑n / (↑n).log) * (↑n).log ≤ C * ↑n
Tactic:
by_cases hn : n = 0
Proof state after:
case pos
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : n = 0
⊢ C * (↑n / (↑n).log) * (↑n).log ≤ C * ↑n

case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
⊢ C * (↑n / (↑n).log) * (↑n).log ≤ C * ↑n
Theorem: vonMangoldt_cheby
Proof state before:
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
⊢ C * (↑n / (↑n).log) * (↑n).log ≤ C * ↑n
Tactic:
by_cases hn1 : n = 1
Proof state after:
case pos
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
hn1 : n = 1
⊢ C * (↑n / (↑n).log) * (↑n).log ≤ C * ↑n

case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
hn1 : ¬n = 1
⊢ C * (↑n / (↑n).log) * (↑n).log ≤ C * ↑n
Theorem: vonMangoldt_cheby
Proof state before:
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
hn1 : ¬n = 1
⊢ C * (↑n / (↑n).log) * (↑n).log ≤ C * ↑n
Tactic:
have : 0 < Real.log n := by
  apply Real.log_pos
  norm_cast
  omega
Proof state after:
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
hn1 : ¬n = 1
this : 0 < (↑n).log
⊢ C * (↑n / (↑n).log) * (↑n).log ≤ C * ↑n
Theorem: vonMangoldt_cheby
Proof state before:
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
hn1 : ¬n = 1
this : 0 < (↑n).log
⊢ C * (↑n / (↑n).log) * (↑n).log ≤ C * ↑n
Tactic:
field_simp
Proof state after:
no goals
Theorem: vonMangoldt_cheby
Proof state before:
case pos
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : n = 0
⊢ C * (↑n / (↑n).log) * (↑n).log ≤ C * ↑n
Tactic:
simp [hn]
Proof state after:
no goals
Theorem: vonMangoldt_cheby
Proof state before:
case pos
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
hn1 : n = 1
⊢ C * (↑n / (↑n).log) * (↑n).log ≤ C * ↑n
Tactic:
simp [hn1, hC_nonneg]
Proof state after:
no goals
Theorem: vonMangoldt_cheby
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
hn1 : ¬n = 1
⊢ 0 < (↑n).log
Tactic:
apply Real.log_pos
Proof state after:
case hx
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
hn1 : ¬n = 1
⊢ 1 < ↑n
Theorem: vonMangoldt_cheby
Proof state before:
case hx
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
hn1 : ¬n = 1
⊢ 1 < ↑n
Tactic:
norm_cast
Proof state after:
case hx
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
hn1 : ¬n = 1
⊢ 1 < n
Theorem: vonMangoldt_cheby
Proof state before:
case hx
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
hn : ¬n = 0
hn1 : ¬n = 1
⊢ 1 < n
Tactic:
omega
Proof state after:
no goals
Theorem: WeakPNT
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)
Tactic:
have hnv := riemannZeta_ne_zero_of_one_le_re
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)
Theorem: WeakPNT
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)
Tactic:
have l1 (n : ℕ) : 0 ≤ Λ n := vonMangoldt_nonneg
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)
Theorem: WeakPNT
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)
Tactic:
have l2 s (hs : 1 < s.re) : (-deriv ζ₁ / ζ₁) s = LSeries Λ s - 1 / (s - 1) := by
  have hs₁ : s ≠ 1 := by contrapose! hs ; simp [hs]
  simp [LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs, neg_logDeriv_ζ₁_eq hs₁ (hnv hs₁ hs.le)]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
l2 : ∀ (s : ℂ), 1 < s.re → (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)
Theorem: WeakPNT
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
l2 : ∀ (s : ℂ), 1 < s.re → (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)
Tactic:
have l3 : ContinuousOn (-deriv ζ₁ / ζ₁) {s | 1 ≤ s.re} := continuousOn_neg_logDeriv_ζ₁.mono (by tauto)
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
l2 : ∀ (s : ℂ), 1 < s.re → (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
l3 : ContinuousOn (-deriv ζ₁ / ζ₁) {s | 1 ≤ s.re}
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)
Theorem: WeakPNT
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
l2 : ∀ (s : ℂ), 1 < s.re → (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
l3 : ContinuousOn (-deriv ζ₁ / ζ₁) {s | 1 ≤ s.re}
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)
Tactic:
have l4 : cheby Λ := vonMangoldt_cheby
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
l2 : ∀ (s : ℂ), 1 < s.re → (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
l3 : ContinuousOn (-deriv ζ₁ / ζ₁) {s | 1 ≤ s.re}
l4 : cheby fun n => ↑(Λ n)
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)
Theorem: WeakPNT
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
l2 : ∀ (s : ℂ), 1 < s.re → (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
l3 : ContinuousOn (-deriv ζ₁ / ζ₁) {s | 1 ≤ s.re}
l4 : cheby fun n => ↑(Λ n)
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)
Tactic:
have l5 (σ' : ℝ) (hσ' : 1 < σ') : Summable (nterm Λ σ') := by
  simpa only [← nterm_eq_norm_term] using (@ArithmeticFunction.LSeriesSummable_vonMangoldt σ' hσ').norm
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
l2 : ∀ (s : ℂ), 1 < s.re → (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
l3 : ContinuousOn (-deriv ζ₁ / ζ₁) {s | 1 ≤ s.re}
l4 : cheby fun n => ↑(Λ n)
l5 : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(Λ n)) σ')
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)
Theorem: WeakPNT
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
l2 : ∀ (s : ℂ), 1 < s.re → (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
l3 : ContinuousOn (-deriv ζ₁ / ζ₁) {s | 1 ≤ s.re}
l4 : cheby fun n => ↑(Λ n)
l5 : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(Λ n)) σ')
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)
Tactic:
apply WienerIkeharaTheorem' l1 l5 l4 l3 l2
Proof state after:
no goals
Theorem: WeakPNT
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
s : ℂ
hs : 1 < s.re
⊢ (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
Tactic:
have hs₁ : s ≠ 1 := by contrapose! hs ; simp [hs]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
s : ℂ
hs : 1 < s.re
hs₁ : s ≠ 1
⊢ (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
Theorem: WeakPNT
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
s : ℂ
hs : 1 < s.re
hs₁ : s ≠ 1
⊢ (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
Tactic:
simp [LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs, neg_logDeriv_ζ₁_eq hs₁ (hnv hs₁ hs.le)]
Proof state after:
no goals
Theorem: WeakPNT
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
s : ℂ
hs : 1 < s.re
⊢ s ≠ 1
Tactic:
contrapose! hs
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
s : ℂ
hs : s = 1
⊢ s.re ≤ 1
Theorem: WeakPNT
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
s : ℂ
hs : s = 1
⊢ s.re ≤ 1
Tactic:
simp [hs]
Proof state after:
no goals
Theorem: WeakPNT
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
l2 : ∀ (s : ℂ), 1 < s.re → (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
⊢ {s | 1 ≤ s.re} ⊆ {z | z = 1 ∨ riemannZeta z ≠ 0}
Tactic:
tauto
Proof state after:
no goals
Theorem: WeakPNT
Proof state before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
l2 : ∀ (s : ℂ), 1 < s.re → (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
l3 : ContinuousOn (-deriv ζ₁ / ζ₁) {s | 1 ≤ s.re}
l4 : cheby fun n => ↑(Λ n)
σ' : ℝ
hσ' : 1 < σ'
⊢ Summable (nterm (fun n => ↑(Λ n)) σ')
Tactic:
simpa only [← nterm_eq_norm_term] using (@ArithmeticFunction.LSeriesSummable_vonMangoldt σ' hσ').norm
Proof state after:
no goals
Theorem: limiting_fourier_variant
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
ψ : CS 2 ℂ
hψpos : ∀ (y : ℝ), 0 ≤ (𝓕 ψ.toFun y).re ∧ (𝓕 ψ.toFun y).im = 0
hx : 1 ≤ x
⊢ ∑' (n : ℕ), ↑(f n) / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
sorry
Proof state after:
no goals
Theorem: crude_upper_bound
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
ψ : CS 2 ℂ
hψpos : ∀ (y : ℝ), 0 ≤ (𝓕 ψ.toFun y).re ∧ (𝓕 ψ.toFun y).im = 0
⊢ ∃ B, ∀ (x : ℝ), 0 < x → ‖∑' (n : ℕ), ↑(f n) / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ ≤ B
Tactic:
sorry
Proof state after:
no goals
Theorem: auto_cheby
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
⊢ cheby fun n => ↑(f n)
Tactic:
sorry
Proof state after:
no goals
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux1
Proof state before:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace ℝ G
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) (μ.prod volume)
hfg' : Integrable (fun x => (B (f x)) (g' x)) (μ.prod volume)
hfg : Integrable (fun x => (B (f x)) (g x)) (μ.prod volume)
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
⊢ ∫ (x : E), ∫ (t : ℝ), (B (f (x, t))) (g' (x, t)) ∂μ = ∫ (x : E), -∫ (t : ℝ), (B (f' (x, t))) (g (x, t)) ∂μ
Tactic:
apply integral_congr_ae
Proof state after:
case h
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace ℝ G
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) (μ.prod volume)
hfg' : Integrable (fun x => (B (f x)) (g' x)) (μ.prod volume)
hfg : Integrable (fun x => (B (f x)) (g x)) (μ.prod volume)
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
⊢ (fun a => ∫ (t : ℝ), (B (f (a, t))) (g' (a, t))) =ᶠ[ae μ] fun a => -∫ (t : ℝ), (B (f' (a, t))) (g (a, t))
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux1
Proof state before:
case h
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace ℝ G
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) (μ.prod volume)
hfg' : Integrable (fun x => (B (f x)) (g' x)) (μ.prod volume)
hfg : Integrable (fun x => (B (f x)) (g x)) (μ.prod volume)
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
⊢ (fun a => ∫ (t : ℝ), (B (f (a, t))) (g' (a, t))) =ᶠ[ae μ] fun a => -∫ (t : ℝ), (B (f' (a, t))) (g (a, t))
Tactic:
filter_upwards [hf'g.prod_right_ae, hfg'.prod_right_ae, hfg.prod_right_ae]
  with x hf'gx hfg'x  hfgx
Proof state after:
case h
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace ℝ G
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) (μ.prod volume)
hfg' : Integrable (fun x => (B (f x)) (g' x)) (μ.prod volume)
hfg : Integrable (fun x => (B (f x)) (g x)) (μ.prod volume)
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
x : E
hf'gx : Integrable (fun y => (B (f' (x, y))) (g (x, y))) volume
hfg'x : Integrable (fun y => (B (f (x, y))) (g' (x, y))) volume
hfgx : Integrable (fun y => (B (f (x, y))) (g (x, y))) volume
⊢ ∫ (t : ℝ), (B (f (x, t))) (g' (x, t)) = -∫ (t : ℝ), (B (f' (x, t))) (g (x, t))