Approximating measures for Bernstein's theorem

The Chafaï-style approximating measures for the non-constant part of a completely monotone function in Bernstein's theorem. For a completely monotone f with L = lim_{t→∞} f t, the densities ρ_n(t) = (-1)ⁿ/(n-1)! · tⁿ⁻¹ · f⁽ⁿ⁾(t) are nonnegative on [0, ∞), the positive support used by chafaiMeasure; they define finite measures whose total mass is bounded by f(0) - f(∞) = f(0) - L, and after the rescaling t ↦ (n-1)/t give measures chafaiRescaled f n on ℝ≥0 whose Laplace kernels (1 - xp/(n-1))₊ⁿ⁻¹ converge to e^{-xp}. These feed the Prokhorov tightness argument and, in the limit, represent f - L (mass f(0) - L), i.e. the non-constant part; the full Bernstein representing measure adds the atom L · δ₀ at 0 (the constant L = ∫ e^{-tx} d(L·δ₀)). That final assembly — recovering f itself, not merely f - L — is performed downstream in the Bernstein-theorem file, not here. This file supplies only the approximating infrastructure.

These build on the IsCompletelyMonotone API in CompletelyMonotone/Basic.lean and CompletelyMonotone/Integral/Basic.lean.

Main declarations

• TauCeti.chafaiDensity, TauCeti.chafaiMeasure: the approximating densities and measures.
• TauCeti.bernsteinKernel, TauCeti.continuous_bernsteinKernel, TauCeti.bernsteinKernel_nonneg, TauCeti.bernsteinKernel_le_one, TauCeti.bernsteinKernelBoundedContinuous, TauCeti.bernsteinKernelBoundedContinuous_apply, TauCeti.integrable_bernsteinKernel, TauCeti.bernsteinKernel_tendsto: the rescaled Laplace kernel, its bundled bounded-continuous p-dependence on the nonnegative half-line, and its pointwise limit e^{-xp} (bundled as TauCeti.laplaceKernelBoundedContinuous in CompletelyMonotone/Laplace/Kernel.lean).
• TauCeti.integral_exp_neg_mul_add_smul_dirac_zero: adjoining an atom c • δ₀ adds exactly c to the transform, the kernel being 1 at 0.
• TauCeti.chafaiRescaled, TauCeti.chafaiRescaled_mass_eq: the ℝ≥0-valued pushed-forward measures and mass preservation.
• TauCeti.chafaiRescaled_integral_bernsteinKernel, TauCeti.chafaiRescaled_integral_bernsteinKernelBoundedContinuous, TauCeti.ae_nonneg_bernsteinKernel_chafaiRescaled: characteristic lemmas pairing the rescaled Chafaï measures with the Bernstein kernel without unfolding either definition.
• TauCeti.chafaiMeasure_finite_mass, TauCeti.chafaiRescaled_finite_mass: finiteness and the total-mass bound ≤ f(0) - L.
• TauCeti.chafaiRescaled_prokhorov_mass_bound, TauCeti.chafaiRescaled_tendsto_laplace_integral_of_weak: Prokhorov-ready mass bounds and the Laplace test-function specialization of weak convergence for the rescaled measures.
• TauCeti.chafaiRescaled_lintegral_coe_le: first-moment / coe-lintegral bound.
• TauCeti.chafaiRescaled_integral_bernsteinKernel_eq_sub_tendsto_atTop: Chafaï reconstruction identity f x - L = ∫ bernsteinKernel ∂chafaiRescaled.
• TauCeti.integral_bernsteinKernel_sub_laplaceKernel_tendsto_zero_of_mass_bound: Bernstein-kernel to Laplace-kernel error tends to 0.

References

• Roadmap: TauCetiRoadmap/OneParameterSemigroups/README.md, Part B (Bernstein theorem milestone).

• D. Chafaï, Aspects of the Bernstein theorem (2013).

• R. Schilling, R. Song, Z. Vondraček, Bernstein Functions (de Gruyter, 2nd ed. 2012), Ch. 1.

Smoothness-index helpers

Measure construction for Bernstein

noncomputable def TauCeti.chafaiDensity (f : ℝ → ℝ) (n : ℕ) (t : ℝ) : ℝ

The density ρ_n(t) = (-1)ⁿ/(n-1)! · tⁿ⁻¹ · f⁽ⁿ⁾(t) for nonzero n, used for the n-th approximating measure in the Bernstein proof (Chafaï 2013). By convention the n = 0 branch returns 0.

Equations

• TauCeti.chafaiDensity f n t = if n = 0 then 0 else (-1) ^ n / ↑(n - 1).factorial * t ^ (n - 1) * iteratedDerivWithin n f (Set.Ici 0) t

@[simp]

theorem TauCeti.chafaiDensity_zero (f : ℝ → ℝ) (t : ℝ) : chafaiDensity f 0 t = 0

chafaiDensity f 0 = 0.

@[simp]

theorem TauCeti.chafaiDensity_of_ne_zero {n : ℕ} (hn : n ≠ 0) (f : ℝ → ℝ) (t : ℝ) : chafaiDensity f n t = (-1) ^ n / ↑(n - 1).factorial * t ^ (n - 1) * iteratedDerivWithin n f (Set.Ici 0) t

The defining formula for chafaiDensity at a nonzero order.

theorem TauCeti.continuousOn_chafaiDensity {f : ℝ → ℝ} {n : ℕ} (hf : ContDiffOn ℝ (↑n) f (Set.Ici 0)) : ContinuousOn (chafaiDensity f n) (Set.Ici 0)

chafaiDensity f n is continuous on [0, ∞) when f has n continuous derivatives there.

noncomputable def TauCeti.chafaiMeasure (f : ℝ → ℝ) (n : ℕ) : MeasureTheory.Measure ℝ

The n-th Chafaï approximating measure σ_n for the Bernstein representation, with density ρ_n on (0, ∞).

Equations

• TauCeti.chafaiMeasure f n = (MeasureTheory.volume.restrict (Set.Ioi 0)).withDensity fun (t : ℝ) => ENNReal.ofReal (TauCeti.chafaiDensity f n t)

theorem TauCeti.chafaiMeasure_eq_withDensity (f : ℝ → ℝ) (n : ℕ) : chafaiMeasure f n = (MeasureTheory.volume.restrict (Set.Ioi 0)).withDensity fun (t : ℝ) => ENNReal.ofReal (chafaiDensity f n t)

chafaiMeasure as a withDensity, exposed as a lemma rather than an unfoldable body.

@[simp]

theorem TauCeti.chafaiMeasure_apply (f : ℝ → ℝ) (n : ℕ) {s : Set ℝ} (hs : MeasurableSet s) : (chafaiMeasure f n) s = ∫⁻ (t : ℝ) in s, ENNReal.ofReal (chafaiDensity f n t) ∂MeasureTheory.volume.restrict (Set.Ioi 0)

The mass chafaiMeasure f n assigns to a measurable set, as a set lintegral of the density.

theorem TauCeti.chafaiDensity_nonneg {f : ℝ → ℝ} {n : ℕ} {t : ℝ} (ht : 0 ≤ t) (hsign : 0 ≤ (-1) ^ n * iteratedDerivWithin n f (Set.Ici 0) t) : 0 ≤ chafaiDensity f n t

The density ρ_n(t) is nonnegative when t ≥ 0 and the n-th derivative has the alternating sign at t.

theorem TauCeti.chafaiDensity_one {f : ℝ → ℝ} (t : ℝ) : chafaiDensity f 1 t = -iteratedDerivWithin 1 f (Set.Ici 0) t

For n = 1, the density simplifies to -f'(t).

Rescaled measures and Prokhorov extraction

noncomputable def TauCeti.bernsteinKernel (n : ℕ) (x p : ℝ) : ℝ

The Bernstein kernel φ_n(x,p) = max(1 - xp/(n-1), 0)ⁿ⁻¹ for n ≥ 2. After the change of variable p = (n-1)/t, the Taylor integral kernel on [0, T] becomes φ_n(x, p), which converges pointwise to e^{-xp} as n → ∞ (the classical (1-x/n)ⁿ → e^{-x} limit).

Equations

