Hardy zeta

11.22. HardyZeta.ZeroTopology🔗

theorem finite_zeros_in_bounded_interval (a b : ℝ) :
    {t : ℝ | t ∈ Icc a b ∧ hardyXi t = 0}.Finite := bya:ℝb:ℝ⊢ {t | t ∈ Icc a b ∧ hardyXi t = 0}.Finite
  have hc := ((isCompact_Icc : IsCompact (Icc a b)).image
    continuous_criticalPoint).inter_riemannZetaZeros_finitea:ℝb:ℝhc:(criticalPoint '' Icc a b ∩ riemannZetaZeros).Finite⊢ {t | t ∈ Icc a b ∧ hardyXi t = 0}.Finite
  have hp := hc.preimage criticalPoint_injective.injOna:ℝb:ℝhc:(criticalPoint '' Icc a b ∩ riemannZetaZeros).Finitehp:(criticalPoint ⁻¹' (criticalPoint '' Icc a b ∩ riemannZetaZeros)).Finite⊢ {t | t ∈ Icc a b ∧ hardyXi t = 0}.Finite
  apply hp.subseta:ℝb:ℝhc:(criticalPoint '' Icc a b ∩ riemannZetaZeros).Finitehp:(criticalPoint ⁻¹' (criticalPoint '' Icc a b ∩ riemannZetaZeros)).Finite⊢ {t | t ∈ Icc a b ∧ hardyXi t = 0} ⊆ criticalPoint ⁻¹' (criticalPoint '' Icc a b ∩ riemannZetaZeros)
  intro t hta:ℝb:ℝhc:(criticalPoint '' Icc a b ∩ riemannZetaZeros).Finitehp:(criticalPoint ⁻¹' (criticalPoint '' Icc a b ∩ riemannZetaZeros)).Finitet:ℝht:t ∈ {t | t ∈ Icc a b ∧ hardyXi t = 0}⊢ t ∈ criticalPoint ⁻¹' (criticalPoint '' Icc a b ∩ riemannZetaZeros)
  exact ⟨⟨t, ht.1, rfl⟩, (hardyXi_eq_zero_iff t).mp ht.2⟩All goals completed! 🐙

theorem constant_sign_on_Ioi {f : ℝ → ℝ} (hf : Continuous f) (T : ℝ)
    (hne : ∀ t, T < t → f t ≠ 0) :
    (∀ t, T < t → 0 < f t) ∨ (∀ t, T < t → f t < 0) := byf:ℝ → ℝhf:Continuous fT:ℝhne:∀ (t : ℝ), T < t → f t ≠ 0⊢ (∀ (t : ℝ), T < t → 0 < f t) ∨ ∀ (t : ℝ), T < t → f t < 0
  have hbase : T < T + 1 := by linarithf:ℝ → ℝhf:Continuous fT:ℝhne:∀ (t : ℝ), T < t → f t ≠ 0hbase:T < T + 1⊢ (∀ (t : ℝ), T < t → 0 < f t) ∨ ∀ (t : ℝ), T < t → f t < 0
  rcases lt_or_gt_of_ne (hne (T + 1) hbase) with hn | hpinlf:ℝ → ℝhf:Continuous fT:ℝhne:∀ (t : ℝ), T < t → f t ≠ 0hbase:T < T + 1hn:f (T + 1) < 0⊢ (∀ (t : ℝ), T < t → 0 < f t) ∨ ∀ (t : ℝ), T < t → f t < 0inrf:ℝ → ℝhf:Continuous fT:ℝhne:∀ (t : ℝ), T < t → f t ≠ 0hbase:T < T + 1hp:0 < f (T + 1)⊢ (∀ (t : ℝ), T < t → 0 < f t) ∨ ∀ (t : ℝ), T < t → f t < 0
  ·inlf:ℝ → ℝhf:Continuous fT:ℝhne:∀ (t : ℝ), T < t → f t ≠ 0hbase:T < T + 1hn:f (T + 1) < 0⊢ (∀ (t : ℝ), T < t → 0 < f t) ∨ ∀ (t : ℝ), T < t → f t < 0 rightinlf:ℝ → ℝhf:Continuous fT:ℝhne:∀ (t : ℝ), T < t → f t ≠ 0hbase:T < T + 1hn:f (T + 1) < 0⊢ ∀ (t : ℝ), T < t → f t < 0
    intro t htinlf:ℝ → ℝhf:Continuous fT:ℝhne:∀ (t : ℝ), T < t → f t ≠ 0hbase:T < T + 1hn:f (T + 1) < 0t:ℝht:T < t⊢ f t < 0
    by_contra hinlf:ℝ → ℝhf:Continuous fT:ℝhne:∀ (t : ℝ), T < t → f t ≠ 0hbase:T < T + 1hn:f (T + 1) < 0t:ℝht:T < th:¬f t < 0⊢ False
    obtain ⟨u, hu, hz⟩ := isPreconnected_Ioi.intermediate_value₂ hbase ht
      hf.continuousOn continuousOn_const hn.le (le_of_not_gt h)inlf:ℝ → ℝhf:Continuous fT:ℝhne:∀ (t : ℝ), T < t → f t ≠ 0hbase:T < T + 1hn:f (T + 1) < 0t:ℝht:T < th:¬f t < 0u:ℝhu:u ∈ Ioi Thz:f u = 0⊢ False
    exact hne u hu hzAll goals completed! 🐙
  ·inrf:ℝ → ℝhf:Continuous fT:ℝhne:∀ (t : ℝ), T < t → f t ≠ 0hbase:T < T + 1hp:0 < f (T + 1)⊢ (∀ (t : ℝ), T < t → 0 < f t) ∨ ∀ (t : ℝ), T < t → f t < 0 leftinrf:ℝ → ℝhf:Continuous fT:ℝhne:∀ (t : ℝ), T < t → f t ≠ 0hbase:T < T + 1hp:0 < f (T + 1)⊢ ∀ (t : ℝ), T < t → 0 < f t
    intro t htinrf:ℝ → ℝhf:Continuous fT:ℝhne:∀ (t : ℝ), T < t → f t ≠ 0hbase:T < T + 1hp:0 < f (T + 1)t:ℝht:T < t⊢ 0 < f t
    by_contra hinrf:ℝ → ℝhf:Continuous fT:ℝhne:∀ (t : ℝ), T < t → f t ≠ 0hbase:T < T + 1hp:0 < f (T + 1)t:ℝht:T < th:¬0 < f t⊢ False
    obtain ⟨u, hu, hz⟩ := isPreconnected_Ioi.intermediate_value₂ ht hbase
      hf.continuousOn continuousOn_const (le_of_not_gt h) hp.leinrf:ℝ → ℝhf:Continuous fT:ℝhne:∀ (t : ℝ), T < t → f t ≠ 0hbase:T < T + 1hp:0 < f (T + 1)t:ℝht:T < th:¬0 < f tu:ℝhu:u ∈ Ioi Thz:f u = 0⊢ False
    exact hne u hu hzAll goals completed! 🐙

/-- Failure of the exact positive-height target forces xi to have a strict eventual sign. -/

theorem eventual_sign_of_not_zerosAboveEveryHeight (h : ¬ ZerosAboveEveryHeight) :
    ∃ T : ℝ, 0 < T ∧
      ((∀ t, T < t → 0 < hardyXi t) ∨ (∀ t, T < t → hardyXi t < 0)) := byh:¬ZerosAboveEveryHeight⊢ ∃ T, 0 < T ∧ ((∀ (t : ℝ), T < t → 0 < hardyXi t) ∨ ∀ (t : ℝ), T < t → hardyXi t < 0)
  unfold ZerosAboveEveryHeight at hh:¬∀ (T : ℝ), ∃ t, T < t ∧ riemannZeta (criticalPoint t) = 0⊢ ∃ T, 0 < T ∧ ((∀ (t : ℝ), T < t → 0 < hardyXi t) ∨ ∀ (t : ℝ), T < t → hardyXi t < 0)
  push Not at hh:∃ T, ∀ (t : ℝ), T < t → riemannZeta (criticalPoint t) ≠ 0⊢ ∃ T, 0 < T ∧ ((∀ (t : ℝ), T < t → 0 < hardyXi t) ∨ ∀ (t : ℝ), T < t → hardyXi t < 0)
  obtain ⟨T, hT⟩ := hT:ℝhT:∀ (t : ℝ), T < t → riemannZeta (criticalPoint t) ≠ 0⊢ ∃ T, 0 < T ∧ ((∀ (t : ℝ), T < t → 0 < hardyXi t) ∨ ∀ (t : ℝ), T < t → hardyXi t < 0)
  refine ⟨max T 1, lt_of_lt_of_le zero_lt_one (le_max_right _ _), ?_⟩T:ℝhT:∀ (t : ℝ), T < t → riemannZeta (criticalPoint t) ≠ 0⊢ (∀ (t : ℝ), max T 1 < t → 0 < hardyXi t) ∨ ∀ (t : ℝ), max T 1 < t → hardyXi t < 0
  apply constant_sign_on_Ioi continuous_hardyXiT:ℝhT:∀ (t : ℝ), T < t → riemannZeta (criticalPoint t) ≠ 0⊢ ∀ (t : ℝ), max T 1 < t → hardyXi t ≠ 0
  intro t ht hzT:ℝhT:∀ (t : ℝ), T < t → riemannZeta (criticalPoint t) ≠ 0t:ℝht:max T 1 < thz:hardyXi t = 0⊢ False
  exact hT t (lt_of_le_of_lt (le_max_left _ _) ht) ((hardyXi_eq_zero_iff t).mp hz)All goals completed! 🐙

end HardyZeta