Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.FloorButhe.eval_lhsE

PrimeNumberTheoremAnd.IEANTN.FKS2Cor23 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor23.lean:333 to 345

Mathematical statement

Exact Lean statement

theorem eval_lhsE (s : ℝ) :
    Expr.eval (fun _ => s) lhsE
      = (195/100 + (39/10) * (s*s)⁻¹ + (195/10) * ((s*s)*(s*s))⁻¹) * Real.exp (-(s*s)/2)
        + (10452/10000) * (s*s) * Real.exp (-(s*s))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem eval_lhsE (s : ℝ) :    Expr.eval (fun _ => s) lhsE      = (195/100 + (39/10) * (s*s)⁻¹ + (195/10) * ((s*s)*(s*s))⁻¹) * Real.exp (-(s*s)/2)        + (10452/10000) * (s*s) * Real.exp (-(s*s)) := by  have h8 : Real.exp (s^2 * (-1/16 : ℝ)) ^ 8 = Real.exp (s^2 * (-1/2 : ℝ)) := by    rw [← Real.exp_nat_mul]; congr 1; push_cast; ring  have h16 : Real.exp (s^2 * (-1/16 : ℝ)) ^ 16 = Real.exp (-s^2) := by    rw [← Real.exp_nat_mul]; congr 1; push_cast; ring  simp only [lhsE, pow8, sqx, s2, s4, e2, Expr.eval_add, Expr.eval_mul, Expr.eval_const,    Expr.eval_inv, Expr.eval_exp, Expr.eval_var]  push_cast  ring_nf  rw [h8, h16]