Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.corollary_23_all

PrimeNumberTheoremAnd.IEANTN.FKS2Cor23All · PrimeNumberTheoremAnd/IEANTN/FKS2Cor23All.lean:27 to 50

Source documentation

FKS2 Corollary 23 (complete). Every Table-6 row gives an admissible asymptotic bound for Eπ with R = 5.5666305.

Exact Lean statement

theorem corollary_23_all (Aπ B C x₀ : ℝ) (h : [Aπ, B, C, x₀] ∈ table6) :
    Eπ.classicalBound Aπ B C 5.5666305 (Real.exp x₀)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem corollary_23_all (Aπ B C x₀ : ℝ) (h : [Aπ, B, C, x₀] ∈ table6) :    Eπ.classicalBound Aπ B C 5.5666305 (Real.exp x₀) := by  fin_cases h  · rw [show (1.00:ℝ) = 1 by norm_num]; exact corollary_23_row1  · rw [show (1.00:ℝ) = 1 by norm_num, show (1.000:ℝ) = 1 by norm_num]    exact corollary_23_row2  · rw [show (0.50:ℝ) = 0.5 by norm_num, show (1.50:ℝ) = 1.5 by norm_num,        show (2.000:ℝ) = 2 by norm_num]    exact corollary_23_row3  · rw [show (1.00:ℝ) = 1 by norm_num, show (1.50:ℝ) = 1.5 by norm_num,        show (3.000:ℝ) = 3 by norm_num]    exact corollary_23_row4  · rw [show (1.50:ℝ) = 1.5 by norm_num, show (3.000:ℝ) = 3 by norm_num]    exact corollary_23_row5  · rw [show (1.50:ℝ) = 1.5 by norm_num, show (1.90:ℝ) = 1.9 by norm_num,        show (1.000:ℝ) = 1 by norm_num]    exact corollary_23_row6  · rw [show (1.50:ℝ) = 1.5 by norm_num, show (1.000:ℝ) = 1 by norm_num]    exact corollary_23_row7  · rw [show (1.50:ℝ) = 1.5 by norm_num, show (2.00:ℝ) = 2 by norm_num,        show (1.000:ℝ) = 1 by norm_num]    exact corollary_23_row8  · rw [show (2.00:ℝ) = 2 by norm_num, show (3.000:ℝ) = 3 by norm_num]    exact corollary_23_row9