Theorem 3.23 — (1/π) Im F(λ+iε) → (Dμ)(λ) a.e.; supports of μ_sc and minimal support of μ_ac

Proved

TeschlQM.Herglotz.boundary_im_eq_deriv

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

differentiation-of-measuresherglotz-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$ . Then the limit

\operatorname{Im}(F(\lambda)) = \lim_{\varepsilon\downarrow 0} \frac1\pi \operatorname{Im}\bigl(F(\lambda + i\varepsilon)\bigr) \in [0, \infty]

exists (finite or infinite) for $\mu$ -almost every and for Lebesgue-almost every $\lambda$ , and it equals the derivative $(D\mu)(\lambda)$ at every $\lambda$ where $(D\mu)(\lambda)$ exists. Moreover, the set $\{\lambda \mid \operatorname{Im}(F(\lambda)) = \infty\}$ is a support for the singularly continuous part $\mu_{sc}$ , and $\{\lambda \mid 0 < \operatorname{Im}(F(\lambda)) < \infty\}$ is a minimal support for the absolutely continuous part $\mu_{ac}$ .

These are the boundary-value characterizations of the spectral types used later for Schrödinger operators.

Formalization Note. The book's (3.91) defines $\operatorname{Im}(F(\lambda))$ with the factor $\frac1\pi$ and (3.92) then writes $(D\mu)(\lambda) = \frac1\pi\operatorname{Im}(F(\lambda))$ , which would apply the factor twice; consistent with Theorem 3.22 the identity is stated as $(D\mu)(\lambda) = \lim_{\varepsilon\downarrow0}\frac1\pi\operatorname{Im}F(\lambda+i\varepsilon)$ . Limits are taken in ℝ≥0∞ along 𝓝[>] 0; the two support sets are defined through these limits (the set where the limit exists and is $\infty$ , resp. exists and lies in $(0,\infty)$ ), so no value is assigned where the limit fails to exist.

Preamble

import Mathlib
import Definitions.Def_TeschlQM_Herglotz_borelTransform
import Definitions.Def_TeschlQM_Herglotz_HasMeasureDeriv
import Definitions.Def_TeschlQM_Herglotz_IsSupport
import Definitions.Def_TeschlQM_Herglotz_IsMinimalSupport
import Definitions.Def_TeschlQM_Herglotz_acPart
import Definitions.Def_TeschlQM_Herglotz_scPart

open MeasureTheory Filter
open scoped ENNReal Topology

Formal statement

namespace TeschlQM.Herglotz

/-- Teschl, p. 109, Theorem 3.23. Let `μ` be a finite Borel measure and `F` its Borel transform.
The limit (3.91) `Im(F(λ)) = lim_{ε↓0} (1/π) Im(F(λ + iε))` exists in `[0, ∞]` (finite or
infinite) for `μ`-a.e. and for Lebesgue-a.e. `λ`; it equals `(Dμ)(λ)` whenever `(Dμ)(λ)` exists
((3.92), read with the factor `1/π` taken once, consistent with Theorem 3.22); the set where it
is `∞` is a support for the singularly continuous part `μ_sc`, and the set where it lies in
`(0, ∞)` is a minimal support for the absolutely continuous part `μ_ac`. -/
theorem boundary_im_eq_deriv (μ : Measure ℝ) [IsFiniteMeasure μ] :
    (∀ᵐ (t : ℝ) ∂μ, ∃ L : ℝ≥0∞, Tendsto (fun ε : ℝ => ENNReal.ofReal
        ((borelTransform μ ((t : ℂ) + (ε : ℂ) * Complex.I)).im / Real.pi)) (𝓝[>] (0 : ℝ)) (𝓝 L)) ∧
    (∀ᵐ (t : ℝ) ∂(volume : Measure ℝ), ∃ L : ℝ≥0∞, Tendsto (fun ε : ℝ => ENNReal.ofReal
        ((borelTransform μ ((t : ℂ) + (ε : ℂ) * Complex.I)).im / Real.pi)) (𝓝[>] (0 : ℝ)) (𝓝 L)) ∧
    (∀ (t : ℝ) (d : ℝ≥0∞), HasMeasureDeriv μ t d →
      Tendsto (fun ε : ℝ => ENNReal.ofReal
        ((borelTransform μ ((t : ℂ) + (ε : ℂ) * Complex.I)).im / Real.pi)) (𝓝[>] (0 : ℝ)) (𝓝 d)) ∧
    IsSupport (scPart μ) {t : ℝ | Tendsto (fun ε : ℝ => ENNReal.ofReal
        ((borelTransform μ ((t : ℂ) + (ε : ℂ) * Complex.I)).im / Real.pi)) (𝓝[>] (0 : ℝ)) (𝓝 ⊤)} ∧
    IsMinimalSupport (acPart μ) {t : ℝ | ∃ L : ℝ≥0∞, 0 < L ∧ L < ⊤ ∧
      Tendsto (fun ε : ℝ => ENNReal.ofReal
        ((borelTransform μ ((t : ℂ) + (ε : ℂ) * Complex.I)).im / Real.pi)) (𝓝[>] (0 : ℝ)) (𝓝 L)} := by sorry

end TeschlQM.Herglotz

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 109, Theorem 3.23

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). For $t\in\mathbb{R}$ and $\varepsilon>0$ , let

g_t(\varepsilon)=\max\!\Big(0,\tfrac{1}{\pi}\operatorname{Im}F(t+i\varepsilon)\Big)\in[0,\infty),

where negative values are replaced by $0$ . All limits below are taken as $\varepsilon\to0$ through positive values, in the topology of $[0,\infty]$ . The statement asserts five things:

For $\mu$ -almost every $t$ , $g_t(\varepsilon)$ converges to some $L\in[0,\infty]$ . The limit $L=\infty$ is allowed.
The same holds for Lebesgue-almost every $t$ .
For every $t\in\mathbb{R}$ and $d\in[0,\infty]$ : if $\mu((t-\varepsilon,t+\varepsilon))/(2\varepsilon)\to d$ , then $g_t(\varepsilon)\to d$ .
Let $S_\infty=\{t : g_t(\varepsilon)\to\infty\}$ . Then $\mu_{sc}(\mathbb{R}\setminus S_\infty)=0$ . Here $\mu_{sc}$ is the singular part of $\mu$ with respect to Lebesgue measure, restricted to the set $\{t:\mu(\{t\})=0\}$ of non-atoms of $\mu$ .
Let $S_{ac}=\{t : g_t(\varepsilon)\to L \text{ for some } 0<L<\infty\}$ . Then $\mu_{ac}(\mathbb{R}\setminus S_{ac})=0$ . Moreover, every Borel set $M_0\subseteq S_{ac}$ with $\mu_{ac}(M_0)=0$ has Lebesgue measure $0$ . Here

\mu_{ac}(A)=\int_A \tfrac{d\mu}{d\lambda}\,d\lambda,

where $\frac{d\mu}{d\lambda}$ is the Radon–Nikodym derivative of $\mu$ with respect to Lebesgue measure $\lambda$ .

If $\mu=0$ , then $g_t\equiv0$ for every $t$ . Parts 1–3 hold with limit $0$ , and part 3 applies only for $d=0$ . $\mu_{sc}=0$ , so part 4 is trivial. $S_{ac}=\varnothing$ and $\mu_{ac}=0$ , so part 5 is also satisfied.

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