LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Iterates of the stroboscopic map, and equilibria as fixed points

Statement

Retain all notation and hypotheses of The stroboscopic (time- $P$ ) map of a $P$ -periodic first-order system: $U \subseteq R^{n}$ is open, $P > 0$ , and $F : R \times U \to R^{n}$ is continuous, locally Lipschitz in the state variable, and $P$ -periodic.

If $z \in D_{P}$ and $θ_{P} (z) \in D_{P}$ , then $[0, 2 P] \subseteq J_{z}$ and

$θ_{P} (θ_{P} (z)) = x_{z} (2 P) .$

If $z_{*} \in U$ satisfies $F (t, z_{*}) = 0$ for every $t \in R$ , then $z_{*} \in D_{P}$ and $θ_{P} (z_{*}) = z_{*}$ .

Facts & Assumptions

Given: The hypotheses of The stroboscopic (time- $P$ ) map of a $P$ -periodic first-order system: an open $U \subseteq R^{n}$ , a number $P > 0$ , and a continuous map $F : R \times U \to R^{n}$ , locally Lipschitz in the state variable and $P$ -periodic; for clause 1 a point $z \in D_{P}$ with $θ_{P} (z) \in D_{P}$ ; for clause 2 a point $z_{*} \in U$ with $F (t, z_{*}) = 0$ for every $t$ .

[F1]

Each initial value problem $x^{'} = F (t, x)$ , $x (t_{0}) = x_{0}$ satisfies the Picard-Lindelof hypotheses, so it has a unique maximal solution whose domain is an open interval containing $t_{0}$ , and every other solution through the same data is a restriction of it (Every Picard–Lindelöf initial value problem has one maximal solution on an open interval, Extensions, maximal solutions, maximal intervals, and global solutions).

[F2]

The stroboscopic map satisfies $θ_{P} (w) = x_{w} (P)$ for $w \in D_{P}$ , and $D_{P} = {w \in U : [0, P] \subseteq J_{w}}$ (The stroboscopic (time- $P$ ) map of a $P$ -periodic first-order system).

[F3]

If two locally unique solutions of the same continuous equation are defined on adjacent intervals, agree at the common endpoint, and solve the equation there, their piecewise union is a solution on the union interval (Locally unique ODE solutions agree on overlaps and glue across a common endpoint).

[F4]

The right-hand side is $P$ -periodic, so $F (t + P, x) = F (t, x)$ for all $(t, x)$ (The stroboscopic (time- $P$ ) map of a $P$ -periodic first-order system).

Proof

technique · direct

1.1F2givenconstruct

Put $w : = θ_{P} (z) = x_{z} (P)$ , a point of $D_{P}$ by hypothesis, and let $x_{w} : J_{w} \to U$ be the maximal solution of $x^{'} = F (t, x)$ , $x (0) = w$ ; by [F2] the interval $J_{w}$ contains $[0, P]$ . Define $y : [0, 2 P] \to U$ by $y (t) : = x_{z} (t)$ for $t \in [0, P]$ and $y (t) : = x_{w} (t - P)$ for $t \in [P, 2 P]$ .

2.1step 1.1F3F4algebra

The curve $y$ is well defined and continuous: at the common point $P$ both formulas give $y (P) = x_{z} (P) = w = x_{w} (0)$ . On $[0, P]$ it solves the system by definition of $x_{z}$ . On $[P, 2 P]$ , writing $s = t - P$ , one has $y^{'} (t) = x_{w}^{'} (s) = F (s, x_{w} (s)) = F (s + P, x_{w} (s)) = F (t, y (t))$ by $P$ -periodicity [F4]. At $t = P$ the one-sided derivatives are $y^{'} (P^{-}) = F (P, w)$ and $y^{'} (P^{+}) = F (0, w)$ , equal by [F4]; hence $y^{'} (P) = F (P, y (P))$ . The domain-relative endpoint derivatives of the ODE solution definition and the gluing fact [F3] therefore make $y$ a solution on $[0, 2 P]$ .

3.1step 1.1step 2.1F1F2algebra

The curve $y$ satisfies $y (0) = x_{z} (0) = z$ , so $y$ is a solution of the initial value problem with data $(0, z)$ on $[0, 2 P]$ . By the uniqueness clause of [F1] every solution through $(0, z)$ is a restriction of the maximal solution $x_{z}$ , so $[0, 2 P] \subseteq J_{z}$ and $y = x_{z} ∣_{[0, 2 P]}$ . In particular $x_{z} (2 P) = y (2 P) = x_{w} (P) = θ_{P} (w) = θ_{P} (θ_{P} (z))$ .

4.1F1F2given∎

For clause 2, the constant curve $c (t) : = z_{*}$ is a solution of the system on $R$ because $c^{'} (t) = 0 = F (t, c (t))$ ; it satisfies $c (0) = z_{*}$ , so by the uniqueness clause of [F1] it is a restriction of $x_{z_{*}}$ . Hence $[0, P] \subseteq J_{z_{*}}$ , that is $z_{*} \in D_{P}$ , and $θ_{P} (z_{*}) = x_{z_{*}} (P) = c (P) = z_{*}$ .

Remarks

Clause 1 is the precise sense in which iterating a stroboscopic map follows the continuous solution across successive periods: each iterate requires the previous value to lie in $D_{P}$ again, and then the iterate equals the value of the same maximal solution at the corresponding multiple of $P$ . The identity extends by induction to $k$ -fold iterates as long as every intermediate value lies in $D_{P}$ .
No claim is made that $D_{P}$ is nonempty, open, or forward invariant, or that $θ_{P}$ has periodic points. Clause 2 shows only that every equilibrium of the $P$ -periodic vector field gives a fixed point of $θ_{P}$ with domain membership.

Depends on

Dependency tree · 2 levels

Sources

G. Teschl, Ordinary Differential Equations and Dynamical Systems, Section 6.4 and Section 4.6, printed pages 198 and 133-141