Source indexedtheorem · leanprover/lean4:v4.32.0

Ramanujan.low_contrib_raw_le_three_tenths

PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations · PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:292 to 321

Mathematical statement

Exact Lean statement

theorem low_contrib_raw_le_three_tenths :
    (3914 : ℝ) ^ 6 / exp (3914 : ℝ) *
      ((100000000000000000720 : ℝ) *
        (exp (3870 : ℝ) / (3870 : ℝ) ^ 7
          + 7 *
            (sqrt (exp (3870 : ℝ)) / (log 2) ^ 8
              + (2 : ℝ) ^ 8 * exp (3870 : ℝ) / (3870 : ℝ) ^ 8)))
      ≤ (3 : ℝ) / 10

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem low_contrib_raw_le_three_tenths :    (3914 : ℝ) ^ 6 / exp (3914 : ℝ) *      ((100000000000000000720 : ℝ) *        (exp (3870 : ℝ) / (3870 : ℝ) ^ 7          + 7 *            (sqrt (exp (3870 : ℝ)) / (log 2) ^ 8              + (2 : ℝ) ^ 8 * exp (3870 : ℝ) / (3870 : ℝ) ^ 8)))      ≤ (3 : ℝ) / 10 := by  have h44 : exp (3870 : ℝ) / exp (3914 : ℝ) = exp (-(44 : ℝ)) := by    have h := (exp_sub (3870 : ℝ) (3914 : ℝ)).symm    simpa [show (3870 : ℝ) - 3914 = (-(44 : ℝ)) by norm_num] using h  have h1979 : exp (1935 : ℝ) / exp (3914 : ℝ) = exp (-(1979 : ℝ)) := by    have h := (exp_sub (1935 : ℝ) (3914 : ℝ)).symm    simpa [show (1935 : ℝ) - 3914 = (-(1979 : ℝ)) by norm_num] using h  rw [sqrt_exp_3870]  have hrewrite :      (3914 : ℝ) ^ 6 / exp (3914 : ℝ) *          ((100000000000000000720 : ℝ) *            (exp (3870 : ℝ) / (3870 : ℝ) ^ 7              + 7 *                (exp (1935 : ℝ) / (log 2) ^ 8                  + (2 : ℝ) ^ 8 * exp (3870 : ℝ) / (3870 : ℝ) ^ 8)))        = (3914 : ℝ) ^ 6 * (100000000000000000720 : ℝ) *            (exp (-(44 : ℝ)) / (3870 : ℝ) ^ 7              + 7 * (exp (-(1979 : ℝ)) / (log 2) ^ 8                + (2 : ℝ) ^ 8 * exp (-(44 : ℝ)) / (3870 : ℝ) ^ 8)) := by    rw [← h44, ← h1979]    field_simp  rw [hrewrite]  exact low_contrib_le_three_tenths