/- Copyright (c) 2026 Michael R. Douglas. All rights reserved. Released under Apache 2.0 license. # Bernstein's Theorem — Basic definitions and properties `IsCompletelyMonotone` definition, basic CM properties (nonneg, bounded, deriv_nonpos, deriv_cm_sign, tendsto_atTop), set transfer lemmas, integral_neg_deriv, integral_mass. Split from `Bernstein.lean`. -/ import Mathlib.MeasureTheory.Integral.Bochner.Basic import Mathlib.MeasureTheory.Measure.Lebesgue.Basic import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus import Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts import Mathlib.Analysis.Calculus.IteratedDeriv.Defs import Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas import Mathlib.Analysis.Calculus.Taylor import Mathlib.MeasureTheory.Integral.IntegralEqImproper noncomputable section open MeasureTheory Set intervalIntegral Filter /-- A function `f : ℝ → ℝ` is completely monotone on `[0, ∞)` if it is C^∞ on `[0, ∞)` and `(-1)^n f^{(n)}(t) ≥ 0` for all `n ∈ ℕ, t ≥ 0`. This is Widder's definition ("The Laplace Transform", p. 145). It is equivalent to the forward-difference characterization `∑_{k=0}^n (-1)^k C(n,k) f(t+kh) ≥ 0`, but the smooth version avoids a ~500-line bootstrap from differences to derivatives in Lean. Examples: constants ≥ 0, `e^{-αt}` (α ≥ 0), `1/(t+α)^β` (α,β > 0). -/ def IsCompletelyMonotone (f : ℝ → ℝ) : Prop := ContDiffOn ℝ (↑(⊤ : ℕ∞)) f (Set.Ici 0) ∧ ∀ (n : ℕ) (t : ℝ), 0 ≤ t → 0 ≤ (-1 : ℝ) ^ n * iteratedDerivWithin n f (Set.Ici 0) t /-! ## Smoothness index helpers for `↑(⊤ : ℕ∞)` in `WithTop ℕ∞` -/ lemma coe_top_ne_zero : (↑(⊤ : ℕ∞) : WithTop ℕ∞) ≠ 0 := WithTop.coe_ne_zero.mpr (ENat.top_ne_zero) lemma nat_le_coe_top (n : ℕ) : (↑n : WithTop ℕ∞) ≤ ↑(⊤ : ℕ∞) := WithTop.coe_le_coe.mpr le_top lemma nat_lt_coe_top (n : ℕ) : (↑n : WithTop ℕ∞) < ↑(⊤ : ℕ∞) := WithTop.coe_lt_coe.mpr (WithTop.coe_lt_top n) /-! ## Basic properties of CM functions -/ /-- A CM function is nonneg (n=0 case). -/ lemma IsCompletelyMonotone.nonneg (hcm : IsCompletelyMonotone f) (t : ℝ) (ht : 0 ≤ t) : 0 ≤ f t := by simpa [iteratedDerivWithin_zero] using hcm.2 0 t ht /-- A CM function is non-increasing on [0, ∞) (n=1 case gives f' ≤ 0). -/ lemma IsCompletelyMonotone.deriv_nonpos (hcm : IsCompletelyMonotone f) (t : ℝ) (ht : 0 ≤ t) : iteratedDerivWithin 1 f (Set.Ici 0) t ≤ 0 := by have := hcm.2 1 t ht simp only [pow_one] at this linarith /-- A CM function is bounded by f(0) on [0, ∞). -/ lemma IsCompletelyMonotone.bounded (hcm : IsCompletelyMonotone f) (t : ℝ) (ht : 0 ≤ t) : f t ≤ f 0 := by have htop : (↑(⊤ : ℕ∞) : WithTop ℕ∞) ≠ 0 := coe_top_ne_zero have hanti : AntitoneOn f (Set.Ici 0) := antitoneOn_of_deriv_nonpos (convex_Ici 0) hcm.1.continuousOn ((hcm.1.differentiableOn htop).mono interior_subset) (fun x hx => by rw [interior_Ici] at hx have h1 := hcm.deriv_nonpos x (le_of_lt hx) rwa [iteratedDerivWithin_one, derivWithin_of_mem_nhds (Ici_mem_nhds hx)] at h1) exact hanti (Set.mem_Ici.mpr le_rfl) (Set.mem_Ici.mpr ht) ht /-- The sign condition for `-f'` being CM: `(-1)^n D^n(-f') = (-1)^{n+1} D^{n+1}f ≥ 0`. The smoothness part (ContDiffOn) is blocked on C^ω vs C^∞ mismatch in `WithTop ℕ∞` and is omitted since this lemma is not used downstream. -/ lemma IsCompletelyMonotone.deriv_cm_sign (hcm : IsCompletelyMonotone f) (n : ℕ) (t : ℝ) (ht : 0 ≤ t) : 0 ≤ (-1 : ℝ) ^ n * iteratedDerivWithin n (fun t => -iteratedDerivWithin 1 f (Set.Ici 0) t) (Set.Ici 0) t := by rw [iteratedDerivWithin_fun_neg, iteratedDerivWithin_one, ← iteratedDerivWithin_succ'] have := hcm.2 (n + 1) t ht simp only [pow_succ] at this ⊢ linarith /-- A CM function has a limit at infinity: it is antitone and bounded below by 0, so `f(t) → L ≥ 0` as `t → ∞`. -/ lemma IsCompletelyMonotone.tendsto_atTop (hcm : IsCompletelyMonotone f) : ∃ L, Filter.Tendsto f Filter.atTop (nhds L) ∧ 0 ≤ L := by have htop : (↑(⊤ : ℕ∞) : WithTop ℕ∞) ≠ 0 := coe_top_ne_zero have hanti : AntitoneOn f (Set.Ici 0) := antitoneOn_of_deriv_nonpos (convex_Ici 0) hcm.1.continuousOn ((hcm.1.differentiableOn htop).mono interior_subset) (fun x hx => by rw [interior_Ici] at hx have h1 := hcm.deriv_nonpos x (le_of_lt hx) rwa [iteratedDerivWithin_one, derivWithin_of_mem_nhds (Ici_mem_nhds hx)] at h1) set g := fun t : ℝ => f (max t 0) have hg_anti : Antitone g := fun a b hab => hanti (Set.mem_Ici.mpr (le_max_right _ _)) (Set.mem_Ici.mpr (le_max_right _ _)) (max_le_max_right 0 hab) have hg_bdd : BddBelow (Set.range g) := ⟨0, fun _ ⟨t, ht⟩ => ht ▸ hcm.nonneg _ (le_max_right _ _)⟩ refine ⟨⨅ i, g i, ?_, le_ciInf (fun t => hcm.nonneg _ (le_max_right _ _))⟩ exact (tendsto_atTop_ciInf hg_anti hg_bdd).congr' (Filter.eventually_atTop.mpr ⟨0, fun t ht => by simp [g, max_eq_left ht]⟩) /-! ## Set transfer for iterated derivatives -/ /-- `iteratedDerivWithin` on `Icc x T` agrees with `iteratedDerivWithin` on `Ici 0` at interior points, since both equal `iteratedDeriv n f t` when `0 < t`. -/ lemma iteratedDerivWithin_Icc_eq_Ici {n : ℕ} (hcm : IsCompletelyMonotone f) {x T t : ℝ} (hx : 0 ≤ x) (hxT : x < T) (ht : t ∈ Set.Ioo x T) : iteratedDerivWithin n f (Set.Icc x T) t = iteratedDerivWithin n f (Set.Ici 0) t := by have ht_pos : 0 < t := lt_of_le_of_lt hx ht.1 have hcda : ContDiffAt ℝ (↑n : WithTop ℕ∞) f t := (hcm.1.of_le (nat_le_coe_top _)).contDiffAt (Ici_mem_nhds ht_pos) rw [iteratedDerivWithin_eq_iteratedDeriv (uniqueDiffOn_Icc hxT) hcda (Set.Ioo_subset_Icc_self ht), ← iteratedDerivWithin_eq_iteratedDeriv (uniqueDiffOn_Ici 0) hcda (Set.mem_Ici.mpr (le_of_lt ht_pos))] /-- **CM sign condition for Taylor remainder**: For a CM function, the Taylor integral remainder `∫_x^T (T-t)^{n-1}/(n-1)! f^{(n)}(t) dt` has sign `(-1)^n`. This connects `taylor_integral_remainder` to the CM condition via `iteratedDerivWithin_Icc_eq_Ici` (set transfer at interior points) and `Ioo_ae_eq_Icc` (boundary is Lebesgue-null). Needs extra heartbeats for ae filter + iteratedDerivWithin reasoning. -/ lemma IsCompletelyMonotone.taylor_nonneg_remainder (hcm : IsCompletelyMonotone f) {x T : ℝ} {n : ℕ} (hx : 0 ≤ x) (hxT : x < T) : 0 ≤ (-1 : ℝ) ^ n * ∫ t in x..T, (↑(n - 1).factorial)⁻¹ * (T - t) ^ (n - 1) * iteratedDerivWithin n f (Set.Icc x T) t := by rw [← intervalIntegral.integral_const_mul] apply intervalIntegral.integral_nonneg_of_ae_restrict (le_of_lt hxT) have hIoo : ∀ t ∈ Set.Ioo x T, (0 : ℝ) ≤ ((-1 : ℝ) ^ n * ((↑(n - 1).factorial)⁻¹ * (T - t) ^ (n - 1) * iteratedDerivWithin n f (Set.Icc x T) t)) := fun t ht => calc (0 : ℝ) ≤ (↑(n - 1).factorial)⁻¹ * (T - t) ^ (n - 1) * ((-1 : ℝ) ^ n * iteratedDerivWithin n f (Set.Icc x T) t) := mul_nonneg (mul_nonneg (inv_nonneg.mpr (Nat.cast_nonneg _)) (pow_nonneg (sub_nonneg.mpr (le_of_lt ht.2)) _)) (by rw [iteratedDerivWithin_Icc_eq_Ici hcm hx hxT ht] exact hcm.2 n t (le_of_lt (lt_of_le_of_lt hx ht.1))) _ = _ := by ring have h_mem : ∀ᵐ t ∂volume.restrict (Set.Icc x T), t ∈ Set.Ioo x T := by rw [ae_restrict_iff' measurableSet_Icc] exact (Ioo_ae_eq_Icc (a := x) (b := T)).mono (fun t h ht => h.mpr ht) exact h_mem.mono fun t ht => by simp only [Pi.zero_apply]; exact hIoo t ht /-! ## Bernstein's Theorem -/ /-- For a CM function `f` on `[0,∞)`, the n=1 Taylor integral remainder gives `f(x) - f(T) = ∫_x^T (-f'(t)) dt`, where the integrand is nonneg by the CM condition. This shows `f` is the integral of its (nonneg) negative derivative. -/ lemma IsCompletelyMonotone.integral_neg_deriv (hcm : IsCompletelyMonotone f) (x T : ℝ) (hx : 0 ≤ x) (hxT : x < T) : f x - f T = ∫ t in x..T, -iteratedDerivWithin 1 f (Icc x T) t := by have hsubset : Icc x T ⊆ Set.Ici 0 := Icc_subset_Ici_self.trans (Set.Ici_subset_Ici.mpr hx) have hcm_Icc : ContDiffOn ℝ (↑(0 + 1) : WithTop ℕ∞) f (Icc x T) := (hcm.1.mono hsubset).of_le (nat_le_coe_top _) have hud : UniqueDiffOn ℝ (Icc x T) := uniqueDiffOn_Icc hxT have hf_cont : ContinuousOn f (Icc x T) := hcm_Icc.continuousOn have hf_diff : DifferentiableOn ℝ f (Icc x T) := hcm_Icc.differentiableOn (by norm_num : (↑(0 + 1) : WithTop ℕ∞) ≠ 0) -- iteratedDerivWithin 1 f (Icc x T) is continuous on Icc x T (from C^1) have hdw_cont : ContinuousOn (iteratedDerivWithin 1 f (Icc x T)) (Icc x T) := hcm_Icc.continuousOn_iteratedDerivWithin (show (1 : ℕ) ≤ (↑(0 + 1) : WithTop ℕ∞) by norm_num) hud -- Right derivative: for t ∈ Ioo x T, f has right derivative = iteratedDerivWithin 1 -- At interior points, Icc x T ∈ nhds t, so HasDerivWithinAt → HasDerivAt → HasDerivWithinAt Ioi have hderiv_right : ∀ t ∈ Ioo x T, HasDerivWithinAt f (iteratedDerivWithin 1 f (Icc x T) t) (Ioi t) t := by intro t ht rw [iteratedDerivWithin_one] exact ((hf_diff t (Ioo_subset_Icc_self ht)).hasDerivWithinAt.hasDerivAt (Icc_mem_nhds ht.1 ht.2)).hasDerivWithinAt -- Integrability: iteratedDerivWithin 1 is continuous on Icc, hence integrable have hint : IntervalIntegrable (iteratedDerivWithin 1 f (Icc x T)) volume x T := by rw [intervalIntegrable_iff_integrableOn_Icc_of_le hxT.le enorm_ne_top] exact hdw_cont.integrableOn_compact isCompact_Icc -- FTC (right derivative version): ∫_x^T f' = f(T) - f(x) have hFTC := intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le hxT.le hf_cont hderiv_right hint -- f(x) - f(T) = -∫_x^T f' = ∫_x^T (-f') rw [intervalIntegral.integral_neg] linarith [hFTC] /-- The integral of `-f'` on `[0, T]` equals `f(0) - f(T)` and is bounded by `f(0)`. -/ lemma IsCompletelyMonotone.integral_mass (hcm : IsCompletelyMonotone f) (T : ℝ) (hT : 0 < T) : ∫ t in (0 : ℝ)..T, -iteratedDerivWithin 1 f (Icc 0 T) t = f 0 - f T := by linarith [IsCompletelyMonotone.integral_neg_deriv hcm 0 T le_rfl hT] end