Inverting the integral of a positive continuous function

For a function continuous and positive on a compact real interval, its accumulated integral has a strictly increasing C¹ inverse on the interval from zero to the total integral. The inverse extends to a C¹ function on all of ℝ and has derivative the reciprocal of the original function on the integral's range. This supplies the real-calculus construction used in arc-length reparametrization.

Main results

• TauCeti.exists_contDiff_inverse_intervalIntegral: an inverse for the accumulated integral, with both inverse identities and its derivative.

theorem TauCeti.exists_orderIso_contDiff_inverse_intervalIntegral {w : ℝ → ℝ} (hw : Continuous w) {m : ℝ} (hm : 0 < m) (hwm : ∀ (t : ℝ), m ≤ w t) (a : ℝ) : ∃ (ψ : ℝ ≃o ℝ), ContDiff ℝ 1 ⇑ψ ∧ (∀ (t : ℝ), ψ (∫ (r : ℝ) in a..t, w r) = t) ∧ (∀ (s : ℝ), ∫ (r : ℝ) in a..ψ s, w r = s) ∧ ∀ (s : ℝ), HasDerivAt (⇑ψ) (w (ψ s))⁻¹ s

The accumulated integral of a continuous function bounded below by a positive constant is inverted by a C¹ order isomorphism of ℝ whose derivative is the reciprocal of the function at the inverse point.

theorem TauCeti.exists_contDiff_inverse_intervalIntegral {v : ℝ → ℝ} {a b : ℝ} (hab : a ≤ b) (hv : ContinuousOn v (Set.Icc a b)) (hpos : ∀ t ∈ Set.Icc a b, 0 < v t) : ∃ (ψ : ℝ → ℝ), StrictMono ψ ∧ ContDiff ℝ 1 ψ ∧ (∀ t ∈ Set.Icc a b, ψ (∫ (r : ℝ) in a..t, v r) = t) ∧ ∀ s ∈ Set.Icc 0 (∫ (r : ℝ) in a..b, v r), ψ s ∈ Set.Icc a b ∧ ∫ (r : ℝ) in a..ψ s, v r = s ∧ HasDerivAt ψ (v (ψ s))⁻¹ s

Accumulated speed t ↦ ∫ r in a..t, v r, for a speed v continuous and positive on [a, b], has an inverse ψ on [0, ∫ r in a..b, v r] which is the restriction of a strictly increasing C¹ function on ℝ, maps into [a, b], and has derivative the reciprocal speed.