Stieltjes functions

A Stieltjes function on (0, ∞) is a function with a representation

f(t) = a / t + b + ∫ x, 1 / (t + x) ∂μ,

where a and b are nonnegative and μ is a positive measure on ℝ≥0 satisfying μ {0} = 0 and ∫ (1 + x)⁻¹ ∂μ < ∞. Removing the atom at zero makes the singular coefficient a canonical. The weighted integrability condition is the standard sharp condition: the representing measure need not be finite, but it makes the transform finite at every positive parameter. Values outside (0, ∞) are deliberately unconstrained.

This file introduces the representation predicate and the function class, proves that the defining integral is genuinely integrable at every positive parameter, and develops the basic cone API and the elementary reciprocal examples. These are the foundations for the Stieltjes/Bernstein-function correspondences requested by the one-parameter-semigroups roadmap.

Main declarations

• TauCeti.RepresentsStieltjes: a measure and two nonnegative coefficients represent a function by the Stieltjes formula on (0, ∞).
• TauCeti.IsStieltjesFunction: existence of a Stieltjes representation.
• TauCeti.measurable_stieltjesWeight and TauCeti.integrable_stieltjesWeight: the weight is measurable, and every finite measure satisfies the weight condition.
• TauCeti.lintegral_inv_le_of_forall_integral_inv_add_le: an affine bound on the Stieltjes transform of a Stieltjes measure on ℝ≥0 near the origin bounds ∫ y, y⁻¹ ∂ν.
• TauCeti.IsStieltjesFunction.add, TauCeti.IsStieltjesFunction.smul: Stieltjes functions form a convex cone.
• TauCeti.isStieltjesFunction_const, TauCeti.isStieltjesFunction_inv, TauCeti.isStieltjesFunction_inv_const_add: the basic examples.

References

• R. Schilling, R. Song, Z. Vondraček, Bernstein Functions: Theory and Applications, 2nd ed., Definition 2.1 and Theorem 2.2.
• Roadmap: TauCetiRoadmap/OneParameterSemigroups/README.md, Part B, the Stieltjes/Bernstein-function relationships target.

noncomputable def TauCeti.stieltjesWeight (x : NNReal) : ℝ

The weight controlling a Stieltjes representing measure.

Equations

• TauCeti.stieltjesWeight x = (1 + ↑x)⁻¹

@[simp]

theorem TauCeti.stieltjesWeight_apply (x : NNReal) : stieltjesWeight x = (1 + ↑x)⁻¹

Evaluation of the standard Stieltjes weight.

def TauCeti.RepresentsStieltjes (μ : MeasureTheory.Measure NNReal) (a b : NNReal) (f : ℝ → ℝ) : Prop

A measure μ with coefficients a, b ≥ 0 represents f as a Stieltjes function if its standard weight is integrable and the Stieltjes formula holds on (0, ∞).

Equations

• TauCeti.RepresentsStieltjes μ a b f = (μ {0} = 0 ∧ MeasureTheory.Integrable TauCeti.stieltjesWeight μ ∧ ∀ (t : ℝ), 0 < t → f t = ↑a / t + ↑b + ∫ (x : NNReal), (t + ↑x)⁻¹ ∂μ)

