LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Sine chord and Lipschitz bounds

Statement

For $0 \leq u \leq π / 2$ , $\sin u \geq \frac{2 u}{π} .$ For all real $u, v$ , $∣ \sin u - \sin v ∣ \leq ∣ u - v ∣ .$

Facts & Assumptions

Given: Real $u, v$ , with $0 \leq u \leq π / 2$ for the first inequality.

[F1]

The derivatives of sine and cosine are cosine and minus sine: $\sin^{'} = \cos$ , $\cos^{'} = - \sin$ , and $\sin 0 = 0$ .

[F2]

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$ : products and quotients of differentiable functions obey the product and quotient rules wherever the denominator is nonzero.

[F3]

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)$ : a function continuous on a closed interval and differentiable on its interior has a point where its endpoint increment equals its derivative times the interval length.

[F4]

Signs, monotonicity intervals, and ranges of sine and cosine, Quarter-turn values and shifts by pi/2 and pi, and The derivatives of sine and cosine are cosine and minus sine: $0 \leq \sin u$ on $[0, π / 2]$ , $∣ \cos u ∣ \leq 1$ on $R$ , and $\sin (π / 2) = 1$ .

[F5]

For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term and A function differentiable at $c$ is continuous at $c$ : the identity function has derivative $1$ , and every differentiable real function is continuous at each point where it is differentiable.

Proof

1.1givenF1F2F3F4F5constructalgebra

Define $h (u) = \sin u - u \cos u$ . By [F1], [F2], and [F5], $h$ is differentiable and hence continuous, with $h^{'} (u) = u \sin u \geq 0$ on $(0, π / 2)$ by [F4]. For $u > 0$ , the mean value theorem on $[0, u]$ gives $h (u) \geq h (0) = 0$ ; at $u = 0$ equality is immediate.

2.1givenF1F2F3F4F5step 1.1algebra

For $0 < u < π / 2$ , define $r (u) = \sin u / u$ . By the quotient rule, the identity derivative in [F5], and step 1.1, $r^{'} (u) = (u \cos u - \sin u) / u^{2} = - h (u) / u^{2} \leq 0$ . The function $r$ is continuous on $[u, π / 2]$ by [F5], so the mean value theorem gives $r (u) \geq r (π / 2) = 2 / π$ by [F3] and [F4]; at $u = π / 2$ equality holds. Multiplying by $u$ and checking $u = 0$ proves the first inequality.

3.1givenF1F3F4F5algebra∎

If $u \neq v$ , sine is continuous on the closed interval between them and differentiable inside by [F1] and [F5]. The mean value theorem gives $∣ \sin u - \sin v ∣ = ∣ \cos c ∣ ∣ u - v ∣ \leq ∣ u - v ∣$ for some interior $c$ , by [F3] and [F4]. If $u = v$ , both sides are zero.

Depends on

Used by

Dependency tree · two levels

32 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Lloyd N. Trefethen, Approximation Theory and Approximation Practice, Ch. 3 (standard reference, not scraped)
Tobin A. Driscoll and Richard J. Braun, Fundamentals of Numerical Computation, Problems and conditioning (standard reference, not scraped)