Prove2Me

Theorem 3.22 — D̲μ ≤ liminf (1/π) Im F(λ+iε) ≤ limsup (1/π) Im F(λ+iε) ≤ D̄μ

Proved
TeschlQM.Herglotz.deriv_le_boundary_im

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

differentiation-of-measuresherglotz-functionsmeasure-theoryp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1

Let μ\mu be a finite Borel measure on R\mathbb{R} with Borel transform FF, and let D‾μ\underline{D}\mu, D‾μ\overline{D}\mu be its lower and upper derivatives with respect to Lebesgue measure. Then for every λ∈R\lambda \in \mathbb{R}

(D‾μ)(λ)≤lim inf⁡ε↓01πIm⁡F(λ+iε)≤lim sup⁡ε↓01πIm⁡F(λ+iε)≤(D‾μ)(λ).(\underline{D}\mu)(\lambda) \le \liminf_{\varepsilon\downarrow 0} \frac1\pi \operatorname{Im} F(\lambda + i\varepsilon) \le \limsup_{\varepsilon\downarrow 0} \frac1\pi \operatorname{Im} F(\lambda + i\varepsilon) \le (\overline{D}\mu)(\lambda).

So the boundary values of Im⁡F\operatorname{Im} F are squeezed between the lower and upper derivatives of μ\mu, which is how the Radon–Nikodym derivative of μ\mu is read off from FF.

Formalization Note. The printed (3.90) has 1πF(λ+iε)\frac1\pi F(\lambda + i\varepsilon) without Im⁡\operatorname{Im}, a complex number that cannot be compared with the real derivatives; the proof on the same page estimates Im⁡(F(λ+iε))\operatorname{Im}(F(\lambda + i\varepsilon)), and that is what is stated. Since Im⁡F(λ+iε)=∫ε/((t−λ)2+ε2) dμ(t)≥0\operatorname{Im} F(\lambda + i\varepsilon) = \int \varepsilon/((t-\lambda)^2+\varepsilon^2)\,d\mu(t) \ge 0 for ε>0\varepsilon > 0, the quantities are compared in [0,∞][0,\infty] via ENNReal.ofReal, which loses nothing on nonnegative reals.

Preamble
import Mathlib
import Definitions.Def_TeschlQM_Herglotz_borelTransform
import Definitions.Def_TeschlQM_Herglotz_lowerDeriv
import Definitions.Def_TeschlQM_Herglotz_upperDeriv

open MeasureTheory Filter
open scoped ENNReal Topology
Formal statement
namespace TeschlQM.Herglotz

/-- Teschl, p. 108, Theorem 3.22. Let `μ` be a finite Borel measure and `F` its Borel transform.
Then, for every `λ ∈ ℝ`, (3.90)
`(D̲μ)(λ) ≤ liminf_{ε↓0} (1/π) Im F(λ + iε) ≤ limsup_{ε↓0} (1/π) Im F(λ + iε) ≤ (D̄μ)(λ)`.
The printed (3.90) omits `Im`; the proof on pp. 108–109 estimates `Im(F(λ + iε))`, which is
nonnegative for `ε > 0`, so the quantities are compared in `[0, ∞]`. -/
theorem deriv_le_boundary_im (μ : Measure ℝ) [IsFiniteMeasure μ] (t : ℝ) :
    lowerDeriv μ t ≤ liminf (fun ε : ℝ => ENNReal.ofReal
        ((borelTransform μ ((t : ℂ) + (ε : ℂ) * Complex.I)).im / Real.pi)) (𝓝[>] (0 : ℝ)) ∧
    liminf (fun ε : ℝ => ENNReal.ofReal
        ((borelTransform μ ((t : ℂ) + (ε : ℂ) * Complex.I)).im / Real.pi)) (𝓝[>] (0 : ℝ)) ≤
      limsup (fun ε : ℝ => ENNReal.ofReal
        ((borelTransform μ ((t : ℂ) + (ε : ℂ) * Complex.I)).im / Real.pi)) (𝓝[>] (0 : ℝ)) ∧
    limsup (fun ε : ℝ => ENNReal.ofReal
        ((borelTransform μ ((t : ℂ) + (ε : ℂ) * Complex.I)).im / Real.pi)) (𝓝[>] (0 : ℝ)) ≤
      upperDeriv μ t := by sorry

end TeschlQM.Herglotz
Source
Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 108, Theorem 3.22
Read-back

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

Let μ\mu be a finite Borel measure on R\mathbb{R}, let t∈Rt\in\mathbb{R}, and let F(z)=∫Rdμ(s)s−zF(z)=\int_{\mathbb{R}}\frac{d\mu(s)}{s-z} be its Borel transform (Bochner integral, 00 if not integrable). For ε>0\varepsilon>0 define

g(ε)=max⁡ ⁣(0, 1πIm⁡F(t+iε))∈[0,∞).g(\varepsilon)=\max\!\Big(0,\ \tfrac{1}{\pi}\operatorname{Im} F(t+i\varepsilon)\Big)\in[0,\infty).

This is a real number converted to [0,∞][0,\infty], with negative values replaced by 00.

Also define

(D‾μ)(t)=lim inf⁡ε↓0μ((t−ε,t+ε))2εand(D‾μ)(t)=lim sup⁡ε↓0μ((t−ε,t+ε))2ε,(\underline{D}\mu)(t)=\liminf_{\varepsilon\downarrow0}\frac{\mu((t-\varepsilon,t+\varepsilon))}{2\varepsilon} \quad\text{and}\quad (\overline{D}\mu)(t)=\limsup_{\varepsilon\downarrow0}\frac{\mu((t-\varepsilon,t+\varepsilon))}{2\varepsilon},

both computed in [0,∞][0,\infty]. The statement asserts the chain

(D‾μ)(t) ≤ lim inf⁡ε↓0g(ε) ≤ lim sup⁡ε↓0g(ε) ≤ (D‾μ)(t).(\underline{D}\mu)(t)\ \le\ \liminf_{\varepsilon\downarrow 0} g(\varepsilon)\ \le\ \limsup_{\varepsilon\downarrow 0} g(\varepsilon)\ \le\ (\overline{D}\mu)(t).

All liminfs and limsups are taken in [0,∞][0,\infty], with ε→0\varepsilon\to0 through strictly positive values.

If μ=0\mu=0, every quantity in the chain is 00.

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