internlm/Lean-Github huggingface dataset:
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_2.e_a.e_a
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
⊢ ∫ (t : ℝ), ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) =
    ∑' (n : ℕ), ∫ (t : ℝ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)
Tactic:
have := @MellinOfSmooth1b ψ diffΨ suppΨ 2 2 (by norm_num) ε εpos
Proof state after:
case calc_2.e_a.e_a
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
this : (fun s => ‖𝓜 (fun x => ↑(Smooth1 ψ ε x)) s‖) =O[𝓟 {s | 2 ≤ s.re ∧ s.re ≤ 2}] fun s => 1 / (ε * ‖s‖ ^ 2)
⊢ ∫ (t : ℝ), ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) =
    ∑' (n : ℕ), ∫ (t : ℝ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_2.e_a.e_a
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
this : (fun s => ‖𝓜 (fun x => ↑(Smooth1 ψ ε x)) s‖) =O[𝓟 {s | 2 ≤ s.re ∧ s.re ≤ 2}] fun s => 1 / (ε * ‖s‖ ^ 2)
⊢ ∫ (t : ℝ), ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) =
    ∑' (n : ℕ), ∫ (t : ℝ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)
Tactic:
simp_rw [Asymptotics.isBigO_iff] at this
Proof state after:
case calc_2.e_a.e_a
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
this : ∃ c, ∀ᶠ (x : ℂ) in 𝓟 {s | 2 ≤ s.re ∧ s.re ≤ 2}, ‖‖𝓜 (fun x => ↑(Smooth1 ψ ε x)) x‖‖ ≤ c * ‖1 / (ε * ‖x‖ ^ 2)‖
⊢ ∫ (t : ℝ), ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) =
    ∑' (n : ℕ), ∫ (t : ℝ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_2.e_a.e_a
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
this : ∃ c, ∀ᶠ (x : ℂ) in 𝓟 {s | 2 ≤ s.re ∧ s.re ≤ 2}, ‖‖𝓜 (fun x => ↑(Smooth1 ψ ε x)) x‖‖ ≤ c * ‖1 / (ε * ‖x‖ ^ 2)‖
⊢ ∫ (t : ℝ), ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) =
    ∑' (n : ℕ), ∫ (t : ℝ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)
Tactic:
obtain ⟨c, hc⟩ := this
Proof state after:
case calc_2.e_a.e_a.intro
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ᶠ (x : ℂ) in 𝓟 {s | 2 ≤ s.re ∧ s.re ≤ 2}, ‖‖𝓜 (fun x => ↑(Smooth1 ψ ε x)) x‖‖ ≤ c * ‖1 / (ε * ‖x‖ ^ 2)‖
⊢ ∫ (t : ℝ), ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) =
    ∑' (n : ℕ), ∫ (t : ℝ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_2.e_a.e_a.intro
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ᶠ (x : ℂ) in 𝓟 {s | 2 ≤ s.re ∧ s.re ≤ 2}, ‖‖𝓜 (fun x => ↑(Smooth1 ψ ε x)) x‖‖ ≤ c * ‖1 / (ε * ‖x‖ ^ 2)‖
⊢ ∫ (t : ℝ), ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) =
    ∑' (n : ℕ), ∫ (t : ℝ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)
Tactic:
simp only [Real.norm_eq_abs, Complex.abs_abs, one_div, mul_inv_rev, norm_mul,
  norm_inv, norm_pow, eventually_principal, mem_setOf_eq, and_imp] at hc
Proof state after:
case calc_2.e_a.e_a.intro
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), 2 ≤ x.re → x.re ≤ 2 → |‖𝓜 (fun x => ↑(Smooth1 ψ ε x)) x‖| ≤ c * ((|‖x‖| ^ 2)⁻¹ * |ε|⁻¹)
⊢ ∫ (t : ℝ), ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) =
    ∑' (n : ℕ), ∫ (t : ℝ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_2.e_a.e_a.intro
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), 2 ≤ x.re → x.re ≤ 2 → |‖𝓜 (fun x => ↑(Smooth1 ψ ε x)) x‖| ≤ c * ((|‖x‖| ^ 2)⁻¹ * |ε|⁻¹)
⊢ ∫ (t : ℝ), ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) =
    ∑' (n : ℕ), ∫ (t : ℝ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)
