A finite Borel measure is uniquely determined by its transform on the upper half-plane

Proved

TeschlQM.Herglotz.borelTransform_unique

by Mazecto · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

complex-analysismeasure-theoryspectral-theory

Let $\mu,\nu$ be finite Borel measures on $\mathbb R$ . If

F_\mu(z)=F_\nu(z)\qquad(\operatorname{Im}z>0),

then $\mu=\nu$ . Equality is required only on the open upper half-plane; both measures may have atoms and singular parts.

Preamble

import Definitions.Def_TeschlQM_Herglotz_borelTransform
import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
import Mathlib.MeasureTheory.Integral.DominatedConvergence
import Mathlib.MeasureTheory.Integral.Prod
import Mathlib.MeasureTheory.Constructions.BorelSpace.Order
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.FunProp
import Mathlib.Tactic.SplitIfs
import Mathlib.Tactic.NormNum

open MeasureTheory Filter Set
open scoped Topology

Formal statement

theorem TeschlQM.Herglotz.borelTransform_unique (μ ν : Measure ℝ) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    (h : ∀ z : ℂ, 0 < z.im →
      TeschlQM.Herglotz.borelTransform μ z = TeschlQM.Herglotz.borelTransform ν z) : μ = ν := by sorry

Source

G. Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99 (2009), p. 108, Theorem 3.21 and its proof, Eq. (3.89); https://www.mat.univie.ac.at/~gerald/ftp/book-schroe/schroe.pdf (PDF p. 119).

View graph