Source indexedtheorem · leanprover/lean4:v4.32.0

Ramanujan.low_contrib_le_three_tenths

PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations · PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:223 to 286

Mathematical statement

Exact Lean statement

theorem low_contrib_le_three_tenths :
    (3914 : ℝ) ^ 6 * (100000000000000000720 : ℝ) *
      (exp (-(44 : ℝ)) / (3870 : ℝ) ^ 7
        + 7 * (exp (-(1979 : ℝ)) / (log 2) ^ 8
          + (2 : ℝ) ^ 8 * exp (-(44 : ℝ)) / (3870 : ℝ) ^ 8))
      ≤ (3 : ℝ) / 10

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem low_contrib_le_three_tenths :    (3914 : ℝ) ^ 6 * (100000000000000000720 : ℝ) *      (exp (-(44 : ℝ)) / (3870 : ℝ) ^ 7        + 7 * (exp (-(1979 : ℝ)) / (log 2) ^ 8          + (2 : ℝ) ^ 8 * exp (-(44 : ℝ)) / (3870 : ℝ) ^ 8))      ≤ (3 : ℝ) / 10 := by  have hAcoeff :      (3914 : ℝ) ^ 6 * (100000000000000000720 : ℝ) / (3870 : ℝ) ^ 7 ≤        (30000000000000000 : ℝ) := by    norm_num  have hCcoeff :      (3914 : ℝ) ^ 6 * (100000000000000000720 : ℝ) * (7 * (2 : ℝ) ^ 8) / (3870 : ℝ) ^ 8        ≤ (20000000000000000 : ℝ) := by    norm_num  have hBcoeff0 :      (3914 : ℝ) ^ 6 * (100000000000000000720 : ℝ) * 7 ≤        (30000000000000000000000000000000000000000000 : ℝ) := by    norm_num  have hA :      (3914 : ℝ) ^ 6 * (100000000000000000720 : ℝ) * exp (-(44 : ℝ)) / (3870 : ℝ) ^ 7 ≤        (1 : ℝ) / 20 := by    rw [show (3914 : ℝ) ^ 6 * (100000000000000000720 : ℝ) * exp (-(44 : ℝ)) / (3870 : ℝ) ^ 7        = ((3914 : ℝ) ^ 6 * (100000000000000000720 : ℝ) / (3870 : ℝ) ^ 7) *            exp (-(44 : ℝ)) by ring]    exact le_trans (mul_le_mul hAcoeff exp_neg44_small (by positivity) (by positivity))      (by norm_num)  have hC :      (3914 : ℝ) ^ 6 * (100000000000000000720 : ℝ) *        (7 * (2 : ℝ) ^ 8) * exp (-(44 : ℝ)) / (3870 : ℝ) ^ 8 ≤ (1 : ℝ) / 20 := by    rw [show (3914 : ℝ) ^ 6 * (100000000000000000720 : ℝ) *          (7 * (2 : ℝ) ^ 8) * exp (-(44 : ℝ)) / (3870 : ℝ) ^ 8        = ((3914 : ℝ) ^ 6 * (100000000000000000720 : ℝ) * (7 * (2 : ℝ) ^ 8) /              (3870 : ℝ) ^ 8) * exp (-(44 : ℝ)) by ring]    exact le_trans (mul_le_mul hCcoeff exp_neg44_small (by positivity) (by positivity))      (by norm_num)  have hB :      (3914 : ℝ) ^ 6 * (100000000000000000720 : ℝ) * 7 *        (exp (-(1979 : ℝ)) / (log 2) ^ 8) ≤ (1 : ℝ) / 20 := by    have hBcoeff :        (3914 : ℝ) ^ 6 * (100000000000000000720 : ℝ) * 7 / (log 2) ^ 8          ≤ (30000000000000000000000000000000000000000000 : ℝ) * 1000 := by      rw [show (3914 : ℝ) ^ 6 * (100000000000000000720 : ℝ) * 7 / (log 2) ^ 8          = ((3914 : ℝ) ^ 6 * (100000000000000000720 : ℝ) * 7) * (1 / (log 2) ^ 8) by ring]      exact le_trans (mul_le_mul_of_nonneg_left inv_log2_pow8_le_1000 (by positivity))        (mul_le_mul_of_nonneg_right hBcoeff0 (by positivity))    rw [show (3914 : ℝ) ^ 6 * (100000000000000000720 : ℝ) * 7 *          (exp (-(1979 : ℝ)) / (log 2) ^ 8)        = ((3914 : ℝ) ^ 6 * (100000000000000000720 : ℝ) * 7 / (log 2) ^ 8) *            exp (-(1979 : ℝ)) by ring]    exact le_trans (mul_le_mul hBcoeff exp_neg1979_small (by positivity) (by positivity))      (by norm_num)  have hrewrite_main :      (3914 : ℝ) ^ 6 * (100000000000000000720 : ℝ) *        (exp (-(44 : ℝ)) / (3870 : ℝ) ^ 7          + 7 * (exp (-(1979 : ℝ)) / (log 2) ^ 8            + (2 : ℝ) ^ 8 * exp (-(44 : ℝ)) / (3870 : ℝ) ^ 8))      = (3914 : ℝ) ^ 6 * (100000000000000000720 : ℝ) * exp (-(44 : ℝ)) / (3870 : ℝ) ^ 7        + (3914 : ℝ) ^ 6 * (100000000000000000720 : ℝ) * 7 *            (exp (-(1979 : ℝ)) / (log 2) ^ 8)        + (3914 : ℝ) ^ 6 * (100000000000000000720 : ℝ) *            (7 * (2 : ℝ) ^ 8) * exp (-(44 : ℝ)) / (3870 : ℝ) ^ 8 := by    ring  rw [hrewrite_main]  nlinarith [hA, hB, hC]