Source indexedlemma · leanprover/lean4:v4.32.0

Eψ.classicalBound.to_numericalBound

PrimeNumberTheoremAnd.Defs · PrimeNumberTheoremAnd/Defs.lean:258 to 278

Mathematical statement

Exact Lean statement

@[blueprint
  "classical-to-numeric"
  (title := "Classic bound implies numerical bound")
  (statement := /--
  A classical bound for $x \geq x_0$ implies a numerical
  bound for $x \geq \max(x_0,
  \exp( R (2B/C)^2  ))$. -/)
  (proof := /-- Immediate from previous lemma -/)
  (latexEnv := "lemma")
  (discussion := 901)]
lemma Eψ.classicalBound.to_numericalBound
    (A B C R x₀ x₁ : ℝ) (hA : 0 < A) (hB : 0 < B)
    (hC : 0 < C) (hR : 0 < R)
    (hEψ : Eψ.classicalBound A B C R x₀)
    (hx₁ : x₁ ≥ max x₀ (Real.exp (R * (2 * B / C) ^ 2))) :
    Eψ.numericalBound x₁ (fun x ↦ admissible_bound A B C R x)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "classical-to-numeric"  (title := "Classic bound implies numerical bound")  (statement := /--  A classical bound for $x \geq x_0$ implies a numerical  bound for $x \geq \max(x_0,  \exp( R (2B/C)^2  ))$. -/)  (proof := /-- Immediate from previous lemma -/)  (latexEnv := "lemma")  (discussion := 901)]lemma Eψ.classicalBound.to_numericalBound    (A B C R x₀ x₁ : ℝ) (hA : 0 < A) (hB : 0 < B)    (hC : 0 < C) (hR : 0 < R)    (hEψ : Eψ.classicalBound A B C R x₀)    (hx₁ : x₁ ≥ max x₀ (Real.exp (R * (2 * B / C) ^ 2))) :    Eψ.numericalBound x₁ (fun x ↦ admissible_bound A B C R x) :=  fun x hx ↦    le_trans (hEψ x (le_trans (le_max_left ..) (le_trans hx₁ hx)))      (admissible_bound.mono A B C R hA hB hC hR        (Set.mem_Ici.mpr (le_trans (le_max_right ..) hx₁))        (Set.mem_Ici.mpr (le_trans (le_max_right ..) (le_trans hx₁ hx))) hx)