Prove2Me

§3 (10) — λ˙=aλ2\dot\lambda=a\lambda^2, λ↑∞\lambda\uparrow\infty at TT, and ss is an increasing C1C^1 bijection [0,T)→[0,∞)[0,T)\to[0,\infty)

Proved
ChitourPrescribedTime.Linear.timeChange_properties

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

control-theoryp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1prescribed-time

Let T>0T>0 and let a:[0,T]→Ra:[0,T]\to\mathbb R be continuous and nonnegative with A(t)=∫tTa(ξ) dξ>0A(t)=\int_t^T a(\xi)\,d\xi>0 for all t∈[0,T)t\in[0,T). Put λ(t)=1/A(t)\lambda(t) = 1/A(t) and s(t)=∫0tλ(ξ) dξs(t)=\int_0^t\lambda(\xi)\,d\xi for 0≤t<T0\le t<T. Then:

  1. λ\lambda is differentiable on [0,T)[0,T) (one-sided at t=0t=0) with
λ˙(t)λ(t)2=a(t),t∈[0,T);\frac{\dot\lambda(t)}{\lambda(t)^2} = a(t), \qquad t\in[0,T);
  1. λ(t)>0\lambda(t)>0 for t∈[0,T)t\in[0,T);
  2. λ\lambda is nondecreasing on [0,T)[0,T);
  3. λ(t)→+∞\lambda(t)\to+\infty as t→T−t\to T^-;
  4. ss is C1C^1 on [0,T)[0,T) with s′(t)=λ(t)s'(t)=\lambda(t) (one-sided at 00);
  5. ss is strictly increasing on [0,T)[0,T);
  6. ss maps [0,T)[0,T) onto [0,∞)[0,\infty).

These facts make ss a legitimate new time: estimates proved on [0,∞)[0,\infty) in the variable ss transfer to the prescribed interval [0,T)[0,T).

Formalization Note The paper says "λ\lambda is increasing". Since λ˙=aλ2\dot\lambda = a\lambda^2 vanishes wherever aa does, strict increase is false in general (take a≡0a\equiv 0 on a subinterval), so item 3 states monotonicity (nondecreasing). Derivatives are taken within [0,T)[0,T), which gives the right derivative at t=0t=0 and the two-sided derivative at interior points.

Preamble
import Mathlib
import Definitions.Def_ChitourPrescribedTime_Linear_timeChange
Formal statement
namespace ChitourPrescribedTime.Linear

/-- §3, p. 1027, (10) and the sentence after it: for an admissible weight `a`, the parameter
`λ = 1/A` satisfies `λ̇ = a λ²` on `[0, T)`, is positive and nondecreasing on `[0, T)` and tends to
`+∞` as `t → T⁻`; the time `s(t) = ∫_0^t λ` is a strictly increasing `C¹` bijection from `[0, T)`
onto `[0, ∞)`. The page's "increasing" for `λ` is read as nondecreasing (`λ̇ = aλ²` vanishes
where `a` does). Derivatives are taken within `[0, T)` (one-sided at `t = 0`). -/
theorem timeChange_properties (T : ℝ) (a : ℝ → ℝ) (ha : AdmissibleWeight T a) :
    (∀ t ∈ Set.Ico 0 T, HasDerivWithinAt (lam T a) (a t * lam T a t ^ 2) (Set.Ico 0 T) t) ∧
    (∀ t ∈ Set.Ico 0 T, 0 < lam T a t) ∧
    MonotoneOn (lam T a) (Set.Ico 0 T) ∧
    Filter.Tendsto (lam T a) (nhdsWithin T (Set.Iio T)) Filter.atTop ∧
    (∀ t ∈ Set.Ico 0 T, HasDerivWithinAt (sTime T a) (lam T a t) (Set.Ico 0 T) t) ∧
    ContDiffOn ℝ 1 (sTime T a) (Set.Ico 0 T) ∧
    StrictMonoOn (sTime T a) (Set.Ico 0 T) ∧
    sTime T a '' Set.Ico 0 T = Set.Ici 0 := by sorry

end ChitourPrescribedTime.Linear
Source
Chitour, Ushirobira, Bouhemou, Stabilization for a Perturbed Chain of Integrators in Prescribed Time, SIAM J. Control Optim. 58 (2020), p. 1027, §3, eq. (10) and the sentence after it
Human review

  • Endorsed by Shuze Chen · Oct 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph