noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19PrintedHeightReal (x level : ℕ) : ℝ

The printed equation-(19) height uses the exponential I, not the legacy maximum W.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19PrintedHeightReal x level = 2 ^ level * Real.log ↑x ^ 200 * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Equation20Ilx x level

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19PrintedHeight (x level : ℕ) : ℕ

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19PrintedHeight x level = ⌈AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19PrintedHeightReal x level⌉₊

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_actual_W_sq_le_Ilx_eventually : ∃ (X₀ : ℝ), ∀ (x : ℕ), X₀ ≤ ↑x → ∀ (L level : ℕ), ↑L ≤ Real.log ↑x ^ 100 → chen1973Lemma6Eq19I x L level ^ 2 ≤ chen1973Lemma6Equation20Ilx x level

Bind directly to the already public exponential I used by equation (20).

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_printedHeight_weight_payment : ∃ (X₀ : ℝ), ∀ (x : ℕ), X₀ ≤ ↑x → ∀ (L level : ℕ), ↑L ≤ Real.log ↑x ^ 100 → ↑(L * 2 ^ level) * Real.log ↑x ^ 100 * chen1973Lemma6Eq19I x L level ^ 2 ≤ ↑(chen1973Lemma6Eq19PrintedHeight x level) ∧ chen1973Lemma6Eq19Height x L level ≤ chen1973Lemma6Eq19PrintedHeight x level

The original height pays the square of the actual arithmetic weight uniformly. The statement is about the exact natural ceiling, not an assumed real cutoff.