Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.Table4Ext.cell_Epi_le_xpow

PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row11 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row11.lean:48 to 75

Source documentation

Transport: a checked cell dominated by the table value eps, with the per-cell numeric certificate eps ≤ exp(-b'/n), gives the row-n curve x^{-1/n} bound for Eπ on the whole cell [exp b, exp b'].

Exact Lean statement

theorem cell_Epi_le_xpow (n : ℕ) (hn : 0 < n) (c : Cell)
    (htrust : Eπ.bound (c.eps : ℝ) (Real.exp (c.b : ℝ)))
    (hnum : (c.eps : ℝ) ≤ Real.exp (-(c.b' : ℝ) / n)) :
    ∀ x ∈ Set.Icc (Real.exp (c.b : ℝ)) (Real.exp (c.b' : ℝ)),
      Eπ x ≤ x ^ (-(1 : ℝ) / n)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem cell_Epi_le_xpow (n : ℕ) (hn : 0 < n) (c : Cell)    (htrust : Eπ.bound (c.eps : ℝ) (Real.exp (c.b : ℝ)))    (hnum : (c.eps : ℝ) ≤ Real.exp (-(c.b' : ℝ) / n)) :    ∀ x ∈ Set.Icc (Real.exp (c.b : ℝ)) (Real.exp (c.b' : ℝ)),      Eπ x ≤ x ^ (-(1 : ℝ) / n) := by  intro x hx  obtain ⟨hx_lo, hx_hi⟩ := hx  have hxpos : (0 : ℝ) < x := lt_of_lt_of_le (Real.exp_pos _) hx_lo  have hnpos : (0 : ℝ) < (n : ℝ) := by exact_mod_cast hn  -- Eπ x ≤ eps  have h1 : Eπ x ≤ (c.eps : ℝ) := htrust x hx_lo  -- log x ≤ b'  have hlogle : Real.log x ≤ (c.b' : ℝ) := (Real.log_le_iff_le_exp hxpos).mpr hx_hi  -- x^(-1/n) = exp(-(log x)/n)  have hxrpow : x ^ (-(1 : ℝ) / n) = Real.exp (-(Real.log x) / n) := by    rw [Real.rpow_def_of_pos hxpos]    congr 1    ring  -- monotonicity: exp(-b'/n) ≤ exp(-(log x)/n)  have hmono : Real.exp (-(c.b' : ℝ) / n) ≤ Real.exp (-(Real.log x) / n) := by    apply Real.exp_le_exp.mpr    rw [neg_div, neg_div]    apply neg_le_neg    gcongr  rw [hxrpow]  calc Eπ x ≤ (c.eps : ℝ) := h1    _ ≤ Real.exp (-(c.b' : ℝ) / n) := hnum    _ ≤ Real.exp (-(Real.log x) / n) := hmono