time_varying_comparison

The time-varying comparison bound, formalized — TARGET 2 of the LeanPunov stream

Seal

Rung rung-1 · Status interfaced — axiom-clean (#print axioms verbatim in The machine seal; build 2627 jobs), with the trajectory-regularity hypotheses hvc, hv, hbound, hnn as named applier-side interfaces — see interfaces.
Links: module index · interface ledger · related lyapunov_comparison, comparison_functions · sources panteley2001growth, panteley1998global, giordano2019coordinated, khalil1996nonlinear (no wiki page yet) · pin pin_comparison.py · lesson lesson_01_error_floor_cascade

Sealed theorems

comparison_shift

The restartable comparison — L2’s bound stated on the scalar $v$ with a movable start point $t_0$.

comparison_tendsto_zero

Vanishing disturbance: $\epsilon (t)\to 0$ drives the driven state to zero, $v(t)\to 0$ — the moving noise floor.

comparison_bounded

No finite escape: a bounded disturbance $\epsilon \le M$ keeps $v(t)\le v(0)+M/a$ for all time.

Why this theorem, and why now

L2 ((~/Code/vault/lean/lyapunov_comparison.md)) sealed the constant-disturbance comparison lemma: a differential inequality $\dot{v}\le -av+\epsilon$ with a fixed ceiling $\epsilon$ is bounded by the Grönwall envelope, and $v$ decays toward the ultimate bound $\epsilon /a$. That is the right first stone, but it does not close the cascade. In a cascaded interconnection the disturbance is not a constant — it is the state of the driving subsystem, and the whole point of a cascade argument is that this driving state decays. Panteley & Loría write the boundedness engine of their Lemma 2 (panteley2001growth eq 35) on exactly this shape,

$$\dot{v}\le -v+c(r)\Vert x_2(t)\Vert$$

where $x_2(t)$ is the driving state and the interconnection coefficient $c(r)$ is fixed on a ball of radius $r$. When the driving subsystem is asymptotically stable, $\Vert x_2(t)\Vert \to 0$, so the whole forcing term $\epsilon (t):=c(r)\Vert x_2(t)\Vert$ vanishes. The question this file answers is the quantitative heart of the cascade: does a vanishing disturbance drive the driven state to zero? The constant lemma cannot say — its floor $\epsilon /a$ is frozen. We need the time-varying statement.

The thesis link is direct. The operational cruise-lag floor $p_e\approx 0.107\mathrm{m}$ ((~/Code/notes/…) current_sota.md §4.5, eq 4.14) is the ultimate bound of a persistent disturbance. The risk-aware program that this stream underwrites needs the companion fact: if the excitation decays — as it does once a maneuver settles — the tracking error’s floor decays with it, to zero. comparison_tendsto_zero is that fact. Its sibling comparison_bounded is the safety complement: even a merely bounded (non-vanishing) disturbance cannot cause a finite escape — $v$ stays under the explicit ceiling $v(0)+M/a$.

Sources and provenance

• panteley2001growth (Panteley & Loría, Automatica 37, 2001): Lemma 2 and its eq 35 — the perturbed decrease driven by the interconnection term; the vanishing-disturbance regime is the $\Vert x_2(t)\Vert \to 0$ limit of that inequality.
• panteley1998global (Panteley & Loría, Syst. Control Lett. 33, 1998): the UGAS/cascade vocabulary.
• giordano2019coordinated (framing paper): eq 22 triangular decoupling — the cascade whose driven subsystem this bounds.
• Khalil, Nonlinear Systems: the terms comparison lemma, ultimate bound, and finite escape time (concepts cited by name; precise section numbers pending the queued Khalil OCR, flagged not fabricated).
• Mathlib substrate: Mathlib.Analysis.ODE.Gronwall (gronwallBound, gronwallBound_of_K_ne_0, le_gronwallBound_of_liminf_deriv_right_le — negative $K$ permitted), Real.tendsto_exp_comp_nhds_zero, tendsto_const_mul_atBot_of_neg, NormedAddGroup.tendsto_nhds_zero.
• SymPy pin of the variation-of-constants identity: (~/Code/vault/lean/pin_comparison.py) — six asserts, all passing.

The precise statements

All three declarations live in TimeVaryingComparison.lean beside this document, namespace Leanpunov, on scalar functions $v,v^{\prime },\epsilon :\mathbb{R}\to \mathbb{R}$.

Lemma (restartable comparison), comparison_shift. If $v$ is continuous on $[t_0,T]$, right-differentiable there with derivative $v^{\prime }$, and satisfies the constant-ceiling decrease $v^{\prime }(t)\le -av(t)+c$ on $[t_0,T)$, then for all $t\in [t_0,T]$

$$v(t)\le \text{gronwallBound}(v(t_0))(-a)c(t-t_0).$$

This is L2’s lyapunov_comparison stated directly on the scalar $v$ and with a movable start point $t_0$ — the one new capability the asymptotic proof needs (it restarts the clock at the moment $\epsilon$ falls below the ceiling).

Theorem (vanishing disturbance), comparison_tendsto_zero. Let $a>0$. If $v$ is continuous on $[0,\infty )$, right-differentiable with derivative $v^{\prime }$, nonnegative ($0\le v$), obeys $v^{\prime }(t)\le -av(t)+\epsilon (t)$, and the disturbance satisfies $\epsilon (t)\to 0$ as $t\to \infty$, then

$$v(t)⟶0(t\to \infty ).$$

Theorem (no finite escape), comparison_bounded. Let $a>0$ and $M\ge 0$. If $v$ is continuous and right-differentiable on $[0,\infty )$ with $v^{\prime }(t)\le -av(t)+\epsilon (t)$, the disturbance is bounded $\epsilon (t)\le M$, and $v(0)\ge 0$, then for every $t\ge 0$

$$v(t)\le v(0)+\frac{M}{a}.$$

The constant $M/a$ is the ultimate-bound / noise-floor level — the exact time-varying analogue of L2’s $\epsilon /a$.

Scratch work — where the two bounds come from

Everything rides on one object: the comparison-ODE solution $w(t)=\delta e^{-at}+\frac{c}{a}(1-e^{-at})$, the integrating-factor solution of $\dot{w}=-aw+c$, $w(0)=\delta$. Mathlib’s gronwallBound $\delta K\epsilon x=\delta e^{Kx}+\frac{\epsilon }{K}(e^{Kx}-1)$ is this $w$ at $K=-a$, $\epsilon =c$; the SymPy pin confirms gronwallBound $-$ $w$ $\equiv 0$ and that $w$ solves the ODE with $w(0)=\delta$.

Two elementary facts about $w$ carry the two theorems. Write $E:=e^{-as}\in (0,1]$ for $s\ge 0$.

1. Floor gap (asymptotics). The additive Grönwall term obeys $\frac{c}{-a}(E-1)=\frac{c}{a}(1-E)\le \frac{c}{a}$, because the deficit is $\frac{c}{a}-\frac{c}{-a}(E-1)=\frac{c}{a}E\ge 0$ (pin assert 5). So the whole bound sits under transient $+$ floor: $v\le v(t_0)E+c/a$. Choose the ceiling $c=a\delta /2$; then the floor is $c/a=\delta /2$, and the transient $v(t_0)E\to 0$. Eventually $v<\delta /2+\delta /2=\delta$ — for every $\delta$, hence $v\to 0$.

2. Boundedness gap (no escape). $(\delta +c/a)-w=\delta (1-E)+\frac{c}{a}E\ge 0$ (pin assert 6): with $\delta =v(0)\ge 0$ and $c=M$, every summand is nonnegative, so $w(s)\le v(0)+M/a$ for all $s$. Bounded ceiling, bounded state.

Proof narrative (teacher-verifiable)

comparison_shift. Identical machinery to L2: le_gronwallBound_of_liminf_deriv_right_le needs only a right lower-slope (Dini) condition, which HasDerivWithinAt.liminf_right_slope_le extracts from the supplied right-derivative, plus $v(t_0)\le v(t_0)$ (le_rfl). No chain rule is needed here because $v$ is already scalar — L2 had to push $V$ through the trajectory $x$; we take $v=V\circ x$ as the primitive object.

comparison_tendsto_zero. Fix a target $\delta >0$. Since $\epsilon \to 0$ and the ceiling $c=a\delta /2>0$, there is a time $T_0\ge 0$ past which $\epsilon (t)\le c$ (Iio_mem_nhds turns the convergence into an eventual bound; eventually_atTop extracts the threshold $T_0$). On $[T_0,\infty )$ the disturbance is dominated by the constant $c$, so comparison_shift applies with start point $T_0$: for $t\ge T_0$,

$$v(t)\le v(T_0)e^{-a(t-T_0)}+\frac{c}{a}(1-e^{-a(t-T_0)})\le v(T_0)e^{-a(t-T_0)}+\frac{c}{a}.$$

The transient $v(T_0)e^{-a(t-T_0)}\to 0$: the exponent $-a(t-T_0)\to -\infty$ (tendsto_const_mul_atBot_of_neg, since $-a<0$), so the exponential $\to 0$ (Real.tendsto_exp_comp_nhds_zero), and scaling by the constant $v(T_0)$ keeps the limit $0$. Because the floor $c/a=\delta /2<\delta$, eventually the transient drops below $\delta -c/a$, giving $v(t)<\delta$. Nonnegativity closes the squeeze: $\Vert v(t)\Vert =v(t)<\delta$. As $\delta$ was arbitrary, NormedAddGroup.tendsto_nhds_zero yields $v\to 0$. The three eventual facts (past $T_0$; transient below $\delta -c/a$; $t\ge 0$) are combined with filter_upwards; the final scalar chain is linarith.

comparison_bounded. Apply comparison_shift from $t_0=0$ with constant ceiling $M$ (valid since $\epsilon \le M$). Expand gronwallBound at $K=-a\ne 0$ and bound the two terms: $v(0)e^{-at}\le v(0)$ because $v(0)\ge 0$ and $e^{-at}\le 1$ (mul_le_of_le_one_right, Real.exp_le_one_iff), and the floor term is $\le M/a$ by the same gap identity as above. Sum: $v(t)\le v(0)+M/a$. No limit is taken — this is a uniform-in-$t$ ceiling, the finite-escape guard.

Why the Lean is honest about hypotheses. Mathlib’s total fderiv/derivative returns junk on non-differentiable inputs, so a decrease predicate could be vacuously true; every theorem here consumes an explicit HasDerivWithinAt witness for $v^{\prime }$, disarming that trap exactly as L2 did with Differentiable ℝ V.

Interfaces left named (not faked)

Per the stream’s “interface, don’t fake” rule, the trajectory-regularity hypotheses are named applier-side hypotheses, not silent sorries and not substituted weaker math:

• hvc (continuity of $v$ on the half-line) and hv (the pointwise right-derivative $v^{\prime }$) are the solution regularity an applier supplies from the actual closed-loop trajectory — the same role L4a’s IsSolutionTo precedent plays. Here $v=V\circ x$ is the Lyapunov value along a solution; its continuity and right-differentiability come from the chain rule on a differentiable $V$ and a solution $x$, which is upstream scaffolding, not this theorem’s content.
• hbound (the differential inequality itself) is the field-level Lyapunov decrease pulled back along the trajectory — the honest input, exactly the object Panteley–Loría assume.
• hnn (nonnegativity of $v$) is the energy/Lyapunov-function property; it is what lets the upper comparison bound close to a two-sided squeeze. Without it the theorem still proves $\mathrm{limsup}v\le 0$; with it (the operative case, $V\ge 0$) it upgrades to $v\to 0$.

Nothing in the content of the comparison bound — the Grönwall envelope, the exponential decay, the floor arithmetic — is hypothesized; only the trajectory’s existence and regularity, which is precisely the scaffolding the campaign permits as an interface.

Post-proof analysis

The moral. The constant lemma froze the floor at $\epsilon /a$; the time-varying lemma lets the floor move with the disturbance. The proof needed no new deep analysis — just the ability to restart Grönwall past the settling time (comparison_shift’s movable $t_0$) plus one exponential limit. That is the whole reason cascade arguments work: the driven subsystem inherits the driver’s decay through a shifted comparison, not through any global re-derivation.

Honest boundary. comparison_bounded is stated for a bounded disturbance $\epsilon \le M$, which is the operative regime here (a disturbance that tends to zero is eventually bounded, and continuous on compacts, hence bounded on $[0,\infty )$). The sharper classical statement — boundedness under a merely integrable disturbance, ${\int }_0^{\infty }\epsilon <\infty$ with $\epsilon$ possibly unbounded — is a different sufficient condition that would need the Bochner integral of the convolution ${\int }_0^t{e}^{-a(t-s)}\epsilon (s)ds$; it is deliberately left unformalized, flagged here as a named gap, not smuggled in. The bounded-$\epsilon$ result is the one the cascade actually uses.

The machine seal

lake build compiles green (full target, 2627 jobs). #print axioms for all three theorems:

'Leanpunov.comparison_shift'         depends on axioms: [propext, Classical.choice, Quot.sound]
'Leanpunov.comparison_tendsto_zero'  depends on axioms: [propext, Classical.choice, Quot.sound]
'Leanpunov.comparison_bounded'       depends on axioms: [propext, Classical.choice, Quot.sound]

No sorryAx, nothing beyond the three permitted axioms. The build copy lives at ~/lean/leanpunov/Leanpunov/TimeVaryingComparison.lean; this directory’s copy is the tracked source of truth, imported into Leanpunov.lean.