• TauCeti.bernsteinKernel n x p = if n ≤ 1 then 0 else max (1 - x * p / ↑(n - 1)) 0 ^ (n - 1)

@[simp]

theorem TauCeti.bernsteinKernel_of_le_one {n : ℕ} (hn : n ≤ 1) (x p : ℝ) : bernsteinKernel n x p = 0

The Bernstein kernel vanishes for n ≤ 1.

@[simp]

theorem TauCeti.bernsteinKernel_of_two_le {n : ℕ} (hn : 2 ≤ n) (x p : ℝ) : bernsteinKernel n x p = max (1 - x * p / ↑(n - 1)) 0 ^ (n - 1)

The defining formula for the Bernstein kernel at 2 ≤ n.

theorem TauCeti.continuous_bernsteinKernel (n : ℕ) (x : ℝ) : Continuous (bernsteinKernel n x)

The Bernstein kernel is continuous in p for fixed n and x.

@[simp]

theorem TauCeti.bernsteinKernel_nonneg (n : ℕ) (x p : ℝ) : 0 ≤ bernsteinKernel n x p

The Bernstein kernel is nonnegative.

theorem TauCeti.bernsteinKernel_le_one {n : ℕ} {x p : ℝ} (hx : 0 ≤ x) (hp : 0 ≤ p) : bernsteinKernel n x p ≤ 1

On the nonnegative half-plane, the Bernstein kernel is bounded above by 1.

noncomputable def TauCeti.bernsteinKernelBoundedContinuous (n : ℕ) {x : ℝ} (hx : 0 ≤ x) : BoundedContinuousFunction NNReal ℝ

The Bernstein kernel as a bundled bounded continuous test function of the nonnegative variable p, for fixed n and nonnegative x.

Equations

