structure FKS.Inputs : Type

• b₁ : ℝ
• b₂ : ℝ
• b₃ : ℝ
• hRvM : riemannZeta.Riemann_vonMangoldt_bound self.b₁ self.b₂ self.b₃
• ZDB : zero_density_bound
• H₀ : ℝ
• hH₀ : riemannZeta.RH_up_to self.H₀
• R : ℝ
• hR : riemannZeta.classicalZeroFree self.R
• S₀ : ℝ
• T₀ : ℝ
• hS₀T₀ : (riemannZeta.zeroes_sum Set.univ (Set.Ioo 0 self.T₀) fun (ρ : ℂ) => 1 / ρ.im) < self.S₀

def FKS.table_1 : List (ℝ × ℝ)

theorem FKS.table_1_prop {T₀ S₀ : ℝ} (h : (T₀, S₀) ∈ table_1) : (riemannZeta.zeroes_sum Set.univ (Set.Ioo 0 T₀) fun (ρ : ℂ) => 1 / ρ.im) < S₀

def FKS.table_8 : List (ℝ × ℝ × ℝ × ℝ × ℝ × ℝ × ℝ × ℝ × ℝ)

theorem FKS.theorem_2_7 (I : Inputs) {k δ α d η₀ η μ σ H T : ℝ} (hk : k ∈ Set.Icc (10 ^ 9 / I.H₀) 1) (hα : α > 0) (hδ : δ ≥ 1) (hη₀ : η₀ = 0.23622) (hμ : μ ∈ Set.Icc (1 + η₀) (1 + η)) (hη : η ∈ Set.Ioo η₀ 0.5) (hσ : σ > 0.5 + d / Real.log I.H₀) (hH : H ∈ Set.Ico 1002 I.H₀) (hT : T ≥ I.H₀) : riemannZeta.N' σ T ≤ (T - H) * Real.log T / (2 * Real.pi * d) * Real.log (1 + KLN.CC₁ I.H₀ α d δ k H σ * Real.log (k * T) ^ (2 * σ) * Real.log T ^ (4 * (1 - σ)) * T ^ (8 / 3 * (1 - σ)) / (T - H)) + KLN.CC₂ I.H₀ d η k H μ σ * Real.log T ^ 2 / (2 * Real.pi * d) ∧ riemannZeta.N' σ T ≤ KLN.CC₁ I.H₀ α d δ k H σ * Real.log (k * T) ^ (2 * σ) * Real.log T ^ (5 - 4 * σ) * T ^ (8 / 3 * (1 - σ)) / (2 * Real.pi * d) + KLN.CC₂ I.H₀ d η k H μ σ * Real.log T ^ 2 / (2 * Real.pi * d)

noncomputable def FKS.corollary_2_9 {σ₁ σ₂ α δ d CC_1 c₁ CC_2 c₂ : ℝ} (h : (σ₁, σ₂, α, δ, d, CC_1, c₁, CC_2, c₂) ∈ table_8) : zero_density_bound

noncomputable def FKS.corollary_2_9_merged : zero_density_bound

Need to merge all the individual estimates above into one single estimate

noncomputable def FKS.Inputs.default : Inputs

noncomputable def FKS.Inputs.RvM (I : Inputs) (U : ℝ) : ℝ

noncomputable def FKS.Inputs.B₁ (I : Inputs) (U V : ℝ) : ℝ

theorem FKS.lemma_2_1 (I : Inputs) {U V : ℝ} (hU : U ≥ 1) (hV : V ≥ U) : (riemannZeta.zeroes_sum Set.univ (Set.Ico U V) fun (ρ : ℂ) => 1 / ρ.im) ≤ I.B₁ U V

theorem FKS.corollary_2_3 (I : Inputs) {V : ℝ} (hV : V > I.T₀) : (riemannZeta.zeroes_sum Set.univ (Set.Ioo 0 V) fun (ρ : ℂ) => 1 / ρ.im) < I.S₀ + I.B₁ I.T₀ V

noncomputable def FKS.s₀ (σ U V : ℝ) : ℝ

noncomputable def Real.Gamma.incomplete (s x : ℝ) : ℝ

noncomputable def Complex.Gamma.incomplete (s : ℂ) (x : ℝ) : ℂ

noncomputable def FKS.Inputs.B₀ (I : Inputs) (σ U V : ℝ) : ℝ

