Riemann integration and definite integrals

The Riemann integral via tagged partitions, iterated-integral formulas, moments, and closed-form evaluations of specific definite integrals (Serret's integral, integrals of 1/(1+u^n), areas between cosine powers, sinc squared); integrals defining a named special function go to Special functions.

TheoremA function continuous on \((0,1)\) with vanishing moments is zero on \((0,1)\)#●ready to prove

Let \(f : \mathbb{R} \to \mathbb{R}\) be continuous on \([0,1]\), and suppose that \(\int_0^1 f(x)\,x^n\,dx = 0\) for every natural number \(n = 0, 1, 2, \dots\). Then \(f(x) = 0\) for every \(x \in [0,1]\).

public theorem_wanted eqOn_zero_of_integral_mul_pow_eq_zero
    (f : ℝ → ℝ) (hf : ContinuousOn f (Set.Icc 0 1))
    (h : ∀ n : ℕ, (∫ x in 0..1, f x * x ^ n) = 0) :
    Set.EqOn f 0 (Set.Icc 0 1)
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of one variable), problem ma_proofbench_l1_51.

TheoremBhandari's arcsine-over-sine integral#✓fully proved

Let \(G = \sum_{n \ge 0} (-1)^n/(2n+1)^2\) be Catalan's constant, and for \(s > 0\) let \(S_s = \sum_{n \ge 0} 1/(n + s)^2\). Then the integral \(\int_0^{\pi/2} \frac{\arcsin(\sin^2 x)}{\sin x}\,dx\) equals \(-2G - \frac{\pi^2}{2\sqrt 2} + \frac{S_{1/8} + S_{3/8}}{8\sqrt 2}\).

The series \(S_{1/8}\) and \(S_{3/8}\) are the trigamma values \(\psi_1(1/8)\) and \(\psi_1(3/8)\); Catalan's constant and these trigamma values are written out as their defining series.

Proof: The route follows Bhandari's reduction to log-tangent integrals, followed by an Abel-regularized Fourier expansion and residue-class evaluation.

public theorem arcsin_div_sin_integral : ∫ x in (0 : ℝ)..(Real.pi / 2), Real.arcsin
  ((Real.sin x) ^ 2) / Real.sin x = -2 * tsum
  (fun n : ℕ => (-1 : ℝ) ^ n / ((2 * (n : ℝ) + 1) ^ 2)) - Real.pi ^ 2 / (2 * Real.sqrt 2) + 1 /
  (8 * Real.sqrt 2) *
  (tsum (fun n : ℕ => (1 : ℝ) / (((n : ℝ) + (1 / 8 : ℝ)) ^ 2)) + tsum
  (fun n : ℕ => (1 : ℝ) / (((n : ℝ) + (3 / 8 : ℝ)) ^ 2)))
Sources

TheoremCauchy's formula for the twice-iterated integral#●ready to prove

Let \(E\) be a real Banach space, let \(\alpha \le \beta\) be real numbers and let \(f : \mathbb{R} \to E\) be continuous on \([\alpha, \beta]\). Then for every \(s \in [\alpha, \beta]\),

\[\int_\alpha^s \Bigl(\int_\alpha^t f(\tau)\,d\tau\Bigr)\,dt = \int_\alpha^s (s - t)\, f(t)\,dt.\]
public theorem_wanted intervalIntegral_intervalIntegral_eq_integral_sub_smul
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    {α β : ℝ} (hαβ : α ≤ β) (f : ℝ → E) (hf : ContinuousOn f (Set.Icc α β)) :
    ∀ s ∈ Set.Icc α β,
      (∫ t in α..s, (∫ τ in α..t, f τ))
        = (∫ t in α..s, (s - t) • f t)
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of one variable), problem ma_proofbench_l1_44.

TheoremIntegral of \(1/(a + b\cos\theta)\) over a period#●ready to prove

Let \(a\) and \(b\) be real numbers with \(a > |b|\). Then

\[\int_0^{2\pi} \frac{d\theta}{a + b\cos\theta} = \frac{2\pi}{\sqrt{a^2 - b^2}}.\]
public theorem_wanted integral_one_div_add_mul_cos_eq (a b : ℝ) (hab : a > |b|) :
    (∫ θ in 0..(2 * Real.pi), (1 / (a + b * Real.cos θ))) =
      (2 * Real.pi) / Real.sqrt (a ^ 2 - b ^ 2)
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Functions of a complex variable; General properties of functions of one complex variable), problem ma_proofbench_l1_89.

TheoremIntegral of the squared sinc function over the half-line#●ready to prove

The integral of \((\sin x / x)^2\) over \((0, \infty)\) is \(\pi/2\):

\[\int_0^\infty \left(\frac{\sin x}{x}\right)^2 dx = \frac{\pi}{2}.\]
public theorem_wanted integral_sin_div_sq_Ioi_eq_pi_div_two :
    ∫ x in Set.Ioi (0 : ℝ), (Real.sin x / x) ^ 2 = Real.pi / 2
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of one variable), problem ma_proofbench_l1_35.

TheoremSerret's integral#●ready to prove

With \(\log\) the natural logarithm,

\[\int_0^1 \frac{\log(1+x)}{1+x^2}\,dx = \frac{\pi}{8}\log 2.\]
public theorem_wanted integral_log_one_add_div_one_add_sq
    : (∫ x in 0..1, Real.log (1 + x) / (1 + x ^ 2))
      =
    (Real.pi / 8) * Real.log 2
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of one variable), problem ma_proofbench_l1_58.

TheoremThe integral of \(x f(x) f'(x)\) equals \(-1/2\)#●ready to prove

Let \(a\lt b\) and let \(f : \mathbb{R} \to \mathbb{R}\) be continuously differentiable on \([a,b]\) with \(f(a)=f(b)=0\) and

\[ \int_a^b f(x)^2\,dx=1. \]

Then

\[ \int_a^b x\,f(x)\,f'(x)\,dx=-\frac12. \]
public theorem_wanted integral_mul_mul_deriv_eq_neg_half {a b : ℝ} (hab : a < b) {f : ℝ → ℝ}
    (hf : ContDiffOn ℝ 1 f (Set.Icc a b))
    (hfa : f a = 0) (hfb : f b = 0)
    (hnorm : (∫ x in a..b, (f x) ^ 2) = 1) :
    (∫ x in a..b, x * f x * deriv f x) = (-(1 / 2 : ℝ))
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of one variable), problem ma_proofbench_l1_16.

TheoremUniformly continuous integrable functions vanish at infinity#●ready to prove

Let \(f : \mathbb{R} \to \mathbb{R}\) be uniformly continuous and Lebesgue integrable on \(\mathbb{R}\). Then \(f(x) \to 0\) as \(|x| \to \infty\).

public theorem_wanted UniformContinuous.tendsto_cocompact_zero_of_integrable
    (f : ℝ → ℝ) (hfuc : UniformContinuous f) (hint : MeasureTheory.Integrable f) :
    Tendsto f (comap (fun x : ℝ => ‖x‖) atTop) (𝓝 0)
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of one variable), problem ma_proofbench_l1_48.

TheoremUnit-window bound for the integral of \(\sin(t^2)\)#●ready to prove

Let \(f : \mathbb{R} \to \mathbb{R}\) be given by \(f(x) = \int_x^{x+1} \sin(t^2)\,dt\). Then \(|f(x)| < 1/x\) for every real \(x > 0\).

public theorem_wanted abs_integral_sin_sq_lt_inv (f : ℝ → ℝ)
    (hf : f = fun x : ℝ => ∫ t in x..(x + 1), Real.sin (t ^ 2))
    (x : ℝ) (hx : 0 < x) :
    |f x| < 1 / x
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of one variable), problem ma_proofbench_l1_29.
1 fully proved8 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.