Source indexedtheorem · leanprover/lean4:v4.32.0

CH2.Phi_star_conj_neg

PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3426 to 3436

Source documentation

Conjugation symmetry of Φ^\star: Φ^\star(-\overline{w}) = -\overline{Φ^\star(w)}. This is the complex-argument generalization of Phi_star_conj_symm.

Exact Lean statement

theorem Phi_star_conj_neg (ν ε : ℝ) (w : ℂ) :
    Phi_star ν ε (-(starRingEnd ℂ w)) = -(starRingEnd ℂ (Phi_star ν ε w))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem Phi_star_conj_neg (ν ε : ℝ) (w : ℂ) :    Phi_star ν ε (-(starRingEnd ℂ w)) = -(starRingEnd ℂ (Phi_star ν ε w)) := by  dsimp [Phi_star]  simp only [neg_mul, map_div₀, map_sub, map_mul, map_ofNat, Complex.conj_ofReal, Complex.conj_I]  rw [B_conj]  simp only [map_add, map_neg, map_mul, Complex.conj_ofReal, Complex.conj_I, map_ofNat]  rw [B_conj]  simp only [Complex.conj_ofReal]  rw [show -(2 * (π : ℂ) * I * -(starRingEnd ℂ) w) + (ν : ℂ)        = -(2 * (π : ℂ) * -I * (starRingEnd ℂ) w) + (ν : ℂ) by ring,    mul_neg, div_neg, neg_neg]