Theorem 3.21 — uniqueness of μ and the Stieltjes inversion formula

Proved

TeschlQM.Herglotz.stieltjes_inversion

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

complex-analysisherglotz-functionsmeasure-theoryp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1

Let $\mu$ be a finite Borel measure on $\mathbb{R}$ with Borel transform $F$ . Then $\mu$ is uniquely determined by $F$ : any finite Borel measure $\nu$ whose Borel transform coincides with $F$ on $\mathbb{C}_+$ equals $\mu$ . Moreover, for all $\lambda_1 < \lambda_2$ the Stieltjes inversion formula holds:

\frac12\bigl(\mu((\lambda_1, \lambda_2)) + \mu([\lambda_1, \lambda_2])\bigr) = \lim_{\varepsilon \downarrow 0} \frac1\pi \int_{\lambda_1}^{\lambda_2} \operatorname{Im}\bigl(F(\lambda + i\varepsilon)\bigr)\, d\lambda .

The formula recovers $\mu$ from the boundary behaviour of $\operatorname{Im} F$ ; atoms at the endpoints are counted with weight $\tfrac12$ .

Formalization Note. The book writes the formula for an interval $(\lambda_1, \lambda_2)$ and leaves $\lambda_1 < \lambda_2$ implicit; it is a hypothesis here (at $\lambda_1 = \lambda_2$ the left side is $\tfrac12\mu(\{\lambda_1\})$ while the right side is $0$ ). The integral is the interval integral ∫ t in l₁..l₂, the limit is along 𝓝[>] 0, and the measure values are converted to reals with toReal (finite measure).

Preamble

import Mathlib
import Definitions.Def_TeschlQM_Herglotz_borelTransform

open MeasureTheory Filter
open scoped Topology

Formal statement

namespace TeschlQM.Herglotz

/-- Teschl, p. 108, Theorem 3.21. Let `F` be the Borel transform of a finite Borel measure `μ`.
Then `μ` is unique (any finite Borel measure `ν` whose Borel transform agrees with `F` on `ℂ₊`
equals `μ`) and is recovered by the Stieltjes inversion formula (3.89): for `λ₁ < λ₂`,
`½ (μ((λ₁, λ₂)) + μ([λ₁, λ₂])) = lim_{ε↓0} (1/π) ∫_{λ₁}^{λ₂} Im(F(λ + iε)) dλ`. -/
theorem stieltjes_inversion (μ : Measure ℝ) [IsFiniteMeasure μ] :
    (∀ ν : Measure ℝ, IsFiniteMeasure ν →
      (∀ z : ℂ, 0 < z.im → borelTransform ν z = borelTransform μ z) → ν = μ) ∧
    ∀ l₁ l₂ : ℝ, l₁ < l₂ →
      Tendsto (fun ε : ℝ =>
          (1 / Real.pi) * ∫ t in l₁..l₂, (borelTransform μ ((t : ℂ) + (ε : ℂ) * Complex.I)).im)
        (𝓝[>] (0 : ℝ))
        (𝓝 (((μ (Set.Ioo l₁ l₂)).toReal + (μ (Set.Icc l₁ l₂)).toReal) / 2)) := by sorry

end TeschlQM.Herglotz

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 108, Theorem 3.21

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $\mu$ be a finite Borel measure on $\mathbb{R}$ . For any Borel measure $\rho$ , let

F_\rho(z)=\int_{\mathbb{R}}\frac{d\rho(t)}{t-z},

a Bochner integral that is set to $0$ when the integrand is not integrable. The statement asserts two things.

Uniqueness. For every finite Borel measure $\nu$ on $\mathbb{R}$ : if $F_\nu(z)=F_\mu(z)$ for all $z$ with $\operatorname{Im} z>0$ , then $\nu=\mu$ .
Inversion formula. For all real $l_1<l_2$ ,

\lim_{\varepsilon\downarrow 0}\ \frac{1}{\pi}\int_{l_1}^{l_2} \operatorname{Im} F_\mu(t+i\varepsilon)\,dt \;=\; \frac{\mu\big((l_1,l_2)\big)+\mu\big([l_1,l_2]\big)}{2}.

The limit is taken as $\varepsilon\to 0$ through strictly positive values. The interval integral is a real Lebesgue integral over $(l_1,l_2]$ ; if the integrand is not integrable there, it is set to $0$ . Both measures on the right are finite real numbers.

The hypothesis $l_1<l_2$ excludes empty and reversed intervals. If $\mu=0$ , part 1 says the only finite measure whose transform vanishes on the upper half plane is $0$ . In part 2 both sides are $0$ .

Human review

Endorsed by Shuze Chen · Oct 2, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 2, 2026
Confirmed by the mission captain (proposal self-audit).

View graph