Corollary 3.24 — μ is purely absolutely continuous on I if limsup Im F(λ+iε) < ∞ on I

Proved

TeschlQM.Herglotz.purely_ac_of_limsup_lt_top

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

herglotz-functionsmeasure-theoryp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1spectral-theory

Let $\mu$ be a finite Borel measure on $\mathbb{R}$ with Borel transform $F$ , and let $I \subseteq \mathbb{R}$ be a Borel set. If

\limsup_{\varepsilon\downarrow 0} \operatorname{Im} F(\lambda + i\varepsilon) < \infty \qquad \text{for all } \lambda \in I,

then $\mu$ is purely absolutely continuous on $I$ : the restriction $\mu|_I$ is absolutely continuous with respect to Lebesgue measure.

Formalization Note. The book does not say what $I$ is (an interval in all its applications); any Borel set is allowed here, which includes intervals. The $\limsup$ is taken in ℝ≥0∞ of the nonnegative quantities $\operatorname{Im} F(\lambda + i\varepsilon)$ , $\varepsilon > 0$ .

Preamble

import Mathlib
import Definitions.Def_TeschlQM_Herglotz_borelTransform

open MeasureTheory Filter
open scoped ENNReal Topology

Formal statement

namespace TeschlQM.Herglotz

/-- Teschl, p. 109, Corollary 3.24. Let `μ` be a finite Borel measure and `F` its Borel
transform. If `limsup_{ε↓0} Im(F(λ + iε)) < ∞` for all `λ` in a Borel set `I ⊆ ℝ`, then `μ` is
purely absolutely continuous on `I`: its restriction to `I` is absolutely continuous with
respect to Lebesgue measure. -/
theorem purely_ac_of_limsup_lt_top (μ : Measure ℝ) [IsFiniteMeasure μ] (I : Set ℝ)
    (hI : MeasurableSet I)
    (h : ∀ t ∈ I, limsup (fun ε : ℝ => ENNReal.ofReal
        (borelTransform μ ((t : ℂ) + (ε : ℂ) * Complex.I)).im) (𝓝[>] (0 : ℝ)) < ⊤) :
    μ.restrict I ≪ volume := by sorry

end TeschlQM.Herglotz

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 109, Corollary 3.24

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}$ and $F(z)=\int_{\mathbb{R}}\frac{d\mu(s)}{s-z}$ its Borel transform (Bochner integral, $0$ if not integrable). Let $I\subseteq\mathbb{R}$ be a Borel-measurable set. Assume that for every $t\in I$ ,

\limsup_{\varepsilon\downarrow0}\ \max\!\big(0,\operatorname{Im}F(t+i\varepsilon)\big) < \infty .

The limsup is taken in $[0,\infty]$ over positive $\varepsilon$ , with negative values of $\operatorname{Im}F$ replaced by $0$ and no factor $1/\pi$ .

The conclusion is that the restriction of $\mu$ to $I$ is absolutely continuous with respect to Lebesgue measure $\lambda$ :

\lambda(A)=0 \implies \mu(A\cap I)=0 \quad\text{for every set } A .

If $I=\varnothing$ , the hypothesis is vacuous and so is the conclusion. If $\mu=0$ , the hypothesis holds on every $I$ and the conclusion is trivial.

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