Source indexedlemma · leanprover/lean4:v4.32.0

Eθ.classicalBound.to_numericalBound

PrimeNumberTheoremAnd.Defs · PrimeNumberTheoremAnd/Defs.lean:280 to 291

Mathematical statement

Exact Lean statement

@[blueprint "classical-to-numeric"]
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"]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)