• TauCeti.bernsteinKernelBoundedContinuous n hx = { toFun := fun (p : NNReal) => TauCeti.bernsteinKernel n x ↑p, continuous_toFun := ⋯, map_bounded' := ⋯ }

@[simp]

theorem TauCeti.bernsteinKernelBoundedContinuous_apply (n : ℕ) {x : ℝ} (hx : 0 ≤ x) (p : NNReal) : (bernsteinKernelBoundedContinuous n hx) p = bernsteinKernel n x ↑p

The bundled Bernstein kernel evaluates to the unbundled kernel on ℝ≥0.

theorem TauCeti.integrable_bernsteinKernel (μ : MeasureTheory.Measure NNReal) [MeasureTheory.IsFiniteMeasure μ] (n : ℕ) {x : ℝ} (hx : 0 ≤ x) : MeasureTheory.Integrable (fun (p : NNReal) => bernsteinKernel n x ↑p) μ

The Bernstein kernel at a nonnegative point is integrable against a finite measure. For 0 ≤ x, the map p ↦ bernsteinKernel n x p is integrable against any finite measure on ℝ≥0. The companion of TauCeti.integrable_exp_neg_mul, which says the same of the Laplace kernel.

@[simp]

theorem TauCeti.integral_exp_neg_mul_add_smul_dirac_zero (μ : MeasureTheory.Measure NNReal) [MeasureTheory.IsFiniteMeasure μ] (c : NNReal) {x : ℝ} (hx : 0 ≤ x) : ∫ (p : NNReal), Real.exp (-(x * ↑p)) ∂(μ + c • MeasureTheory.Measure.dirac 0) = ∫ (p : NNReal), Real.exp (-(x * ↑p)) ∂μ + ↑c

An atom at 0 shifts the Laplace transform by its mass. The kernel takes the value 1 at p = 0, so adjoining c • δ₀ to a finite measure adds exactly c.

theorem TauCeti.measurable_bernsteinKernel (n : ℕ) (x : ℝ) : Measurable (bernsteinKernel n x)

The Bernstein kernel is measurable in p for fixed n and x.

theorem TauCeti.bernsteinKernel_tendsto (x p : ℝ) : Filter.Tendsto (fun (n : ℕ) => bernsteinKernel n x p) Filter.atTop (nhds (Real.exp (-(x * p))))

Pointwise convergence of the Bernstein kernel to the Laplace kernel: φ_n(x,p) → e^{-xp} as n → ∞.

noncomputable def TauCeti.chafaiRescaling (n : ℕ) (t : ℝ) : NNReal

The rescaling map t ↦ max ((n-1)/t) 0, valued in ℝ≥0.

Equations

• TauCeti.chafaiRescaling n t = ((↑n - 1) / t).toNNReal

theorem TauCeti.measurable_chafaiRescaling (n : ℕ) : Measurable (chafaiRescaling n)

The rescaling map t ↦ max ((n-1)/t) 0, valued in ℝ≥0, is measurable.

@[simp]

theorem TauCeti.chafaiRescaling_coe_of_nonneg {n : ℕ} (hn : 1 ≤ n) {t : ℝ} (ht : 0 ≤ t) : ↑(chafaiRescaling n t) = (↑n - 1) / t

On the nonnegative part of the source, the ℝ≥0 rescaling coerces back to (n-1)/t.

noncomputable def TauCeti.chafaiRescaled (f : ℝ → ℝ) (n : ℕ) : MeasureTheory.Measure NNReal

The rescaled measure σ̃_n: pushforward of chafaiMeasure f n under the ℝ≥0 rescaling.

Equations

• TauCeti.chafaiRescaled f n = MeasureTheory.Measure.map (TauCeti.chafaiRescaling n) (TauCeti.chafaiMeasure f n)

theorem TauCeti.chafaiRescaled_eq_map (f : ℝ → ℝ) (n : ℕ) : chafaiRescaled f n = MeasureTheory.Measure.map (chafaiRescaling n) (chafaiMeasure f n)

chafaiRescaled as a pushforward, exposed as a lemma rather than an unfoldable body.

@[simp]

theorem TauCeti.chafaiRescaled_apply (f : ℝ → ℝ) (n : ℕ) {s : Set NNReal} (hs : MeasurableSet s) : (chafaiRescaled f n) s = (chafaiMeasure f n) (chafaiRescaling n ⁻¹' s)

The mass chafaiRescaled f n assigns to a measurable set, as the pushforward formula.

theorem TauCeti.chafaiRescaled_integral (f : ℝ → ℝ) (n : ℕ) {g : NNReal → ℝ} (hg : MeasureTheory.AEStronglyMeasurable g (chafaiRescaled f n)) : ∫ (x : NNReal), g x ∂chafaiRescaled f n = ∫ (t : ℝ), g (chafaiRescaling n t) ∂chafaiMeasure f n

Integrating against chafaiRescaled f n is integrating the pullback along the Chafaï rescaling against chafaiMeasure f n.

theorem TauCeti.bernsteinKernel_chafaiRescaling_of_pos {n : ℕ} (hn : 2 ≤ n) (x : ℝ) {t : ℝ} (ht : 0 < t) : bernsteinKernel n x ↑(chafaiRescaling n t) = max (1 - x / t) 0 ^ (n - 1)

On positive source points, pulling the Bernstein kernel back along the Chafaï rescaling gives the classical finite-order kernel (max (1 - x / t) 0) ^ (n - 1).

@[simp]

theorem TauCeti.ae_nonneg_bernsteinKernel_chafaiRescaled (f : ℝ → ℝ) (n : ℕ) (x : ℝ) : 0 ≤ᵐ[chafaiRescaled f n] fun (p : NNReal) => bernsteinKernel n x ↑p

The Bernstein kernel is nonnegative almost everywhere against every rescaled Chafaï measure. This is the public positivity lemma consumers need before using monotone or positivity facts for the kernel pairing.

theorem TauCeti.ae_nonneg_bernsteinKernelBoundedContinuous_chafaiRescaled (f : ℝ → ℝ) (n : ℕ) {x : ℝ} (hx : 0 ≤ x) : 0 ≤ᵐ[chafaiRescaled f n] fun (p : NNReal) => (bernsteinKernelBoundedContinuous n hx) p

Bundled version of ae_nonneg_bernsteinKernel_chafaiRescaled for the bounded-continuous Bernstein kernel.

@[simp]

theorem TauCeti.chafaiRescaled_integral_bernsteinKernel (f : ℝ → ℝ) (n : ℕ) (x : ℝ) : ∫ (p : NNReal), bernsteinKernel n x ↑p ∂chafaiRescaled f n = ∫ (t : ℝ), bernsteinKernel n x ↑(chafaiRescaling n t) ∂chafaiMeasure f n

Characteristic pairing of the rescaled Chafaï measure with the Bernstein kernel: integrating p ↦ φ_n(x,p) against chafaiRescaled f n is the same as integrating its Chafaï-rescaling pullback against the original Chafaï measure.

theorem TauCeti.chafaiRescaled_integral_bernsteinKernelBoundedContinuous (f : ℝ → ℝ) (n : ℕ) {x : ℝ} (hx : 0 ≤ x) : ∫ (p : NNReal), (bernsteinKernelBoundedContinuous n hx) p ∂chafaiRescaled f n = ∫ (t : ℝ), bernsteinKernel n x ↑(chafaiRescaling n t) ∂chafaiMeasure f n

Bounded-continuous characteristic pairing of the rescaled Chafaï measure with the Bernstein kernel. This lets weak-convergence consumers use the bundled test function while the right-hand side is the concrete pullback along the Chafaï rescaling.

theorem TauCeti.chafaiMeasure_compl_Ioi (f : ℝ → ℝ) (n : ℕ) : (chafaiMeasure f n) (Set.Ioi 0)ᶜ = 0

chafaiMeasure f n lives on (0, ∞): its complement has zero mass.

theorem TauCeti.chafaiRescaled_mass_eq (f : ℝ → ℝ) (n : ℕ) : (chafaiRescaled f n) Set.univ = (chafaiMeasure f n) Set.univ

Pushforward preserves total mass.

theorem TauCeti.integral_chafaiDensity_le_pred (f : ℝ → ℝ) {k : ℕ} (hk : 2 ≤ k) (hf : ContDiffOn ℝ (↑k) f (Set.Ici 0)) (T : ℝ) (hT : 0 ≤ T) (hsign : 0 ≤ (-1) ^ (k - 1) * iteratedDerivWithin (k - 1) f (Set.Ici 0) T) : ∫ (t : ℝ) in 0..T, chafaiDensity f k t ≤ ∫ (t : ℝ) in 0..T, chafaiDensity f (k - 1) t

Monotonicity of the finite-interval Chafaï-density integrals in the order: for 2 ≤ k and 0 ≤ T, the integral of the k-th density on [0,T] is bounded above by the integral of the preceding density, assuming the endpoint has the required alternating sign.

@[simp]

theorem TauCeti.chafaiMeasure_zero (f : ℝ → ℝ) : chafaiMeasure f 0 = 0

The public n = 0 convention for Chafaï measures: the zeroth approximating measure is zero.

@[simp]

theorem TauCeti.chafaiRescaled_zero (f : ℝ → ℝ) : chafaiRescaled f 0 = 0

The rescaled Chafaï measure on the target type ℝ≥0 shares the n = 0 zero convention: chafaiRescaled f 0 = 0, as the pushforward of the zero measure.

theorem TauCeti.chafaiMeasure_finite_mass_of_tendsto (f : ℝ → ℝ) (hcm : IsCompletelyMonotone f) (n : ℕ) (L : ℝ) (hL : Filter.Tendsto f Filter.atTop (nhds L)) : MeasureTheory.IsFiniteMeasure (chafaiMeasure f n) ∧ (chafaiMeasure f n) Set.univ ≤ ENNReal.ofReal (f 0 - L)

Total mass bound with a chosen limit: chafaiMeasure f n is finite with total mass ≤ f(0) - L whenever f(t) → L at infinity.

theorem TauCeti.chafaiMeasure_finite_mass (f : ℝ → ℝ) (hcm : IsCompletelyMonotone f) : ∃ (L : ℝ), Filter.Tendsto f Filter.atTop (nhds L) ∧ 0 ≤ L ∧ ∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (chafaiMeasure f n) ∧ (chafaiMeasure f n) Set.univ ≤ ENNReal.ofReal (f 0 - L)

Natural total mass bound: for a completely monotone f, the Chafaï measures are finite and uniformly bounded by f(0) - L, where L is the automatically obtained limit of f at infinity.

theorem TauCeti.chafaiRescaled_finite_mass (f : ℝ → ℝ) (hcm : IsCompletelyMonotone f) : ∃ (L : ℝ), Filter.Tendsto f Filter.atTop (nhds L) ∧ 0 ≤ L ∧ ∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (chafaiRescaled f n) ∧ (chafaiRescaled f n) Set.univ ≤ ENNReal.ofReal (f 0 - L)

Natural rescaled total mass bound: for a completely monotone f, the rescaled Chafaï measures on ℝ≥0 are finite and uniformly bounded by f(0) - L, where L is the automatically obtained limit of f at infinity.

theorem TauCeti.chafaiRescaled_lintegral_coe_le (f : ℝ → ℝ) (hcm : IsCompletelyMonotone f) (n : ℕ) : ∫⁻ (p : NNReal), ENNReal.ofReal ↑p ∂chafaiRescaled f n ≤ ENNReal.ofReal (-derivWithin f (Set.Ici 0) 0)

Uniform first-moment bound for the rescaled Chafaï measures.

theorem TauCeti.chafaiRescaled_prokhorov_mass_bound (f : ℝ → ℝ) (hcm : IsCompletelyMonotone f) : ∃ (L : ℝ) (C : NNReal), Filter.Tendsto f Filter.atTop (nhds L) ∧ 0 ≤ L ∧ ↑C = f 0 - L ∧ ∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (chafaiRescaled f n) ∧ (chafaiRescaled f n) Set.univ ≤ ↑C

Prokhorov-ready mass bound for the rescaled Chafaï measures: a completely monotone function supplies a nonnegative real mass constant C = f(0) - L, where L is the limit of f at infinity, such that every chafaiRescaled f n is finite and has total mass at most C.

Chafaï reconstruction and Bernstein-to-Laplace replacement

theorem TauCeti.chafaiRescaled_integral_bernsteinKernel_eq_sub_tendsto_atTop (f : ℝ → ℝ) (hcm : IsCompletelyMonotone f) (n : ℕ) (hn : 2 ≤ n) (x : ℝ) (hx : 0 ≤ x) (L : ℝ) (hL : Filter.Tendsto f Filter.atTop (nhds L)) : ∫ (p : NNReal), bernsteinKernel n x ↑p ∂chafaiRescaled f n = f x - L

Chafaï reconstruction identity for the nonconstant part.

theorem TauCeti.integral_bernsteinKernel_sub_laplaceKernel_tendsto_zero_of_mass_bound {C : ℝ} (σ : ℕ → MeasureTheory.Measure NNReal) (hmass : ∀ᶠ (n : ℕ) in Filter.atTop, (σ n) Set.univ ≤ ENNReal.ofReal C) (x : ℝ) (hx : 0 ≤ x) : Filter.Tendsto (fun (n : ℕ) => ∫ (p : NNReal), bernsteinKernel n x ↑p - Real.exp (-(x * ↑p)) ∂σ n) Filter.atTop (nhds 0)

Bernstein-to-Laplace replacement against a uniformly finite sequence of measures.

theorem TauCeti.chafaiRescaled_tendsto_laplace_integral_of_weak {f : ℝ → ℝ} {μ₀ : MeasureTheory.Measure NNReal} {l : Filter ℕ} (hweak : ∀ (g : BoundedContinuousFunction NNReal ℝ), Filter.Tendsto (fun (n : ℕ) => ∫ (p : NNReal), g p ∂chafaiRescaled f n) l (nhds (∫ (p : NNReal), g p ∂μ₀))) {x : ℝ} (hx : 0 ≤ x) : Filter.Tendsto (fun (n : ℕ) => ∫ (p : NNReal), Real.exp (-(x * ↑p)) ∂chafaiRescaled f n) l (nhds (∫ (p : NNReal), Real.exp (-(x * ↑p)) ∂μ₀))

Weak convergence of the rescaled Chafaï measures specializes to the Laplace kernel: if all bounded-continuous test integrals for chafaiRescaled f n converge to those for μ₀, then the integrals of p ↦ exp (-x * p) converge for every x ≥ 0.