Tactic:
simp only [Complex.norm_eq_abs, Complex.abs_abs] at hc
Proof state after:
case calc_2.e_a.e_a.intro
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
c : ℝ
hc :
  ∀ (x : ℂ), 2 ≤ x.re → x.re ≤ 2 → Complex.abs (𝓜 (fun x => ↑(Smooth1 ψ ε x)) x) ≤ c * ((Complex.abs x ^ 2)⁻¹ * |ε|⁻¹)
⊢ ∫ (t : ℝ), ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) =
    ∑' (n : ℕ), ∫ (t : ℝ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_2.e_a.e_a.intro
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
c : ℝ
hc :
  ∀ (x : ℂ), 2 ≤ x.re → x.re ≤ 2 → Complex.abs (𝓜 (fun x => ↑(Smooth1 ψ ε x)) x) ≤ c * ((Complex.abs x ^ 2)⁻¹ * |ε|⁻¹)
⊢ ∫ (t : ℝ), ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) =
    ∑' (n : ℕ), ∫ (t : ℝ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)
Tactic:
replace hc (t : ℝ) := hc (2 + t * I) (by simp) (by simp)
Proof state after:
case calc_2.e_a.e_a.intro
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
c : ℝ
hc :
  ∀ (t : ℝ), Complex.abs (𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) ≤ c * ((Complex.abs (2 + ↑t * I) ^ 2)⁻¹ * |ε|⁻¹)
⊢ ∫ (t : ℝ), ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) =
    ∑' (n : ℕ), ∫ (t : ℝ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_2.e_a.e_a.intro
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
c : ℝ
hc :
  ∀ (t : ℝ), Complex.abs (𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) ≤ c * ((Complex.abs (2 + ↑t * I) ^ 2)⁻¹ * |ε|⁻¹)
⊢ ∫ (t : ℝ), ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) =
    ∑' (n : ℕ), ∫ (t : ℝ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)
Tactic:
sorry
Proof state after:
no goals
Theorem: SmoothedChebyshevDirichlet
Proof state before:
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: SmoothedChebyshevDirichlet
Proof state before:
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
c : ℝ
hc :
  ∀ (x : ℂ), 2 ≤ x.re → x.re ≤ 2 → Complex.abs (𝓜 (fun x => ↑(Smooth1 ψ ε x)) x) ≤ c * ((Complex.abs x ^ 2)⁻¹ * |ε|⁻¹)
t : ℝ
⊢ 2 ≤ (2 + ↑t * I).re
Tactic:
simp
Proof state after:
no goals
Theorem: SmoothedChebyshevDirichlet
Proof state before:
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
c : ℝ
hc :
  ∀ (x : ℂ), 2 ≤ x.re → x.re ≤ 2 → Complex.abs (𝓜 (fun x => ↑(Smooth1 ψ ε x)) x) ≤ c * ((Complex.abs x ^ 2)⁻¹ * |ε|⁻¹)
t : ℝ
⊢ (2 + ↑t * I).re ≤ 2
Tactic:
simp
Proof state after:
no goals
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_3
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
⊢ 1 / (2 * ↑π * I) *
      (I *
        ∑' (n : ℕ),
          ∫ (t : ℝ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)) =
    1 / (2 * ↑π * I) *
      (I * ∑' (n : ℕ), ↑(Λ n) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I))
Tactic:
field_simp
Proof state after:
case calc_3
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
⊢ (I *
        ∑' (n : ℕ),
          ∫ (t : ℝ), ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I)) /
      (2 * ↑π * I) =
    (I * ∑' (n : ℕ), ↑(Λ n) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)) /
      (2 * ↑π * I)
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_3
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
⊢ (I *
        ∑' (n : ℕ),
          ∫ (t : ℝ), ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I)) /
      (2 * ↑π * I) =
    (I * ∑' (n : ℕ), ↑(Λ n) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)) /
      (2 * ↑π * I)
Tactic:
congr
Proof state after:
case calc_3.e_a.e_a.e_f
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
⊢ (fun n =>
      ∫ (t : ℝ), ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I)) =
    fun n => ↑(Λ n) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_3.e_a.e_a.e_f
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
⊢ (fun n =>
      ∫ (t : ℝ), ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I)) =
    fun n => ↑(Λ n) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)
Tactic:
ext n
Proof state after:
case calc_3.e_a.e_a.e_f.h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
⊢ ∫ (t : ℝ), ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I) =
    ↑(Λ n) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_3.e_a.e_a.e_f.h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
⊢ ∫ (t : ℝ), ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I) =
    ↑(Λ n) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)
Tactic:
rw [← MeasureTheory.integral_mul_left ]
Proof state after:
case calc_3.e_a.e_a.e_f.h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
⊢ ∫ (t : ℝ), ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I) =
    ∫ (a : ℝ), ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑a * I) * (↑X / ↑n) ^ (2 + ↑a * I))
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_3.e_a.e_a.e_f.h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
⊢ ∫ (t : ℝ), ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I) =
    ∫ (a : ℝ), ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑a * I) * (↑X / ↑n) ^ (2 + ↑a * I))
Tactic:
congr
Proof state after:
case calc_3.e_a.e_a.e_f.h.e_f
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
⊢ (fun t => ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I)) = fun a =>
    ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑a * I) * (↑X / ↑n) ^ (2 + ↑a * I))
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_3.e_a.e_a.e_f.h.e_f
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
⊢ (fun t => ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I)) = fun a =>
    ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑a * I) * (↑X / ↑n) ^ (2 + ↑a * I))
Tactic:
ext t
Proof state after:
case calc_3.e_a.e_a.e_f.h.e_f.h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
t : ℝ
⊢ ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I) =
    ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I))
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case calc_3.e_a.e_a.e_f.h.e_f.h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
t : ℝ
⊢ ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I) =
    ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I))
Tactic:
by_cases n_ne_zero : n = 0
Proof state after:
case pos
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
t : ℝ
n_ne_zero : n = 0
⊢ ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I) =
    ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I))

case neg
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I) =
    ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I))
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case pos
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
t : ℝ
n_ne_zero : n = 0
⊢ ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I) =
    ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I))

case neg
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I) =
    ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I))
Tactic:
simp [n_ne_zero]
Proof state after:
case neg
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I) =
    ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I))
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑(Λ n) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I) =
    ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I))
Tactic:
rw [mul_div_assoc, mul_assoc]
Proof state after:
case neg
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I))) =
    ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I))
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I))) =
    ↑(Λ n) * (mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I))
Tactic:
congr
Proof state after:
case neg.e_a.e_a
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I) = (↑X / ↑n) ^ (2 + ↑t * I)
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg.e_a.e_a
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑X ^ (2 + ↑t * I) / ↑n ^ (2 + ↑t * I) = (↑X / ↑n) ^ (2 + ↑t * I)
Tactic:
rw [(div_eq_iff ?_).mpr]
Proof state after:
case neg.e_a.e_a
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑X ^ (2 + ↑t * I) = (↑X / ↑n) ^ (2 + ↑t * I) * ↑n ^ (2 + ↑t * I)

ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑n ^ (2 + ↑t * I) ≠ 0
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg.e_a.e_a
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑X ^ (2 + ↑t * I) = (↑X / ↑n) ^ (2 + ↑t * I) * ↑n ^ (2 + ↑t * I)

ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑n ^ (2 + ↑t * I) ≠ 0
Tactic:
have := @mul_cpow_ofReal_nonneg (a := X / (n : ℝ)) (b := (n : ℝ)) (r := 2 + t * I) ?_ ?_
Proof state after:
case neg.e_a.e_a.refine_3
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
this : (↑(X / ↑n) * ↑↑n) ^ (2 + ↑t * I) = ↑(X / ↑n) ^ (2 + ↑t * I) * ↑↑n ^ (2 + ↑t * I)
⊢ ↑X ^ (2 + ↑t * I) = (↑X / ↑n) ^ (2 + ↑t * I) * ↑n ^ (2 + ↑t * I)

case neg.e_a.e_a.refine_1
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ 0 ≤ X / ↑n

case neg.e_a.e_a.refine_2
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ 0 ≤ ↑n

ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
⊢ ↑n ^ (2 + ↑t * I) ≠ 0