Source indexedlemma · leanprover/lean4:v4.32.0

BKLNW.G1''_nonneg

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean:472 to 483

Mathematical statement

Exact Lean statement

lemma G1''_nonneg {A₁ A₂ E : ℝ} (hA1 : 0 ≤ A₁) (hA2 : 0 ≤ A₂) {y : ℝ} (hy20 : 20 ≤ y) :
    0 ≤ G1'' A₁ A₂ E y

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma G1''_nonneg {A₁ A₂ E : ℝ} (hA1 : 0 ≤ A₁) (hA2 : 0 ≤ A₂) {y : ℝ} (hy20 : 20 ≤ y) :    0 ≤ G1'' A₁ A₂ E y := by  unfold G1'' eTdd  have t1 : (0 : ℝ) ≤ A₁ * (((1 / 2 : ℝ) ^ 2 * y - 2 * (1 / 2)) * Real.exp (-((1 / 2 : ℝ) * y))) := by    apply mul_nonneg hA1    apply mul_nonneg _ (Real.exp_pos _).le    nlinarith [hy20]  have t2 : (0 : ℝ) ≤ A₂ * (((2 / 3 : ℝ) ^ 2 * y - 2 * (2 / 3)) * Real.exp (-((2 / 3 : ℝ) * y))) := by    apply mul_nonneg hA2    apply mul_nonneg _ (Real.exp_pos _).le    nlinarith [hy20]  linarith [t1, t2]