Mathlib.NumberTheory.LSeries.RiemannZeta

en · official · sha256:40ae657a56e4cc4024164d8a78ffacdb6e71a56aa764e2d2d68465bdbf6211e2

/-- The completed Riemann zeta function, `Λ(s)`, which satisfies `Λ(s) = π ^ (-s / 2) Γ(s / 2) ζ(s)` (up to a minor correction at `s = 0`). -/ def completedRiemannZeta (s : ℂ) : ℂ := completedHurwitzZetaEven 0 s

Referencing norms: DeclCompletedRiemannZeta, completed-kind, completed-name, completed-reason, completed-status

en · official · sha256:8d2760aeca3cf00e0f72e0092a3ea2afbc0a0747a95940277eb2ae38e15f6e65

/-- Riemann zeta functional equation, formulated for `ζ`: if `1 - s ∉ ℕ`, then we have `ζ (1 - s) = 2 ^ (1 - s) * π ^ (-s) * Γ s * sin (π * (1 - s) / 2) * ζ s`. -/ theorem riemannZeta_one_sub {s : ℂ} (hs : ∀ n : ℕ, s ≠ -n) (hs' : s ≠ 1) : riemannZeta (1 - s) = 2 * (2 * π) ^ (-s) * Gamma s * cos (π * s / 2) * riemannZeta s := by rw [riemannZeta, hurwitzZetaEven_one_sub 0 hs (Or.inr hs'), cosZeta_zero, hurwitzZetaEven_zero]

Referencing norms: DeclFunctionalEquation, funceq-kind, funceq-name, funceq-reason, funceq-status

en · official · sha256:7127db29e929986bbf5af0c6ef0d6075973a882f3d0701cff7f2893aca8f5a8b

/-- A formal statement of the **Riemann hypothesis** – constructing a term of this type is worth a million dollars. -/ @[wikidata Q205966] def RiemannHypothesis : Prop := ∀ (s : ℂ) (_ : riemannZeta s = 0) (_ : ¬∃ n : ℕ, s = -2 * (n + 1)) (_ : s ≠ 1), s.re = 1 / 2

Referencing norms: DeclRiemannHypothesis, NativeDeclaration, blocked_reason, concept_alignment, import_status, native_kind, native_name, rh-alignment, rh-kind, rh-name, rh-reason, rh-status

en · official · sha256:b466f4f635c83fd3814800e4b6f1d14382713d812afb1bb881f07676717859cb

/-- The Riemann zeta function `ζ(s)`. -/ @[wikidata Q187235] def riemannZeta := hurwitzZetaEven 0

Referencing norms: DeclRiemannZeta, riemannzeta-kind, riemannzeta-name, riemannzeta-reason, riemannzeta-status

en · official · sha256:58dfbb11b3f26b7123c39738090633739a7058936d268acad682d770a67fdbe4

/-- The trivial zeroes of the zeta function. -/ theorem riemannZeta_neg_two_mul_nat_add_one (n : ℕ) : riemannZeta (-2 * (n + 1)) = 0 := hurwitzZetaEven_neg_two_mul_nat_add_one 0 n

Referencing norms: DeclTrivialZero, Import_TrivialZeroLocation, candidate_trivial_zero_index, is_known_trivial_zero_location, trivialzero-alignment, trivialzero-kind, trivialzero-name, trivialzero-status

en · official · sha256:6da23419fa11dc9fd350d188f2565792aedf4d4dbcbc4e0017483756273a5ca7

/-- We have `ζ(0) = -1 / 2`. -/ theorem riemannZeta_zero : riemannZeta 0 = -1 / 2 := by simp_rw [riemannZeta, hurwitzZetaEven, Function.update_self, ite_true]

Referencing norms: DeclRiemannZetaZero, zetazero-kind, zetazero-name, zetazero-reason, zetazero-status