Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.zeroes_rect_positive_height_card_le_zeroes_sum_order

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:149 to 171

Mathematical statement

Exact Lean statement

lemma zeroes_rect_positive_height_card_le_zeroes_sum_order (T : ℝ) :
    (Nat.card (riemannZeta.zeroes_rect (.Ioo 0 1) (.Ioo 0 T)) : ℝ) ≤
      riemannZeta.zeroes_sum (.Ioo 0 1) (.Ioo 0 T) (fun _ ↦ (1 : ℝ))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma zeroes_rect_positive_height_card_le_zeroes_sum_order (T : ℝ) :    (Nat.card (riemannZeta.zeroes_rect (.Ioo 0 1) (.Ioo 0 T)) : ℝ) ≤      riemannZeta.zeroes_sum (.Ioo 0 1) (.Ioo 0 T) (fun _ ↦ (1 : ℝ)) := by  classical  haveI : Finite (riemannZeta.zeroes_rect (.Ioo 0 1) (.Ioo 0 T)) :=    Set.finite_coe_iff.mpr (zeroes_rect_Ioo_critical_positive_height_finite T)  letI := Fintype.ofFinite (riemannZeta.zeroes_rect (.Ioo 0 1) (.Ioo 0 T))  unfold riemannZeta.zeroes_sum  rw [tsum_fintype]  calc    (Nat.card (riemannZeta.zeroes_rect (.Ioo 0 1) (.Ioo 0 T)) : ℝ)        = ∑ _rho : riemannZeta.zeroes_rect (.Ioo 0 1) (.Ioo 0 T), (1 : ℝ) := by          simp [Nat.card_eq_fintype_card]    _ ≤ ∑ rho : riemannZeta.zeroes_rect (.Ioo 0 1) (.Ioo 0 T),          (riemannZeta.order (rho : ℂ) : ℝ) := by          refine Finset.sum_le_sum fun rho _ ↦ ?_          have horder : (1 : ℤ) ≤ riemannZeta.order (rho : ℂ) :=            riemannZeta_one_le_order_nontrivialZero              ⟨(rho : ℂ), rho.property.1, Set.mem_univ _, rho.property.2.2⟩          exact_mod_cast horder    _ = ∑ rho : riemannZeta.zeroes_rect (.Ioo 0 1) (.Ioo 0 T),          (1 : ℝ) * (riemannZeta.order (rho : ℂ) : ℝ) := by          simp