Источник / закреплённая редакция
Mathlib.NumberTheory.LSeries.RiemannZeta
Источник пакета mathlib.zeta · mathlib4@de5ce8a9a66a4aa68a9bdbb35b63a06d34d9ca11:Mathlib/NumberTheory/LSeries/RiemannZeta.lean
- work
- urn:arxo:mathlib.zeta#MATHLIB_ZETA_LEAN
- номер
- mathlib4@de5ce8a9a66a4aa68a9bdbb35b63a06d34d9ca11:Mathlib/NumberTheory/LSeries/RiemannZeta.lean
- вид
- urn:arxo:mathlib.zeta#treatise
MATHLIB_ZETA_LEAN_EDITION
- edition
- urn:arxo:mathlib.zeta#MATHLIB_ZETA_LEAN_EDITION
- язык
- en
- официальность
- official
- материализация
- PINNED_OFFICIAL_BYTES
- жизненный цикл
- —
Публикации
| URI | Тип | documentHash | Получено |
|---|---|---|---|
| https://raw.githubusercontent.com/leanprover-community/mathlib4/de5ce8a9a66a4aa68a9bdbb35b63a06d34d9ca11/Mathlib/NumberTheory/LSeries/RiemannZeta.lean | text/plain; charset=utf-8 | sha256:8d24b729a30f1fef0820f0f7c9cdbb5910df30dfac2c597eb666794bead08b1c | 2026-09-16T20:30:00Z |
Фрагменты — 6
completedRiemannZeta · defn · на него ссылаются: 5
en · official · sha256:40ae657a56e4cc4024164d8a78ffacdb6e71a56aa764e2d2d68465bdbf6211e2EN
/-- 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Ссылаются нормы: DeclCompletedRiemannZeta, completed-kind, completed-name, completed-reason, completed-status
riemannZeta_one_sub · lemma · на него ссылаются: 5
en · official · sha256:8d2760aeca3cf00e0f72e0092a3ea2afbc0a0747a95940277eb2ae38e15f6e65EN
/-- 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]Ссылаются нормы: DeclFunctionalEquation, funceq-kind, funceq-name, funceq-reason, funceq-status
RiemannHypothesis · defn · на него ссылаются: 12
en · official · sha256:7127db29e929986bbf5af0c6ef0d6075973a882f3d0701cff7f2893aca8f5a8bEN
/-- 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Ссылаются нормы: DeclRiemannHypothesis, NativeDeclaration, blocked_reason, concept_alignment, import_status, native_kind, native_name, rh-alignment, rh-kind, rh-name, rh-reason, rh-status
riemannZeta · defn · на него ссылаются: 5
en · official · sha256:b466f4f635c83fd3814800e4b6f1d14382713d812afb1bb881f07676717859cbEN
/-- The Riemann zeta function `ζ(s)`. -/
@[wikidata Q187235]
def riemannZeta := hurwitzZetaEven 0Ссылаются нормы: DeclRiemannZeta, riemannzeta-kind, riemannzeta-name, riemannzeta-reason, riemannzeta-status
riemannZeta_neg_two_mul_nat_add_one · lemma · на него ссылаются: 8
en · official · sha256:58dfbb11b3f26b7123c39738090633739a7058936d268acad682d770a67fdbe4EN
/-- 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Ссылаются нормы: DeclTrivialZero, Import_TrivialZeroLocation, candidate_trivial_zero_index, is_known_trivial_zero_location, trivialzero-alignment, trivialzero-kind, trivialzero-name, trivialzero-status
riemannZeta_zero · lemma · на него ссылаются: 5
en · official · sha256:6da23419fa11dc9fd350d188f2565792aedf4d4dbcbc4e0017483756273a5ca7EN
/-- We have `ζ(0) = -1 / 2`. -/
theorem riemannZeta_zero : riemannZeta 0 = -1 / 2 := by
simp_rw [riemannZeta, hurwitzZetaEven, Function.update_self, ite_true]Ссылаются нормы: DeclRiemannZetaZero, zetazero-kind, zetazero-name, zetazero-reason, zetazero-status
Хэш рядом с текстом — sha256 его точных байтов. Он и есть проверка того, что показанный текст совпадает с закреплённым в пакете: расхождение роняет статику оракула.