Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.Floor.etheta_le_floor

PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor · PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:17 to 39

Source documentation

Eθ ≤ 4/5 on [2, e^10], via the θ engine + ⌊x⌋ stitching. checkAllThetaRelErrorReal start limit checks real unit intervals for N < limit; since exp 10 < 22027, the relevant floors satisfy N < 22027 and use the [N, N+1) real certificate branch.

Exact Lean statement

theorem etheta_le_floor :
    ∀ x ∈ Set.Icc (2:ℝ) (Real.exp 10), Eθ x ≤ (4/5 : ℝ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem etheta_le_floor :    ∀ x ∈ Set.Icc (2:ℝ) (Real.exp 10), Eθ x ≤ (4/5 : ℝ) := by  have hcheck : checkAllThetaRelErrorReal 2 22027 (4/5) 20 = true := by native_decide  intro x hx  obtain ⟨hx2, hxe⟩ := hx  have hxpos : (0:ℝ) ≤ x := by linarith  set N := ⌊x⌋₊ with hN  have hNlo : (N:ℝ) ≤ x := Nat.floor_le hxpos  have hNhi : x < (N:ℝ) + 1 := Nat.lt_floor_add_one x  have hN2 : 2 ≤ N := Nat.le_floor (by exact_mod_cast hx2)  have hxlt : x < 22027 := lt_of_le_of_lt hxe exp10_lt  have hNlim : N < 22027 := (Nat.floor_lt hxpos).mpr (by exact_mod_cast hxlt)  have hNpos : 0 < N := by omega  have himpl := checkAllThetaRelErrorReal_implies 2 22027 (4/5) 20 hcheck N hNpos hN2    (by omega : N ≤ 22027)  rw [if_pos hNlim] at himpl  have h := abs_theta_sub_le_mul_of_checkThetaRelErrorReal    N 20 (4/5) (by norm_num) (by norm_num) himpl x hNlo hNhi  have hcast : ((4/5 : ℚ) : ℝ) = (4/5 : ℝ) := by norm_num  rw [hcast] at h  unfold Eθ  rw [div_le_iff₀ (by linarith : (0:ℝ) < x)]  exact h