`BookProof.ChapterF3.mehler_arc_integral` (w : ℝ) (hw : 0 < w) : (∫ _x in (0 : ℝ)..w, Real.sqrt (1 / w) * Real.sqrt (1 / (2 * Real.pi))) = Real.sqrt (w / (2 * Real.pi))

Initializing...

`BookProof.ChapterF3.mehler_arc_integral` (w : ℝ) (hw : 0 < w) : (∫ _x in (0 : ℝ)..w, Real.sqrt (1 / w) * Real.sqrt (1 / (2 * Real.pi))) = Real.sqrt (w / (2 * Real.pi)) · Prove2Me