Definite integral: computing ∫₀³(x²−4)dx as a limit of left sums and by the moment formula

Goal and scope

Let f(x)=x²−4, a=0, b=3. (1) Using only the Riemann definition (the common limit of all valid tagged-partition sums as the mesh tends to zero) and the premise that f is integrable, find I(f,0,3) as the limit of the N-piece left sums L_N; (2) recompute it independently with the moment formula listed in this MKO and compare; (3) find the reversed integral I(f,3,0); (4) use N=3 and N=50 to show that a finite left sum is not the integral, and explain why the signed integral is not a nonnegative area.

Treats only one continuous polynomial within the MKO's scope, f(x)=x²−4 (integer coefficients, degree 2), and its signed Riemann integral over the finite interval [0,3]. Integrability of f is taken from MKO assumption a1 and is not proved here; what is proved is that, given integrability, the integral must equal −3. The general fundamental theorem of calculus is neither used nor claimed; general integrable functions, Lebesgue integration and area theory are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• finite_sum_rules
• seq_limit_def
• archimedean
• order_basics
• numeric_evaluation

• G1 — f(x)=x²−4 with endpoints a=0≤b=3. f is a polynomial of degree 2 with integer coefficients (ascending coefficients −4, 0, 1), as MKO assumption a1 requires.
• G2 — MKO assumption a1: f is continuous on all of ℝ and integrable on finite intervals; so I(f,0,3) exists and is a real number.
• G3 — The left sum of MKO assumption a3: for a≤b and a positive integer N, Δx=(b−a)/N, x_i=a+iΔx and L_N=Σ_{i=0}^{N−1} f(x_i)Δx. Here Δx=3/N and x_i=3i/N.

• f(x)=x^2-4 — the integrand polynomial
• I(f,a,b) — the oriented definite integral of f from a to b
• N — number of equal pieces, a positive integer
• \Delta x=\tfrac{3}{N} — length of each piece, which is also the mesh
• x_i=\tfrac{3i}{N} — the division point at index i; for 0≤i<N, also the left tag of piece i+1
• L_N — the N-piece left sum
• S(f,P,\xi) — the Riemann sum of a tagged partition (P,ξ)

Rules and sources

• finite_sum_rules · prerequisite — Finite sums: Σ_{i=1}^{0} a_i=0 and Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}; Σ(a_i+b_i)=Σa_i+Σb_i; Σ c·a_i=c·Σa_i.
• seq_limit_def · prerequisite — Limit of a sequence: a_n→L means that for every ε>0 there is N such that |a_n−L|<ε for all n≥N.
• archimedean · prerequisite — Archimedean property: for every real x there is a natural number n>x; hence for every ε>0 there is n with 1/n<ε.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
• power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
• nat_induction · prerequisite — Principle of induction: for a family P(n) starting at n₀, if P(n₀) holds and P(n)⇒P(n+1) for every n≥n₀, then P(n) holds for every n≥n₀.
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
• abs_rules · prerequisite — Absolute value (reals): |u|=u if u≥0 and |u|=−u if u<0; |u|≥0; |uv|=|u||v|; triangle inequality |u+v|≤|u|+|v|; |u|<r ⇔ −r<u<r.
• modus_ponens · prerequisite — Modus ponens: from P and P⇒Q infer Q.
• neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_riemann_def · cited — For a continuous polynomial f on a finite real interval a≤b, its Riemann integral is the common limit of all valid tagged-partition sums as the mesh tends to zero. · mko-definite-integral
• mko_reverse · cited — Reversing endpoints changes the sign: I(f,a,b)=−I(f,b,a); equal endpoints give I(f,a,a)=0. · mko-definite-integral
• mko_moment · cited — This slice explicitly uses the moment formula I(x^n,a,b)=(b^{n+1}−a^{n+1})/(n+1); for f=Σc_k x^k the moments are summed coefficientwise: I(f,a,b)=Σc_k(b^{k+1}−a^{k+1})/(k+1). · mko-definite-integral
• riemann_limit_meaning · prerequisite — The precise meaning of 'the common limit is I': for every ε>0 there is δ>0 such that every tagged partition (P,ξ) of [a,b] with mesh less than δ has |S(f,P,ξ)−I|<ε. A partition P is a finite strictly increasing list of points t_0=a<t_1<t_2 up to t_m=b; a tag ξ_j lies in [t_{j−1},t_j]; the mesh is the largest t_j−t_{j−1}; S(f,P,ξ)=Σ_{j=1}^{m} f(ξ_j)(t_j−t_{j−1}).
• limit_unique · prerequisite — Limits of sequences are unique: if s_N→L and s_N→L′, then L=L′.
• L_sum_sq · lemma — For every positive integer N, Σ_{i=0}^{N−1} i²=(N−1)N(2N−1)/6.

Main derivation

I(f,0,3)

\forall\varepsilon>0\ \exists\delta>0:\ \operatorname{mesh}(P)<\delta\Rightarrow|S(f,P,\xi)-I(f,0,3)|<\varepsilon

