Pipeline-generated

How 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.

Cm Math Balances

1 · Prerequisites

2 · Summary

The finite-balance and continuation layer of the non-relativistic classical mechanics collection, all of it mathematics: the algebraic identities behind centre-of-mass and kinetic-energy splittings, momentum, angular-momentum and work-energy balances for finitely many labelled curves, the compact-continuation criterion for locally Lipschitz ordinary differential equations, and the distributional and algebraic machinery of an isolated impulse. Every item on this page carries domain: mathematics and depends only on mathematical suppliers; nothing here asserts that the adopted balances describe nature, and the physical reading of masses, forces, impulses and energies remains with the consuming classical-mechanics pages.

The differentiation layer is Differentiation of sums, scalar multiples, inner products, cross products and squared norms of differentiable curves in $R^{3}$ , which proves the sum, scalar-multiple, inner-product, cross-product and squared-norm rules for differentiable curves in $R^{3}$ . On it rest the balance identities: Centre of mass, the identity $\sum_{i} m_{i} ρ_{i} = 0$ , and the splitting of the kinetic sum $\sum_{i} m_{i} ∥ x_{i}^{'} ∥_{2}^{2}$ into centre-of-mass and relative parts (with the two-body reduced-mass case) introduces the centre of mass $X$ , proves $\sum_{i} m_{i} ρ_{i} = 0$ and the splitting $\sum_{i} m_{i} ∥ x_{i}^{'} ∥_{2}^{2} = M ∥ X^{'} ∥_{2}^{2} + \sum_{i} m_{i} ∥ ρ_{i}^{'} ∥_{2}^{2}$ , with the two-body reduced-mass identity $\sum_{i} m_{i} ∥ ρ_{i}^{'} ∥_{2}^{2} = μ ∥ r^{'} ∥_{2}^{2}$ ; Total momentum and total angular momentum balances for a finite system with antisymmetric pair forces; pairwise central forces make the internal torque vanish derives $P^{'} = \sum_{i} f_{i}$ and $J^{'} = \sum_{i} x_{i} \times f_{i} + \sum_{i < j} (x_{i} - x_{j}) \times f_{i j}$ from antisymmetric pair forces and shows that pairwise central forces kill the internal torque term; and Work-energy balance $\frac{d}{d t} (K + U (t, x (t))) = \partial_{t} U (t, x (t)) + \sum_{i} ⟨ d_{i} (t), x_{i}^{'} (t) ⟩$ for forces $m_{i} x_{i}^{''} = - \nabla_{x_{i}} U + d_{i}$ proves $\frac{d}{d t} (K + U (t, x (t))) = \partial_{t} U (t, x (t)) + \sum_{i} ⟨ d_{i}, x_{i}^{'} ⟩$ for forces $m_{i} x_{i}^{''} = - \nabla_{x_{i}} U + d_{i}$ , with the autonomous conserved case. The potential has a $C^{1}$ extension to an open time neighborhood; relative derivatives retain included endpoints of closed and half-open time intervals. The variable-mass material accounting is Variable-mass momentum balance: from $m^{'} = r_{i n} - r_{o u t}$ and $(m v)^{'} = F + r_{i n} w_{i n} - r_{o u t} w_{o u t}$ to $m v^{'} = F + r_{i n} (w_{i n} - v) - r_{o u t} (w_{o u t} - v)$ , whose two adopted balance identities imply $m v^{'} = F + r_{i n} (w_{i n} - v) - r_{o u t} (w_{o u t} - v)$ and exhibit why $(m v)^{'} = F$ alone is not the open-system law.

The continuation layer is the pair Compact continuation for locally Lipschitz ODEs: a solution whose graph stays in a compact subset of the domain near a finite endpoint extends past it and A non-extendable solution leaves every compact subset of the domain near its finite endpoint; an autonomous solution trapped in a compact subset of its state domain cannot break down there: a solution of $x^{'} = F (t, x)$ whose graph stays in a compact subset of the open domain near a finite endpoint $b$ extends past $b$ (and the autonomous trapped-state case is clause 2), while a non-extendable solution must leave every compact subset of the domain as the endpoint is approached. The criterion is about compact trapping, not about pointwise finiteness or boundedness of $F$ .

The impulse layer begins with The distributional derivative of a piecewise $C^{1}$ function with a jump: $(u_{p})^{'} = u_{p_{r e g}^{'}} + [p] δ_{t_{*}}$ , which computes the distributional derivative of a piecewise $C^{1}$ function with a jump, $(u_{p})^{'} = u_{p_{r e g}^{'}} + [p] δ_{t_{*}}$ , and declares the Axiom of Countable Choice used by the Lebesgue-integration suppliers it cites. On it rests Isolated reciprocal impulse with full-vector restitution: momentum jumps $\pm J$ , conservation of total momentum, the restitution solution and the kinetic-energy change $- \frac{1 - e^{2}}{2} μ ∥ v_{2}^{-} - v_{1}^{-} ∥_{2}^{2}$ : under the isolated reciprocal impulse model, the momentum jumps are $\pm J$ , total momentum is preserved, the restitution law determines the post-impulse velocities uniquely, and the kinetic-energy change is $- \frac{1 - e^{2}}{2} μ ∥ v_{2}^{-} - v_{1}^{-} ∥_{2}^{2}$ . The adopted impulse model is stated as a mathematical hypothesis about pairings against smooth test functions; no contact or restitution law is derived from smooth forces.

The companion page cm-math-balances-examples records explicit arithmetic checks of the impulse formulas, a rocket computation, and worked continuation boundary cases.

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

LemmaStatement: AI-adaptedProof: AI-adaptedOpen item page →

Differentiation of sums, scalar multiples, inner products, cross products and squared norms of differentiable curves in $R^{3}$

Statement

Let $I \subseteq R$ be an interval with at least two points (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length), let $t_{0} \in I$ , let $x, y : I \to R^{3}$ be differentiable at $t_{0}$ (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral) and let $λ : I \to R$ be differentiable at $t_{0}$ (The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set). Write $x^{'} (t_{0}), y^{'} (t_{0}) \in R^{3}$ for the derivatives, $⟨ \cdot, \cdot ⟩$ for the Euclidean inner product and $∥ \cdot ∥_{2}$ for the Euclidean norm (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ), and $\times$ for the cross product (The cross product in $R^{3}$ ). Then:

$x + y$ and $λ x$ are differentiable at $t_{0}$ , with $(x + y)^{'} (t_{0}) = x^{'} (t_{0}) + y^{'} (t_{0})$ and $(λ x)^{'} (t_{0}) = λ^{'} (t_{0}) x (t_{0}) + λ (t_{0}) x^{'} (t_{0})$ ;
$t \mapsto ⟨ x (t), y (t) ⟩$ is differentiable at $t_{0}$ , with derivative $⟨ x^{'} (t_{0}), y (t_{0}) ⟩ + ⟨ x (t_{0}), y^{'} (t_{0}) ⟩$ ;
$t \mapsto x (t) \times y (t)$ is differentiable at $t_{0}$ , with derivative $x^{'} (t_{0}) \times y (t_{0}) + x (t_{0}) \times y^{'} (t_{0})$ ;
$t \mapsto ∥ x (t) ∥_{2}^{2}$ is differentiable at $t_{0}$ , with derivative $2 ⟨ x^{'} (t_{0}), x (t_{0}) ⟩$ .

Facts & Assumptions

Given: An interval $I \subseteq R$ with at least two points, a point $t_{0} \in I$ , curves $x, y : I \to R^{3}$ and a function $λ : I \to R$ , with $x, y, λ$ differentiable at $t_{0}$ .

[L1]

A function $f : I \to R^{m}$ is differentiable at $t_{0}$ if and only if every component $f_{k}$ is differentiable at $t_{0}$ as a real function on $I$ , and then $f^{'} (t_{0})_{k} = f_{k}^{'} (t_{0})$ ; moreover sums and scalar multiples of differentiable curves are differentiable with $(f + g)^{'} (t_{0}) = f^{'} (t_{0}) + g^{'} (t_{0})$ and $(μ f)^{'} (t_{0}) = μ f^{'} (t_{0})$ for $μ \in R$ (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral).

[L2]

Sums, scalar multiples and products of real functions differentiable at $t_{0}$ are differentiable at $t_{0}$ with the sum, scalar-multiple and product rules (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ); the limit-point hypothesis of that theorem is part of the meaning of differentiability at $t_{0}$ (The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set, Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ).

[L3]

The Euclidean inner product and norm are $⟨ u, w ⟩ = \sum_{k < 3} u_{k} w_{k}$ and $∥ u ∥_{2} = \sqrt{⟨ u, u ⟩}$ ; the inner product is bilinear and symmetric (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , Laws of finite sums and finite products).

[L4]

For all $u, v \in R^{3}$ the cross product is bilinear-alternating: $(u, v) \mapsto u \times v$ is bilinear, $u \times u = 0$ , and $u \times v = - (v \times u)$ ; in coordinates $(u \times v)_{0} = u_{1} v_{2} - u_{2} v_{1}$ , $(u \times v)_{1} = u_{2} v_{0} - u_{0} v_{2}$ , $(u \times v)_{2} = u_{0} v_{1} - u_{1} v_{0}$ (The cross product in $R^{3}$ , The cross product is bilinear, alternating, and orthogonal to both factors).

Proof

technique · direct

1.1givenL1L2

By [L1] the components $x_{k}, y_{k} : I \to R$ are differentiable at $t_{0}$ with $x_{k}^{'} (t_{0}) = x^{'} (t_{0})_{k}$ and $y_{k}^{'} (t_{0}) = y^{'} (t_{0})_{k}$ , and by [L2] each of the functions $x_{k} + y_{k}$ , $λ x_{k}$ , $x_{k} y_{k}$ is differentiable at $t_{0}$ with the sum, scalar-multiple and product rules; this proves clause 1 componentwise, since $(x + y)_{k} = x_{k} + y_{k}$ and $(λ x)_{k} = λ x_{k}$ .

2.1step 1.1L2L3

The scalar function $t \mapsto ⟨ x (t), y (t) ⟩ = \sum_{k < 3} x_{k} (t) y_{k} (t)$ is a finite sum of products of functions differentiable at $t_{0}$ , hence by [L2] differentiable at $t_{0}$ with derivative $\sum_{k < 3} (x_{k}^{'} (t_{0}) y_{k} (t_{0}) + x_{k} (t_{0}) y_{k}^{'} (t_{0}))$ ; by [L3] this is $⟨ x^{'} (t_{0}), y (t_{0}) ⟩ + ⟨ x (t_{0}), y^{'} (t_{0}) ⟩$ , which is clause 2.

2.2step 1.1L1L2L4

Each component of $t \mapsto x (t) \times y (t)$ is, by [L4], one of the differences $x_{1} y_{2} - x_{2} y_{1}$ , $x_{2} y_{0} - x_{0} y_{2}$ , $x_{0} y_{1} - x_{1} y_{0}$ of products of functions differentiable at $t_{0}$ , so [L2] makes it differentiable at $t_{0}$ with derivative $(x_{1}^{'} y_{2} + x_{1} y_{2}^{'}) - (x_{2}^{'} y_{1} + x_{2} y_{1}^{'})$ , and by [L4] and bilinearity this is the corresponding component of $x^{'} (t_{0}) \times y (t_{0}) + x (t_{0}) \times y^{'} (t_{0})$ ; reassembling the three components with [L1] gives clause 3.

3.1step 2.1L3algebra∎

Applying clause 2 at $y : = x$ gives differentiability of $t \mapsto ⟨ x (t), x (t) ⟩ = ∥ x (t) ∥_{2}^{2}$ with derivative $⟨ x^{'} (t_{0}), x (t_{0}) ⟩ + ⟨ x (t_{0}), x^{'} (t_{0}) ⟩ = 2 ⟨ x^{'} (t_{0}), x (t_{0}) ⟩$ , the two terms being equal by symmetry of the inner product [L3]; this is clause 4.

TheoremStatement: AI-adaptedProof: AI-adaptedOpen item page →

Centre of mass, the identity $\sum_{i} m_{i} ρ_{i} = 0$ , and the splitting of the kinetic sum $\sum_{i} m_{i} ∥ x_{i}^{'} ∥_{2}^{2}$ into centre-of-mass and relative parts (with the two-body reduced-mass case)

Statement

Let $N \in N$ , $N \geq 1$ , let $I \subseteq R$ be an interval with at least two points (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length), let $m_{1}, \dots, m_{N} > 0$ and let $x_{i} : I \to R^{3}$ be differentiable at every point of $I$ (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral). All sums over $i$ range over $1, \dots, N$ : for a real family $a_{1}, \dots, a_{N}$ , define $\sum_{i} a_{i} : = \sum_{k < N} b_{k}$ , where $b : N \to R$ has $b_{k} = a_{k + 1}$ for $k < N$ and $b_{k} = 0$ for $k \geq N$ , using the finite sums of Laws of finite sums and finite products; vector sums are defined coordinatewise, and sums of curves pointwise. Put $M : = \sum_{i} m_{i} > 0$ , $X : = M^{- 1} \sum_{i} m_{i} x_{i}$ and $ρ_{i} : = x_{i} - X$ . The symbols $⟨ \cdot, \cdot ⟩$ and $∥ \cdot ∥_{2}$ denote the Euclidean inner product and norm on $R^{3}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ). Then:

$X$ and every $ρ_{i}$ are differentiable on $I$ , with $X^{'} = M^{- 1} \sum_{i} m_{i} x_{i}^{'}$ and $ρ_{i}^{'} = x_{i}^{'} - X^{'}$ , and the identities $\sum_{i} m_{i} ρ_{i} = 0$ and $\sum_{i} m_{i} ρ_{i}^{'} = 0$ hold on $I$ ;
for every $t \in I$ , $\sum_{i} m_{i} ∥ x_{i}^{'} (t) ∥_{2}^{2} = M ∥ X^{'} (t) ∥_{2}^{2} + \sum_{i} m_{i} ∥ ρ_{i}^{'} (t) ∥_{2}^{2};$
if $N = 2$ , then with $r : = x_{1} - x_{2}$ and $μ : = m_{1} m_{2} / M$ one has $\sum_{i} m_{i} ∥ ρ_{i}^{'} (t) ∥_{2}^{2} = μ ∥ r^{'} (t) ∥_{2}^{2}$ and hence $\sum_{i} m_{i} ∥ x_{i}^{'} (t) ∥_{2}^{2} = M ∥ X^{'} (t) ∥_{2}^{2} + μ ∥ r^{'} (t) ∥_{2}^{2}$ for every $t \in I$ .

Facts & Assumptions

Given: A natural $N \geq 1$ , an interval $I \subseteq R$ with at least two points, positive reals $m_{1}, \dots, m_{N}$ and curves $x_{i} : I \to R^{3}$ differentiable at every point of $I$ .

[L1]

If $f, g : I \to R^{m}$ are differentiable at $t$ and $μ \in R$ , then $f + g$ and $μ f$ are differentiable at $t$ with $(f + g)^{'} (t) = f^{'} (t) + g^{'} (t)$ and $(μ f)^{'} (t) = μ f^{'} (t)$ ; a vector-valued function is differentiable exactly when all its components are (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral).

[L2]

The Euclidean inner product is bilinear and symmetric, $⟨ u, w ⟩ = \sum_{k < 3} u_{k} w_{k}$ , and $∥ u ∥_{2}^{2} = ⟨ u, u ⟩$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[L3]

Under the statement's shifted indexing convention, additivity and scaling in Laws of finite sums and finite products clauses 1–2 give $\sum_{i} (α a_{i} + β b_{i}) = α \sum_{i} a_{i} + β \sum_{i} b_{i}$ for real families and, by applying those scalar laws to each coordinate, vector families. Clause 4 also gives $\sum_{i} a_{i} \geq a_{j}$ for every $1 \leq j \leq N$ when all $a_{i} \geq 0$ .

Proof

technique · direct

1.1givenL1L3

Since $N \geq 1$ and all masses are positive, [L3] gives $M \geq m_{1} > 0$ , so $M^{- 1}$ is defined. Each $x_{i}$ is differentiable on $I$ , so repeated application of [L1] makes the finite sum $\sum_{i} m_{i} x_{i}$ and its scalar multiple $X = M^{- 1} \sum_{i} m_{i} x_{i}$ differentiable on $I$ with $X^{'} = M^{- 1} \sum_{i} m_{i} x_{i}^{'}$ , and then every $ρ_{i} = x_{i} - X$ is differentiable on $I$ with $ρ_{i}^{'} = x_{i}^{'} - X^{'}$ .

2.1step 1.1L1L3algebra

Using the definition of $X$ and [L3], $\sum_{i} m_{i} ρ_{i} = \sum_{i} m_{i} x_{i} - M X = \sum_{i} m_{i} x_{i} - \sum_{i} m_{i} x_{i} = 0$ on $I$ ; differentiating this identity through the sum formula of step 1.1 gives $\sum_{i} m_{i} ρ_{i}^{'} = 0$ on $I$ .

3.1step 2.1L2L3algebra

For every $t \in I$ , substituting $x_{i}^{'} = X^{'} + ρ_{i}^{'}$ and expanding with bilinearity and symmetry [L2], $\sum_{i} m_{i} ∥ x_{i}^{'} ∥_{2}^{2} = \sum_{i} m_{i} (∥ X^{'} ∥_{2}^{2} + 2 ⟨ X^{'}, ρ_{i}^{'} ⟩ + ∥ ρ_{i}^{'} ∥_{2}^{2}) = M ∥ X^{'} ∥_{2}^{2} + 2 ⟨ X^{'}, \sum_{i} m_{i} ρ_{i}^{'} ⟩ + \sum_{i} m_{i} ∥ ρ_{i}^{'} ∥_{2}^{2},$ and the middle term vanishes by step 2.1; this is clause 2.

4.1step 3.1L1L2L3algebra∎

Let $N = 2$ . From the definitions, $X = \frac{m_{1} x_{1} + m_{2} x_{2}}{M}$ and $r = x_{1} - x_{2}$ , so $ρ_{1} = x_{1} - X = \frac{M x_{1} - m_{1} x_{1} - m_{2} x_{2}}{M} = \frac{m_{2}}{M} r$ and $ρ_{2} = x_{2} - X = \frac{M x_{2} - m_{1} x_{1} - m_{2} x_{2}}{M} = - \frac{m_{1}}{M} r$ ; differentiating by [L1] and expanding squared norms by [L2] gives $\sum_{i} m_{i} ∥ ρ_{i}^{'} ∥_{2}^{2} = (\frac{m_{1} m_{2}^{2} + m_{2} m_{1}^{2}}{M^{2}}) ∥ r^{'} ∥_{2}^{2} = \frac{m_{1} m_{2} (m_{1} + m_{2})}{M^{2}} ∥ r^{'} ∥_{2}^{2} = μ ∥ r^{'} ∥_{2}^{2}$ , because $M = m_{1} + m_{2}$ . Substitution into clause 2 gives clause 3.

TheoremStatement: AI-adaptedProof: AI-adaptedOpen item page →

Total momentum and total angular momentum balances for a finite system with antisymmetric pair forces; pairwise central forces make the internal torque vanish

Statement

Let $I \subseteq R$ be an interval with at least two points (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length), let $N \geq 1$ , let $m_{1}, \dots, m_{N} > 0$ , and let $x_{i} : I \to R^{3}$ be twice differentiable, i.e. differentiable with derivative $x_{i}^{'}$ differentiable (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral). Write $p_{i} : = m_{i} x_{i}^{'}$ and suppose there are maps $f_{i} : I \to R^{3}$ and, for every ordered pair $i \neq j$ in ${1, \dots, N}$ , maps $f_{i j} : I \to R^{3}$ such that

$f_{i j} (t) = - f_{j i} (t), p_{i}^{'} (t) = f_{i} (t) + \sum_{j \neq i} f_{i j} (t) (t \in I) .$

Write $P : = \sum_{i} p_{i}$ , $J : = \sum_{i} x_{i} \times p_{i}$ (cross product in $R^{3}$ , The cross product in $R^{3}$ ). Then:

$P$ is differentiable on $I$ with $P^{'} (t) = \sum_{i} f_{i} (t)$ for all $t \in I$ ;
$J$ is differentiable on $I$ with $J^{'} (t) = \sum_{i} x_{i} (t) \times f_{i} (t) + \sum_{i < j} (x_{i} (t) - x_{j} (t)) \times f_{i j} (t) (t \in I);$
if in addition, for every $i < j$ , $f_{i j}$ is parallel to $x_{i} - x_{j}$ — that is, there is a real function $λ_{i j}$ on $I$ with $f_{i j} = λ_{i j} (x_{i} - x_{j})$ — then $J^{'} (t) = \sum_{i} x_{i} (t) \times f_{i} (t)$ for all $t \in I$ .

Facts & Assumptions

Given: An interval $I \subseteq R$ with at least two points, $N \geq 1$ , positive reals $m_{1}, \dots, m_{N}$ , twice differentiable curves $x_{i} : I \to R^{3}$ , velocities $v_{i} : = x_{i}^{'}$ , momenta $p_{i} = m_{i} v_{i}$ , and maps $f_{i}, f_{i j}$ with $f_{i j} = - f_{j i}$ and $p_{i}^{'} = f_{i} + \sum_{j \neq i} f_{i j}$ on $I$ .

[L1]

Sums and scalar multiples of curves differentiable at $t$ are differentiable at $t$ with the expected derivatives (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral).

[L2]

Finite sums over finite sets may be reindexed along bijections and are additive over disjoint unions (Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule clauses 1 and 2); consequently, for vectors $a_{i j}$ indexed by the ordered pairs $(i, j)$ with $i \neq j$ , the set of such pairs is the disjoint union over the unordered pairs $i < j$ of the two-element sets ${(i, j), (j, i)}$ , so $\sum_{i} \sum_{j \neq i} a_{i j} = \sum_{i < j} (a_{i j} + a_{j i})$ . Scalar factors distribute over finite sums (Laws of finite sums and finite products).

[L3]

For differentiable curves $u, v : I \to R^{3}$ and $t \in I$ , the cross product $t \mapsto u (t) \times v (t)$ is differentiable at $t$ with derivative $u^{'} (t) \times v (t) + u (t) \times v^{'} (t)$ (Differentiation of sums, scalar multiples, inner products, cross products and squared norms of differentiable curves in $R^{3}$ ).

[L4]

The cross product is bilinear and alternating, so $u \times u = 0$ , $u \times v = - (v \times u)$ and $u \times (v + w) = u \times v + u \times w$ for $u, v, w \in R^{3}$ (The cross product in $R^{3}$ , The cross product is bilinear, alternating, and orthogonal to both factors).

Proof

technique · direct

1.1givenL1L2algebra

Since $P$ is the finite sum of the differentiable curves $p_{i}$ , [L1] gives $P^{'} = \sum_{i} p_{i}^{'}$ ; substituting the balance equation and using $f_{i j} = - f_{j i}$ with the reindexing rule [L2], $\sum_{i} \sum_{j \neq i} f_{i j} = \sum_{i < j} (f_{i j} + f_{j i}) = 0$ , so $P^{'} = \sum_{i} f_{i}$ ; this is clause 1.

2.1step 1.1givenL1L3

Each term $x_{i} \times p_{i}$ is differentiable on $I$ with derivative $x_{i}^{'} \times p_{i} + x_{i} \times p_{i}^{'}$ by [L3], and [L1] makes their finite sum $J$ differentiable with $J^{'} = \sum_{i} x_{i}^{'} \times p_{i} + \sum_{i} x_{i} \times p_{i}^{'} = \sum_{i} x_{i}^{'} \times p_{i} + \sum_{i} x_{i} \times f_{i} + \sum_{i} \sum_{j \neq i} x_{i} \times f_{i j} .$

3.1step 2.1L4algebra

The first sum in step 2.1 vanishes termwise: $x_{i}^{'} \times p_{i} = m_{i} x_{i}^{'} \times x_{i}^{'} = 0$ by alternation [L4].

4.1step 2.1step 3.1L2L4algebra

The double sum in step 2.1 equals $\sum_{i < j} (x_{i} \times f_{i j} + x_{j} \times f_{j i}) = \sum_{i < j} (x_{i} - x_{j}) \times f_{i j}$ : the first equality reindexes the ordered pairs by the unordered ones [L2], and the second uses $f_{j i} = - f_{i j}$ , bilinearity and $u \times (- w) = - (u \times w)$ [L4]. Combining with steps 2.1 and 3.1 gives clause 2.

5.1step 4.1givenL4algebra∎

Under the parallelism hypothesis, $(x_{i} - x_{j}) \times f_{i j} = λ_{i j} (x_{i} - x_{j}) \times (x_{i} - x_{j}) = 0$ for every $i < j$ by alternation [L4]; hence the double sum in clause 2 vanishes and $J^{'} = \sum_{i} x_{i} \times f_{i}$ , which is clause 3.

TheoremStatement: AI-adaptedProof: AI-adaptedOpen item page →

Work-energy balance $\frac{d}{d t} (K + U (t, x (t))) = \partial_{t} U (t, x (t)) + \sum_{i} ⟨ d_{i} (t), x_{i}^{'} (t) ⟩$ for forces $m_{i} x_{i}^{''} = - \nabla_{x_{i}} U + d_{i}$

Statement

Let $N \geq 1$ , let $I \subseteq R$ be an interval with at least two points (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length), let $Q \subseteq R^{3 N}$ be nonempty and open, and let $U : I \times Q \to R$ be the restriction of a function $\hat{U} : J \times Q \to R$ of class $C^{1}$ , where $J \subseteq R$ is an open interval containing $I$ ( $C^{k}$ Euclidean maps and diffeomorphisms). Write points of $Q$ as $q = (q_{1}, \dots, q_{N})$ with $q_{i} \in R^{3}$ ; for $t \in I$ , $q \in Q$ and each $i$ let $\nabla_{x_{i}} U (t, q) \in R^{3}$ be the gradient of $u \mapsto U (t, q_{1}, \dots, q_{i - 1}, u, q_{i + 1}, \dots, q_{N})$ at $u = q_{i}$ (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case), and let $\partial_{t} U$ and the spatial derivatives on $I \times Q$ denote the derivatives of $\hat{U}$ restricted there. At an included endpoint of $I$ , derivatives of curves are limits relative to $I$ (one-sided there); this preserves closed and half-open time intervals. Let $m_{1}, \dots, m_{N} > 0$ , let $x : I \to Q$ be twice differentiable (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral), put $K (t) : = \frac{1}{2} \sum_{i} m_{i} ∥ x_{i}^{'} (t) ∥_{2}^{2}$ (Euclidean norm, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ), let $d_{i} : I \to R^{3}$ be maps, and suppose

$m_{i} x_{i}^{''} (t) = - \nabla_{x_{i}} U (t, x (t)) + d_{i} (t) (t \in I, 1 \leq i \leq N) .$

Then:

$K$ is differentiable on $I$ with $K^{'} (t) = \sum_{i} ⟨ m_{i} x_{i}^{''} (t), x_{i}^{'} (t) ⟩$ ;
$t \mapsto U (t, x (t))$ is differentiable on $I$ with $\frac{d}{d t} U (t, x (t)) = \partial_{t} U (t, x (t)) + \sum_{i} ⟨ \nabla_{x_{i}} U (t, x (t)), x_{i}^{'} (t) ⟩;$
consequently $\frac{d}{d t} (K (t) + U (t, x (t))) = \partial_{t} U (t, x (t)) + \sum_{i} ⟨ d_{i} (t), x_{i}^{'} (t) ⟩ (t \in I);$ in particular, if $d_{i} \equiv 0$ for all $i$ then $\frac{d}{d t} (K + U (t, x (t))) = \partial_{t} U (t, x (t))$ , and if in addition $\partial_{t} U \equiv 0$ then $t \mapsto K (t) + U (t, x (t))$ is constant on $I$ .

Facts & Assumptions

Given: The data of the statement: $N \geq 1$ , an interval $I$ with at least two points, open $Q \subseteq R^{3 N}$ , a function $U : I \times Q \to R$ with the stated $C^{1}$ extension $\hat{U}$ to $J \times Q$ , positive masses $m_{i}$ , a twice differentiable $x : I \to Q$ , and maps $d_{i} : I \to R^{3}$ with $m_{i} x_{i}^{''} = - \nabla_{x_{i}} U (t, x (t)) + d_{i}$ on $I$ .

[L1]

For a differentiable curve $u : I \to R^{3}$ , the function $t \mapsto ∥ u (t) ∥_{2}^{2}$ is differentiable with derivative $2 ⟨ u^{'} (t), u (t) ⟩$ (Differentiation of sums, scalar multiples, inner products, cross products and squared norms of differentiable curves in $R^{3}$ , The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral); sums and scalar multiples of differentiable real functions are differentiable with the sum and scalar-multiple rules (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

[L2]

Total differentiability and the chain rule: if $g$ is totally differentiable at $a$ and $f$ at $g (a)$ , then $D (f \circ g) (a) = D f (g (a)) \circ D g (a)$ (The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder, The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ). A $C^{1}$ map is totally differentiable at every point, and its total derivative at $a$ is the linear map with matrix the Jacobian $J f (a)$ (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative, The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, $C^{k}$ Euclidean maps and diffeomorphisms).

[L3]

The total derivative computes directional derivatives: $D_{v} f (a) = D f (a) v$ (A total derivative computes every directional derivative, and its matrix is the Jacobian).

[L4]

The Euclidean inner product is bilinear and symmetric, $⟨ u, w ⟩ = \sum_{k < 3} u_{k} w_{k}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ), and finite sums are linear (Laws of finite sums and finite products).

[L5]

A differentiable real function with zero derivative on an interval is constant (A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant).

Proof

technique · direct

1.1givenL1L4algebra

Each $x_{i}^{'}$ is differentiable on $I$ because $x$ is twice differentiable, so [L1] gives differentiability of $t \mapsto ∥ x_{i}^{'} (t) ∥_{2}^{2}$ with derivative $2 ⟨ x_{i}^{''} (t), x_{i}^{'} (t) ⟩$ ; by the sum and scalar rules of [L1] and linearity of the finite sum [L4], $K$ is differentiable with $K^{'} = \frac{1}{2} \sum_{i} m_{i} \cdot 2 ⟨ x_{i}^{''}, x_{i}^{'} ⟩ = \sum_{i} ⟨ m_{i} x_{i}^{''}, x_{i}^{'} ⟩,$ which is clause 1.

1.2givenL2L3L4algebra

The curve $γ : I \to R \times Q$ , $γ (t) : = (t, x (t))$ , is differentiable (its components are the identity and the components of $x$ ; The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral), with $γ^{'} (t) = (1, x^{'} (t))$ under the identification $R \times R^{3 N} = R^{1 + 3 N}$ . Since $\hat{U}$ is $C^{1}$ on the open neighborhood $J \times Q$ of $γ (I)$ , [L2] gives the usual chain rule at interior points. At an included endpoint, $γ (t + h) = γ (t) + h γ^{'} (t) + o (h)$ as $h \to 0$ relative to $I$ , and total differentiability gives $\hat{U} (γ (t) + v) = \hat{U} (γ (t)) + D \hat{U} (γ (t)) v + o (∣ v ∣)$ . Substituting the first expansion into the second proves the same relative derivative there. Thus $(U \circ γ)^{'} (t) = D \hat{U} (γ (t)) γ^{'} (t)$ , and [L3] evaluates the right side as the matrix product of the Jacobian of $U$ at $γ (t)$ with $(1, x^{'} (t))$ , that is $\frac{d}{d t} U (t, x (t)) = \partial_{t} U (t, x (t)) + \sum_{i} \sum_{k < 3} \partial_{i, k} U (t, x (t)) x_{i, k}^{'} (t) = \partial_{t} U (t, x (t)) + \sum_{i} ⟨ \nabla_{x_{i}} U (t, x (t)), x_{i}^{'} (t) ⟩,$ the last step regrouping the coordinates of $Q$ into the $N$ blocks $R^{3}$ and using the coordinate formula for the inner product [L4]; this is clause 2.

2.1step 1.1step 1.2givenL4L5algebra∎

Adding the identities of clauses 1 and 2 and substituting $m_{i} x_{i}^{''} = - \nabla_{x_{i}} U (t, x (t)) + d_{i}$ , the two occurrences of $\sum_{i} ⟨ \nabla_{x_{i}} U (t, x (t)), x_{i}^{'} (t) ⟩$ cancel, leaving clause 3. If $d_{i} \equiv 0$ the derivative is $\partial_{t} U (t, x (t))$ , and if also $\partial_{t} U \equiv 0$ then the derivative of $K + U (t, x (t))$ vanishes identically on the interval $I$ , so that function is constant by [L5].

TheoremStatement: AI-adaptedProof: AI-adaptedOpen item page →

Variable-mass momentum balance: from $m^{'} = r_{i n} - r_{o u t}$ and $(m v)^{'} = F + r_{i n} w_{i n} - r_{o u t} w_{o u t}$ to $m v^{'} = F + r_{i n} (w_{i n} - v) - r_{o u t} (w_{o u t} - v)$

Statement

Let $I \subseteq R$ be an interval with nonempty interior (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length), let $m : I \to (0, \infty)$ and $v : I \to R^{3}$ be differentiable (The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral), and let $F : I \to R^{3}$ , $r_{i n}, r_{o u t} : I \to [0, \infty)$ and $w_{i n}, w_{o u t} : I \to R^{3}$ be maps. Suppose the two material balance identities

$m^{'} (t) = r_{i n} (t) - r_{o u t} (t), (m v)^{'} (t) = F (t) + r_{i n} (t) w_{i n} (t) - r_{o u t} (t) w_{o u t} (t)$

hold for every $t \in I$ , where $m v$ denotes the pointwise scalar multiple. Then

$m (t) v^{'} (t) = F (t) + r_{i n} (t) (w_{i n} (t) - v (t)) - r_{o u t} (t) (w_{o u t} (t) - v (t)) (t \in I) .$

In particular, if $F \equiv 0$ , $r_{i n} \equiv 0$ and $r_{o u t} \equiv r$ for a constant $r \geq 0$ , then $m v^{'} = - r (w_{o u t} - v)$ : the acceleration is governed by the momentum carried away per unit time relative to the body, not by $(m v)^{'} = 0$ .

The two balance identities are the adopted content of the material momentum accounting — the mathematical rendering of "gains $r_{i n} d t$ of matter with velocity $w_{i n}$ , loses $r_{o u t} d t$ with velocity $w_{o u t}$ , and feels the external force $F$ ". They are not derived here from any closed-system law; the deduction below is their product-rule consequence.

Facts & Assumptions

Given: An interval $I$ with nonempty interior, a differentiable positive real function $m$ and vector curve $v$ , maps $F, w_{i n}, w_{o u t}$ into $R^{3}$ , nonnegative functions $r_{i n}, r_{o u t}$ , and the two material balance identities on $I$ .

[L1]

A vector-valued curve $t \mapsto m v (t)$ is differentiable with $(m v)_{k}^{'} = (m v_{k})^{'}$ for each coordinate, and products of real differentiable functions obey the product rule $(f g)^{'} = f^{'} g + f g^{'}$ (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set).

Proof

technique · direct

1.1givenL1

By [L1] the product rule applies coordinatewise to $m v$ : $(m v)^{'} = m^{'} v + m v^{'}$ , since $(m v)_{k} = m v_{k}$ and $(m v_{k})^{'} = m^{'} v_{k} + m v_{k}^{'}$ for each coordinate $k$ .

2.1step 1.1givenL1algebra∎

Substituting the first balance identity into the second and using step 1.1, $m v^{'} = (m v)^{'} - m^{'} v = F + r_{i n} w_{i n} - r_{o u t} w_{o u t} - (r_{i n} - r_{o u t}) v = F + r_{i n} (w_{i n} - v) - r_{o u t} (w_{o u t} - v),$ the last step grouping the $r_{i n}$ -terms and the $r_{o u t}$ -terms and using bilinearity of scalar multiplication. This is the displayed conclusion; the special case $F \equiv 0$ , $r_{i n} \equiv 0$ , $r_{o u t} \equiv r$ is its immediate substitution, in that case the assumed momentum balance is $(m v)^{'} = - r w_{o u t}$ , so $(m v)^{'} = 0$ at a time $t$ exactly when $r w_{o u t} (t) = 0$ .

TheoremStatement: AI-adaptedProof: AI-adaptedOpen item page →

Compact continuation for locally Lipschitz ODEs: a solution whose graph stays in a compact subset of the domain near a finite endpoint extends past it

Statement

Let $n \geq 1$ , let $D \subseteq R \times R^{n}$ be open, and let $F : D \to R^{n}$ be continuous and locally Lipschitz in the state variable, locally uniformly in time, in the sense of Local Lipschitz continuity in the state variable, locally uniform in time and parameters. Let $t_{0} < b$ be reals, let $x_{0} \in R^{n}$ with $(t_{0}, x_{0}) \in D$ , and let $x : [t_{0}, b) \to R^{n}$ be a solution of the initial value problem

$x^{'} (t) = F (t, x (t)), x (t_{0}) = x_{0}$

on $[t_{0}, b)$ (First-order systems, initial value problems, and solutions on intervals). Suppose there is a compact set $K \subseteq D$ and a real $δ > 0$ such that

$(t, x (t)) \in K for every t \in (b - δ, b) \cap [t_{0}, b) .$

Then:

there is $ε > 0$ and a solution $\tilde{x} : [t_{0}, b + ε) \to R^{n}$ of the same initial value problem with $\tilde{x} (t) = x (t)$ for all $t \in [t_{0}, b)$ ; in particular $\tilde{x} (b) = \lim_{t ↑ b} x (t)$ exists and lies in the state projection of $K$ ;
if moreover $D = R \times U$ for an open $U \subseteq R^{n}$ and $F$ is autonomous, $F (t, z) = G (z)$ with $G : U \to R^{n}$ continuous and locally Lipschitz in the state variable (Local Lipschitz continuity in the state variable, locally uniform in time and parameters), and if there is a compact $K_{0} \subseteq U$ with $x (t) \in K_{0}$ for every $t \in (b - δ, b) \cap [t_{0}, b)$ , then the extension conclusion of clause 1 holds as well.

Facts & Assumptions

Given: The data of the statement: open $D \subseteq R \times R^{n}$ , a continuous $F$ that is locally Lipschitz in the state variable in the sense of [L2], a solution $x$ of the initial value problem on $[t_{0}, b)$ , and a compact $K \subseteq D$ with $(t, x (t)) \in K$ for all $t \in (b - δ, b) \cap [t_{0}, b)$ .

[L1]

At every point $(t_{*}, y_{*}) \in D$ , the initial value problem has a unique local solution on some interval around $t_{*}$ ; any two solutions through the same initial data agree on every common subinterval containing the initial time (Picard-Lindelöf local existence and uniqueness for first-order systems, First-order systems, initial value problems, and solutions on intervals).

[L2]

In the cylinder terminology of Local Lipschitz continuity in the state variable, locally uniform in time and parameters, this item uses $C = [a, c] \times \overline{B} (z, r) \subseteq D$ , where $a, c \in R$ , $a \leq c$ , $z \in R^{n}$ , $r > 0$ , and $\overline{B} (z, r) = {w \in R^{n} : ∥ w - z ∥_{2} \leq r}$ (Open ball, closed ball and sphere in a metric space). $F$ is locally Lipschitz in the state variable when every such cylinder carries a finite $L$ with $∥ F (t, u) - F (t, w) ∥_{2} \leq L ∥ u - w ∥_{2}$ for $(t, u), (t, w) \in C$ (Local Lipschitz continuity in the state variable, locally uniform in time and parameters).

[L3]

A curve solves the initial value problem on an interval exactly when it is continuous there, has graph in $D$ , and satisfies the Volterra equation $x (t) = x_{0} + \int_{t_{0}}^{t} F (s, x (s)) d s$ ; the oriented integral is additive over subintervals (A first-order initial value problem is equivalent to its Volterra integral equation, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ ).

[L4]

For $s < t$ and an integrable curve $g$ with values in $R^{n}$ one has $∥ \int_{s}^{t} g ∥_{2} \leq \int_{s}^{t} ∥ g ∥_{2}$ , and for a real integrable $u \leq M$ on $[s, t]$ one has $\int_{s}^{t} u \leq M (t - s)$ (For $a \leq b$ and $f : [a, b] \to R^{m}$ integrable when $a < b$ , $∥ \int_{a}^{b} f ∥_{2} \leq \int_{a}^{b} ∥ f ∥_{2}$ ; for $a < b$ , $∥ f ∥_{2}$ is integrable, If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ ).

[L5]

The Euclidean norm is a norm on $R^{n}$ , so it satisfies the triangle inequality $∥ u + w ∥_{2} \leq ∥ u ∥_{2} + ∥ w ∥_{2}$ (Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation) and the reverse triangle inequality $∣ ∥ u ∥_{2} - ∥ w ∥_{2} ∣ \leq ∥ u - w ∥_{2}$ (The reverse triangle inequality in a normed space); moreover $(R^{n}, d_{2})$ is complete: every Cauchy sequence in $R^{n}$ converges ( $R$ and $R^{n}$ for $n \geq 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $R$ , Complete metric space: every Cauchy sequence converges in the space, Vector-valued functions $f : A \to R^{m}$ , their limits and continuity, with the dictionary to the metric notions).

[L6]

A continuous real-valued function on a nonempty compact metric space is bounded and attains its bounds (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value); a compact subset of a metric space is closed (A compact subset of a metric space is closed and bounded), and closed means open complement (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Open ball, closed ball and sphere in a metric space).

[L7]

Continuity conventions: differentiability implies continuity, and vector-valued continuity is componentwise (A function differentiable at $c$ is continuous at $c$ , A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions, Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form). For every positive real $η$ there is a natural $k \geq 1$ with $1 / k < η$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

[L8]

A continuous real-valued function on a closed interval $[s, t]$ , $s < t$ , is integrable; hence a continuous curve into $R^{n}$ on $[s, t]$ is integrable componentwise (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral).

Proof

technique · direct

1.1givenL5L6L7

If $δ > b - t_{0}$ replace $δ$ by $b - t_{0}$ ; then the interval $(b - δ, b) \cap [t_{0}, b)$ is nonempty. Choose any $t$ in it; the hypothesis gives $(t, x (t)) \in K$ , so $K$ is nonempty. The norm function $z \mapsto ∥ F (z) ∥_{2}$ is continuous on the compact metric subspace $K$ : given $z_{0} \in K$ and $ε > 0$ , continuity of $F$ at $z_{0}$ [L7] gives $δ_{0} > 0$ with $∥ F (z) - F (z_{0}) ∥_{2} < ε$ whenever $d_{2} (z, z_{0}) < δ_{0}$ , and the reverse triangle inequality [L5] then gives $∣ ∥ F (z) ∥_{2} - ∥ F (z_{0}) ∥_{2} ∣ \leq ∥ F (z) - F (z_{0}) ∥_{2} < ε$ . Hence [L6] gives $M : = \max {∥ F (z) ∥_{2} : z \in K} < + \infty$ .

2.1step 1.1givenL3L4L7L8

For $s, t$ with $b - δ < s < t < b$ : since $x$ solves the initial value problem, [L3] gives $x (t) = x_{0} + \int_{t_{0}}^{t} F (u, x (u)) d u$ and $x (s) = x_{0} + \int_{t_{0}}^{s} F (u, x (u)) d u$ , hence $x (t) - x (s) = \int_{s}^{t} F (u, x (u)) d u$ ; the integrand is continuous in $u$ on $[s, t]$ because $u \mapsto F (u, x (u))$ is a composition of continuous maps (the components of $x$ are continuous by differentiability, [L7]) and $(u, x (u)) \in K$ on this interval, so its components are integrable on $[s, t]$ by [L8]. By [L4], $∥ x (t) - x (s) ∥_{2} \leq \int_{s}^{t} ∥ F (u, x (u)) ∥_{2} d u \leq M (t - s)$ .

3.1step 2.1L5L7algebra

The limit $x_{b} : = \lim_{t ↑ b} x (t)$ exists. Indeed, choose $k_{0} \geq 1$ with $1 / k_{0} < \min {δ, b - t_{0}}$ [L7] and put $y_{k} : = x (b - 1 / k)$ for $k \geq k_{0}$ ; by step 2.1, $∥ y_{k} - y_{l} ∥_{2} \leq M ∣ 1 / k - 1 / l ∣$ for all $k, l \geq k_{0}$ , so $(y_{k})$ is a Cauchy sequence in $R^{n}$ and converges, by [L5], to some $x_{b} \in R^{n}$ . Given $η > 0$ , choose $k \geq k_{0}$ with $1 / k < η / (4 (M + 1))$ and $∥ y_{k} - x_{b} ∥_{2} < η / 2$ ; then for every $t \in (\max {b - δ, b - η / (4 (M + 1))}, b)$ , step 2.1 gives $∥ x (t) - x_{b} ∥_{2} \leq ∥ x (t) - y_{k} ∥_{2} + ∥ y_{k} - x_{b} ∥_{2} \leq M (∣ t - b ∣ + 1 / k) + η / 2 < M \cdot η / (2 (M + 1)) + η / 2 < η$ . Hence $\lim_{t ↑ b} x (t) = x_{b}$ .

4.1step 3.1L6

The point $(b, x_{b})$ lies in $K$ , hence in $D$ : for $t \in (b - δ, b) \cap [t_{0}, b)$ the points $(t, x (t))$ lie in $K$ and converge to $(b, x_{b})$ as $t ↑ b$ (in the product metric, the first coordinate trivially and the second by step 3.1); since $K$ is closed [L6], its complement is open, so a point outside $K$ would have a ball around it disjoint from $K$ , which is impossible for $(b, x_{b})$ because every such ball contains some $(t, x (t))$ .

5.1step 2.1step 3.1step 4.1givenL3L4L6L8algebra

Extend $x$ to the continuous curve $\overset{ˉ}{x} : [t_{0}, b] \to R^{n}$ by $\overset{ˉ}{x} (t) : = x (t)$ for $t < b$ and $\overset{ˉ}{x} (b) : = x_{b}$ ; it is continuous by step 3.1. Let $0 < h_{0} < δ$ . For $s \in (b - h_{0}, b)$ and $t \in (s, b)$ , step 2.1 and additivity of the integral [L3] give $(x (t) - x (s)) - \int_{s}^{b} F (u, \overset{ˉ}{x} (u)) d u = - \int_{t}^{b} F (u, \overset{ˉ}{x} (u)) d u$ ; since $(u, \overset{ˉ}{x} (u)) \in K$ for every $u \in [s, b]$ (for $u < b$ by hypothesis, for $u = b$ by step 4.1), one has $∥ F (u, \overset{ˉ}{x} (u)) ∥_{2} \leq M$ there, and the norm inequality [L4] gives $∥ (x (t) - x (s)) - \int_{s}^{b} F (u, \overset{ˉ}{x} (u)) d u ∥_{2} \leq \int_{t}^{b} ∥ F (u, \overset{ˉ}{x} (u)) ∥_{2} d u \leq M (b - t) \to 0$ as $t ↑ b$ . With $x (t) \to x_{b}$ (step 3.1) this yields $x_{b} - x (s) = \int_{s}^{b} F (u, \overset{ˉ}{x} (u)) d u$ . Hence the left difference quotient satisfies $∥ \frac{\overset{ˉ}{x} (b) - \overset{ˉ}{x} (s)}{b - s} - F (b, x_{b}) ∥_{2} \leq \sup_{s \leq u \leq b} ∥ F (u, \overset{ˉ}{x} (u)) - F (b, x_{b}) ∥_{2} ⟶ 0 (s ↑ b)$ because for every $η > 0$ continuity of $\overset{ˉ}{x}$ at $b$ and of $F$ at $(b, x_{b})$ makes the displayed integrand smaller than $η$ for all $u \in [s, b]$ once $s$ is sufficiently close to $b$ ; [L6] ensures each supremum is finite. So $\overset{ˉ}{x}$ is differentiable at every point of $[b - h_{0}, b]$ as a function on that interval, with ${\overset{ˉ}{x}}^{'} (t) = F (t, \overset{ˉ}{x} (t))$ for $t < b$ and left derivative $F (b, x_{b})$ at $t = b$ ; it is therefore, for every such $h_{0}$ , a solution of the initial value problem $z^{'} = F (t, z)$ , $z (b) = x_{b}$ on $[b - h_{0}, b]$ in the sense of [L1] and [L3].

5.2step 4.1L1L2

Apply the local existence conclusion of Picard-Lindelöf [L1] at $(b, x_{b}) \in D$ , whose hypotheses on $F$ are the assumed continuity and local Lipschitz continuity in the state variable [L2]. It gives a solution through $(b, x_{b})$ on some interval around $b$ ; choose $h > 0$ so $[b - h, b + h]$ is contained in that interval and denote the restricted solution by $y$ . Then $y$ is a solution on $[b - h, b + h]$ through $(b, x_{b})$ .

6.1step 5.2step 5.1L1algebra

Let $h^{'} : = \min {h, δ / 2} > 0$ , where $h$ is the Picard-Lindelöf half-length of step 5.2; by step 5.1 the curve $\overset{ˉ}{x}$ is a solution on $[b - h^{'}, b]$ through $(b, x_{b})$ , and the restriction of $y$ is a solution on $[b - h, b] \supseteq [b - h^{'}, b]$ through the same point; by the uniqueness clause of [L1] they agree on $[b - h^{'}, b]$ . Define $\tilde{x} : [t_{0}, b + h) \to R^{n}$ by $\tilde{x} (t) : = \overset{ˉ}{x} (t)$ for $t \leq b$ and $\tilde{x} (t) : = y (t)$ for $b < t < b + h$ . Then $\tilde{x}$ is continuous, and it is differentiable with ${\tilde{x}}^{'} (t) = F (t, \tilde{x} (t))$ at every $t \in [t_{0}, b + h)$ : for $t < b$ and for $t > b$ this is the respective solution property, while at $t = b$ the left difference quotient tends to $F (b, x_{b})$ by step 5.1 and the right difference quotient is the two-sided derivative $y^{'} (b) = F (b, x_{b})$ of the solution $y$ ; the two agree, so the derivative of $\tilde{x}$ at $b$ exists and equals $F (b, x_{b}) = F (b, \tilde{x} (b))$ . With $ε : = h$ this is an extension as asserted in clause 1.

7.1step 1.1step 2.1step 3.1step 4.1step 5.2step 5.1step 6.1givenL6algebra∎

Under the hypotheses of clause 2, the argument of steps 1.1-6.1 applies with $K$ replaced by the given compact $K_{0} \subseteq U$ : the bound of step 1.1 is $M : = \max {∥ G (z) ∥_{2} : z \in K_{0}} < + \infty$ by [L6], the Lipschitz estimate of step 2.1 becomes $∥ x (t) - x (s) ∥_{2} \leq M (t - s)$ because $F (u, x (u)) = G (x (u))$ and $x (u) \in K_{0}$ for $u \in (b - δ, b) \cap [t_{0}, b)$ , the limit point of step 4.1 lies in $K_{0}$ since $K_{0}$ is compact hence closed [L6], and $(b, x_{b}) \in R \times U = D$ because $x_{b} \in K_{0} \subseteq U$ ; the local solution of step 5.2 and the gluing of step 6.1 are then carried out for the same field $F (t, z) = G (z)$ at $(b, x_{b})$ . This proves clause 2 with the same $ε = h$ .

CorollaryStatement: AI-adaptedProof: AI-adaptedOpen item page →

A non-extendable solution leaves every compact subset of the domain near its finite endpoint; an autonomous solution trapped in a compact subset of its state domain cannot break down there

Statement

Let $n \geq 1$ , let $D \subseteq R \times R^{n}$ be open, and let $F : D \to R^{n}$ be continuous and locally Lipschitz in the state variable in the sense of Local Lipschitz continuity in the state variable, locally uniform in time and parameters. Let $t_{0} < b$ be reals, let $x_{0} \in R^{n}$ with $(t_{0}, x_{0}) \in D$ , and let $x : [t_{0}, b) \to R^{n}$ be a solution of the initial value problem $x^{'} = F (t, x)$ , $x (t_{0}) = x_{0}$ (First-order systems, initial value problems, and solutions on intervals). Suppose $x$ admits no extension past $b$ : there do not exist $ε > 0$ and a solution $\tilde{x} : [t_{0}, b + ε) \to R^{n}$ of the same initial value problem with $\tilde{x} (t) = x (t)$ for every $t \in [t_{0}, b)$ . Then:

for every compact $K \subseteq D$ and every $η > 0$ there is $t \in (b - η, b) \cap [t_{0}, b)$ with $(t, x (t)) \notin K$ ; that is, the graph of $x$ leaves every compact subset of $D$ that could contain it arbitrarily close to $b$ ;
if $D = R \times U$ for an open $U \subseteq R^{n}$ , $F$ is autonomous, $F (t, z) = G (z)$ with $G : U \to R^{n}$ continuous and locally Lipschitz in the state variable, and there are a compact $K_{0} \subseteq U$ and $δ > 0$ with $x (t) \in K_{0}$ for all $t \in (b - δ, b) \cap [t_{0}, b)$ , then the no-extension hypothesis is false: $x$ does extend past $b$ .

Facts & Assumptions

Given: The data of the statement and the no-extension hypothesis on $x$ .

[L1]

Compact continuation: under the hypotheses of the statement without the no-extension hypothesis, if there are a compact $K \subseteq D$ and $δ > 0$ with $(t, x (t)) \in K$ for all $t \in (b - δ, b) \cap [t_{0}, b)$ , then $x$ extends past $b$ ; and the same holds for an autonomous field $F (t, z) = G (z)$ on $D = R \times U$ when $x (t) \in K_{0}$ for a compact $K_{0} \subseteq U$ and all $t \in (b - δ, b) \cap [t_{0}, b)$ (Compact continuation for locally Lipschitz ODEs: a solution whose graph stays in a compact subset of the domain near a finite endpoint extends past it).

Proof

technique · contrapositive

1.1givenL1

Clause 1 is the contrapositive of the compact continuation statement in [L1]: if for some compact $K \subseteq D$ and some $η > 0$ every $t \in (b - η, b) \cap [t_{0}, b)$ had $(t, x (t)) \in K$ , then [L1] would produce an extension of $x$ past $b$ , contradicting the no-extension hypothesis; hence for every compact $K \subseteq D$ and every $η > 0$ such a $t$ exists.

2.1step 1.1givenL1∎

Clause 2 likewise contradicts the no-extension hypothesis: the autonomy and trapping hypotheses are exactly those of the second part of [L1], which would give an extension of $x$ past $b$ ; therefore no such trapping compact set $K_{0}$ can exist under the no-extension hypothesis, and a fortiori every autonomous solution that is trapped in such a $K_{0}$ near $b$ does extend past $b$ .

LemmaStatement: AI-adaptedProof: AI-adaptedOpen item page →

The distributional derivative of a piecewise $C^{1}$ function with a jump: $(u_{p})^{'} = u_{p_{r e g}^{'}} + [p] δ_{t_{*}}$

Statement

Assume the Axiom of Countable Choice ( ${A C}_{ω}$ , The Axiom of Countable Choice ( ${A C}_{ω}$ )), used only through the Borel-measurability, Lebesgue-integration and distribution suppliers cited below. Let $I \subseteq R$ be an open interval (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length), let $t_{*} \in I$ , and let $p : I \to R$ satisfy:

$p$ is continuous on $I ∖ {t_{*}}$ and of class $C^{1}$ on each of the two open intervals $I \cap (- \infty, t_{*})$ and $I \cap (t_{*}, \infty)$ ;
the one-sided limits $p (t_{*}^{-}) : = \lim_{t ↑ t_{*}} p (t)$ , $p (t_{*}^{+}) : = \lim_{t ↓ t_{*}} p (t)$ and the one-sided limits of the derivative $p^{'} (t_{*}^{-}) : = \lim_{t ↑ t_{*}} p^{'} (t)$ , $p^{'} (t_{*}^{+}) : = \lim_{t ↓ t_{*}} p^{'} (t)$ all exist in $R$ .

Fix a value $p (t_{*}) \in R$ arbitrarily (for instance $p (t_{*}) : = 0$ ) and define $p_{r e g}^{'} : I \to R$ by $p_{r e g}^{'} (t) : = p^{'} (t)$ for $t \neq t_{*}$ and $p_{r e g}^{'} (t_{*}) : = 0$ . Put $[p] : = p (t_{*}^{+}) - p (t_{*}^{-})$ and let $u_{p}, u_{p_{r e g}^{'}} \in D^{'} (I)$ be the associated regular distributions (Regular distribution from a locally integrable function, A locally integrable function on $R^{n}$ ): $u_{p} (φ) = \int_{I} p (t) φ (t) d λ (t), u_{p_{r e g}^{'}} (φ) = \int_{I} p_{r e g}^{'} (t) φ (t) d λ (t) .$

Then $p$ and $p_{r e g}^{'}$ are locally integrable on $I$ , and

$(u_{p})^{'} = u_{p_{r e g}^{'}} + [p] δ_{t_{*}}$

in $D^{'} (I)$ (Distributional derivative, Dirac delta and its derivatives): that is, for every test function $φ \in D (I)$ ,

$- \int_{I} p (t) φ^{'} (t) d λ (t) = \int_{I} p_{r e g}^{'} (t) φ (t) d λ (t) + [p] φ (t_{*}) .$

Both integrals are over the Lebesgue measure $λ$ on $R$ , and the pairing convention of the two sides is complex-linear in $φ$ ; it therefore suffices that the identity hold for real-valued test functions.

Facts & Assumptions

Given: ${A C}_{ω}$ , an open interval $I$ , a point $t_{*} \in I$ , and a real function $p$ satisfying the piecewise- $C^{1}$ and one-sided-limit hypotheses above.

[L1]

The test space $D (I)$ consists of the compactly supported $C^{\infty}$ functions on $I$ ; for $φ \in D (I)$ the pairing of a distribution $u$ is written $⟨ u, φ ⟩$ , and $(u^{'}) (φ) = - u (φ^{'})$ ; the Dirac distribution satisfies $δ_{t_{*}} (φ) = φ (t_{*})$ ; $\int_{I}$ and $\int_{E}$ denote the Lebesgue integral, with $\int_{E} f d λ = \int f χ_{E} d λ$ ; a locally integrable $f$ defines the regular distribution $u_{f} (φ) = \int_{I} f φ d λ$ (Distribution, Distributional derivative, Dirac delta and its derivatives, Test function space d of an open set, Regular distribution from a locally integrable function, A locally integrable function on $R^{n}$ , Integral over a measurable subset).

[L2]

Complex Lebesgue integration by parts: for complex $C^{1}$ functions $u, v$ on a closed interval $[a, b]$ , $a < b$ , one has $\int_{a}^{b} u^{'} v = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u v^{'}$ and $\int_{a}^{b} u^{'} = u (b) - u (a)$ (Complex integration by parts on intervals and decaying lines).

[L3]

Functions agreeing almost everywhere have the same integral over every measurable set, and the Lebesgue integral is linear on $L^{1}$ (Two integrable functions are equal almost everywhere exactly when all of their indefinite integrals agree, The Lebesgue integral is linear on $L^{1} (μ)$ ); a bounded real function on a closed bounded interval that is continuous except at finitely many points is Riemann integrable, and a bounded Borel Riemann integrable function on a box is Lebesgue integrable with the same integral (A bounded function on $[a, b]$ that is continuous except at finitely many points is Riemann integrable, Riemann–Lebesgue comparison for distribution test integrands).

[L4]

A real function continuous on $[a, b]$ and differentiable on $(a, b)$ has $f (b) - f (a) = f^{'} (c) (b - a)$ for some $c \in (a, b)$ . (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ )

[L5]

A compact subset of the metric space $R$ is closed, hence Borel, and under ${A C}_{ω}$ every singleton in $R$ is Lebesgue-null (A compact subset of a metric space is closed and bounded, Every at most countable subset of $R^{n}$ is Lebesgue null; in particular $λ_{1} (Q) = 0$ ).

[L6]

For nonnegative measurable functions, pointwise order implies the same order of their Lebesgue integrals; with the integral-over-a-set convention, $E \subseteq F$ gives $\int_{E} h d λ \leq \int_{F} h d λ$ (Monotonicity and nonnegative homogeneity of the nonnegative integral, Integral over a measurable subset).

[L7]

A continuous real function on a nonempty compact metric space is bounded and attains its bounds (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

Proof

technique · direct

1.1givenL1L3L5L6L7

Local integrability: put $I_{-} : = I \cap (- \infty, t_{*})$ and $I_{+} : = I \cap (t_{*}, \infty)$ . Both are open, and $p$ and $p_{r e g}^{'}$ are continuous on each. For any open $O \subseteq R$ , the preimage on either half is open relative to that open half, hence open in $R$ ; the preimage at $t_{*}$ is either empty or ${t_{*}}$ . Thus both functions are Borel on $I$ . Let $K \subseteq I$ be compact. If $K = \emptyset$ , its integral is zero. Otherwise choose $c < t_{*} < d$ with $K \cup {t_{*}} \subset (c, d)$ and $[c, d] \subset I$ . Extending each one-sided reading of $p$ and $p_{r e g}^{'}$ to $t_{*}$ by its finite one-sided limit gives continuous functions on $[c, t_{*}]$ and $[t_{*}, d]$ ; [L7] bounds them there, and the fixed finite values at $t_{*}$ preserve boundedness. Hence $p$ and $p_{r e g}^{'}$ are bounded on $[c, d]$ , and their absolute values are Borel and continuous except possibly at $t_{*}$ . By [L3] they are Riemann integrable and Lebesgue integrable on $[c, d]$ . The set $K$ is Borel by [L5], and [L6] gives $\int_{K} ∣ p ∣ d λ \leq \int_{[c, d]} ∣ p ∣ d λ < \infty$ and $\int_{K} ∣ p_{r e g}^{'} ∣ d λ \leq \int_{[c, d]} ∣ p_{r e g}^{'} ∣ d λ < \infty$ . Thus both functions are locally integrable and define the regular distributions in [L1].

1.2givenL1L2L3L5algebra

Let $φ \in D (I)$ be real-valued. Choose $a < t_{*} < b$ with $supp φ \cup {t_{*}} \subset (a, b)$ and $[a, b] \subset I$ ; compactness of the support and openness of $I$ allow this, without requiring a symmetric interval around $t_{*}$ . Since $φ$ vanishes outside $[a, b]$ , [L1] and [L3] give $\int_{I} p φ^{'} d λ = \int_{[a, b]} p φ^{'} d λ = \int_{[a, t_{*}]} p φ^{'} d λ + \int_{[t_{*}, b]} p φ^{'} d λ,$ the second equality splitting the integral over the two overlapping half-intervals by linearity and the identity $χ_{[a, b]} = χ_{[a, t_{*}]} + χ_{[t_{*}, b]} - χ_{{t_{*}}}$ (the subtracted term contributes $0$ because the singleton ${t_{*}}$ has measure zero).

2.1step 1.2givenL2L3L4L5algebra

On the left half-interval define ${\overset{ˉ}{p}}_{-} (t) : = p (t)$ for $t < t_{*}$ and ${\overset{ˉ}{p}}_{-} (t_{*}) : = p (t_{*}^{-})$ ; on $[a, t_{*}]$ this extension is continuous. For $t < t_{*}$ , the mean value theorem [L4] on $[t, t_{*}]$ gives $({\overset{ˉ}{p}}_{-} (t_{*}) - {\overset{ˉ}{p}}_{-} (t)) / (t_{*} - t) = p^{'} (ξ_{t})$ for some $t < ξ_{t} < t_{*}$ . As $t ↑ t_{*}$ this tends to $p^{'} (t_{*}^{-})$ , proving the endpoint derivative. Its derivative is continuous up to $t_{*}$ ; extend beyond $t_{*}$ by the affine function $p (t_{*}^{-}) + p^{'} (t_{*}^{-}) (t - t_{*})$ to obtain a $C^{1}$ function on an open neighborhood of $[a, t_{*}]$ . On $[a, t_{*}]$ , $p$ and ${\overset{ˉ}{p}}_{-}$ agree except at $t_{*}$ , so [L3] and [L5] give $\int_{[a, t_{*}]} p φ^{'} d λ = \int_{a}^{t_{*}} {\overset{ˉ}{p}}_{-} φ^{'} d λ$ . Lebesgue integration by parts [L2] for the $C^{1}$ pair $({\overset{ˉ}{p}}_{-}, φ)$ gives $\int_{a}^{t_{*}} {\overset{ˉ}{p}}_{-} φ^{'} = {\overset{ˉ}{p}}_{-} (t_{*}) φ (t_{*}) - {\overset{ˉ}{p}}_{-} (a) φ (a) - \int_{a}^{t_{*}} {\overset{ˉ}{p}}_{-}^{'} φ = p (t_{*}^{-}) φ (t_{*}) - \int_{[a, t_{*}]} p_{r e g}^{'} φ d λ,$ because $φ (a) = 0$ and ${\overset{ˉ}{p}}_{-}^{'} = p_{r e g}^{'}$ on $(a, t_{*})$ ; the last integrals agree by [L3] and [L5].

2.2step 1.2givenL2L3L4L5algebra

On the right half-interval define ${\overset{ˉ}{p}}_{+} (t) : = p (t)$ for $t > t_{*}$ and ${\overset{ˉ}{p}}_{+} (t_{*}) : = p (t_{*}^{+})$ . The mean value theorem [L4] on $[t_{*}, t]$ shows that the right derivative of ${\overset{ˉ}{p}}_{+}$ at $t_{*}$ is $p^{'} (t_{*}^{+})$ ; extending affinely to the left gives a $C^{1}$ function on a neighborhood of $[t_{*}, b]$ . Since $p$ and ${\overset{ˉ}{p}}_{+}$ , and $p_{r e g}^{'}$ and ${\overset{ˉ}{p}}_{+}^{'}$ , agree except at $t_{*}$ , [L3] and [L5] give equality of their integrals against the tests on $[t_{*}, b]$ . Integration by parts [L2], together with $φ (b) = 0$ , now gives $\int_{[t_{*}, b]} p φ^{'} d λ = \int_{t_{*}}^{b} {\overset{ˉ}{p}}_{+} φ^{'} d λ = {\overset{ˉ}{p}}_{+} (b) φ (b) - {\overset{ˉ}{p}}_{+} (t_{*}) φ (t_{*}) - \int_{t_{*}}^{b} {\overset{ˉ}{p}}_{+}^{'} φ = - p (t_{*}^{+}) φ (t_{*}) - \int_{[t_{*}, b]} p_{r e g}^{'} φ d λ .$

3.1step 2.1step 2.2L1L3algebra∎

Adding the two identities of steps 2.1 and 2.2 and substituting into step 1.2 gives $\int_{I} p φ^{'} d λ = - (p (t_{*}^{+}) - p (t_{*}^{-})) φ (t_{*}) - \int_{I} p_{r e g}^{'} φ d λ = - [p] φ (t_{*}) - \int_{I} p_{r e g}^{'} φ d λ,$ that is, $⟨ (u_{p})^{'}, φ ⟩ = - \int_{I} p φ^{'} d λ = \int_{I} p_{r e g}^{'} φ d λ + [p] φ (t_{*}) = ⟨ u_{p_{r e g}^{'}} + [p] δ_{t_{*}}, φ ⟩$ for every real-valued $φ \in D (I)$ by [L1]. Since both sides are complex-linear in $φ$ , the identity extends to all $φ \in D (I)$ by applying it to $Re φ$ and $Im φ$ ; hence $(u_{p})^{'} = u_{p_{r e g}^{'}} + [p] δ_{t_{*}}$ in $D^{'} (I)$ .

TheoremStatement: AI-adaptedProof: AI-adaptedOpen item page →

Isolated reciprocal impulse with full-vector restitution: momentum jumps $\pm J$ , conservation of total momentum, the restitution solution and the kinetic-energy change $- \frac{1 - e^{2}}{2} μ ∥ v_{2}^{-} - v_{1}^{-} ∥_{2}^{2}$

Statement

Assume the Axiom of Countable Choice ( ${A C}_{ω}$ , The Axiom of Countable Choice ( ${A C}_{ω}$ )), inherited from the jump lemma below. Let $I \subseteq R$ be an open interval with at least two points (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length), let $t_{*} \in I$ , let $m_{1}, m_{2} > 0$ , and let $x_{1}, x_{2} : I \to R^{3}$ be continuous on $I$ and twice continuously differentiable on each of the two open intervals $I \cap (- \infty, t_{*})$ and $I \cap (t_{*}, \infty)$ (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, $C^{k}$ Euclidean maps and diffeomorphisms). Assume the one-sided limits $v_{i}^{-} : = \lim_{t ↑ t_{*}} x_{i}^{'} (t), v_{i}^{+} : = \lim_{t ↓ t_{*}} x_{i}^{'} (t) (i = 1, 2)$ exist in $R^{3}$ . Define $p_{i} : I \to R^{3}$ by $p_{i} (t) : = m_{i} x_{i}^{'} (t)$ for $t \neq t_{*}$ and fix the representative value $p_{i} (t_{*}) : = 0$ (Vector-valued functions $f : A \to R^{m}$ , their limits and continuity, with the dictionary to the metric notions). Let $F_{1}, F_{2} : I \to R^{3}$ be continuous and let $J \in R^{3}$ . The isolated reciprocal impulse model at $t_{*}$ consists of the two requirements:

regular dynamics off the impulse: $m_{i} x_{i}^{''} (t) = F_{i} (t)$ for every $t \in I ∖ {t_{*}}$ and $i = 1, 2$ ;
impulse pairing: for every $Φ \in C_{c}^{\infty} (I; R^{3})$ — meaning every map whose three components lie in $C_{c}^{\infty} (I)$ (Test function space d of an open set, $C^{k}$ Euclidean maps and diffeomorphisms) — $- \int_{I} ⟨ p_{1} (t), Φ^{'} (t) ⟩ d λ (t) = \int_{I} ⟨ F_{1} (t), Φ (t) ⟩ d λ (t) + ⟨ J, Φ (t_{*}) ⟩,$ $- \int_{I} ⟨ p_{2} (t), Φ^{'} (t) ⟩ d λ (t) = \int_{I} ⟨ F_{2} (t), Φ (t) ⟩ d λ (t) - ⟨ J, Φ (t_{*}) ⟩,$ with integrals against Lebesgue measure $λ$ and the Euclidean inner product $⟨ \cdot, \cdot ⟩$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ), using the fixed representative $p_{i} (t_{*}) = 0$ above.

Under this model, with $M : = m_{1} + m_{2}$ and $μ : = m_{1} m_{2} / M$ :

a. $m_{1} (v_{1}^{+} - v_{1}^{-}) = J$ and $m_{2} (v_{2}^{+} - v_{2}^{-}) = - J$ ; consequently the total momentum is continuous across the impulse, $p_{1} (t_{*}^{+}) + p_{2} (t_{*}^{+}) = p_{1} (t_{*}^{-}) + p_{2} (t_{*}^{-})$ .

b. Let $e \in [0, 1]$ satisfy the restitution law $v_{2}^{+} - v_{1}^{+} = - e (v_{2}^{-} - v_{1}^{-})$ . Then the post-impulse velocities are uniquely determined: with $V : = \frac{m_{1} v_{1}^{-} + m_{2} v_{2}^{-}}{M} = \frac{m_{1} v_{1}^{+} + m_{2} v_{2}^{+}}{M}$ , $v_{1}^{+} = V + \frac{m_{2}}{M} e (v_{2}^{-} - v_{1}^{-}), v_{2}^{+} = V - \frac{m_{1}}{M} e (v_{2}^{-} - v_{1}^{-}) .$

c. The kinetic-energy change across the impulse is $Δ K : = \frac{m_{1} ∥ v_{1}^{+} ∥_{2}^{2} + m_{2} ∥ v_{2}^{+} ∥_{2}^{2}}{2} - \frac{m_{1} ∥ v_{1}^{-} ∥_{2}^{2} + m_{2} ∥ v_{2}^{-} ∥_{2}^{2}}{2} = - \frac{1 - e^{2}}{2} μ ∥ v_{2}^{-} - v_{1}^{-} ∥_{2}^{2} \leq 0;$ in particular $Δ K = 0$ for $e = 1$ and $Δ K = - \frac{1}{2} μ ∥ v_{2}^{-} - v_{1}^{-} ∥_{2}^{2}$ for $e = 0$ .

Facts & Assumptions

Given: ${A C}_{ω}$ ; an open interval $I$ , a point $t_{*} \in I$ , masses $m_{1}, m_{2} > 0$ ; position curves $x_{1}, x_{2}$ continuous on $I$ and twice differentiable off $t_{*}$ with one-sided velocity limits $v_{i}^{\pm}$ ; continuous $F_{1}, F_{2}$ and a vector $J$ ; the isolated reciprocal impulse model of the statement; and, for claims b and c, a number $e \in [0, 1]$ satisfying the restitution law.

[L1]

Jump lemma: for a real function $p$ on $I$ that is continuous and $C^{1}$ off $t_{*}$ and whose one-sided limits $p (t_{*}^{\pm})$ and $p^{'} (t_{*}^{\pm})$ exist, the regular distributions of $p$ and of its off- $t_{*}$ derivative satisfy $(u_{p})^{'} = u_{p_{r e g}^{'}} + [p] δ_{t_{*}}$ with $[p] = p (t_{*}^{+}) - p (t_{*}^{-})$ (The distributional derivative of a piecewise $C^{1}$ function with a jump: $(u_{p})^{'} = u_{p_{r e g}^{'}} + [p] δ_{t_{*}}$ , The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[L2]

Two-body kinetic identity: for all vectors $u, w \in R^{3}$ and $V : = \frac{m_{1} u + m_{2} w}{M}$ , $m_{1} ∥ u ∥_{2}^{2} + m_{2} ∥ w ∥_{2}^{2} = M ∥ V ∥_{2}^{2} + μ ∥ u - w ∥_{2}^{2};$ this is the two-body case of the kinetic splitting identity, whose proof is the algebraic expansion of the right-hand side (Centre of mass, the identity $\sum_{i} m_{i} ρ_{i} = 0$ , and the splitting of the kinetic sum $\sum_{i} m_{i} ∥ x_{i}^{'} ∥_{2}^{2}$ into centre-of-mass and relative parts (with the two-body reduced-mass case), The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ). The Euclidean norm is a norm on $R^{3}$ , hence homogeneous: $∥ c w ∥_{2} = ∣ c ∣ ∥ w ∥_{2}$ for real $c$ (Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation).

[L3]

Test-function cutoffs: for compact $K \subseteq Ω$ with $Ω \subseteq R^{m}$ open there is a smooth compactly supported $χ \in C_{c}^{\infty} (Ω)$ with $0 \leq χ \leq 1$ and $χ = 1$ on a neighbourhood of $K$ ; in particular some $χ \in C_{c}^{\infty} (I)$ has $χ (t_{*}) = 1$ (Test function cutoffs and euclidean localization, Test function space d of an open set, $C^{k}$ Euclidean maps and diffeomorphisms). The Euclidean inner product is bilinear and symmetric (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

Proof

technique · direct

1.1givenL3algebra

For $k \in {0, 1, 2}$ , let $e_{k} \in R^{3}$ be the vector with $k$ th coordinate $1$ and other coordinates $0$ , and let $δ_{k l} = 1$ if $k = l$ and $0$ otherwise. Fix a real-valued $φ \in C_{c}^{\infty} (I)$ ; the vector test function $Φ : = φ e_{k}$ has components $(φ e_{k})_{l} = δ_{k l} φ$ and lies in $C_{c}^{\infty} (I; R^{3})$ . Reading the impulse pairing of the model for this $Φ$ gives $- \int_{I} p_{1, k} (t) φ^{'} (t) d λ (t) = \int_{I} F_{1, k} (t) φ (t) d λ (t) + J_{k} φ (t_{*}), - \int_{I} p_{2, k} (t) φ^{'} (t) d λ (t) = \int_{I} F_{2, k} (t) φ (t) d λ (t) - J_{k} φ (t_{*}) .$

2.1step 1.1givenL1

Each component $p_{i, k}$ satisfies the hypotheses of the jump lemma [L1]: it is continuous and $C^{1}$ off $t_{*}$ , its one-sided limits exist, and its one-sided derivative limits exist too, because off $t_{*}$ one has $p_{i, k}^{'} = m_{i} x_{i, k}^{''} = F_{i, k}$ by the regular-dynamics requirement of the model and $F_{i, k}$ is continuous on $I$ . Moreover the off- $t_{*}$ derivative of $p_{i, k}$ is $F_{i, k}$ , so $(p_{i, k})_{r e g}^{'} = F_{i, k}$ except possibly at $t_{*}$ , which does not change the regular distribution or its integral. Hence [L1] gives, for every real $φ \in C_{c}^{\infty} (I)$ , $- \int_{I} p_{i, k} φ^{'} d λ = \int_{I} F_{i, k} φ d λ + [p_{i, k}] φ (t_{*}) .$

3.1step 2.1givenL3algebra

Comparing the identity of step 2.1 with the model identity of step 1.1 for the same $φ$ , the terms $\int_{I} F_{i, k} φ d λ$ cancel and leave $([p_{1, k}] - J_{k}) φ (t_{*}) = 0$ and $([p_{2, k}] + J_{k}) φ (t_{*}) = 0$ for every $φ \in C_{c}^{\infty} (I)$ ; choosing by [L3] a $φ$ with $φ (t_{*}) = 1$ gives $[p_{1, k}] = J_{k}$ and $[p_{2, k}] = - J_{k}$ . As $k$ is arbitrary, $m_{1} (v_{1}^{+} - v_{1}^{-}) = J$ and $m_{2} (v_{2}^{+} - v_{2}^{-}) = - J$ , and adding these two vector equations gives $p_{1} (t_{*}^{+}) + p_{2} (t_{*}^{+}) = p_{1} (t_{*}^{-}) + p_{2} (t_{*}^{-})$ ; this is claim a.

4.1step 3.1givenalgebra

For claim b, let $V : = \frac{m_{1} v_{1}^{-} + m_{2} v_{2}^{-}}{M}$ and $d : = v_{2}^{-} - v_{1}^{-}$ . By step 3.1, $V = \frac{m_{1} v_{1}^{+} + m_{2} v_{2}^{+}}{M}$ as well. The restitution law reads $v_{2}^{+} - v_{1}^{+} = - e d$ . Writing $d^{+} : = v_{2}^{+} - v_{1}^{+}$ and solving the pair of linear equations ( $v_{2}^{+} = v_{1}^{+} + d^{+}$ and $m_{1} v_{1}^{+} + m_{2} v_{2}^{+} = M V$ ) gives $v_{1}^{+} = V - \frac{m_{2}}{M} d^{+} = V + \frac{m_{2}}{M} e d$ and $v_{2}^{+} = V + \frac{m_{1}}{M} d^{+} = V - \frac{m_{1}}{M} e d$ ; conversely these displayed vectors satisfy both equations, so they are the unique solution and claim b holds.

5.1step 4.1givenL2algebra∎

For claim c, apply the kinetic identity [L2] to the pairs $(v_{1}^{-}, v_{2}^{-})$ and $(v_{1}^{+}, v_{2}^{+})$ , whose centre-of-mass velocities are both $V$ : $\frac{m_{1} ∥ v_{1}^{\pm} ∥_{2}^{2} + m_{2} ∥ v_{2}^{\pm} ∥_{2}^{2}}{2} = \frac{M ∥ V ∥_{2}^{2}}{2} + \frac{μ ∥ v_{2}^{\pm} - v_{1}^{\pm} ∥_{2}^{2}}{2} .$ Subtracting the minus identity from the plus identity cancels the centre-of-mass term, and the restitution law gives $∥ v_{2}^{+} - v_{1}^{+} ∥_{2}^{2} = e^{2} ∥ v_{2}^{-} - v_{1}^{-} ∥_{2}^{2}$ by homogeneity of the norm [L2], so $Δ K = \frac{μ}{2} (e^{2} - 1) ∥ v_{2}^{-} - v_{1}^{-} ∥_{2}^{2} = - \frac{1 - e^{2}}{2} μ ∥ v_{2}^{-} - v_{1}^{-} ∥_{2}^{2} \leq 0$ because $0 \leq e \leq 1$ ; the cases $e = 1$ and $e = 0$ are the stated substitutions. This is claim c.

5 · Examples, experiments and counterexamples

None yet.

Cm Math Balances

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

Differentiation of sums, scalar multiples, inner products, cross products and squared norms of differentiable curves in R3R3

Statement

Facts & Assumptions

Proof

Centre of mass, the identity ∑imiρi=0∑i​mi​ρi​=0, and the splitting of the kinetic sum ∑imi∥xi′∥22∑i​mi​∥xi′​∥22​ into centre-of-mass and relative parts (with the two-body reduced-mass case)

Statement

Facts & Assumptions

Proof

Total momentum and total angular momentum balances for a finite system with antisymmetric pair forces; pairwise central forces make the internal torque vanish

Statement

Facts & Assumptions

Proof

Work-energy balance ddt(K+U(t,x(t)))=∂tU(t,x(t))+∑i⟨di(t),xi′(t)⟩dtd​(K+U(t,x(t)))=∂t​U(t,x(t))+∑i​⟨di​(t),xi′​(t)⟩ for forces mixi′′=−∇xiU+dimi​xi′′​=−∇xi​​U+di​

Statement

Facts & Assumptions

Proof

Variable-mass momentum balance: from m′=rin−routm′=rin​−rout​ and (mv)′=F+rinwin−routwout(mv)′=F+rin​win​−rout​wout​ to mv′=F+rin(win−v)−rout(wout−v)mv′=F+rin​(win​−v)−rout​(wout​−v)

Statement

Facts & Assumptions

Proof

Compact continuation for locally Lipschitz ODEs: a solution whose graph stays in a compact subset of the domain near a finite endpoint extends past it

Statement

Facts & Assumptions

Proof

A non-extendable solution leaves every compact subset of the domain near its finite endpoint; an autonomous solution trapped in a compact subset of its state domain cannot break down there

Statement

Facts & Assumptions

Proof

The distributional derivative of a piecewise C1C1 function with a jump: (up)′=upreg′+[p] δt∗(up​)′=upreg′​​+[p]δt∗​​

Statement

Facts & Assumptions

Proof

Isolated reciprocal impulse with full-vector restitution: momentum jumps ±J±J, conservation of total momentum, the restitution solution and the kinetic-energy change −1−e22μ∥v2−−v1−∥22−21−e2​μ∥v2−​−v1−​∥22​

Statement

Facts & Assumptions

Proof

5 · Examples, experiments and counterexamples

Sources

Differentiation of sums, scalar multiples, inner products, cross products and squared norms of differentiable curves in $R^{3}$

Centre of mass, the identity $\sum_{i} m_{i} ρ_{i} = 0$ , and the splitting of the kinetic sum $\sum_{i} m_{i} ∥ x_{i}^{'} ∥_{2}^{2}$ into centre-of-mass and relative parts (with the two-body reduced-mass case)

Work-energy balance $\frac{d}{d t} (K + U (t, x (t))) = \partial_{t} U (t, x (t)) + \sum_{i} ⟨ d_{i} (t), x_{i}^{'} (t) ⟩$ for forces $m_{i} x_{i}^{''} = - \nabla_{x_{i}} U + d_{i}$

Variable-mass momentum balance: from $m^{'} = r_{i n} - r_{o u t}$ and $(m v)^{'} = F + r_{i n} w_{i n} - r_{o u t} w_{o u t}$ to $m v^{'} = F + r_{i n} (w_{i n} - v) - r_{o u t} (w_{o u t} - v)$

The distributional derivative of a piecewise $C^{1}$ function with a jump: $(u_{p})^{'} = u_{p_{r e g}^{'}} + [p] δ_{t_{*}}$

Isolated reciprocal impulse with full-vector restitution: momentum jumps $\pm J$ , conservation of total momentum, the restitution solution and the kinetic-energy change $- \frac{1 - e^{2}}{2} μ ∥ v_{2}^{-} - v_{1}^{-} ∥_{2}^{2}$