Source indexedtheorem · leanprover/lean4:v4.32.0

SmoothedChebyshevPull2_aux1

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:1347 to 1364

Mathematical statement

Exact Lean statement

theorem SmoothedChebyshevPull2_aux1 {T σ₁ : ℝ} (σ₁lt : σ₁ < 1)
  (holoOn : HolomorphicOn (ζ' / ζ) (Icc σ₁ 2 ×ℂ Icc (-T) T \ {1})) :
  ContinuousOn (fun (t : ℝ) ↦ -ζ' (σ₁ + t * I) / ζ (σ₁ + t * I)) (Icc (-T) T)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem SmoothedChebyshevPull2_aux1 {T σ₁ : ℝ} (σ₁lt : σ₁ < 1)  (holoOn : HolomorphicOn (ζ' / ζ) (Icc σ₁ 2 ×ℂ Icc (-T) T \ {1})) :  ContinuousOn (fun (t : ℝ) ↦ -ζ' (σ₁ + t * I) / ζ (σ₁ + t * I)) (Icc (-T) T) := by  rw [show (fun (t : ℝ) ↦ -ζ' (↑σ₁ + ↑t * I) / ζ (↑σ₁ + ↑t * I)) =      -(ζ' / ζ) ∘ (fun (t : ℝ) ↦ ↑σ₁ + ↑t * I) by ext; simp; ring_nf]  apply ContinuousOn.neg  apply holoOn.continuousOn.comp (by fun_prop)  intro t ht  simp only [Set.mem_sdiff, mem_singleton_iff]  constructor  · apply mem_reProdIm.mpr    simp only [add_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im, I_im, mul_one, sub_self,      add_zero, add_im, mul_im, zero_add, left_mem_Icc, ht, and_true]    linarith  · intro h    replace h := congr_arg re h    simp at h    linarith