Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Jensen Real-Zero Count

Abstract

Jensen theory bounds the real-part crossing count by a logarithmic term.

Theorem 1.1 (Jensen Real-Zero Count).

Lean statement: D5/S3/Weil/ZetaRvm/ReZeroCount.reZeroSet_card_le

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaRvm/ReZeroCount.reZeroSet_card_le (✓ std3). ∎

Source. Repository-derived.

Commentary.

Jensen theory bounds the real-part crossing count by a logarithmic term.

References