theorem FKS.lemma_2_5 (I : Inputs) {σ U V : ℝ} (hT₀ : I.ZDB.T₀ ≥ 2) (hσ : σ ≥ 5 / 8) (hσ' : σ ∈ I.ZDB.σ_range) (hU : U ≥ I.ZDB.T₀) (hV : V > U) : s₀ σ U V ≤ I.B₀ σ U V

theorem FKS.remark_2_6_a (x : ℝ) (hx : 0 ≤ x) : Real.Gamma.incomplete 3 x = (x ^ 2 + 2 * (x + 1)) * Real.exp (-x)

theorem FKS.remark_2_6_b (s : ℝ) (h : s > 1) : Filter.Tendsto (fun (x : ℝ) => Real.Gamma.incomplete s x / (x ^ (s - 1) * Real.exp (-x))) Filter.atTop (nhds 1)

theorem FKS.theorem_3_1 {x T : ℝ} (hx : x > Real.exp 50) (hodd : ∃ (X : ℝ), Odd X ∧ x = X / 2) (hT : T ∈ Set.Ioo 50 x) : Eψ x ≤ (riemannZeta.zeroes_sum (Set.Ioo 0 1) (Set.Ioo (-T) T) fun (ρ : ℂ) => ‖↑x ^ (ρ - 1) / ρ‖) + 2 * Real.log x ^ 2 / T

theorem FKS.theorem_3_2 (α ω : ℝ) (hα : α ∈ Set.Ioc 0 (1 / 2)) (hω : ω ∈ Set.Icc 0 1) : ∃ (M : ℝ) (xM : ℝ), ∀ (x T : ℝ), T ∈ Set.Ioo (max 51 (Real.log x)) ((x ^ α - 2) / 5) → ∃ Tstar ∈ Set.Icc T (2.45 * T), ∀ x ≥ xM, ‖↑(Chebyshev.psi x) - (↑x - riemannZeta.zeroes_sum (Set.Ioo 0 1) (Set.Ioo (-Tstar) Tstar) fun (ρ : ℂ) => ↑x ^ ρ / ρ)‖ ≤ M * x / T * Real.log x ^ (1 - ω)

noncomputable def FKS.ε₁ (x T : ℝ) : ℝ

theorem FKS.proposition_3_4 {x T : ℝ} (hx : x > Real.exp 50) (hT : T ∈ Set.Ioo (3 * Real.log x) (√x / 3)) : Eψ x ≤ (riemannZeta.zeroes_sum (Set.Ioo 0 1) (Set.Ioo (-T) T) fun (ρ : ℂ) => ‖↑x ^ (ρ - 1) / ρ‖) + ε₁ x T

noncomputable def FKS.riemannZeta.Sigma (T x a b : ℝ) : ℝ

noncomputable def FKS.ε₂ (I : Inputs) (x σ₁ T : ℝ) : ℝ

theorem FKS.proposition_3_6 (I : Inputs) {σ₁ T x : ℝ} (hσ_1 : σ₁ ∈ Set.Icc 0.5 1) (hT : T > I.T₀) (x✝ : ℝ) : riemannZeta.Sigma T x✝ 0 σ₁ ≤ ε₂ I x✝ σ₁ T

noncomputable def FKS.Hσ (H₀ R σ : ℝ) : ℝ

theorem FKS.riemannZeta.Hσ_zeroes (H₀ R σ : ℝ) (hH₀ : riemannZeta.RH_up_to H₀) (hR : riemannZeta.classicalZeroFree R) : riemannZeta.N' σ (Hσ H₀ R σ) = 0

noncomputable def FKS.σn (σ₁ σ₂ : ℝ) (n N : ℕ) : ℝ

noncomputable def FKS.Hn (H₀ R σ₁ σ₂ : ℝ) (n N : ℕ) : ℝ

theorem FKS.remark_3_7 {H₀ R σ : ℝ} (hσ : σ < 1 - 1 / (R * Real.log H₀)) : Hσ H₀ R σ = H₀

noncomputable def FKS.ε₃ (I : Inputs) (x σ₁ σ₂ : ℝ) (N : ℕ) (T : ℝ) : ℝ

theorem FKS.proposition_3_8 (I : Inputs) (x : ℝ) {σ₁ σ₂ : ℝ} (N : ℕ) (T : ℝ) (hσ₁ : σ₁ ∈ Set.Icc (5 / 8) 1) (hσ₂ : σ₂ ∈ Set.Ioc σ₁ 1) (hσ : Set.Icc σ₁ σ₂ ⊆ I.ZDB.σ_range) (hT : T ≥ I.H₀) : riemannZeta.Sigma T x σ₁ σ₂ ≤ ε₃ I x σ₁ σ₂ N T

theorem FKS.corollary_3_10 {σ₁ σ₂ T x : ℝ} (hσ₁ : σ₁ ∈ Set.Icc 0.9 1) (hσ₂ : σ₂ ∈ Set.Ioc σ₁ 1) : riemannZeta.Sigma T x σ₁ σ₂ ≤ 125994e-8 * x ^ (σ₂ - 1)

theorem FKS.proposition_3_11 (I : Inputs) {σ₂ T x : ℝ} (K : ℕ) (hσ₂ : σ₂ ∈ Set.Ioc (5 / 8) 1) (t_seq : Fin (K + 2) → ℝ) (ht0 : t_seq 0 = max (Hσ I.H₀ I.R σ₂) (Real.exp (√(Real.log x) / I.R))) (htK : t_seq (Fin.last (K + 1)) = T) (ht_incr : StrictMono t_seq) : riemannZeta.Sigma T x σ₂ 1 ≤ 2 * riemannZeta.N' σ₂ T * x ^ (-1 / (I.R * Real.log (t_seq 0))) / t_seq 0 ∧ riemannZeta.Sigma T x σ₂ 1 ≤ 2 * ∑ k ∈ Finset.Ioo 0 (Fin.last (K + 1)), riemannZeta.N' σ₂ (t_seq k) * (x ^ (-1 / (I.R * Real.log (t_seq (k - 1)))) / t_seq (k - 1) - x ^ (-1 / (I.R * Real.log (t_seq k))) / t_seq k) + x ^ (-1 / (I.R * Real.log (t_seq (Fin.last K).castSucc))) / t_seq (Fin.last K).castSucc * riemannZeta.N' σ₂ T

noncomputable def FKS.ε₄ (I : Inputs) (t₀ x σ₂ : ℝ) (K : ℕ) (T : ℝ) : ℝ

theorem FKS.corollary_3_12 (I : Inputs) {σ₂ t₀ T x : ℝ} (K : ℕ) (hσ₂ : σ₂ ∈ Set.Ioc (5 / 8) 1) (ht₀ : t₀ = max (Hσ I.H₀ I.R σ₂) (Real.exp (√(Real.log x) / I.R))) (hT : T > t₀) (ZDB : zero_density_bound) : riemannZeta.Sigma T x σ₂ 1 ≤ ε₄ I t₀ x σ₂ K T

theorem FKS.proposition_3_14 (I : Inputs) {c : ℝ} (K : ℕ) (hc : c > 1) (hK : K ≥ 2) : have t₀ := fun (x : ℝ) => Real.exp (√(Real.log x) / I.R); have T := fun (x : ℝ) => t₀ x ^ c; have σ₂ := fun (x : ℝ) => 1 - 2 / (I.R * Real.log (t₀ x)); have w₁ := 1 + (c - 1) / ↑K; have C := 2 * I.ZDB.c₁ (σ₂ 1) * Real.exp (16 * w₁ / (3 * I.R)) * w₁ ^ 3; have f := fun (x : ℝ) => C * Real.log (t₀ x) ^ (3 + 4 / (I.R * Real.log (t₀ x))) / t₀ x ^ 2; Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => ε₄ I (t₀ x) x (σ₂ x) K (T x)) f ∧ AntitoneOn (fun (x : ℝ) => ε₄ I (t₀ x) x (σ₂ x) K (T x)) (Set.Ioi (Real.exp (I.R * Real.exp 2))) ∧ AntitoneOn (fun (x : ℝ) => ε₄ I (t₀ x) x (σ₂ x) K (T x) * t₀ x ^ 2 / Real.log (t₀ x) ^ 3) (Set.Ioi (Real.exp (I.R * Real.exp 2)))

