`BookProof.ChapterDisplacedThermalOverlap.dtBorn_eq_softmax` {m : ℕ} (nbar : ℝ≥0) (q : ℝ) (k : Fin m → ℝ) (j : Fin m) : dtBorn nbar q k j = BookProof.ChapterSoftmaxSharpness.scoreS

Proved

BookProof.ChapterDisplacedThermalOverlap.dtBorn_eq_softmax

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterDisplacedThermalOverlap.

BookProof.ChapterDisplacedThermalOverlap.dtBorn_eq_softmax {m : ℕ} (nbar : ℝ≥0) (q : ℝ) (k : Fin m → ℝ) (j : Fin m) : dtBorn nbar q k j = BookProof.ChapterSoftmaxSharpness.scoreSoftmax (inverseTemperature nbar) (fun l => -(q - k l) ^ 2) j

Formalization note: Lean 4 identifier BookProof.ChapterDisplacedThermalOverlap.dtBorn_eq_softmax.

Preamble

-- Generated from ChapterDisplacedThermalOverlap.lean — theorem BookProof.ChapterDisplacedThermalOverlap.dtBorn_eq_softmax
import Mathlib
import Definitions.Def_ChapterDisplacedThermalOverlap
import Definitions.Def_ChapterSoftmaxSharpness
open BookProof.ChapterSoftmaxSharpness
open BookProof.ChapterDisplacedThermalOverlap


noncomputable section

open MeasureTheory ProbabilityTheory Real
open scoped NNReal

Formal statement

theorem BookProof.ChapterDisplacedThermalOverlap.dtBorn_eq_softmax {m : ℕ} (nbar : ℝ≥0) (q : ℝ) (k : Fin m → ℝ) (j : Fin m) :
    dtBorn nbar q k j
      = BookProof.ChapterSoftmaxSharpness.scoreSoftmax (inverseTemperature nbar)
          (fun l => -(q - k l) ^ 2) j := by sorry

View graph