Source indexedtheorem · leanprover/lean4:v4.32.0

sumResiduesIn_eq12_eq

PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:492 to 531

Source documentation

Part 5 (residue bookkeeping): the sum of residues of the eq.(12) integrand f over the poles inside the rectangle equals Φ(-1) - zeroes_sum. The two pole contributions are s = 1 (residue Φ(-1)) and the non-trivial zeros ρ (residue -ord(ρ)·Φ(-ρ)); the set-characterization of the pole set and the residue values are supplied at the call site.

Exact Lean statement

theorem sumResiduesIn_eq12_eq {f Φ : ℂ → ℂ} {a T : ℝ}
    (hf_mero : MeromorphicOn f (Rectangle ((-a : ℝ) - (T : ℂ) * I) ((1 + a : ℝ) + (T : ℂ) * I)))
    (hfin : (riemannZeta.zeroes_rect (Set.Ioo 0 1) (Set.Ioo (-T) T)).Finite)
    (h1mem : (1 : ℂ) ∈ Rectangle ((-a : ℝ) - (T : ℂ) * I) ((1 + a : ℝ) + (T : ℂ) * I))
    (hZsub : (riemannZeta.zeroes_rect (Set.Ioo 0 1) (Set.Ioo (-T) T) : Set ℂ) ⊆
      Rectangle ((-a : ℝ) - (T : ℂ) * I) ((1 + a : ℝ) + (T : ℂ) * I))
    (h1notZ : (1 : ℂ) ∉ riemannZeta.zeroes_rect (Set.Ioo 0 1) (Set.Ioo (-T) T))
    (hset : Rectangle ((-a : ℝ) - (T : ℂ) * I) ((1 + a : ℝ) + (T : ℂ) * I) ∩
          {s | meromorphicOrderAt f s < 0}
        = insert (1 : ℂ) (riemannZeta.zeroes_rect (Set.Ioo 0 1) (Set.Ioo (-T) T)) ∩
          {s | meromorphicOrderAt f s < 0})
    (hres1 : residue f 1 = Φ (-1))
    (hresZ : ∀ ρ ∈ riemannZeta.zeroes_rect (Set.Ioo 0 1) (Set.Ioo (-T) T),
      residue f ρ = -(riemannZeta.order ρ : ℂ) * Φ (-ρ)) :
    sumResiduesIn f (Rectangle ((-a : ℝ) - (T : ℂ) * I) ((1 + a : ℝ) + (T : ℂ) * I) ∩
        {s | meromorphicOrderAt f s < 0})
      = Φ (-1) - riemannZeta.zeroes_sum (Set.Ioo 0 1) (Set.Ioo (-T) T) (fun ρ ↦ Φ (-ρ))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem sumResiduesIn_eq12_eq {f Φ : ℂ → ℂ} {a T : ℝ}    (hf_mero : MeromorphicOn f (Rectangle ((-a : ℝ) - (T : ℂ) * I) ((1 + a : ℝ) + (T : ℂ) * I)))    (hfin : (riemannZeta.zeroes_rect (Set.Ioo 0 1) (Set.Ioo (-T) T)).Finite)    (h1mem : (1 : ℂ) ∈ Rectangle ((-a : ℝ) - (T : ℂ) * I) ((1 + a : ℝ) + (T : ℂ) * I))    (hZsub : (riemannZeta.zeroes_rect (Set.Ioo 0 1) (Set.Ioo (-T) T) : Set ℂ) ⊆      Rectangle ((-a : ℝ) - (T : ℂ) * I) ((1 + a : ℝ) + (T : ℂ) * I))    (h1notZ : (1 : ℂ) ∉ riemannZeta.zeroes_rect (Set.Ioo 0 1) (Set.Ioo (-T) T))    (hset : Rectangle ((-a : ℝ) - (T : ℂ) * I) ((1 + a : ℝ) + (T : ℂ) * I) ∩          {s | meromorphicOrderAt f s < 0}        = insert (1 : ℂ) (riemannZeta.zeroes_rect (Set.Ioo 0 1) (Set.Ioo (-T) T)) ∩          {s | meromorphicOrderAt f s < 0})    (hres1 : residue f 1 = Φ (-1))    (hresZ : ∀ ρ ∈ riemannZeta.zeroes_rect (Set.Ioo 0 1) (Set.Ioo (-T) T),      residue f ρ = -(riemannZeta.order ρ : ℂ) * Φ (-ρ)) :    sumResiduesIn f (Rectangle ((-a : ℝ) - (T : ℂ) * I) ((1 + a : ℝ) + (T : ℂ) * I) ∩        {s | meromorphicOrderAt f s < 0})      = Φ (-1) - riemannZeta.zeroes_sum (Set.Ioo 0 1) (Set.Ioo (-T) T) (fun ρ ↦ Φ (-ρ)) := by  have h1notZF : (1 : ℂ) ∉ hfin.toFinset := by rw [hfin.mem_toFinset]; exact h1notZ  -- Step 1: replace the pole-set sum by the sum over `{1} ∪ Z`.  rw [sumResiduesIn_inter_eq_of_set_eq hset ?_]  · -- Step 2: evaluate the finite sum over `insert 1 Z`.    rw [show insert (1 : ℂ) (riemannZeta.zeroes_rect (Set.Ioo 0 1) (Set.Ioo (-T) T))          = ((insert (1 : ℂ) hfin.toFinset : Finset ℂ) : Set ℂ) by          rw [Finset.coe_insert, hfin.coe_toFinset], sumResiduesIn, Finset.tsum_subtype',      Finset.sum_insert h1notZF, hres1,      zeroes_sum_eq_toFinset_sum (fun ρ ↦ Φ (-ρ)) hfin]    have hsum : ∑ z ∈ hfin.toFinset, residue f z        = ∑ z ∈ hfin.toFinset, -(Φ (-z) * (riemannZeta.order z : ℂ)) :=      Finset.sum_congr rfl fun z hz => by        rw [hresZ z (hfin.mem_toFinset.mp hz)]; ring    rw [hsum, Finset.sum_neg_distrib]    ring  · -- residues vanish at non-pole points of `{1} ∪ Z`.    intro s hs hs_not    have hsbox : s ∈ Rectangle ((-a : ℝ) - (T : ℂ) * I) ((1 + a : ℝ) + (T : ℂ) * I) := by      rcases Set.mem_insert_iff.mp hs with h1 | hZ      · rw [h1]; exact h1mem      · exact hZsub hZ    have hord : 0 ≤ meromorphicOrderAt f s := not_lt.mp (by simpa using hs_not)    exact residue_eq_zero_of_not_pole_of_meromorphicAt (hf_mero s hsbox) hord