noncomputable def FKS.ε (I : Inputs) (x₀ σ₂ c : ℝ) (N K : ℕ) : ℝ

theorem FKS.theorem_1_1 (I : Inputs) (x₀ σ₂ c : ℝ) (N K : ℕ) (hlog : Real.log x₀ > 1000) (hσ₂ : σ₂ ∈ Set.Ioo 0.9 1) (hc : c ∈ Set.Icc 2 30) (hN : N ≥ 1) (hK : K ≥ 1) (x : ℝ) : x ≥ x₀ → Eψ x ≤ ε I x₀ σ₂ c N K

def FKS.table_5 : List (ℝ × ℝ × ℝ × ℝ × ℝ × ℝ × ℝ)

theorem FKS.theorem_1_1b {log_x0 σ2 c N K ε1 ε2 ε3 ε4 ε_total : ℝ} (h : (log_x0, σ2, ε1, ε2, ε3, ε4, ε_total) ∈ table_5) (x : ℝ) : Real.log x ≥ log_x0 → Eψ x ≤ ε_total

theorem FKS.lemma_5_3 {x : ℝ} (h : Real.log x ∈ Set.Ioc 0 2100) : Eψ x ≤ 2 * Real.log x ^ (3 / 2) * Real.exp (-0.8476836 * √(Real.log x))

theorem FKS.lemma_5_4 {x : ℝ} (h : Real.log x ∈ Set.Ioc 2100 200000) : Eψ x ≤ 9.22022 * Real.log x ^ (3 / 2) * Real.exp (-0.8476836 * √(Real.log x))

noncomputable def FKS.A (x₀ : ℝ) : ℝ

theorem FKS.theorem_1_2b (x₀ : ℝ) (h : Real.log x₀ ≥ 1000) : Eψ.classicalBound (A x₀) (3 / 2) 2 5.5666305 x₀

theorem FKS.FKS_corollary_1_3 : Eψ.classicalBound 121.096 (3 / 2) 2 5.5666305 2

theorem FKS.FKS_corollary_1_4 : Eψ.classicalBound 9.22022 (3 / 2) 0.8476836 1 2