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.

Differentiation of a variable-limit convolution integral with a C-one matrix kernel

Statement

Let $n \geq 1$ , equip $R^{n}$ with the Euclidean inner product and norm of The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , and let $I \subseteq R$ be an interval with nonempty interior (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length), let $t_{0} \in I$ , let $U \subseteq R$ be an open interval with $I - I : = {t - s : t, s \in I} \subseteq U$ , let $g : U \to M_{n} (R)$ have $C^{1}$ entries (The vector space $M_{m \times n} (F) : = F^{m \times n}$ of $m$ by $n$ matrices over a field, with entrywise operations, $C^{k}$ Euclidean maps and diffeomorphisms) and let $f : I \to R^{n}$ be continuous (Vector-valued functions $f : A \to R^{m}$ , their limits and continuity, with the dictionary to the metric notions). For $B = (b_{i j}) \in M_{n} (R)$ and $v \in R^{n}$ , define $(B v)_{i} : = \sum_{j < n} b_{i j} v_{j}$ . This is a linear map by the coordinate formula; the Euclidean norm is a norm by 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 standard coordinate vectors form an ordered basis by The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ , so the map is bounded by A linear map from a finite-dimensional normed space is bounded. Let $∥ B ∥$ denote its induced operator norm (The operator norm as the least bound and as the unit-sphere or unit-ball supremum). All matrix actions in the integrals use this convention. Since $0 \in I - I \subseteq U$ , the value $g (0)$ is defined. Define

$F : I ⟶ R^{n}, F (t) : = \int_{t_{0}}^{t} g (t - s) f (s) d s,$

with the oriented integral of The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral and the matrix action just defined; the integrand is continuous in $s$ , hence integrable on every compact subinterval. Then:

$F$ is differentiable at every interior point $t$ of $I$ (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) and

$F^{'} (t) = g (0) f (t) + \int_{t_{0}}^{t} g^{'} (t - s) f (s) d s .$

If moreover $g^{'}$ is bounded on compact subintervals of $U$ (which holds automatically because $g$ is $C^{1}$ ), then $F$ is of class $C^{1}$ on the interior of $I$ .

Facts & Assumptions

Given: A natural number $n \geq 1$ , an interval $I \subseteq R$ with nonempty interior, a point $t_{0} \in I$ , an open interval $U \supseteq I - I$ , a $C^{1}$ matrix curve $g : U \to M_{n} (R)$ and a continuous curve $f : I \to R^{n}$ .

[F1]

The vector-valued derivative and the oriented Riemann integral are componentwise: $(F^{'})_{i} = (F_{i})^{'}$ and $(\int_{a}^{b} ϕ)_{i} = \int_{a}^{b} ϕ_{i}$ , with $\int_{a}^{b} = - \int_{b}^{a}$ ; the integral is additive over subintervals and linear in the integrand (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$ ).

[F2]

For $a < b$ and an integrable $ϕ : [a, b] \to R^{n}$ one has $∥ \int_{a}^{b} ϕ ∥_{2} \leq \int_{a}^{b} ∥ ϕ ∥_{2}$ , and for real integrable $u \leq v$ one has $\int_{a}^{b} u \leq \int_{a}^{b} v$ (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)$ ). Consequently, for a continuous $ψ$ on the interval with endpoints $a$ and $a + h$ , $h \neq 0$ , $∥ \frac{1}{h} \int_{a}^{a + h} ψ ∥_{2} \leq \sup_{s} ∥ ψ (s) ∥_{2},$ the supremum over that interval.

[F3]

Leibniz's rule on a compact rectangle: 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 on $(a, b)$ with derivative $H (x, t)$ , then $x \mapsto \int_{c}^{d} G (x, t) d t$ is differentiable on $[a, b]$ with derivative $\int_{c}^{d} H (x, t) d t$ (Leibniz's rule on a compact rectangle: an interior parameter derivative with a continuous extension may be passed through a Riemann integral). The component maps below satisfy these hypotheses: sums and products of $C^{1}$ functions are $C^{1}$ by the chain rule and the algebra of derivatives (The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , 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$ ).

[F4]

A closed rectangle in $R^{2}$ is compact (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line), a continuous map on a compact metric space is uniformly continuous (Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous), and a continuous real function on a compact interval is bounded and Riemann integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[F5]

Differentiability at $t$ means that the difference quotients $[F (t + h) - F (t)] / h$ converge to $F^{'} (t)$ as $h \to 0$ through nonzero values (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).

[F6]

The matrix action is linear by its coordinate formula (The vector space $M_{m \times n} (F) : = F^{m \times n}$ of $m$ by $n$ matrices over a field, with entrywise operations, Linear map between vector spaces over the same field). The Euclidean inner product and norm are those of The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , this norm makes $R^{n}$ a normed space by 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 standard coordinate vectors form an ordered basis by The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ . Hence each such matrix action is a bounded linear operator by A linear map from a finite-dimensional normed space is bounded, and its induced operator norm is $∥ B ∥$ (The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

Proof

technique · direct; split the difference quotient into a parameter-derivative term and a moving-endpoint term, take the two limits separately, then check continuity of the derivative

1.1F1given

Fix $t \in \overset{˚}{I}$ and choose $η > 0$ with $[t - η, t + η] \subseteq I$ and $[- η, η] \subseteq U$ . For $0 < ∣ h ∣ \leq η$ , additivity and linearity of the integral [F1] give $F (t + h) - F (t) = \int_{t_{0}}^{t} [g (t + h - s) - g (t - s)] f (s) d s + \int_{t}^{t + h} g (t + h - s) f (s) d s,$ with the second integral oriented and taken over the interval with endpoints $t$ and $t + h$ ; both integrands are continuous on their compact intervals, since every difference of two points of $I$ lies in $I - I \subseteq U$ .

2.1step 1.1F1F3F6given

For a component index $i < n$ , put $ϕ_{i} (u, s) : = (g (u - s) f (s))_{i} = \sum_{j < n} g_{i j} (u - s) f_{j} (s)$ for $(u, s) \in [t - η, t + η] \times J$ , where $J$ is the compact interval with endpoints $t_{0}$ and $t$ . This is continuous, and for fixed $s$ it is differentiable in $u$ with $\partial_{u} ϕ_{i} (u, s) = \sum_{j < n} g_{i j}^{'} (u - s) f_{j} (s)$ , which is continuous on the rectangle; [F3] therefore gives $\lim_{h \to 0} \frac{1}{h} \int_{t_{0}}^{t} [g (t + h - s) - g (t - s)] f (s) d s = \int_{t_{0}}^{t} g^{'} (t - s) f (s) d s,$ for $t_{0} < t$ directly, and for $t_{0} > t$ after reversing the orientation and applying [F3] on $[t, t_{0}]$ ; [F1] identifies the components.

2.2step 1.1F1F2F4F6given

For the second term put $ψ_{h} (s) : = g (t + h - s) f (s)$ on the interval with endpoints $t$ and $t + h$ . Since $g (0) f (t)$ is the value of the constant function $g (0) f (t)$ there, [F1] gives $\frac{1}{h} \int_{t}^{t + h} g (t + h - s) f (s) d s - g (0) f (t) = \frac{1}{h} \int_{t}^{t + h} [ψ_{h} (s) - g (0) f (t)] d s,$ and [F2] bounds its norm by $\sup_{s} ∥ ψ_{h} (s) - g (0) f (t) ∥_{2} = \sup_{s} ∥ g (t + h - s) f (s) - g (0) f (t) ∥_{2}$ over the interval with endpoints $t$ and $t + h$ . As $h \to 0$ the arguments $t + h - s$ lie between $0$ and $h$ (in either order) and tend to $0$ , and $s \to t$ , so continuity of $g$ at $0$ and of $f$ at $t$ makes this supremum tend to $0$ ; hence the second term tends to $g (0) f (t)$ .

3.1step 1.1step 2.1step 2.2F5

Dividing the identity of step 1.1 by $h$ , the two summands are precisely the terms analysed in steps 2.1 and 2.2; their limits exist and sum to $g (0) f (t) + \int_{t_{0}}^{t} g^{'} (t - s) f (s) d s$ . By [F5] this is exactly the differentiability assertion of clause 1 at $t$ , and $t \in \overset{˚}{I}$ was arbitrary.

4.1step 3.1F1F2F4F6∎

For clause 2 write $F^{'} (t) = g (0) f (t) + H (t)$ by step 3.1, with $H (t) : = \int_{t_{0}}^{t} g^{'} (t - s) f (s) d s$ . The term $g (0) f (t)$ is continuous. Fix $t_{1} \in \overset{˚}{I}$ , let $J_{0}$ be the closed interval with endpoints $t_{0}, t_{1}$ , and put $Q : = t_{1} - J_{0} = [α, β] \subseteq I - I \subseteq U$ . Since $U$ is an open interval containing the compact interval $Q$ , choose $η > 0$ small enough that $[t_{1} - η, t_{1} + η] \subseteq I$ and $K_{0} : = [α - η, β + η] \subseteq U$ . Put $J_{1} : = [\min (t_{0}, t_{1} - η), \max (t_{0}, t_{1} + η)] \subseteq I$ . For $t \in [t_{1} - η / 2, t_{1} + η / 2]$ , additivity [F1] gives $H (t) - H (t_{1}) = \int_{t_{1}}^{t} g^{'} (t - s) f (s) d s + \int_{t_{0}}^{t_{1}} [g^{'} (t - s) - g^{'} (t_{1} - s)] f (s) d s .$ In the first integral, $s$ lies between $t_{1}$ and $t$ , so $t - s \in K_{0}$ ; in the second, $u : = t_{1} - s \in Q$ and $t - s = u + (t - t_{1}) \in K_{0}$ . By [F2], the first integral has norm at most $∣ t - t_{1} ∣ \sup_{u \in K_{0}} ∥ g^{'} (u) ∥ \sup_{s \in J_{1}} ∥ f (s) ∥_{2}$ , which tends to $0$ . The second has norm at most $∣ t_{1} - t_{0} ∣ \sup_{s \in J_{0}} ∥ f (s) ∥_{2} \sup_{u \in Q, ∣ δ ∣ \leq ∣ t - t_{1} ∣} ∥ g^{'} (u + δ) - g^{'} (u) ∥$ , which tends to $0$ by uniform continuity of the matrix-valued $g^{'}$ on $K_{0}$ . Hence $H$ is continuous at $t_{1}$ , so $F^{'}$ is continuous on $\overset{˚}{I}$ , proving clause 2.

Differentiation of a variable-limit convolution integral with a C-one matrix kernel

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources