Source indexedtheorem · leanprover/lean4:v4.32.0

CH2.shift_upwards_phi_diff

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3665 to 3675

Source documentation

At a point z = -1 + i t on the vertical line Re z = -1 (with t ≥ 0), the combination Φ_circ - Φ_star equals -Φ_star evaluated on the imaginary axis at i t.

Exact Lean statement

theorem shift_upwards_phi_diff (ν ε : ℝ) (hν : ν > 0) (t : ℝ) (ht : 0 ≤ t) :
    Phi_circ ν ε (-1 + I * t) - Phi_star ν ε (-1 + I * t) = -Phi_star ν ε (I * t)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem shift_upwards_phi_diff (ν ε : ℝ) (hν : ν > 0) (t : ℝ) (ht : 0 ≤ t) :    Phi_circ ν ε (-1 + I * t) - Phi_star ν ε (-1 + I * t) = -Phi_star ν ε (I * t) := by  have h_re : (-2 : ℂ) * ↑π * I * (I * ↑t) + ↑ν ≠ 0 := by    intro h; apply_fun Complex.re at h; simp at h; nlinarith [Real.pi_pos, ht, hν]  have h_im (m : ℤ) (hm : m ≠ 0) : (-2 : ℂ) * ↑π * I * (I * ↑t - ↑m) + ↑ν ≠ 0 := by    intro h; apply_fun Complex.im at h; simp [Real.pi_pos.ne.symm, hm] at h  have h_circ_shift (z : ℂ) : Phi_circ ν ε (z - 1) = Phi_circ ν ε z := by    have h := (Phi_circ_periodic ν ε (z - 1)).symm; rwa [sub_add_cancel] at h  have haff := phi_star_affine_periodic ν ε hν (I * ↑t) 1 h_re (h_im 1 (by norm_num))  simp only [Int.cast_one, one_mul] at haff  rw [show -1 + I * ↑t = I * ↑t - 1 by ring, h_circ_shift, haff]; ring