Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.corollary_24_all

PrimeNumberTheoremAnd.IEANTN.FKS2Cor24All · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24All.lean:31 to 48

Source documentation

FKS2 Corollary 24 (complete). Every Table-7 row (B, I) gives the pointwise bound Eπ x ≤ B x for all x with log x ∈ I.

Exact Lean statement

theorem corollary_24_all (B : ℝ → ℝ) (I : Set ℝ) (h : (B, I) ∈ table7) :
    ∀ x, Real.log x ∈ I → Eπ x ≤ B x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem corollary_24_all (B : ℝ → ℝ) (I : Set ℝ) (h : (B, I) ∈ table7) :    ∀ x, Real.log x ∈ I → Eπ x ≤ B x := by  intro x hx  simp only [table7, List.mem_cons, 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⟩ | h  · exact corollary_24_row1 x hx  · exact corollary_24_row2 x hx  · exact corollary_24_row3 x hx  · exact corollary_24_row4 x hx  · exact corollary_24_row5 x hx  · exact corollary_24_row6 x hx  · exact corollary_24_row7 x hx  · exact corollary_24_row8 x hx  · exact corollary_24_row9 x hx  · exact corollary_24_row10 x hx  · exact corollary_24_row11 x hx  · exact absurd h (by simp)