Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.corollary_8

PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4085 to 4118

Mathematical statement

Exact Lean statement

@[blueprint
  "fks2-corollary-8"
  (title := "FKS2 Corollary 8")
  (statement := /--
  Let $\{b'_i\}_{i=1}^M$ be a set of finite subdivisions of $[\log(x_1),\infty)$, with
  $b'_1 = \log(x_1)$ and $b'_M = \infty$. Define
  $$ \varepsilon_{\pi, num}(x_1) :=
    \max_{1 \leq i \leq M-1}\varepsilon_{\pi, num}(\exp(b'_i),
    \exp(b'_{i+1})).$$
  Then $E_\pi(x) \leq \varepsilon_{\pi,num}(x_1)$ for all $x \geq x_1$.
  -/)
  (proof := /-- This follows directly from Theorem \ref{fks2-theorem-6} by taking the supremum over all partitions ending at infinity. -/)
  (latexEnv := "corollary")
  (discussion := 719)]
theorem corollary_8 {x₁ : ℝ} (hx₁ : x₁ ≥ 14)
    {M : ℕ} (b' : Fin (M + 1) → EReal) (hmono : Monotone b')
    (h_b_start : b' 0 = log x₁)
    (h_b_end : b' (Fin.last M) = ⊤)
    (h_finite : ∀ j : Fin (M+1), b' j = ⊤ → j = Fin.last M)
    (εθ_num : ℝ → ℝ)
    (h_εθ_num : ∀ i : Fin (M+1), Eθ.numericalBound (exp (b' i).toReal) εθ_num) (x : ℝ) (hx : x ≥ x₁) :
    Eπ x ≤ iSup (fun i : Finset.Iio (Fin.last M) ↦
      επ_num (fun j : Fin (i.val.val+1) ↦ (b' ⟨ j.val, by grind ⟩).toReal)
        εθ_num x₁ (exp (b' i.val).toReal)
        (if (i+1) = Fin.last M then ⊤ else exp (b' (i+1)).toReal))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "fks2-corollary-8"  (title := "FKS2 Corollary 8")  (statement := /--  Let $\{b'_i\}_{i=1}^M$ be a set of finite subdivisions of $[\log(x_1),\infty)$, with  $b'_1 = \log(x_1)$ and $b'_M = \infty$. Define  $$ \varepsilon_{\pi, num}(x_1) :=    \max_{1 \leq i \leq M-1}\varepsilon_{\pi, num}(\exp(b'_i),    \exp(b'_{i+1})).$$  Then $E_\pi(x) \leq \varepsilon_{\pi,num}(x_1)$ for all $x \geq x_1$.  -/)  (proof := /-- This follows directly from Theorem \ref{fks2-theorem-6} by taking the supremum over all partitions ending at infinity. -/)  (latexEnv := "corollary")  (discussion := 719)]theorem corollary_8 {x₁ : ℝ} (hx₁ : x₁ ≥ 14)    {M : ℕ} (b' : Fin (M + 1) → EReal) (hmono : Monotone b')    (h_b_start : b' 0 = log x₁)    (h_b_end : b' (Fin.last M) = ⊤)    (h_finite : ∀ j : Fin (M+1), b' j = ⊤ → j = Fin.last M)    (εθ_num : ℝ → ℝ)    (h_εθ_num : ∀ i : Fin (M+1), Eθ.numericalBound (exp (b' i).toReal) εθ_num) (x : ℝ) (hx : x ≥ x₁) :    Eπ x ≤ iSup (fun i : Finset.Iio (Fin.last M) ↦      επ_num (fun j : Fin (i.val.val+1) ↦ (b' ⟨ j.val, by grind ⟩).toReal)        εθ_num x₁ (exp (b' i.val).toReal)        (if (i+1) = Fin.last M then ⊤ else exp (b' (i+1)).toReal)) := by    obtain ⟨i, hi⟩ : ∃ i : Fin M, b' ⟨i.val, by omega⟩ ≤ ↑(log x) ∧ ↑(log x) < b' ⟨i.val + 1, by omega⟩ := by      apply find_ereal_bin b' h_b_end (log x) (by      exact h_b_start.symm ▸ EReal.coe_le_coe_iff.mpr ( Real.log_le_log ( by linarith ) ( by linarith ) ));    convert corollary_8_apply_theorem_6 hx₁ b' hmono h_b_start h_b_end h_finite εθ_num h_εθ_num x hx i hi.1 hi.2 |> le_trans <| ?_ using 1;    refine le_csSup ?_ ?_;    · exact Set.finite_range _ |> Set.Finite.bddAbove;    · simp +zetaDelta only [ge_iff_le, Set.mem_range, Subtype.exists, Fin.Iio_last_eq_map, Finset.mem_map, Finset.mem_univ,    Fin.coe_castSuccEmb, true_and] at *;      refine ⟨ _, ⟨ ⟨ i, by linarith [ Fin.is_lt i ] ⟩, rfl ⟩, ?_ ⟩ ; aesop