Source indexedtheorem · leanprover/lean4:v4.32.0

Ramanujan.style_eq

PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations · PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:26 to 42

Mathematical statement

Exact Lean statement

theorem style_eq (y : ℝ) (hy : 0 < y) :
    y ^ 5 * ((379.7 : ℝ) * (y / 5.573412) ^ (1.52 : ℝ) *
      exp (-(1.89 : ℝ) * (sqrt y / sqrt (5.573412 : ℝ))))
    =
    styleVal y

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem style_eq (y : ℝ) (hy : 0 < y) :    y ^ 5 * ((379.7 : ℝ) * (y / 5.573412) ^ (1.52 : ℝ) *      exp (-(1.89 : ℝ) * (sqrt y / sqrt (5.573412 : ℝ))))    =    styleVal y := by  have hdiv : y / (1393353 / 250000 : ℝ) = y * (250000 / 1393353 : ℝ) := by field_simp  have hposbase : 0 < y * (250000 / 1393353 : ℝ) := by positivity  unfold styleVal  rw [show y ^ 5 = y * (y * (y * (y * y))) by ring,    show (379.7 : ℝ) = (3797 / 10 : ℝ) by norm_num,    show (5.573412 : ℝ) = (1393353 / 250000 : ℝ) by norm_num, hdiv,    rpow_def_of_pos hposbase, show (1.52 : ℝ) = (38 / 25 : ℝ) by norm_num,    show sqrt y / sqrt (1393353 / 250000 : ℝ) = sqrt (y * (250000 / 1393353 : ℝ)) by      rw [← sqrt_div (le_of_lt hy), hdiv],    show (1.89 : ℝ) = (189 / 100 : ℝ) by norm_num,    show (-(189 / 100 : ℝ)) * sqrt (y * (250000 / 1393353 : ℝ)) =      (-189 / 100 : ℝ) * sqrt (y * (250000 / 1393353 : ℝ)) by ring]