Inversion of the parameter of Stieltjes and complete Bernstein functions

The substitution t ↦ t⁻¹ exchanges the two ends of (0, ∞), and the Stieltjes class is stable under the normalized substitution f ↦ (t ↦ f(t⁻¹) / t). On representing data it acts by exchanging the singular coefficient a of a / t with the constant coefficient b, and by the measure transformation

μ ↦ ν, the image of x⁻¹ μ(dx) under x ↦ x⁻¹,

because for x > 0 the kernels satisfy (t⁻¹ + x)⁻¹ / t = x⁻¹ (t + x⁻¹)⁻¹. This measure transformation, MeasureTheory.Measure.stieltjesInversion, preserves the Stieltjes weight condition, never charges 0, and is an involution on measures without an atom at 0. Consequently the substitution is an involution of the Stieltjes class modulo equality on (0, ∞).

Combined with the correspondence f ↦ t f(t) between Stieltjes and complete Bernstein functions, this yields two further standard dualities: f is Stieltjes exactly when t ↦ f(t⁻¹) on (0, ∞) extends to a complete Bernstein function, and for a complete Bernstein function f, the function t ↦ t f(t⁻¹) on (0, ∞) extends to a complete Bernstein function.

Main declarations

• MeasureTheory.Measure.stieltjesInversion: the measure transformation μ ↦ (x⁻¹ • μ).inv.
• MeasureTheory.Measure.integral_stieltjesInversion, MeasureTheory.Measure.lintegral_stieltjesInversion and MeasureTheory.Measure.integrable_stieltjesInversion_iff: integration against the transformed measure.
• MeasureTheory.Measure.stieltjesInversion_singleton_zero and MeasureTheory.Measure.integrable_weight_stieltjesInversion_iff: the transform never charges 0 and preserves the Stieltjes weight condition.
• MeasureTheory.Measure.stieltjesInversion_stieltjesInversion: the transformation is an involution on measures without an atom at 0.
• TauCeti.RepresentsStieltjes.comp_inv_div and TauCeti.representsStieltjes_comp_inv_div_iff: the effect of the substitution on representing data.
• TauCeti.IsStieltjesFunction.comp_inv_div and TauCeti.isStieltjesFunction_comp_inv_div_iff: the Stieltjes class is invariant under the substitution.
• TauCeti.isStieltjesFunction_iff_exists_isCompleteBernsteinFunction_eqOn_comp_inv: f is Stieltjes exactly when t ↦ f(t⁻¹) has a complete Bernstein extension.
• TauCeti.IsCompleteBernsteinFunction.exists_isCompleteBernsteinFunction_eqOn_mul_comp_inv: for a complete Bernstein function f, the function t ↦ t f(t⁻¹) on (0, ∞) has a complete Bernstein extension.

References

• R. Schilling, R. Song, Z. Vondraček, Bernstein Functions: Theory and Applications, de Gruyter, 2nd ed. (2012), Chapter 7.

noncomputable def MeasureTheory.Measure.stieltjesInversion (μ : Measure NNReal) : Measure NNReal

The measure transformation dual to the substitution t ↦ t⁻¹ in a Stieltjes representation: the image of the measure x⁻¹ μ(dx) under x ↦ x⁻¹. The density x⁻¹ is taken in ℝ≥0, so it vanishes at x = 0 and the transformed measure never charges 0.

Equations

• μ.stieltjesInversion = (μ.withDensity fun (x : NNReal) => ↑x⁻¹).inv

theorem MeasureTheory.Measure.integral_stieltjesInversion {μ : Measure NNReal} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : NNReal → E) : ∫ (y : NNReal), g y ∂μ.stieltjesInversion = ∫ (x : NNReal), (↑x)⁻¹ • g x⁻¹ ∂μ

Integration against stieltjesInversion μ in terms of μ.

theorem MeasureTheory.Measure.lintegral_stieltjesInversion {μ : Measure NNReal} (g : NNReal → ENNReal) (hg : Measurable g) : ∫⁻ (y : NNReal), g y ∂μ.stieltjesInversion = ∫⁻ (x : NNReal), ↑x⁻¹ * g x⁻¹ ∂μ

Lower Lebesgue integration against stieltjesInversion μ in terms of μ.

@[simp]

theorem MeasureTheory.Measure.integrable_stieltjesInversion_iff {μ : Measure NNReal} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : NNReal → E} : Integrable g μ.stieltjesInversion ↔ Integrable (fun (x : NNReal) => (↑x)⁻¹ • g x⁻¹) μ

Integrability against stieltjesInversion μ in terms of μ.

@[simp]

theorem MeasureTheory.Measure.stieltjesInversion_singleton_zero {μ : Measure NNReal} : μ.stieltjesInversion {0} = 0

The transformed measure never charges 0, because its density vanishes there.

@[simp]

theorem MeasureTheory.Measure.stieltjesInversion_stieltjesInversion_eq_restrict {μ : Measure NNReal} : μ.stieltjesInversion.stieltjesInversion = μ.restrict {0}ᶜ

Applying stieltjesInversion twice removes exactly the atom at 0.

theorem MeasureTheory.Measure.stieltjesInversion_stieltjesInversion {μ : Measure NNReal} (hμ : μ {0} = 0) : μ.stieltjesInversion.stieltjesInversion = μ

stieltjesInversion is an involution on measures without an atom at 0.

theorem MeasureTheory.Measure.integrable_weight_stieltjesInversion_iff_restrict {μ : Measure NNReal} : Integrable TauCeti.stieltjesWeight μ.stieltjesInversion ↔ Integrable TauCeti.stieltjesWeight (μ.restrict {0}ᶜ)

The transformed measure satisfies the Stieltjes weight condition exactly when the restriction of the original measure to (0, ∞) does. Indeed x⁻¹ (1 + x⁻¹)⁻¹ = (1 + x)⁻¹ for x > 0.

theorem MeasureTheory.Measure.integrable_weight_stieltjesInversion_iff {μ : Measure NNReal} (hμ : μ {0} = 0) : Integrable TauCeti.stieltjesWeight μ.stieltjesInversion ↔ Integrable TauCeti.stieltjesWeight μ

The transformed measure satisfies the Stieltjes weight condition exactly when the original measure does, provided the latter has no atom at 0.

theorem TauCeti.RepresentsStieltjes.comp_inv_div {a b : NNReal} {f : ℝ → ℝ} {μ : MeasureTheory.Measure NNReal} (h : RepresentsStieltjes μ a b f) : RepresentsStieltjes μ.stieltjesInversion b a fun (t : ℝ) => f t⁻¹ / t

Inversion of a Stieltjes representation. If (μ, a, b) represents f, then t ↦ f(t⁻¹) / t is represented by (stieltjesInversion μ, b, a): the singular and constant coefficients are exchanged.

@[simp]

theorem TauCeti.representsStieltjes_comp_inv_div_iff {ν : MeasureTheory.Measure NNReal} {a b : NNReal} {f : ℝ → ℝ} (hν : ν {0} = 0) : (RepresentsStieltjes ν b a fun (t : ℝ) => f t⁻¹ / t) ↔ RepresentsStieltjes ν.stieltjesInversion a b f

The substitution f ↦ (t ↦ f(t⁻¹) / t) is reversible on representing data: (ν, b, a) represents t ↦ f(t⁻¹) / t exactly when (stieltjesInversion ν, a, b) represents f, for any ν without an atom at 0.

theorem TauCeti.IsStieltjesFunction.comp_inv_div {f : ℝ → ℝ} (hf : IsStieltjesFunction f) : IsStieltjesFunction fun (t : ℝ) => f t⁻¹ / t

If f is a Stieltjes function, then so is t ↦ f(t⁻¹) / t.

@[simp]

theorem TauCeti.isStieltjesFunction_comp_inv_div_iff {f : ℝ → ℝ} : (IsStieltjesFunction fun (t : ℝ) => f t⁻¹ / t) ↔ IsStieltjesFunction f

The Stieltjes class is invariant under the involution f ↦ (t ↦ f(t⁻¹) / t).

theorem TauCeti.isStieltjesFunction_iff_exists_isCompleteBernsteinFunction_eqOn_comp_inv {f : ℝ → ℝ} : IsStieltjesFunction f ↔ ∃ (g : ℝ → ℝ), IsCompleteBernsteinFunction g ∧ Set.EqOn g (fun (t : ℝ) => f t⁻¹) (Set.Ioi 0)

Stieltjes functions and complete Bernstein functions under inversion. A function f is Stieltjes exactly when t ↦ f(t⁻¹) on (0, ∞) extends to a complete Bernstein function on [0, ∞).

theorem TauCeti.IsCompleteBernsteinFunction.exists_isCompleteBernsteinFunction_eqOn_mul_comp_inv {f : ℝ → ℝ} (hf : IsCompleteBernsteinFunction f) : ∃ (g : ℝ → ℝ), IsCompleteBernsteinFunction g ∧ Set.EqOn g (fun (t : ℝ) => t * f t⁻¹) (Set.Ioi 0)

Duality of complete Bernstein functions. If f is a complete Bernstein function, then t ↦ t f(t⁻¹) on (0, ∞) extends to a complete Bernstein function on [0, ∞).