diff --git a/TauCeti/Analysis/CompletelyMonotone/Bernstein/Measures.lean b/TauCeti/Analysis/CompletelyMonotone/Bernstein/Measures.lean
index 283d9f0cc..4171f73ce 100644
--- a/TauCeti/Analysis/CompletelyMonotone/Bernstein/Measures.lean
+++ b/TauCeti/Analysis/CompletelyMonotone/Bernstein/Measures.lean
@@ -1153,81 +1153,73 @@ private lemma ibp_kernel_integrableOn (f : ℝ → ℝ) (hcm : IsCompletelyMonot
       _ = (-1 : ℝ) ^ k / ↑(k - 1).factorial * t ^ (k - 1) *
           iteratedDerivWithin k f (Ici 0) t := by field_simp
 
+/-- Raising the sign exponent of the order-`k` kernel by one negates its integral. -/
+private lemma intervalIntegral_neg_one_pow_succ_kernel (f : ℝ → ℝ) (k : ℕ) (x T : ℝ) :
+    ∫ t in x..T, (-1 : ℝ) ^ (k + 1) / ↑(k - 1).factorial * (t - x) ^ (k - 1) *
+        iteratedDerivWithin k f (Ici 0) t =
+      -(∫ t in x..T, (-1 : ℝ) ^ k / ↑(k - 1).factorial * (t - x) ^ (k - 1) *
+        iteratedDerivWithin k f (Ici 0) t) := by
+  rw [← intervalIntegral.integral_neg]
+  refine intervalIntegral.integral_congr_ae (ae_of_all _ fun t _ => ?_)
+  rw [pow_succ (-1 : ℝ) k]
+  ring
+
+/-- For a completely monotone `f` with limit `L` at infinity, `0 ≤ x` and `k ≠ 0`, the order-`k`
+kernel identity implies the order-`k + 1` one: if the order-`k` kernel integrates against the
+`k`-th derivative to `f x - L` on `(x, ∞)`, then so does the order-`k + 1` kernel against the
+`(k + 1)`-st derivative. -/
+private lemma chafai_repeated_ibp_succ (f : ℝ → ℝ) (hcm : IsCompletelyMonotone f)
+    (k : ℕ) (hk : k ≠ 0) (x : ℝ) (hx : 0 ≤ x) (L : ℝ) (hL : Tendsto f atTop (nhds L))
+    (ih : ∫ t in Ioi x, (-1 : ℝ) ^ k / ↑(k - 1).factorial * (t - x) ^ (k - 1) *
+      iteratedDerivWithin k f (Ici 0) t = f x - L) :
+    ∫ t in Ioi x, (-1 : ℝ) ^ (k + 1) / ↑k.factorial * (t - x) ^ k *
+      iteratedDerivWithin (k + 1) f (Ici 0) t = f x - L := by
+  -- Integrate by parts on `[x, T]`; the boundary term decays, so `T → ∞` transfers `ih`.
+  have hk1 : 1 ≤ k := Nat.one_le_iff_ne_zero.mpr hk
+  have hintk := ibp_kernel_integrableOn f hcm k hk1 x hx L hL
+  have hintkp1 := ibp_kernel_integrableOn f hcm (k + 1) (by omega) x hx L hL
+  simp only [show k + 1 - 1 = k by omega] at hintkp1
+  have htend_k : Tendsto (fun T => ∫ t in x..T,
+      (-1 : ℝ) ^ k / ↑(k - 1).factorial * (t - x) ^ (k - 1) *
+      iteratedDerivWithin k f (Ici 0) t) atTop (nhds (f x - L)) := by
+    rw [← ih]
+    exact intervalIntegral_tendsto_integral_Ioi x hintk tendsto_id
+  have htend_sum : Tendsto (fun T =>
+      (-1 : ℝ) ^ (k + 1) / ↑k.factorial * (T - x) ^ k *
+        iteratedDerivWithin k f (Ici 0) T +
+      ∫ t in x..T, (-1 : ℝ) ^ k / ↑(k - 1).factorial * (t - x) ^ (k - 1) *
+        iteratedDerivWithin k f (Ici 0) t) atTop (nhds (f x - L)) := by
+    simpa [zero_add] using (boundary_term_decay f hcm k hk x hx L hL).add htend_k
+  have htend_via_ibp : Tendsto (fun T => ∫ t in x..T,
+      (-1 : ℝ) ^ (k + 1) / ↑k.factorial * (t - x) ^ k *
+      iteratedDerivWithin (k + 1) f (Ici 0) t) atTop (nhds (f x - L)) :=
+    Tendsto.congr' ((eventually_gt_atTop x).mono fun T hxT => by
+      have := ibp_finite_interval f hcm k hk x T hx hxT
+      linarith [intervalIntegral_neg_one_pow_succ_kernel f k x T]) htend_sum
+  exact tendsto_nhds_unique
+    ((intervalIntegral_tendsto_integral_Ioi x hintkp1 tendsto_id).congr
+      (fun T => by simp [id])) htend_via_ibp
+
+/-- **Repeated integration by parts for a completely monotone function.** For `n ≥ 1`, `0 ≤ x`
+and `f` tending to `L` at infinity, integrating the order-`n` kernel
+`(-1) ^ n / (n - 1)! * (t - x) ^ (n - 1)` against the `n`-th derivative of `f` over `(x, ∞)`
+recovers `f x - L`. This is the analytic identity behind the Chafaï reconstruction of `f` from
+its derivatives. -/
 private lemma chafai_repeated_ibp (f : ℝ → ℝ) (hcm : IsCompletelyMonotone f)
     (n : ℕ) (hn : 1 ≤ n) (x : ℝ) (hx : 0 ≤ x)
     (L : ℝ) (hL : Tendsto f atTop (nhds L)) :
     ∫ t in Ioi x, (-1 : ℝ) ^ n / ↑(n - 1).factorial *
       (t - x) ^ (n - 1) *
       iteratedDerivWithin n f (Ici 0) t = f x - L := by
-  -- Induction on `n`. Base case `n = 1`: the integral is `∫ -f'` on `(x, ∞)`, which equals
-  -- `f x - L` by the FTC and `f → L`. Inductive step: one integration by parts lowers the order
-  -- from `k+1` to `k`; the boundary term decays, and the interior term is the `k`-th case.
   induction n with
   | zero => omega
   | succ k ih =>
     by_cases hk : k = 0
-    · -- Base case `n = 1`: reduce to `∫ (x,∞) -f' = f x - L` via the fundamental theorem.
-      subst hk
-      have hsimpl :
-          (fun t => (-1 : ℝ) ^ (0 + 1) / ↑(0 + 1 - 1).factorial *
-            (t - x) ^ (0 + 1 - 1) *
-            iteratedDerivWithin (0 + 1) f (Ici 0) t) =
-          (fun t => -iteratedDerivWithin 1 f (Ici 0) t) := by
-        ext t
-        simp
-      rw [hsimpl]
-      have hintx : IntegrableOn (fun t => -iteratedDerivWithin 1 f (Ici 0) t) (Ioi x) :=
-        hcm.neg_iteratedDerivWithin_one_integrableOn.mono_set (Ioi_subset_Ioi hx)
-      refine tendsto_nhds_unique
-        (intervalIntegral_tendsto_integral_Ioi x hintx tendsto_id) ?_
-      simp only [id]
-      refine Tendsto.congr' ?_ (Tendsto.sub tendsto_const_nhds hL)
-      filter_upwards [eventually_gt_atTop (max x 1)] with T hT
-      have hxT : x < T := lt_of_le_of_lt (le_max_left x 1) hT
-      exact
-        (IsCompletelyMonotone.integral_neg_iteratedDerivWithin_one_Ici_eq_sub hcm hx hxT.le).symm
-    · -- Inductive step `n = k+1`: integrate by parts once and pass to the limit.
-      have hk1 : 1 ≤ k := Nat.one_le_iff_ne_zero.mpr hk
-      have ih_applied := ih hk1
+    · subst hk
+      simpa using hcm.integral_Ioi_neg_iteratedDerivWithin_one_of_nonneg hx hL
+    · have hk1 : 1 ≤ k := Nat.one_le_iff_ne_zero.mpr hk
       simp only [show k + 1 - 1 = k by omega]
-      have hintk := ibp_kernel_integrableOn f hcm k hk1 x hx L hL
-      have hintkp1 := ibp_kernel_integrableOn f hcm (k + 1) (by omega) x hx L hL
-      simp only [show k + 1 - 1 = k by omega] at hintkp1
-      have hibp := fun T (hT : x < T) => ibp_finite_interval f hcm k hk x T hx hT
-      have hbdry := boundary_term_decay f hcm k hk x hx L hL
-      have htend_k : Tendsto (fun T => ∫ t in x..T,
-          (-1 : ℝ) ^ k / ↑(k - 1).factorial * (t - x) ^ (k - 1) *
-          iteratedDerivWithin k f (Ici 0) t) atTop (nhds (f x - L)) := by
-        rw [← ih_applied]
-        exact intervalIntegral_tendsto_integral_Ioi x hintk tendsto_id
-      have hsign : ∀ T, ∫ t in x..T,
-          (-1 : ℝ) ^ (k + 1) / ↑(k - 1).factorial * (t - x) ^ (k - 1) *
-          iteratedDerivWithin k f (Ici 0) t =
-          -(∫ t in x..T, (-1 : ℝ) ^ k / ↑(k - 1).factorial * (t - x) ^ (k - 1) *
-          iteratedDerivWithin k f (Ici 0) t) := by
-        intro T
-        rw [← intervalIntegral.integral_neg]
-        apply intervalIntegral.integral_congr_ae
-        apply ae_of_all
-        intro t _
-        have : (-1 : ℝ) ^ (k + 1) = (-1) ^ k * (-1) := pow_succ (-1) k
-        rw [this]
-        ring
-      have htend_sum : Tendsto (fun T =>
-          (-1 : ℝ) ^ (k + 1) / ↑k.factorial * (T - x) ^ k *
-            iteratedDerivWithin k f (Ici 0) T +
-          ∫ t in x..T, (-1 : ℝ) ^ k / ↑(k - 1).factorial * (t - x) ^ (k - 1) *
-            iteratedDerivWithin k f (Ici 0) t) atTop (nhds (f x - L)) := by
-        simpa [zero_add] using hbdry.add htend_k
-      have htend_via_ibp : Tendsto (fun T => ∫ t in x..T,
-          (-1 : ℝ) ^ (k + 1) / ↑k.factorial * (t - x) ^ k *
-          iteratedDerivWithin (k + 1) f (Ici 0) t) atTop (nhds (f x - L)) :=
-        Tendsto.congr' ((eventually_gt_atTop x).mono fun T hxT => by
-          have := hibp T hxT
-          linarith [hsign T]) htend_sum
-      exact tendsto_nhds_unique
-        ((intervalIntegral_tendsto_integral_Ioi x hintkp1 tendsto_id).congr
-          (fun T => by simp [id])) htend_via_ibp
+      exact chafai_repeated_ibp_succ f hcm k hk x hx L hL (ih hk1)
 
 /-- **Chafaï reconstruction identity** for the nonconstant part. -/
 lemma chafaiRescaled_integral_bernsteinKernel_eq_sub_tendsto_atTop
diff --git a/TauCeti/Analysis/CompletelyMonotone/Integral.lean b/TauCeti/Analysis/CompletelyMonotone/Integral.lean
index 83247d4d3..c6f75abaf 100644
--- a/TauCeti/Analysis/CompletelyMonotone/Integral.lean
+++ b/TauCeti/Analysis/CompletelyMonotone/Integral.lean
@@ -28,6 +28,8 @@ for the first derivative within `[0, ∞)`.
 * `TauCeti.IsCompletelyMonotone.neg_iteratedDerivWithin_one_integrableOn`,
   `TauCeti.IsCompletelyMonotone.integral_Ioi_neg_iteratedDerivWithin_one`: integrability and the
   improper integral of `-f'` on `(0, ∞)`, represented as `iteratedDerivWithin 1`.
+* `TauCeti.IsCompletelyMonotone.integral_Ioi_neg_iteratedDerivWithin_one_of_nonneg`: the same
+  improper integral from an arbitrary nonnegative endpoint, `∫ₓ^∞ (-f') = f x - L`.
 
 ## References
 
@@ -142,22 +144,27 @@ lemma IsCompletelyMonotone.neg_iteratedDerivWithin_one_integrableOn
     fun t ht => hcm.iteratedDerivWithin_one_nonpos ht.le
   exact (integrableOn_Ioi_deriv_of_nonpos hcont hderiv hneg hL).neg
 
-/-- The improper integral `∫₀^∞ (-f') dt = f(0) - L` for completely monotone functions. -/
-lemma IsCompletelyMonotone.integral_Ioi_neg_iteratedDerivWithin_one
-    (hcm : IsCompletelyMonotone f) {L : ℝ} (hL : Tendsto f atTop (nhds L)) :
-    ∫ t in Ioi 0, -iteratedDerivWithin 1 f (Ici 0) t = f 0 - L := by
-  have hcont : ContinuousWithinAt f (Ici 0) 0 :=
-    hcm.contDiffOn.continuousOn.continuousWithinAt self_mem_Ici
-  have hderiv : ∀ t ∈ Ioi 0,
-      HasDerivAt f (iteratedDerivWithin 1 f (Ici 0) t) t := by
-    intro t ht
-    exact hcm.hasDerivAt_iteratedDerivWithin_succ 0 ht
-  have hneg : ∀ t ∈ Ioi 0, iteratedDerivWithin 1 f (Ici 0) t ≤ 0 :=
-    fun t ht => hcm.iteratedDerivWithin_one_nonpos ht.le
-  have hFTC :
-      ∫ t in Ioi 0, iteratedDerivWithin 1 f (Ici 0) t = L - f 0 :=
+/-- The improper integral `∫ₓ^∞ (-f') dt = f x - L` from an arbitrary nonnegative endpoint `x`,
+for a completely monotone function with limit `L` at infinity. -/
+lemma IsCompletelyMonotone.integral_Ioi_neg_iteratedDerivWithin_one_of_nonneg
+    (hcm : IsCompletelyMonotone f) {x : ℝ} (hx : 0 ≤ x) {L : ℝ}
+    (hL : Tendsto f atTop (nhds L)) :
+    ∫ t in Ioi x, -iteratedDerivWithin 1 f (Ici 0) t = f x - L := by
+  have hcont : ContinuousWithinAt f (Ici x) x :=
+    (hcm.contDiffOn.continuousOn.continuousWithinAt hx).mono (Ici_subset_Ici.mpr hx)
+  have hderiv : ∀ t ∈ Ioi x, HasDerivAt f (iteratedDerivWithin 1 f (Ici 0) t) t :=
+    fun t ht => hcm.hasDerivAt_iteratedDerivWithin_succ 0 (hx.trans_lt ht)
+  have hneg : ∀ t ∈ Ioi x, iteratedDerivWithin 1 f (Ici 0) t ≤ 0 :=
+    fun t ht => hcm.iteratedDerivWithin_one_nonpos (hx.trans ht.le)
+  have hFTC : ∫ t in Ioi x, iteratedDerivWithin 1 f (Ici 0) t = L - f x :=
     integral_Ioi_of_hasDerivAt_of_nonpos hcont hderiv hneg hL
   rw [MeasureTheory.integral_neg, hFTC]
   ring
 
+/-- The improper integral `∫₀^∞ (-f') dt = f(0) - L` for completely monotone functions. -/
+lemma IsCompletelyMonotone.integral_Ioi_neg_iteratedDerivWithin_one
+    (hcm : IsCompletelyMonotone f) {L : ℝ} (hL : Tendsto f atTop (nhds L)) :
+    ∫ t in Ioi 0, -iteratedDerivWithin 1 f (Ici 0) t = f 0 - L :=
+  hcm.integral_Ioi_neg_iteratedDerivWithin_one_of_nonneg le_rfl hL
+
 end TauCeti