`BookProof.ChapterDisplacedThermalMulti.dtOverlapMulti_eq_integral` (nbar : ℝ≥0) (a b : EuclideanSpace ℝ (Fin n)) : dtOverlapMulti nbar a b = ∫ x : Fin n → ℝ, ∏ i, (gaussianPDFReal

Proved

BookProof.ChapterDisplacedThermalMulti.dtOverlapMulti_eq_integral

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterDisplacedThermalMulti.

BookProof.ChapterDisplacedThermalMulti.dtOverlapMulti_eq_integral (nbar : ℝ≥0) (a b : EuclideanSpace ℝ (Fin n)) : dtOverlapMulti nbar a b = ∫ x : Fin n → ℝ, ∏ i, (gaussianPDFReal (a i) (tauNN nbar) (x i) * gaussianPDFReal (b i) (tauNN nbar) (x i))

Formalization note: Lean 4 identifier BookProof.ChapterDisplacedThermalMulti.dtOverlapMulti_eq_integral.

Preamble

-- Generated from ChapterDisplacedThermalMulti.lean — theorem BookProof.ChapterDisplacedThermalMulti.dtOverlapMulti_eq_integral
import Mathlib
import Definitions.Def_ChapterDisplacedThermalMulti
import Definitions.Def_ChapterDisplacedThermalOverlap
open BookProof.ChapterDisplacedThermalOverlap
open BookProof.ChapterDisplacedThermalMulti


noncomputable section

open MeasureTheory ProbabilityTheory Real
open scoped NNReal


open BookProof.ChapterDisplacedThermalOverlap

variable {n m : ℕ}

Formal statement

theorem BookProof.ChapterDisplacedThermalMulti.dtOverlapMulti_eq_integral (nbar : ℝ≥0) (a b : EuclideanSpace ℝ (Fin n)) :
    dtOverlapMulti nbar a b
      = ∫ x : Fin n → ℝ, ∏ i, (gaussianPDFReal (a i) (tauNN nbar) (x i)
          * gaussianPDFReal (b i) (tauNN nbar) (x i)) := by sorry

View graph