Source indexedlemma · leanprover/lean4:v4.32.0

PT.table_1_bounds

PrimeNumberTheoremAnd.IEANTN.SecondarySummary · PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:90 to 99

Mathematical statement

Exact Lean statement

lemma table_1_bounds (X σ A B C ε₀ : ℝ) (h : (X, σ, A, B, C, ε₀) ∈ Table_1) :
    1000 ≤ X ∧ 3 / 2 ≤ B ∧ B ≤ 2 ∧ 0 ≤ C ∧ C ^ 2 * 5.5666305 ≤ 4 * 5.573412 ∧
    122 ≤ A + 0.1

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma table_1_bounds (X σ A B C ε₀ : ℝ) (h : (X, σ, A, B, C, ε₀) ∈ Table_1) :    1000 ≤ X ∧ 3 / 2 ≤ B ∧ B ≤ 2 ∧ 0 ≤ C ∧ C ^ 2 * 5.5666305 ≤ 4 * 5.573412 ∧    122 ≤ A + 0.1 := by  simp only [Table_1, List.mem_cons, List.mem_nil_iff, or_false, Prod.mk.injEq] at h  rcases h with ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩ |    ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩ |    ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩ |    ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩ |    ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩ <;>  constructor <;> norm_num