theorem TauCeti.representsStieltjes_iff {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {f : ℝ → ℝ} : RepresentsStieltjes μ a b f ↔ μ {0} = 0 ∧ MeasureTheory.Integrable stieltjesWeight μ ∧ ∀ (t : ℝ), 0 < t → f t = ↑a / t + ↑b + ∫ (x : NNReal), (t + ↑x)⁻¹ ∂μ

Characterization of RepresentsStieltjes without unfolding its body.

theorem TauCeti.measurable_stieltjesWeight : Measurable stieltjesWeight

The standard Stieltjes weight is measurable.

theorem TauCeti.integrable_stieltjesWeight (μ : MeasureTheory.Measure NNReal) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.Integrable stieltjesWeight μ

The standard Stieltjes weight is bounded by 1, so it is integrable against every finite measure.

theorem TauCeti.integrable_inv_add {μ : MeasureTheory.Measure NNReal} (hμ : MeasureTheory.Integrable stieltjesWeight μ) {t : ℝ} (ht : 0 < t) : MeasureTheory.Integrable (fun (x : NNReal) => (t + ↑x)⁻¹) μ

The Stieltjes kernel is integrable at every positive parameter when its standard weight is.

theorem TauCeti.lintegral_inv_le_of_forall_integral_inv_add_le {ν : MeasureTheory.Measure NNReal} (hν : MeasureTheory.Integrable stieltjesWeight ν) {c C : ℝ} (h : ∀ (t : ℝ), 0 < t → ∫ (y : NNReal), (t + ↑y)⁻¹ ∂ν ≤ c + C * t) : ∫⁻ (y : NNReal), (↑y)⁻¹ ∂ν ≤ ENNReal.ofReal c

If the Stieltjes transform of a measure on ℝ≥0 satisfying the standard weighted integrability condition is bounded by c + C t at every positive parameter t, then ∫ y, y⁻¹ ∂ν ≤ c: the parameter may be sent to zero. The bound is stated as a lower Lebesgue integral because y ↦ y⁻¹ is unbounded, and the conclusion carries in particular the finiteness of that integral.

theorem TauCeti.RepresentsStieltjes.measure_singleton_zero {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {f : ℝ → ℝ} (h : RepresentsStieltjes μ a b f) : μ {0} = 0

A Stieltjes representing measure has no atom at zero.

theorem TauCeti.RepresentsStieltjes.integrable_weight {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {f : ℝ → ℝ} (h : RepresentsStieltjes μ a b f) : MeasureTheory.Integrable stieltjesWeight μ

The weighted integrability condition on a Stieltjes representing measure.

theorem TauCeti.RepresentsStieltjes.eq_div_add_add_integral_inv_add {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {f : ℝ → ℝ} (h : RepresentsStieltjes μ a b f) {t : ℝ} (ht : 0 < t) : f t = ↑a / t + ↑b + ∫ (x : NNReal), (t + ↑x)⁻¹ ∂μ

Evaluation of a Stieltjes representation at a positive parameter.

theorem TauCeti.RepresentsStieltjes.nonneg {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {f : ℝ → ℝ} (h : RepresentsStieltjes μ a b f) {t : ℝ} (ht : 0 < t) : 0 ≤ f t

A represented Stieltjes function is nonnegative on (0, ∞).

theorem TauCeti.RepresentsStieltjes.congr {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {f g : ℝ → ℝ} (h : RepresentsStieltjes μ a b f) (hfg : Set.EqOn g f (Set.Ioi 0)) : RepresentsStieltjes μ a b g

A Stieltjes representation depends only on the represented function's values on (0, ∞).

theorem TauCeti.RepresentsStieltjes.add {μ ν : MeasureTheory.Measure NNReal} {a b c d : NNReal} {f g : ℝ → ℝ} (hf : RepresentsStieltjes μ a b f) (hg : RepresentsStieltjes ν c d g) : RepresentsStieltjes (μ + ν) (a + c) (b + d) (f + g)

The sum of two Stieltjes representations is represented by the sum of their coefficients and measures.

theorem TauCeti.RepresentsStieltjes.smul {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {f : ℝ → ℝ} (h : RepresentsStieltjes μ a b f) {r : ℝ} (hr : 0 ≤ r) : RepresentsStieltjes (ENNReal.ofReal r • μ) (r.toNNReal * a) (r.toNNReal * b) (r • f)

A nonnegative scalar multiple of a Stieltjes representation is represented by scaling its coefficients and measure.

def TauCeti.IsStieltjesFunction (f : ℝ → ℝ) : Prop

A real function is a Stieltjes function if it has a standard Stieltjes representation on (0, ∞).

Equations

• TauCeti.IsStieltjesFunction f = ∃ (a : NNReal) (b : NNReal) (μ : MeasureTheory.Measure NNReal), TauCeti.RepresentsStieltjes μ a b f

theorem TauCeti.isStieltjesFunction_iff {f : ℝ → ℝ} : IsStieltjesFunction f ↔ ∃ (a : NNReal) (b : NNReal) (μ : MeasureTheory.Measure NNReal), RepresentsStieltjes μ a b f

Characterization of a Stieltjes function by its representing data.

theorem TauCeti.IsStieltjesFunction.nonneg {f : ℝ → ℝ} (hf : IsStieltjesFunction f) {t : ℝ} (ht : 0 < t) : 0 ≤ f t

A Stieltjes function is nonnegative on (0, ∞).

theorem TauCeti.IsStieltjesFunction.congr {f g : ℝ → ℝ} (hf : IsStieltjesFunction f) (hfg : Set.EqOn g f (Set.Ioi 0)) : IsStieltjesFunction g

The Stieltjes property depends only on values on (0, ∞).

theorem TauCeti.IsStieltjesFunction.add {f g : ℝ → ℝ} (hf : IsStieltjesFunction f) (hg : IsStieltjesFunction g) : IsStieltjesFunction (f + g)

Stieltjes functions are closed under addition.

theorem TauCeti.IsStieltjesFunction.smul {f : ℝ → ℝ} (hf : IsStieltjesFunction f) {r : ℝ} (hr : 0 ≤ r) : IsStieltjesFunction (r • f)

Stieltjes functions are closed under multiplication by a nonnegative scalar.

theorem TauCeti.isStieltjesFunction_const {b : ℝ} (hb : 0 ≤ b) : IsStieltjesFunction fun (x : ℝ) => b

Every nonnegative constant function is Stieltjes.

theorem TauCeti.isStieltjesFunction_zero : IsStieltjesFunction fun (x : ℝ) => 0

The zero function is Stieltjes.

theorem TauCeti.isStieltjesFunction_inv : IsStieltjesFunction fun (t : ℝ) => t⁻¹

The reciprocal t ↦ t⁻¹ is Stieltjes; it is the singular coefficient with zero measure.

theorem TauCeti.isStieltjesFunction_inv_const_add {x : ℝ} (hx : 0 ≤ x) : IsStieltjesFunction fun (t : ℝ) => (x + t)⁻¹

For x ≥ 0, the shifted reciprocal t ↦ (t + x)⁻¹ is Stieltjes. At x = 0 it is the singular term; for 0 < x it is represented by the Dirac mass at x.