Alphabeta MathHow statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
A Lipschitz ODE mode flow is stable to its initial state on a tube
Statement
Fix a mode and times . Suppose solve , both graphs stay in a convex tube on which is -Lipschitz in the state, uniformly in time, and both solutions have initial values at . Then
Facts & Assumptions
Given: Two mode solutions on in a common convex tube and the uniform state-Lipschitz constant .
Smooth hybrid ODE modes, guards, resets, and deterministic event priority: each mode trajectory solves its mode's first-order ODE.
A first-order initial value problem is equivalent to its Volterra integral equation: each solution equals its initial value plus the oriented integral of its vector field.
For and integrable when , ; for , is integrable: the norm of a vector integral is at most the integral of the norm.
Gronwall's integral inequality with variable and constant coefficients: if a continuous nonnegative satisfies , then .
Proof
If , then and the asserted estimate is equality. Hence assume , so [F2] applies on the nondegenerate interval . Subtract the two Volterra equations from [F2]. By [F3] and the state-Lipschitz hypothesis, satisfies .
Apply [F4] with to obtain , which is the asserted estimate.
Depends on
- Smooth hybrid ODE modes, guards, resets, and deterministic event priority
- A first-order initial value problem is equivalent to its Volterra integral equation
- For $a \le b$ and $f : [a,b] \to \mathbb{R}^m$ integrable when $a<b$, $\bigl\lVert\int_a^b f\bigr\rVert_2 \le \int_a^b \lVert f\rVert_2$; for $a<b$, $\lVert f\rVert_2$ is integrable
- Gronwall's integral inequality with variable and constant coefficients
Used by
- Event-driven integration for isolated frictionless spherical impacts Algorithm
- Certified dense-output and reference-guard enclosure data for hybrid events Definition
- Reset and smooth-mode flow propagate a transverse event-time error Lemma
- Finite separated transverse events give an event-aligned hybrid trajectory error bound Theorem
Dependency tree · two levels
40 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Gerald Teschl, Ordinary Differential Equations and Dynamical Systems, Chapter 2 (standard reference, not scraped)