The primitive of a function on the nonnegative half-line

Given f : ℝ → ℝ, this file constructs TauCeti.halfLinePrimitive f, the primitive t ↦ ∫₀ᵗ f of f on [0, ∞). To make the function total on ℝ, the integrand is composed with max · 0, so on [0, ∞) the value is the ordinary integral ∫₀ᵗ f and on (-∞, 0] it is the linear extension t ↦ t * f 0.

The construction is generic calculus: it depends only on Mathlib's fundamental theorem of calculus and knows nothing about complete monotonicity or Bernstein functions.

Main declarations

• TauCeti.halfLinePrimitive: the primitive ∫₀ᵗ f of f on the nonnegative half-line.
• TauCeti.halfLinePrimitive_def: the unconditional defining equation halfLinePrimitive f t = ∫₀ᵗ f (max x 0).
• TauCeti.halfLinePrimitive_eq_integral_of_nonneg, TauCeti.halfLinePrimitive_of_nonpos: the value of the primitive on each half-line.
• TauCeti.continuous_halfLinePrimitive: the primitive is continuous on all of ℝ whenever f is continuous on [0, ∞).
• TauCeti.hasDerivAt_halfLinePrimitive, TauCeti.deriv_halfLinePrimitive: its derivative is f at every nonnegative point.

noncomputable def TauCeti.halfLinePrimitive (f : ℝ → ℝ) (t : ℝ) : ℝ

The primitive of f on the nonnegative half-line. The max canonically extends the integrand to negative arguments; on [0, ∞) this is ∫₀ᵗ f.

Equations

• TauCeti.halfLinePrimitive f t = ∫ (x : ℝ) in 0..t, f (max x 0)

theorem TauCeti.halfLinePrimitive_def (f : ℝ → ℝ) (t : ℝ) : halfLinePrimitive f t = ∫ (x : ℝ) in 0..t, f (max x 0)

The unconditional defining equation of halfLinePrimitive, usable in downstream files where the body of the definition is not available.

theorem TauCeti.halfLinePrimitive_eq_integral_of_nonneg {f : ℝ → ℝ} {t : ℝ} (ht : 0 ≤ t) : halfLinePrimitive f t = ∫ (x : ℝ) in 0..t, f x

On the nonnegative half-line, halfLinePrimitive is the ordinary integral of f from zero.

theorem TauCeti.halfLinePrimitive_of_nonpos {f : ℝ → ℝ} {t : ℝ} (ht : t ≤ 0) : halfLinePrimitive f t = t * f 0

On the nonpositive half-line, halfLinePrimitive is the linear extension t ↦ t * f 0.

@[simp]

theorem TauCeti.halfLinePrimitive_zero (f : ℝ → ℝ) : halfLinePrimitive f 0 = 0

The value of halfLinePrimitive f at the origin is 0.

theorem TauCeti.continuous_halfLinePrimitive {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Ici 0)) : Continuous (halfLinePrimitive f)

If f is continuous on [0, ∞), then halfLinePrimitive f is continuous on all of ℝ; the max extension of the integrand makes the primitive continuous through the origin.

theorem TauCeti.hasDerivAt_halfLinePrimitive {f : ℝ → ℝ} {t : ℝ} (hf : ContinuousOn f (Set.Ici 0)) (ht : 0 ≤ t) : HasDerivAt (halfLinePrimitive f) (f t) t

If f is continuous on [0, ∞), then halfLinePrimitive f has derivative f t at every t ≥ 0. The max extension of the integrand makes the derivative at t = 0 two-sided.

theorem TauCeti.deriv_halfLinePrimitive {f : ℝ → ℝ} {t : ℝ} (hf : ContinuousOn f (Set.Ici 0)) (ht : 0 ≤ t) : deriv (halfLinePrimitive f) t = f t

If f is continuous on [0, ∞), then the derivative of halfLinePrimitive f is f at every t ≥ 0.