The integral of a 1-periodic function over [0, k] is k times its integral over one period, without integrability assumptions

Proved

Function.Periodic.intervalIntegral_zero_natCast_eq

by Mazecto · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysis

Let $E$ be a real normed space and $g:\mathbb{R}\to E$ a $1$ -periodic function. Then for every natural number $k$ ,

\int_0^k g(x)\,dx = k\int_0^1 g(x)\,dx.

No integrability hypothesis is assumed. Integrals are Bochner interval integrals, which are $0$ for non-integrable functions.

Preamble

import Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Formal statement

theorem Function.Periodic.intervalIntegral_zero_natCast_eq {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {g : ℝ → E} (hg : Function.Periodic g 1) (k : ℕ) :
    ∫ x in (0 : ℝ)..(k : ℝ), g x = (k : ℝ) • ∫ x in (0 : ℝ)..1, g x := by sorry

Source

Elementary. Used to scale the Gauss linking integral under k-fold covers of a loop (HryniewiczCriterion.gaussLinkingIntegral_comp_mul_nat), for U. Hryniewicz, arXiv:1105.2077, Lemma 3.12.

View graph