LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-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.

Discrete periodic summation by parts, the scaled Cauchy-Schwarz inequality, and the discrete energy identity

Statement

Use the notation $z_{j + N} = z_{j}$ , $(D_{+} z)_{j} = (z_{j + 1} - z_{j}) / a$ , $(Δ_{a} z)_{j} = (z_{j + 1} - 2 z_{j} + z_{j - 1}) / a^{2}$ , $⟨ z, w ⟩_{a} = a \sum_{j} z_{j} w_{j}$ , $∥ z ∥_{a}^{2} = ⟨ z, z ⟩_{a}$ and $E_{a} (q, p) = \frac{1}{2} (∥ p ∥_{a}^{2} + c^{2} ∥ D_{+} q ∥_{a}^{2})$ of The cyclic spring chain, its discrete energy, and the finite-regularity periodic comparison class.

(a) Summation by parts. For all $z, w \in R^{N}$ ,

$⟨ D_{+} z, D_{+} w ⟩_{a} = - ⟨ Δ_{a} z, w ⟩_{a} .$

(b) Scaled Cauchy-Schwarz. For all $z, w \in R^{N}$ , $∣ ⟨ z, w ⟩_{a} ∣ \leq ∥ z ∥_{a} ∥ w ∥_{a}$ (On $R^{n}$ , abstract Cauchy–Schwarz is exactly the published finite-sum Cauchy–Schwarz inequality, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

(c) Energy identity. Let $I \subseteq R$ be an open interval, let $q : I \to R^{N}$ be $C^{2}$ and let $R : I \to R^{N}$ be continuous with

$q_{j}^{''} = \frac{c^{2}}{a^{2}} (q_{j + 1} - 2 q_{j} + q_{j - 1}) + R_{j} = c^{2} (Δ_{a} q)_{j} + R_{j} (j \in Z / N) .$

Then $t \mapsto E_{a} (q (t), q^{'} (t))$ is $C^{1}$ on $I$ with

$\frac{d}{d t} E_{a} (q (t), q^{'} (t)) = a \sum_{j = 1}^{N} R_{j} (t) q_{j}^{'} (t),$

and consequently $∣ \frac{d}{d t} E_{a} ∣ \leq ∥ R (t) ∥_{a} \sqrt{2 E_{a} (t)}$ whenever $E_{a} \geq 0$ (which always holds).

Facts & Assumptions

Given: $N \geq 2$ , $a > 0$ , $c > 0$ , vectors $z, w$ ; in (c), the $C^{2}$ curve $q$ and the continuous field $R$ satisfying the stated equation.

[F1]

Index shifts in a finite cyclic sum change nothing: $\sum_{j = 1}^{N} z_{j + 1} = \sum_{j = 1}^{N} z_{j}$ , and sums split as $\sum_{j} (α_{j} - β_{j}) = \sum_{j} α_{j} - \sum_{j} β_{j}$ (The cyclic spring chain, its discrete energy, and the finite-regularity periodic comparison class).

[F2]

Cauchy-Schwarz in coordinates (On $R^{n}$ , abstract Cauchy–Schwarz is exactly the published finite-sum Cauchy–Schwarz inequality); the scaled form (b) follows by applying it to $\sqrt{a} z$ and $\sqrt{a} w$ .

[F3]

$E_{a}$ is a finite sum of squares of $C^{1}$ functions, hence $C^{1}$ , and its derivative is computed by the product rule and linearity of the finite sum (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, Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ ).

Proof

technique · direct; shift indices in the finite sum and differentiate the quadratic energy

1.1givenF1algebra

Compute $a \sum_{j} (D_{+} z)_{j} (D_{+} w)_{j} = \frac{1}{a} \sum_{j} (z_{j + 1} - z_{j}) (w_{j + 1} - w_{j})$ . Splitting the sum and shifting the index in the first product term, $\frac{1}{a} \sum_{j} (z_{j + 1} - z_{j}) (w_{j + 1} - w_{j}) = \frac{1}{a} \sum_{j} (z_{j} - z_{j - 1}) w_{j} - \frac{1}{a} \sum_{j} (z_{j + 1} - z_{j}) w_{j} = - \frac{1}{a} \sum_{j} (z_{j + 1} - 2 z_{j} + z_{j - 1}) w_{j},$ which is $- ⟨ Δ_{a} z, w ⟩_{a}$ . This proves (a).

1.2F2algebra

For (b), apply [F2] to the vectors $(\sqrt{a} z_{j})$ and $(\sqrt{a} w_{j})$ .

2.1F3step 1.1algebra

Assume (c). By [F3], $\frac{d}{d t} E_{a} (q (t), q^{'} (t)) = a \sum_{j} (q_{j}^{'} (t) q_{j}^{''} (t) + c^{2} (D_{+} q)_{j} (t) (D_{+} q^{'})_{j} (t)) .$ Applying (a) with $z = q (t)$ , $w = q^{'} (t)$ turns the second term into $- c^{2} a \sum_{j} (Δ_{a} q)_{j} q_{j}^{'}$ . Hence $\frac{d}{d t} E_{a} = a \sum_{j} q_{j}^{'} (q_{j}^{''} - c^{2} (Δ_{a} q)_{j}) = a \sum_{j} R_{j} q_{j}^{'} .$

3.1step 2.1step 1.2algebra∎

By (b), $∣ a \sum_{j} R_{j} q_{j}^{'} ∣ = ∣ ⟨ R, q^{'} ⟩_{a} ∣ \leq ∥ R ∥_{a} ∥ q^{'} ∥_{a} \leq ∥ R ∥_{a} \sqrt{2 E_{a}}$ , because $∥ q^{'} ∥_{a}^{2} \leq 2 E_{a}$ .

Remarks

The identity (a) is the discrete analogue of integration by parts on the circle; cyclicity is exactly what makes the boundary term vanish. On a chain with free or fixed ends the boundary terms would appear explicitly, and such models are not covered by this statement.
The energy identity (c) reduces the discrete energy rate to the pairing of the perturbation $R$ with the velocity; it holds for any continuous $R$ , including the Taylor remainder of the continuum limit.

Discrete periodic summation by parts, the scaled Cauchy-Schwarz inequality, and the discrete energy identity

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources