Volterra operator

AbbreviationThe domain of the Volterra operator#✓fully proved

The space on which the Volterra operator acts is the space of bounded continuous real functions on \([0, 1]\), with the sup norm.

abbrev VolterraSpace := Set.Icc (0 : ℝ) 1 →ᵇ ℝ
Used by 18
Used byThe clamped extension is bounded by the sup norm · The Volterra operator has norm at most one · Factorial bound for powers of the Volterra operator · The Volterra operator is not invertible · Pointwise factorial bound for powers of the Volterra operator · The spectral radius of the Volterra operator is zero · Extension by clamping · The clamped extension agrees with the original function on the unit interval · The clamped extension is continuous · The Volterra operator as a linear map · Sup-norm bound for the Volterra linear map · The Volterra operator · Evaluation formula for the Volterra operator · Volterra integrals vanish at the left endpoint · Nonzero reals lie in the resolvent set of the Volterra operator · The spectrum of the Volterra operator is {0} · Continuity of the Volterra primitive · Sup-norm bound for the Volterra primitive

DefinitionClamping to the unit interval#✓fully proved

For a real number \(t\), its clamp to the unit interval is \(\max(0, \min(t, 1))\), regarded as a point of \([0, 1]\).

def clamp01 (t : ℝ) : Set.Icc (0 : ℝ) 1 :=
  ⟨max 0 (min t 1), le_max_left _ _, max_le zero_le_one (min_le_right _ _)⟩
Used by 5
Used byThe clamped extension is bounded by the sup norm · Extension by clamping · The clamped extension agrees with the original function on the unit interval · The clamped extension is continuous · The Volterra operator as a linear map

DefinitionExtension by clamping#✓fully proved

For a bounded continuous real function \(f\) on \([0, 1]\), its extension to \(\mathbb{R}\) is the function \(t \mapsto f(\max(0, \min(t, 1)))\).

This continuous extension is used to write \((Vf)(x)\), for \(V\) the Volterra operator, as an interval integral over \(\mathbb{R}\).

def volterraExtend (f : VolterraSpace) : ℝ → ℝ :=
  fun t => f (clamp01 t)
Uses 2 · Used by 10
Statement usesThe domain of the Volterra operator · Clamping to the unit interval
Used byThe clamped extension is bounded by the sup norm · Pointwise factorial bound for powers of the Volterra operator · The clamped extension agrees with the original function on the unit interval · The clamped extension is continuous · The Volterra operator as a linear map · Sup-norm bound for the Volterra linear map · Evaluation formula for the Volterra operator · Volterra integrals vanish at the left endpoint · Continuity of the Volterra primitive · Sup-norm bound for the Volterra primitive

TheoremThe clamped extension is continuous#✓fully proved

For every bounded continuous real function \(f\) on \([0, 1]\), its extension \(t \mapsto f(\max(0, \min(t, 1)))\) to \(\mathbb{R}\) by clamping is continuous on \(\mathbb{R}\).

theorem volterraExtend_continuous (f : VolterraSpace) :
    Continuous (volterraExtend f)
Uses 3 · Used by 4
Statement usesThe domain of the Volterra operator · Extension by clamping
Proof usesClamping to the unit interval
Used byPointwise factorial bound for powers of the Volterra operator · The Volterra operator as a linear map · Continuity of the Volterra primitive · Sup-norm bound for the Volterra primitive

TheoremThe clamped extension agrees with the original function on the unit interval#✓fully proved

For every bounded continuous real function \(f\) on \([0, 1]\) and every real \(t\) with \(0 \le t \le 1\), the extension \(s \mapsto f(\max(0, \min(s, 1)))\) of \(f\) to \(\mathbb{R}\) takes the value \(f(t)\) at \(t\).

theorem volterraExtend_apply_of_mem {f : VolterraSpace} {t : ℝ} (ht : t ∈ Set.Icc (0 : ℝ) 1) :
    volterraExtend f t = f ⟨t, ht⟩
Uses 3 · Used by 1
Statement usesThe domain of the Volterra operator · Extension by clamping
Proof usesClamping to the unit interval
Used byPointwise factorial bound for powers of the Volterra operator

TheoremThe clamped extension is bounded by the sup norm#✓fully proved

For every bounded continuous real function \(f\) on \([0, 1]\) and every real \(t\), the extension of \(f\) to \(\mathbb{R}\) by clamping satisfies \(|f(\max(0, \min(t, 1)))| \le \|f\|_\infty\), where \(\|f\|_\infty = \sup_{x \in [0, 1]} |f(x)|\) is the sup norm of \(f\).

theorem norm_volterraExtend_le (f : VolterraSpace) (t : ℝ) :
    ‖volterraExtend f t‖ ≤ ‖f‖
Uses 3 · Used by 1
Statement usesThe domain of the Volterra operator · Extension by clamping
Proof usesClamping to the unit interval
Used bySup-norm bound for the Volterra primitive

TheoremContinuity of the Volterra primitive#✓fully proved

For every bounded continuous real function \(f\) on \([0, 1]\), the function \(x \mapsto \int_0^x \tilde f(t)\,dt\) on \([0, 1]\) is continuous, where \(\tilde f(t) = f(\max(0, \min(t, 1)))\) is the extension of \(f\) to \(\mathbb{R}\) by clamping the argument into \([0, 1]\).

theorem volterraPrimitive_continuous (f : VolterraSpace) :
    Continuous (fun x : Set.Icc (0 : ℝ) 1 => ∫ t in (0 : ℝ)..(x : ℝ), volterraExtend f t)
Uses 3 · Used by 2
Statement usesThe domain of the Volterra operator · Extension by clamping
Proof usesThe clamped extension is continuous
Used byThe Volterra operator as a linear map · Sup-norm bound for the Volterra linear map

TheoremSup-norm bound for the Volterra primitive#✓fully proved

For every bounded continuous real function \(f\) on \([0, 1]\) and every \(x \in [0, 1]\), \(\left|\int_0^x \tilde f(t)\,dt\right| \le \|f\|\), where \(\|f\|\) is the sup norm of \(f\) and \(\tilde f(t) = f(\max(0, \min(t, 1)))\) is the extension of \(f\) to \(\mathbb{R}\) by clamping the argument into \([0, 1]\).

theorem volterraPrimitive_norm_le (f : VolterraSpace) (x : Set.Icc (0 : ℝ) 1) :
    ‖∫ t in (0 : ℝ)..(x : ℝ), volterraExtend f t‖ ≤ ‖f‖
Uses 4 · Used by 2
Statement usesThe domain of the Volterra operator · Extension by clamping
Proof usesThe clamped extension is bounded by the sup norm · The clamped extension is continuous
Used byThe Volterra operator as a linear map · Sup-norm bound for the Volterra linear map

DefinitionThe Volterra operator as a linear map#✓fully proved

The real-linear map \(V\) on the space of bounded continuous real functions on \([0, 1]\) given by \((Vf)(x) = \int_0^x f(t)\,dt\) for \(x \in [0, 1]\).

MathlibExt.Analysis.FunctionalAnalysis.VolterraOperator.volterraLinearMap · 28 lines 
noncomputable def volterraLinearMap : VolterraSpace →ₗ[ℝ] VolterraSpace where
  toFun f :=
    BoundedContinuousFunction.ofNormedAddCommGroup
      (fun x => ∫ t in (0 : ℝ)..(x : ℝ), volterraExtend f t)
      (volterraPrimitive_continuous f) ‖f‖ (volterraPrimitive_norm_le f)
  map_add' f g := by
    apply BoundedContinuousFunction.ext
    intro x
    have hfun : (fun t => volterraExtend (f + g) t)
        = fun t => volterraExtend f t + volterraExtend g t := by
      funext t
      simp [volterraExtend]
    simp only [BoundedContinuousFunction.coe_ofNormedAddCommGroup, hfun,
      BoundedContinuousFunction.add_apply]
    rw [intervalIntegral.integral_add
      ((volterraExtend_continuous f).intervalIntegrable _ _)
      ((volterraExtend_continuous g).intervalIntegrable _ _)]
  map_smul' c f := by
    apply BoundedContinuousFunction.ext
    intro x
    have hfun : (fun t => volterraExtend (c • f) t)
        = fun t => c • volterraExtend f t := by
      funext t
      simp [volterraExtend]
    simp only [BoundedContinuousFunction.coe_ofNormedAddCommGroup, hfun,
      BoundedContinuousFunction.smul_apply]
    rw [intervalIntegral.integral_smul]
    rfl
Uses 6 · Used by 3
Statement usesThe domain of the Volterra operator · Clamping to the unit interval · Extension by clamping · The clamped extension is continuous · Continuity of the Volterra primitive · Sup-norm bound for the Volterra primitive
Used byThe Volterra operator has norm at most one · Sup-norm bound for the Volterra linear map · The Volterra operator

TheoremSup-norm bound for the Volterra linear map#✓fully proved

For every bounded continuous real function \(f\) on \([0, 1]\), the Volterra linear map \(V\) satisfies \(\|Vf\| \le 1 \cdot \|f\|\), where \(\|\cdot\|\) is the sup norm.

theorem volterraLinearMap_norm_le (f : VolterraSpace) :
    ‖volterraLinearMap f‖ ≤ 1 * ‖f‖
Uses 5 · Used by 2
Statement usesThe domain of the Volterra operator · The Volterra operator as a linear map
Proof usesExtension by clamping · Continuity of the Volterra primitive · Sup-norm bound for the Volterra primitive
Used byThe Volterra operator has norm at most one · The Volterra operator

DefinitionThe Volterra operator#✓fully proved

The bounded real-linear operator \(V\) on the space of bounded continuous real functions on \([0, 1]\) (equivalently \(C([0, 1], \mathbb{R})\) with the sup norm) given by \((Vf)(x) = \int_0^x f(t)\,dt\) for \(x \in [0, 1]\).

noncomputable def volterraOperator : VolterraSpace →L[ℝ] VolterraSpace :=
  volterraLinearMap.mkContinuous 1 volterraLinearMap_norm_le
Uses 3 · Used by 9
Statement usesThe domain of the Volterra operator · The Volterra operator as a linear map · Sup-norm bound for the Volterra linear map
Used byThe Volterra operator has norm at most one · Factorial bound for powers of the Volterra operator · The Volterra operator is not invertible · Pointwise factorial bound for powers of the Volterra operator · The spectral radius of the Volterra operator is zero · Evaluation formula for the Volterra operator · Volterra integrals vanish at the left endpoint · Nonzero reals lie in the resolvent set of the Volterra operator · The spectrum of the Volterra operator is {0}

TheoremEvaluation formula for the Volterra operator#✓fully proved

For every bounded continuous real function \(f\) on \([0, 1]\) and every \(x \in [0, 1]\), the Volterra operator \(V\) satisfies \((Vf)(x) = \int_0^x \tilde f(t)\,dt\), where \(\tilde f(t) = f(\max(0, \min(t, 1)))\) is the extension of \(f\) to \(\mathbb{R}\) by clamping the argument into \([0, 1]\).

theorem volterraOperator_apply (f : VolterraSpace) (x : Set.Icc (0 : ℝ) 1) :
    (volterraOperator f) x = ∫ t in (0 : ℝ)..(x : ℝ), volterraExtend f t
Uses 3 · Used by 2
Statement usesThe domain of the Volterra operator · Extension by clamping · The Volterra operator
Used byPointwise factorial bound for powers of the Volterra operator · Volterra integrals vanish at the left endpoint

TheoremVolterra integrals vanish at the left endpoint#✓fully proved

For every bounded continuous real function \(f\) on \([0, 1]\), the Volterra operator \(V\) satisfies \((Vf)(0) = 0\).

theorem volterraOperator_apply_zero (f : VolterraSpace) :
    (volterraOperator f) ⟨0, le_refl 0, zero_le_one⟩ = 0
Uses 4 · Used by 1
Statement usesThe domain of the Volterra operator · The Volterra operator
Proof usesExtension by clamping · Evaluation formula for the Volterra operator
Used byThe Volterra operator is not invertible

TheoremThe Volterra operator has norm at most one#✓fully proved

The Volterra operator \(V\), \((Vf)(x) = \int_0^x f(t)\,dt\), acting on the space of bounded continuous real functions on \([0, 1]\) with the sup norm, has operator norm \(\|V\| \le 1\).

theorem norm_volterraOperator_le_one : ‖volterraOperator‖ ≤ 1
Uses 4
Statement usesThe domain of the Volterra operator · The Volterra operator
Proof usesThe Volterra operator as a linear map · Sup-norm bound for the Volterra linear map

TheoremPointwise factorial bound for powers of the Volterra operator#✓fully proved

Let \(V\) be the Volterra operator \((Vf)(x) = \int_0^x f(t)\,dt\) on the space of bounded continuous real functions on \([0, 1]\). For every natural number \(n\), every such function \(f\) and every \(x \in [0, 1]\), \(|(V^n f)(x)| \le \frac{x^n}{n!} \|f\|_\infty\), where \(\|f\|_\infty\) is the sup norm of \(f\).

theorem pow_volterraOperator_apply_norm_le (n : ℕ) (f : VolterraSpace)
    (x : Set.Icc (0 : ℝ) 1) :
    ‖((volterraOperator ^ n) f) x‖ ≤ ((x : ℝ) ^ n / (Nat.factorial n)) * ‖f‖
Uses 6 · Used by 1
Statement usesThe domain of the Volterra operator · The Volterra operator
Proof usesExtension by clamping · The clamped extension agrees with the original function on the unit interval · The clamped extension is continuous · Evaluation formula for the Volterra operator
Used byFactorial bound for powers of the Volterra operator

TheoremFactorial bound for powers of the Volterra operator#✓fully proved

Let \(V\) be the Volterra operator \((Vf)(x) = \int_0^x f(t)\,dt\) on the space of bounded continuous real functions on \([0, 1]\) with the sup norm. For every natural number \(n\), the operator norm of \(V^n\) satisfies \(\|V^n\| \le 1/n!\).

theorem norm_volterraOperator_pow_le (n : ℕ) : ‖volterraOperator ^ n‖ ≤ 1 / (Nat.factorial n)
Uses 3 · Used by 1
Statement usesThe domain of the Volterra operator · The Volterra operator
Proof usesPointwise factorial bound for powers of the Volterra operator
Used byNonzero reals lie in the resolvent set of the Volterra operator

TheoremNonzero reals lie in the resolvent set of the Volterra operator#✓fully proved

For every nonzero real \(z\), \(z\) lies in the real resolvent set of the Volterra operator \(V\): the bounded operator \(z - V\) is invertible.

The operator \(z - V\) is bijective, with inverse given by the Neumann series \(g \mapsto \sum_{n \ge 0} z^{-(n+1)} V^n g\).

theorem volterraOperator_mem_resolventSet_of_ne_zero {z : ℝ} (hz : z ≠ 0) :
    z ∈ resolventSet ℝ volterraOperator
Uses 3 · Used by 1
Statement usesThe domain of the Volterra operator · The Volterra operator
Proof usesFactorial bound for powers of the Volterra operator
Used byThe spectrum of the Volterra operator is {0}

TheoremThe Volterra operator is not invertible#✓fully proved

The Volterra operator \(V\), \((Vf)(x) = \int_0^x f(t)\,dt\), on the space of bounded continuous real functions on \([0, 1]\) is not a unit in the algebra of bounded linear operators on that space.

The reason is that \((Vf)(0) = 0\) for every \(f\), so \(V\) is not surjective.

theorem not_isUnit_volterraOperator : ¬ IsUnit volterraOperator
Uses 3 · Used by 1
Statement usesThe domain of the Volterra operator · The Volterra operator
Proof usesVolterra integrals vanish at the left endpoint
Used byThe spectrum of the Volterra operator is {0}

TheoremThe spectrum of the Volterra operator is {0}#✓fully proved

The spectrum of the Volterra operator is {0}.

theorem volterraOperator_spectrum : spectrum ℝ volterraOperator = {0}
Uses 4 · Used by 1
Statement usesThe domain of the Volterra operator · The Volterra operator
Proof usesThe Volterra operator is not invertible · Nonzero reals lie in the resolvent set of the Volterra operator
Used byThe spectral radius of the Volterra operator is zero

TheoremThe spectral radius of the Volterra operator is zero#✓fully proved

Let \(V\) be the Volterra operator \((Vf)(x) = \int_0^x f(t)\,dt\) on the space of bounded continuous real functions on \([0, 1]\). Its spectral radius over the real scalars, the supremum of \(|z|\) over real \(z\) in the spectrum of \(V\), is \(0\).

theorem spectralRadius_volterraOperator : spectralRadius ℝ volterraOperator = 0
Uses 3
Statement usesThe domain of the Volterra operator · The Volterra operator
Proof usesThe spectrum of the Volterra operator is {0}

TheoremExpansion of \((XV)^n\) in Bessel numbers#●ready to prove

Let \(X\) and \(V\) be the operators on functions \(\mathbb{R} \to \mathbb{R}\) given by \((Xg)(y) = y \, g(y)\) and \((Vg)(y) = \int_0^y g(t) \, dt\), write \((XV)^n\) and \(V^m\) for iterated composition, and let \(a(m, k)\) be the coefficient of \(x^k\) in the Bessel polynomial \(y_m\). For every natural number \(n \ge 1\), every continuous function \(f : \mathbb{R} \to \mathbb{R}\) and every real number \(x\),

\[(XV)^n f(x) = \sum_{k=0}^{n-1} (-1)^k \, a(n-1, k) \, x^{n-k} \, (V^{n+k} f)(x).\]
public theorem_wanted xMul_volterra_iterate_eq_sum_bessel (n : ℕ) (hn : 1 ≤ n) (f : ℝ → ℝ)
    (hf : Continuous f) (x : ℝ) :
    (fun g : ℝ → ℝ => fun y => y * ∫ t in (0 : ℝ)..y, g t)^[n] f x =
      ∑ k ∈ Finset.range n, (-1 : ℝ) ^ k * ((besselPolynomial (n - 1)).coeff k : ℝ) *
        x ^ (n - k) * (fun g : ℝ → ℝ => fun y => ∫ t in (0 : ℝ)..y, g t)^[n + k] f x
Sources
  • Abdelhay Benmoussa, On the Expansion of (XV)^n and Bessel Numbers, Journal of Integer Sequences 29 (2026), Article 26.3.5, Theorem 1 (jis-2026-26.3.5-thm-1).
Uses 1
Statement usesBessel polynomial
20 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.