LowHeightZeroExclusion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The local exceptional-zero argument with explicit margins

theorem OAI.Ostmann.near_axis_zero_indices_unique line 14
theorem OAI.Ostmann.near_zero_small_height line 35

theorem OAI.Ostmann.near_low_height_zeros_real_unique line 68

Source documentation

The local inequalities force every exceptional low-height zero to be real, and count multiplicities: two distinct indices are impossible.

theorem near_low_height_zeros_real_unique (χ : PrimitiveRealCharacter) (δ R S : ℝ)
    (hδ : 0 < δ) (hδ1 : δ ≤ 1) (hR : δ * R ≤ 1 / 10)
    (hS : δ * (2 * Real.log χ.modulus + S) ≤ 1 / 10)
    (hreal : shiftedRealCharacterZeroSum χ ((1 + δ : ℝ) : ℂ) ≤ 1 / δ + R)
    (hshift : ∀ t : ℝ, |t| ≤ 1 →
      4 * shiftedRealCharacterZeroSum χ (((1 + δ : ℝ) : ℂ) + (t : ℂ) * I) ≤
        3 / δ + realZeroKernel δ (2 * t) + 2 * Real.log χ.modulus + S) :
    (∀ i, 1 - δ / 20 ≤ ((realCharacterActualZeros χ).zeros i).re →
      |((realCharacterActualZeros χ).zeros i).im| ≤ 1 →
      ((realCharacterActualZeros χ).zeros i).im = 0) ∧
    (∀ i j, 1 - δ / 20 ≤ ((realCharacterActualZeros χ).zeros i).re →
      1 - δ / 20 ≤ ((realCharacterActualZeros χ).zeros j).re →
…

Mentions: OAI.Ostmann.PrimitiveRealCharacter, OAI.Ostmann.shiftedRealCharacterZeroSum, OAI.Ostmann.realZeroKernel, OAI.Ostmann.realCharacterActualZeros