Solutions of a scalar linear equation

An absolutely continuous solution of f' = k • f almost everywhere on a compact real interval is the exponential solution with its prescribed initial value. No differentiability at every point, nor an integrability assumption on a separately supplied velocity, is needed. The product exp (-k * t) • f t has zero derivative almost everywhere, so the AC fundamental theorem of calculus makes this product constant on the entire interval.

For imaginary k, this identifies plane curves whose velocity is a fixed rotation and scaling of their position relative to a center. Such equations describe equality in the area–energy inequality for closed plane curves.

For a continuous, time-dependent real coefficient g, a differentiable solution of P' = g • P on an open interval J is P t = exp (∫ₛᵗ g) • P s for all s, t ∈ J (TauCeti.eq_exp_integral_smul_of_hasDerivAt_smul), by the integrating factor exp (-∫ₛᵘ g).

theorem AbsolutelyContinuousOnInterval.eq_exp_smul_of_ae_hasDerivAt_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℝ → E} {a b : ℝ} {k : ℂ} (hf : AbsolutelyContinuousOnInterval f a b) (hd : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → HasDerivAt f (k • f t) t) {t : ℝ} (ht : t ∈ Set.uIcc a b) : f t = Complex.exp (k * (↑t - ↑a)) • f a

An absolutely continuous solution of f' = k • f almost everywhere is the exponential solution, at every point of its parameter interval. The interval may have either orientation.

theorem AbsolutelyContinuousOnInterval.ae_hasDerivAt_smul_sub_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℝ → E} {a b : ℝ} (hf : AbsolutelyContinuousOnInterval f a b) (c : E) (k : ℂ) : (∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → HasDerivAt f (k • (f t - c)) t) ↔ ∃ (w : E), ∀ t ∈ Set.uIcc a b, f t = c + Complex.exp (k * ↑t) • w

An absolutely continuous curve has velocity k • (f - c) almost everywhere exactly when it is an exponential curve about c, with arbitrary amplitude in the complex normed space.

theorem TauCeti.eq_exp_integral_smul_of_hasDerivAt_smul {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {J : Set ℝ} (hJo : IsOpen J) (hJc : J.OrdConnected) {g : ℝ → ℝ} (hg : ContinuousOn g J) {P : ℝ → V} (hP : ∀ u ∈ J, HasDerivAt P (g u • P u) u) {s t : ℝ} (hs : s ∈ J) (ht : t ∈ J) : P t = Real.exp (∫ (u : ℝ) in s..t, g u) • P s

Integrating factor. On an open interval J, a solution of the linear equation P' = g • P with continuous real coefficient g satisfies P t = exp (∫ₛᵗ g) • P s for all s, t ∈ J.