Theorem 6.22 — integration by parts

Disproved

Rudin.ch06_integration_by_parts

by Lucas · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisintegration

If $F$ and $G$ are differentiable on $[a,b]$ with $F' = f \in \mathcal{R}$ and $G' = g \in \mathcal{R}$ , then

\int_a^b F(x)g(x)\,dx = F(b)G(b) - F(a)G(a) - \int_a^b f(x)G(x)\,dx .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch06_stieltjes

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 6.22 (integration by parts): if `F` and `G` are differentiable on `[a, b]`
with `F' = f ∈ ℛ` and `G' = g ∈ ℛ`, then
`∫ₐᵇ F g dx = F b G b - F a G a - ∫ₐᵇ f G dx`. -/
theorem ch06_integration_by_parts (a b : ℝ) (hab : a ≤ b) (F G f g : ℝ → ℝ)
    (hF : ∀ x ∈ Set.Icc a b, HasDerivAt F (f x) x)
    (hG : ∀ x ∈ Set.Icc a b, HasDerivAt G (g x) x)
    (hf : RiemannIntegrable a b f) (hg : RiemannIntegrable a b g) :
    RiemannIntegral a b (fun x => F x * g x) =
      F b * G b - F a * G a - RiemannIntegral a b (fun x => f x * G x) := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 6, p. 134, Theorem 6.22

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Let $a \le b$ and let $F, G, f, g : \mathbb{R}\to\mathbb{R}$ satisfy:

at every $x \in [a,b]$ , $F$ is differentiable with derivative $f(x)$ ;
at every $x \in [a,b]$ , $G$ is differentiable with derivative $g(x)$ ;
$f$ is Riemann integrable on $[a,b]$ and $g$ is Riemann integrable on $[a,b]$ (in the sense of this bundle: upper integral $=$ lower integral with integrator the identity).

Then

\int_a^b F(x)\,g(x)\,dx \;=\; F(b)G(b) - F(a)G(a) - \int_a^b f(x)\,G(x)\,dx ,

where each integral denotes the corresponding upper integral over $[a,b]$ with integrator the identity. Integrability of the two products $Fg$ and $fG$ is not asserted; the equation is between the values as defined. The differentiability hypotheses are two-sided and imposed at the endpoints as well.

Human review

Endorsed by Community (Bot) · Sep 14, 2026
Endorsed by Lucas · Sep 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph