The Vinogradov-Korobov zero-free region, the strongest published for the Riemann zeta function

import Mathlib
import Definitions.Def_SEF_theta
import Definitions.Def_SEF_hecke

/-!
# SEF: the Vinogradov-Korobov zero-free region for the zeta function

There is an absolute constant $c > 0$ such that $\zeta(\sigma + it) \ne 0$
whenever $|t| \ge 3$ and
$\sigma \ge 1 - c / ((\log |t|)^{2/3} (\log \log |t|)^{1/3})$. This literature
milestone is the strongest published zero-free region for $\zeta$ (Vinogradov
and Korobov, 1958); the mission goals go strictly beyond it, since the region
approaches the line $\sigma = 1$ only logarithmically. The Lean statement is
drafted for this mission (there is no source file for it); the citation is
given in the item's source field. Proved in the literature; draft: the proof
is a `sorry`.
-/

namespace SEF

theorem zero_free_region_vinogradov_korobov :
    ∃ c : ℝ, 0 < c ∧
      ∀ σ t : ℝ, 3 ≤ |t| →
        1 - c / ((Real.log |t|) ^ (2 / 3 : ℝ) * (Real.log (Real.log |t|)) ^ (1 / 3 : ℝ)) ≤ σ →
          riemannZeta ⟨σ, t⟩ ≠ 0 := by
  sorry

end SEF