Source indexedlemma · leanprover/lean4:v4.32.0

CH2.h_comp

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:2001 to 2007

Mathematical statement

Exact Lean statement

lemma h_comp (ε ν : ℝ) (hlam : ν ≠ 0) : ContDiff ℝ 2 (fun t : ℝ => (-2 * Real.pi * Complex.I * t + ν) * (Complex.cosh ((-2 * Real.pi * Complex.I * t + ν) / 2) / Complex.sinh ((-2 * Real.pi * Complex.I * t + ν) / 2) + ε) / 2)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma h_comp (ε ν : ℝ) (hlam : ν ≠ 0) : ContDiff ℝ 2 (fun t : ℝ => (-2 * Real.pi * Complex.I * t + ν) * (Complex.cosh ((-2 * Real.pi * Complex.I * t + ν) / 2) / Complex.sinh ((-2 * Real.pi * Complex.I * t + ν) / 2) + ε) / 2) := by  apply_rules [ContDiff.div, ContDiff.mul, ContDiff.add, contDiff_const, contDiff_id] <;> try fun_prop  · exact Complex.conjCLE.contDiff.comp (by fun_prop)  · refine Complex.ofRealCLM.contDiff.comp ?_    refine ContDiff.inv (by fun_prop) ?_    intro x; rw [ne_eq, Complex.normSq_eq_zero]    exact sinh_ne_zero_of_re_ne_zero (by simp [hlam])