`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))

Proved

BookProof.ChapterF3.mehler_arc_integral

by leonardopedro · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterF3.

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))

Formalization note: Lean 4 identifier BookProof.ChapterF3.mehler_arc_integral.

Preamble

-- Generated from ChapterF3.lean — theorem BookProof.ChapterF3.mehler_arc_integral
import Mathlib
import Definitions.Def_ChapterF3
open BookProof.ChapterF3


open scoped BigOperators
open Polynomial


noncomputable section

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]

Formal statement

theorem 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)) := by sorry

View graph