Standard real valued constants

This file is for storing the definition of standard real constants that arise in conjectures.

noncomputable def gompertzConstant : ℝ

Gompertz constant $$\delta = -e * \int_1^∞ e^{-t}/t dt \approx 0.59634$$

Equations

• gompertzConstant = -Real.exp 1 * ∫ (t : ℝ) in Set.Ioi 1, Real.exp (-t) / t

noncomputable def catalanConstant : ℝ

Catalan's constant $$G = \sum_{n=0}^∞ (-1)^n / (2n + 1)^2 \approx 0.91596$$

Equations

• catalanConstant = ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) ^ 2