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.

Elementary bounds for the periodic average, the deviation and its time derivative

Statement

Let $n \geq 1$ , $P > 0$ , $O \subseteq R^{n}$ open, and let $f : R \times O \to R^{n}$ be continuous, continuously partially differentiable in the second variable and $P$ -periodic in time, with average $\overset{ˉ}{f}$ , oscillatory part $f - \overset{ˉ}{f}$ and periodic deviation $g$ as in Periodic averaging data: the average field, the oscillatory part and the periodic deviation (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length). Here $D_{x} f (t, x) : R^{n} \to R^{n}$ denotes the total derivative in the state variable, with coordinate columns $\partial_{x_{j}} f (t, x)$ ; it exists and is continuous by 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 same notation is used for $D_{x} \overset{ˉ}{f}$ and $D_{x} g$ when those total derivatives exist. Let $x_{0} \in O$ , $R > 0$ with $\overline{B} (x_{0}, R) \subseteq O$ (Open ball, closed ball and sphere in a metric space) and let $M, L \geq 0$ satisfy

$∥ f (t, x) ∥_{2} \leq M, ∥ f (t, x) - f (t, y) ∥_{2} \leq L ∥ x - y ∥_{2} (t \in R, x, y \in \overline{B} (x_{0}, R)) .$

Then:

$∥ \overset{ˉ}{f} (x) ∥_{2} \leq M$ and $∥ \overset{ˉ}{f} (x) - \overset{ˉ}{f} (y) ∥_{2} \leq L ∥ x - y ∥_{2}$ for all $x, y \in \overline{B} (x_{0}, R)$ .
$g$ is $P$ -periodic and $∥ g (t, x) ∥_{2} \leq 2 M P$ for every $t \in R$ and $x \in \overline{B} (x_{0}, R)$ ; moreover $∥ g (t, x) - g (t, y) ∥_{2} \leq 2 L P ∥ x - y ∥_{2}$ for all $t \in R$ and $x, y \in \overline{B} (x_{0}, R)$ .
$\partial_{t} g (t, x) = f (t, x) - \overset{ˉ}{f} (x)$ for every $(t, x)$ ; consequently $∥ \partial_{t} g (t, x) ∥_{2} \leq 2 M$ for $x \in \overline{B} (x_{0}, R)$ and $∥ \partial_{t} g (t, x) - \partial_{t} g (t, y) ∥_{2} \leq 2 L ∥ x - y ∥_{2}$ for all $t \in R$ and $x, y \in \overline{B} (x_{0}, R)$ .
$g$ has continuous first partial derivatives on $R \times O$ ; its partial derivative in the second variable is $D_{x} g (t, x) = \int_{0}^{t} (D_{x} f (s, x) - D_{x} \overset{ˉ}{f} (x)) d s$ , and $∥ D_{x} g (t, x) ∥ \leq 2 L P$ for $t \in R$ , $x \in \overline{B} (x_{0}, R)$ , with $∥ \cdot ∥$ the operator norm on $M_{n} (R)$ (The operator norm as the least bound and as the unit-sphere or unit-ball supremum). In particular $g$ is totally differentiable at every point of $R \times O$ (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative).

Facts & Assumptions

Given: The data $n, P, O, f$ of Periodic averaging data: the average field, the oscillatory part and the periodic deviation, the ball centre $x_{0}$ , radius $R$ , constants $M, L$ , and the derived objects $\overset{ˉ}{f}$ and $g$ .

[F1]

$f (t, x)$ is continuous in $(t, x)$ ; for fixed $x$ , $s \mapsto f (s, x)$ is continuous on $[0, P]$ and hence Riemann integrable there; the integrals below are componentwise oriented integrals (Periodic averaging data: the average field, the oscillatory part and the periodic deviation, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, Vector-valued functions $f : A \to R^{m}$ , their limits and continuity, with the dictionary to the metric notions).

[F2]

For integrable vector-valued $ϕ$ and $a < b$ : $∥ \int_{a}^{b} ϕ ∥_{2} \leq \int_{a}^{b} ∥ ϕ ∥_{2}$ , and for real integrable $u \leq v$ : $\int_{a}^{b} u \leq \int_{a}^{b} v$ ; for constant $c$ and $h > 0$ : $\int_{a}^{a + h} c = c h$ (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)$ ).

[F3]

Additivity: $\int_{a}^{b} = \int_{a}^{c} + \int_{c}^{b}$ for oriented integrals, and $\int_{a}^{b} = - \int_{b}^{a}$ (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$ , The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral).

[F4]

Fundamental theorem of calculus: if $u$ is continuous on an interval $I$ and $a \in I$ , then $F (t) : = \int_{a}^{t} u$ is a primitive of $u$ on $I$ (Every continuous function on an interval has a primitive; two primitives differ by a constant; and $\int_{a}^{b} f = G (b) - G (a)$ for any primitive $G$ ); in particular $F$ has derivative $u$ at every point of $I$ , and a periodic function is determined by its values on $[0, P]$ .

[F5]

Leibniz's rule on a compact rectangle (Leibniz's rule on a compact rectangle: an interior parameter derivative with a continuous extension may be passed through a Riemann integral): if $G, H : [a, b] \times [c, d] \to R$ are continuous and for every fixed $t \in [c, d]$ the slice $x \mapsto G (x, t)$ is differentiable with derivative $H (x, t)$ , then $x \mapsto \int_{c}^{d} G (x, t) d t$ has derivative $\int_{c}^{d} H (x, t) d t$ . The componentwise application of this rule to $f$ (whose partial derivatives in the state variable are continuous by hypothesis) supplies the identities of step 3.1 (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative for the passage from partial derivatives to the total derivative).

[F6]

A continuous scalar function on an interval with zero derivative at every interior point 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); applying this to every coordinate gives the same assertion for vector-valued functions.

Proof

technique · direct; estimate the averages and the deviation by the integral norm inequality and monotonicity, and identify the time derivative by the fundamental theorem

1.1F1F2given

Bounds for $\overset{ˉ}{f}$ : for $x \in \overline{B} (x_{0}, R)$ , $∥ \overset{ˉ}{f} (x) ∥_{2} = \frac{1}{P} ∥ \int_{0}^{P} f (s, x) d s ∥_{2} \leq \frac{1}{P} \int_{0}^{P} ∥ f (s, x) ∥_{2} d s \leq \frac{1}{P} \int_{0}^{P} M d s = M$ by [F2]; and for $x, y$ in the ball, $∥ \overset{ˉ}{f} (x) - \overset{ˉ}{f} (y) ∥_{2} = \frac{1}{P} ∥ \int_{0}^{P} (f (s, x) - f (s, y)) d s ∥_{2} \leq \frac{1}{P} \int_{0}^{P} ∥ f (s, x) - f (s, y) ∥_{2} d s \leq L ∥ x - y ∥_{2},$ again by [F2] and the assumed Lipschitz bound; this is clause 1.

2.1step 1.1F1F2F3given

Bounds for $g$ : for $t \in [0, P]$ and $x$ in the ball, step 1.1 and [F2] give $∥ g (t, x) ∥_{2} = ∥ \int_{0}^{t} (f (s, x) - \overset{ˉ}{f} (x)) d s ∥_{2} \leq \int_{0}^{t} (∥ f (s, x) ∥_{2} + ∥ \overset{ˉ}{f} (x) ∥_{2}) d s \leq 2 M P,$ and for $x, y$ in the ball, $∥ g (t, x) - g (t, y) ∥_{2} \leq \int_{0}^{t} (∥ f (s, x) - f (s, y) ∥_{2} + ∥ \overset{ˉ}{f} (x) - \overset{ˉ}{f} (y) ∥_{2}) d s \leq 2 L P ∥ x - y ∥_{2} .$ Since $g$ is $P$ -periodic by its definition (it satisfies $g (t + P, x) = g (t, x)$ and $g (P, x) = 0$ ), the same bounds hold for all $t \in R$ ; this is clause 2.

2.2step 1.1F1F3F4F6given

Time derivative: fix $x$ and put $u (s) : = f (s, x) - \overset{ˉ}{f} (x)$ , a continuous $R^{n}$ -valued function; on $(0, P)$ the fundamental theorem [F4] gives $\frac{\partial}{\partial t} g (t, x) = u (t) = f (t, x) - \overset{ˉ}{f} (x)$ . At $t = 0$ the right difference quotient converges to $u (0) = f (0, x) - \overset{ˉ}{f} (x)$ , while for $t \to 0^{-}$ periodicity reduces the quotient to the left derivative of $g (\cdot, x)$ at $P$ , namely $u (P) = f (P, x) - \overset{ˉ}{f} (x) = f (0, x) - \overset{ˉ}{f} (x)$ by periodicity of $f$ ; the same argument at every $t = k P$ shows the derivative exists there with the same value, and away from these points it is $u (t)$ . Hence $\partial_{t} g (t, x) = f (t, x) - \overset{ˉ}{f} (x)$ everywhere. The oriented integral $H (t) : = \int_{0}^{t} u (s) d s$ has the same derivative by [F4], so $H - g (\cdot, x)$ has zero derivative and vanishes at zero; [F6] gives $g (t, x) = H (t)$ for every real $t$ . The bounds on $f - \overset{ˉ}{f}$ follow from the triangle inequality and step 1.1: $∥ f (t, x) - \overset{ˉ}{f} (x) ∥_{2} \leq M + M = 2 M$ and $∥ f (t, x) - \overset{ˉ}{f} (x) - f (t, y) + \overset{ˉ}{f} (y) ∥_{2} \leq 2 L ∥ x - y ∥_{2}$ ; this is clause 3.

3.1step 1.1step 2.2F1F2F5given∎

Second-variable derivative and its norm bound: first fix $t \in R$ . For $x$ in the open ball $B (x_{0}, R)$ and any unit vector $v \in R^{n}$ , the assumed state-Lipschitz estimate gives $∥ (f (t, x + h v) - f (t, x)) / h ∥_{2} \leq L$ for every sufficiently small nonzero $h$ ; taking $h \to 0$ yields $∥ D_{x} f (t, x) v ∥_{2} \leq L$ . For a boundary point $x \in \overline{B} (x_{0}, R)$ , the sequence $x_{j} = x_{0} + (1 - 1 / (j + 1)) (x - x_{0}), j \in N$ lies in the open ball and tends to $x$ , so continuity of $D_{x} f (t, \cdot)$ gives the same bound at $x$ . Taking the supremum over unit $v$ proves $∥ D_{x} f (t, x) ∥ \leq L$ throughout the closed ball. Next fix any $x \in O$ and a component index $i$ . The map $(s, u) \mapsto f_{i} (s, u)$ , with $u$ near $x$ , is continuous and has continuous partial derivatives in $u$ ; [F5] applied componentwise at fixed $s$ and $t$ gives $\partial_{x_{j}} \int_{0}^{t} f_{i} (s, x) d s = \int_{0}^{t} \partial_{x_{j}} f_{i} (s, x) d s$ (first for $t$ in a compact interval, then by additivity for all $t \in R$ ), and likewise $D_{x} \overset{ˉ}{f} (x) = \frac{1}{P} \int_{0}^{P} D_{x} f (s, x) d s$ . For $x \in \overline{B} (x_{0}, R)$ and every unit $v$ , the vector integral inequality [F2] now gives $∥ D_{x} \overset{ˉ}{f} (x) v ∥_{2} \leq \frac{1}{P} \int_{0}^{P} L d s = L$ , hence $∥ D_{x} \overset{ˉ}{f} (x) ∥ \leq L$ . Using the all-time integral identity of step 2.2, $D_{x} g (t, x) = \int_{0}^{t} (D_{x} f (s, x) - D_{x} \overset{ˉ}{f} (x)) d s$ , continuously in $(t, x)$ . For $x \in \overline{B} (x_{0}, R)$ , $t \in [0, P]$ and every unit $v$ , another application of [F2] gives $∥ D_{x} g (t, x) v ∥_{2} \leq \int_{0}^{t} ∥ (D_{x} f (s, x) - D_{x} \overset{ˉ}{f} (x)) v ∥_{2} d s \leq 2 L t \leq 2 L P .$ Taking the supremum over unit $v$ proves $∥ D_{x} g (t, x) ∥ \leq 2 L P$ on one period; periodicity gives the same bound for all $t$ . This proves clause 4.

Elementary bounds for the periodic average, the deviation and its time derivative

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources