Documentation

TauCeti.Analysis.CompletelyMonotone.Stieltjes.Bernstein

From Stieltjes functions to Bernstein functions #

If

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

then its continuously extended product with the parameter is a Bernstein function:

g t = a + b * t + ∫ x, t / (t + x) ∂μ.

On the open half-line this is exactly t * f(t), while g(0) = a. The value at zero is essential: the literal product 0 * f(0) would lose the coefficient of the possible a / t singularity. This is the first standard Stieltjes--Bernstein correspondence.

The proof differentiates the integral on the open half-line. Its derivative is

∫ x, x / (t + x) ^ 2 ∂μ,

whose derivatives have alternating signs. Continuity at zero follows by dominated convergence; the normalization μ {0} = 0 removes the only point where t / (t + x) does not tend to zero.

Main declarations #

References #

source
noncomputable def TauCeti.stieltjesBernsteinTransform (μ : MeasureTheory.Measure NNReal) (a b : NNReal) (t : ℝ) :
ℝ

The candidate Bernstein transform associated to Stieltjes representing data. Under the normalization and integrability hypotheses of isBernsteinFunction_stieltjesBernsteinTransform, it is a Bernstein function and is continuous on [0, ∞). For representing data, the later theorem RepresentsStieltjes.stieltjesBernsteinTransform_eq_mul identifies it with t * f t for positive t. Its defining equation is stieltjesBernsteinTransform_apply.

Equations
Instances For
    source
    theorem TauCeti.stieltjesBernsteinTransform_apply (μ : MeasureTheory.Measure NNReal) (a b : NNReal) (t : ℝ) :
    stieltjesBernsteinTransform μ a b t = ↑a + ↑b * t + ∫ (x : NNReal), t / (t + ↑x) ∂μ

    The defining equation for the Stieltjes--Bernstein transform.

    source
    @[simp]
    theorem TauCeti.stieltjesBernsteinTransform_zero (μ : MeasureTheory.Measure NNReal) (a b : NNReal) :
    stieltjesBernsteinTransform μ a b 0 = ↑a

    The Stieltjes--Bernstein transform takes the value a at zero.

    source
    theorem TauCeti.integral_div_add_eq_mul_integral_inv_add (μ : MeasureTheory.Measure NNReal) (t : ℝ) :
    ∫ (x : NNReal), t / (t + ↑x) ∂μ = t * ∫ (x : NNReal), (t + ↑x)⁻¹ ∂μ

    The integral term in the Stieltjes--Bernstein transform is the parameter times the corresponding Stieltjes integral.

    source
    theorem TauCeti.integrable_mul_zpow_neg_two_sub_add {μ : MeasureTheory.Measure NNReal} (hμ : MeasureTheory.Integrable stieltjesWeight μ) (n : ℕ) {t : ℝ} (ht : 0 < t) :
    MeasureTheory.Integrable (fun (x : NNReal) => ↑x * (t + ↑x) ^ (-2 - ↑n)) μ

    The kernels in the iterated derivative formula for the integral term of the Stieltjes--Bernstein transform are integrable at positive parameters.

    source
    theorem TauCeti.iteratedDeriv_integral_div_add {μ : MeasureTheory.Measure NNReal} (hμ : MeasureTheory.Integrable stieltjesWeight μ) (n : ℕ) {t : ℝ} (ht : 0 < t) :
    iteratedDeriv (n + 1) (fun (u : ℝ) => ∫ (x : NNReal), u / (u + ↑x) ∂μ) t = (-1) ^ n * ↑(n + 1).factorial * ∫ (x : NNReal), ↑x * (t + ↑x) ^ (-2 - ↑n) ∂μ

    The iterated derivatives of the integral term in the Stieltjes--Bernstein transform at a positive parameter.

    source
    theorem TauCeti.hasDerivAt_stieltjesBernsteinTransform {μ : MeasureTheory.Measure NNReal} {a b : NNReal} (hμ : MeasureTheory.Integrable stieltjesWeight μ) {t : ℝ} (ht : 0 < t) :
    HasDerivAt (stieltjesBernsteinTransform μ a b) (↑b + ∫ (x : NNReal), ↑x / (t + ↑x) ^ 2 ∂μ) t

    The derivative of the Stieltjes--Bernstein transform at a positive parameter.

    source
    theorem TauCeti.deriv_stieltjesBernsteinTransform {μ : MeasureTheory.Measure NNReal} {a b : NNReal} (hμ : MeasureTheory.Integrable stieltjesWeight μ) {t : ℝ} (ht : 0 < t) :
    deriv (stieltjesBernsteinTransform μ a b) t = ↑b + ∫ (x : NNReal), ↑x / (t + ↑x) ^ 2 ∂μ

    The derivative formula for the Stieltjes--Bernstein transform at a positive parameter.

    source
    theorem TauCeti.isBernsteinFunction_integral_div_add {μ : MeasureTheory.Measure NNReal} (hzero : μ {0} = 0) (hμ : MeasureTheory.Integrable stieltjesWeight μ) :
    IsBernsteinFunction fun (t : ℝ) => ∫ (x : NNReal), t / (t + ↑x) ∂μ

    The integral term in the Stieltjes--Bernstein transform is a Bernstein function under the normalization and integrability hypotheses on the representing measure.

    source
    theorem TauCeti.isBernsteinFunction_stieltjesBernsteinTransform {μ : MeasureTheory.Measure NNReal} {a b : NNReal} (hzero : μ {0} = 0) (hμ : MeasureTheory.Integrable stieltjesWeight μ) :
    IsBernsteinFunction (stieltjesBernsteinTransform μ a b)

    The transform built from normalized Stieltjes representing data is a Bernstein function.

    source
    theorem TauCeti.RepresentsStieltjes.stieltjesBernsteinTransform_eq_mul {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {f : ℝ → ℝ} (h : RepresentsStieltjes μ a b f) {t : ℝ} (ht : 0 < t) :
    stieltjesBernsteinTransform μ a b t = t * f t

    Multiplying a represented Stieltjes function by its parameter gives the associated Bernstein transform on the open half-line.

    source
    theorem TauCeti.RepresentsStieltjes.isBernsteinFunction_stieltjesBernsteinTransform {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {f : ℝ → ℝ} (h : RepresentsStieltjes μ a b f) :
    IsBernsteinFunction (stieltjesBernsteinTransform μ a b)

    The transform attached to a Stieltjes representation is a Bernstein function. Its agreement with t * f(t) on (0, ∞) is RepresentsStieltjes.stieltjesBernsteinTransform_eq_mul, and its boundary value at zero is stieltjesBernsteinTransform_zero.