L_N=\sum_{i=0}^{N-1} f(x_i)\,\Delta x

L_N=S(f,P_N,\xi_N),\quad \operatorname{mesh}(P_N)=\tfrac{3}{N}

\operatorname{mesh}(P_N)=\tfrac{3}{N}\ \text{and S01}

L_N\to I(f,0,3)\quad(N\to\infty)

f(x_i)\,\Delta x

\tfrac{27i^2}{N^3}-\tfrac{12}{N}

L_N=\sum_{i=0}^{N-1}\left(\tfrac{27i^2}{N^3}-\tfrac{12}{N}\right)

L_N=\tfrac{27}{N^3}\sum_{i=0}^{N-1} i^2-12

\sum_{i=0}^{N-1} i^2

\tfrac{(N-1)N(2N-1)}{6}

L_N=\tfrac{27}{N^3}\cdot\tfrac{(N-1)N(2N-1)}{6}-12

L_N=-3-\tfrac{27}{2N}+\tfrac{9}{2N^2}

L_3,\ L_{50}

L_3=-7,\quad L_{50}=-\tfrac{16341}{5000}

|L_N-(-3)|

\tfrac{27N-9}{2N^2}\le\tfrac{27}{2N}

|L_N+3|\le\tfrac{27}{2N}\ \ (N\ge 1)

L_N\to -3

L_N\to I(f,0,3),\quad L_N\to -3

I(f,0,3)=-3

I(f,0,3)=I(x^2,0,3)-4\,I(x^0,0,3)

\tfrac{3^3-0^3}{3}-4\cdot\tfrac{3^1-0^1}{1}=9-12=-3

I(f,3,0)

-I(f,0,3)=3

I(f,0,2),\ I(f,2,3)

-\tfrac{16}{3},\ \tfrac{7}{3}

|I(f,0,3)|

3\neq\tfrac{23}{3}=|I(f,0,2)|+|I(f,2,3)|

\text{goals (1) to (4)}

I(f,0,3)=-3,\ I(f,3,0)=3,\ L_3=-7,\ L_{50}=-\tfrac{16341}{5000}

Substeps and lemmas

\sum_{i=0}^{0} i^2

0=\tfrac{(1-1)\cdot 1\cdot(2\cdot 1-1)}{6}

\sum_{i=0}^{N-1} i^2=\tfrac{(N-1)N(2N-1)}{6}

\sum_{i=0}^{N} i^2=\tfrac{N(N+1)(2N+1)}{6}

P(1)\ \land\ \forall N\ge 1\,(P(N)\Rightarrow P(N+1))

\forall N\ge 1:\ P(N)

Reverse audits

• S16 · sufficient_goal_reduction · S08, S11, S12, S13, S15, and_intro_elim — Goal G: the four parts. Sufficient condition H: the conclusions of S08, S11, S12, S13 and S15 together; H⇒G is just conjunction. H is proved forwards from G1 to G3; G is never used as a premise.
• S15 · premise_audit · S11, S14, abs_rules — This compares explicit numbers (N15). Area theory is not developed here; 23/3 is only the sum of the two absolute values.
• S14 · premise_audit · mko_moment, numeric_evaluation, order_basics — This only applies the moment formula on two pieces (N12 to N14, N16); additivity over intervals for general functions is not claimed.
• S13 · inverse_equivalence · S11, mko_reverse — Reversing once more gives I(f,0,3)=−I(f,3,0)=−3, back to S11; the sign rule works in both directions.
• S12 · premise_audit · G1, mko_moment, numeric_evaluation — The moment formula is a rule listed for this slice and is only applied here; agreement of the two routes is a cross-check. It is not, and is not claimed to be, a proof of the general fundamental theorem of calculus.
• S11 · premise_audit · S03, S10, G2, limit_unique — Both limits must concern the same sequence, and S03 relies on existence from G2. Without integrability one would only know that the left sums tend to −3, which could not be called the integral.
• S10 · premise_audit · S09, seq_limit_def, archimedean — The definition requires the bound for all N≥N_1, not only N≤50; this is why the bound of S09 had to be proved for general N rather than read off a finite table.
• S09 · premise_audit · S07, abs_rules, order_basics — N≥1 is needed to know 27N−9>0 and remove the absolute value; the inequality is a one-way bound, not an equality. N10 is a finite check for N=1 to 50.
• S08 · premise_audit · S07, numeric_evaluation — These are values at two N (N5 to N8), used to cross-check the formula of S07 and to show that a finite sum is not the integral; they do not prove the limit.
• S07 · inverse_equivalence · frac_rules, distributive, mul_inverse_nonzero — Multiplying both sides by the nonzero 2N² turns each into the same polynomial −6N²−27N+9 (N3 checks this degree-2 identity); dividing back by 2N² is allowed, so the step is two-way. N4 also checks N=1 to 50 point by point, which is only a finite check.
• S06.3 · premise_audit · S06.1, S06.2, nat_induction — Induction needs both the base and the step; both are proved, and neither uses the lemma itself.
• S06.2 · premise_audit · finite_sum_rules, distributive — It uses only the induction hypothesis for N and the polynomial identity (N−1)N(2N−1)/6+N²=N(N+1)(2N+1)/6 (N1, a grid check of a degree-3 identity).
• S06.1 · premise_audit · finite_sum_rules, numeric_evaluation — Only direct evaluation of both sides is needed (N2).
• S06 · inverse_equivalence · L_sum_sq — The two expressions are equal for every N≥1, so the replacement works in both directions.
• S05 · inverse_equivalence · finite_sum_rules, frac_rules — Backward: multiply 27/N³ back into each term and write 12 as the sum of N copies of 12/N to return to the original; the finite-sum rules used are identities.
• S04 · inverse_equivalence · distributive, frac_rules, power_laws — Backward: factor out 3/N to get (3/N)(9i²/N²−4)=f(x_i)Δx. For N≠0 both expressions are the same number.
• S03 · premise_audit · S01, S02, G2, seq_limit_def, archimedean — This step uses the existence of I(f,0,3) (G2). The converse is not claimed: convergence of one family of left sums does not imply integrability; MKO paragraph 0 also stresses that the definition requires the common limit over all valid tagged partitions.
• S02 · premise_audit · G3, riemann_limit_meaning, order_basics — It needs N≥1, so that Δx=3/N is defined and positive. It claims only that each left sum is a tagged-partition sum; the converse (every tagged-partition sum is a left sum) is false and is not claimed.
• S01 · premise_audit · G1, G2, mko_riemann_def, riemann_limit_meaning — This step only unfolds the definition and records the existence premise; it derives no value. Existence comes from G2 (MKO assumption a1), not from the convergence of one special family of sums later on.

Error controls and negative controls

A finite left sum is not the integral

One misconception the MKO names is taking a finite left sum for the integral. By S09 the error |L_N+3|=(27N−9)/(2N²) is positive for every N≥1, so no left sum with finite N equals −3 (for example L_3=−7 and L_50=−3.2682); only the limit as N→∞ equals the integral.

Reversed endpoints change the sign

∫₃⁰ and ∫₀³ have the same integrand and opposite orientation, so the value is 3, not −3. One may not ignore orientation on the grounds that it is 'the same interval', nor take absolute values by default (MKO assumption a2).

A signed integral is not an area

f is negative on [0,2) and positive on (2,3]; the pieces −16/3 and 7/3 cancel to −3, while the unsigned quantity is the sum of absolute values 23/3. Treating every integral as a nonnegative area would wrongly give 23/3 or 3 instead of −3.

A moment check is not the general FTC

S12 applies the polynomial moment formula listed in this MKO; its agreement with S11 is only a cross-check of two routes. The MKO says the general fundamental theorem of calculus is not treated as a completed prerequisite, and this guide does not claim to prove it.

• L_50=−3.2682 is ∫₀³(x²−4)dx → reject — L_50 differs from −3 by (27·50−9)/(2·50²)=1341/5000≠0; the integral is the limit as N→∞.
• ∫₃⁰(x²−4)dx=∫₀³(x²−4)dx=−3 because it is the same interval → reject — The reversal rule gives I(f,3,0)=−I(f,0,3)=3.
• A definite integral is never negative, so ∫₀³(x²−4)dx should be 23/3 → reject — The integral is signed and equals −3; 23/3 is the sum of the absolute values of the two pieces.
• If one family of equal-piece left sums converges, the function is integrable and the integral is that limit → reject — The Dirichlet function D (1 at rationals, 0 elsewhere) on [0,1]: the left points i/N are rational, so every left sum is 1; but with irrational tags the sums are 0 for arbitrarily small mesh, so there is no common limit and D is not Riemann integrable (MKO paragraph 0).

Result and limitations

Given integrability of f (MKO assumption a1), the Riemann definition and the limit of the left sums L_N=−3−27/(2N)+9/(2N²) give ∫₀³(x²−4)dx=−3; the MKO's moment formula independently gives the same value. With reversed endpoints ∫₃⁰(x²−4)dx=3. The finite left sums L_3=−7 and L_50=−3.2682 differ from the integral; the pieces −16/3 and 7/3 cancel, so the integral is not a nonnegative area.

• Integrability of f (G2) is taken from MKO assumption a1 and is not proved from the definition here; S03 depends on it.
• The moment formula (mko_moment) is a rule listed by the MKO; this guide checks its value independently from the definition for f(x)=x²−4 only and does not prove the general moment formula.
• N4 and N10 are finite checks for N=1 to 50 and support only those points; the conclusions for general N rest on the algebra of S07 and S09 and the polynomial identity N3.

Verification and source binding

17 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 1358dfe43443e21f9926bd2ea2dd97a3b9034b0966a92b412d106d4ae7195ad4
• original source SHA-256: 1358dfe43443e21f9926bd2ea2dd97a3b9034b0966a92b412d106d4ae7195ad4
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)