Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-02
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.

The Bernstein polynomials of f(x)=x2f(x)=x^2 equal x2+x(1−x)/nx^2+x(1-x)/n

Statement

For f(x)=x2f(x)=x^2 and n≥1n\ge1, Bn(f)(x)=x2+x(1−x)/nB_n(f)(x)=x^2+x(1-x)/n. Hence ∥Bn(f)−f∥∞=1/(4n)\lVert B_n(f)-f\rVert_\infty=1/(4n). For n=0n=0, B0(f)=0B_0(f)=0.

Facts & Assumptions

Given: f(x)=x2f(x)=x^2 on [0,1][0,1].

[L1]

The first two Bernstein binomial moments are those of The zeroth, first, and second centred moments of the Bernstein basis.

[L2]

The Bernstein polynomial is defined in The Bernstein polynomial Bn(f)B_n(f) on [0,1][0,1].

Proof

technique · calculation
1.1

For n≥1n\ge1, substitute f(k/n)=(k/n)2f(k/n)=(k/n)^2 in the definition and use [L1] to obtain Bn(f)=x2+x(1−x)/nB_n(f)=x^2+x(1-x)/n.

L1L2algebra
2.1

Since 0≤x(1−x)≤1/40\le x(1-x)\le1/4 with equality at x=1/2x=1/2, the stated supremum error is 1/(4n)1/(4n).

step 1.1algebra
3.1

The separate definition at degree zero gives B0(f)=f(0)=0B_0(f)=f(0)=0.

L2algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 37 results over 13 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources