Source indexedtheorem · leanprover/lean4:v4.32.0

CH2.Phi_star.contDiff_real

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:2009 to 2018

Mathematical statement

Exact Lean statement

theorem Phi_star.contDiff_real (ν ε : ℝ) (hlam : ν ≠ 0) :
    ContDiff ℝ 2 (fun (t : ℝ) ↦ Phi_star ν ε (t : ℂ))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem Phi_star.contDiff_real (ν ε : ℝ) (hlam : ν ≠ 0) :    ContDiff ℝ 2 (fun (t : ℝ) ↦ Phi_star ν ε (t : ℂ)) := by  have h_diff_B : ContDiff ℝ 2 (fun t : ℝ => B ε (-2 * Real.pi * Complex.I * t + ν)) := by    have h_comp := h_comp ε ν hlam    convert! h_comp using 1    ext t    by_cases h : (-(2 * Real.pi * Complex.I * t) + ν : ℂ) = 0 <;> simp_all [Complex.sinh, Complex.cosh, h_B_rational]; ring_nf    norm_num [Complex.ext_iff] at h    simp_all only [not_true_eq_false]  convert! h_diff_B.sub contDiff_const |> fun h => h.div_const (2 * Real.pi * Complex.I) using 1