Integral operators with continuous kernels

AbbreviationContinuous functions on the unit interval#✓fully proved

\(C([0, 1], \mathbb{R})\) denotes the space of bounded continuous functions \([0, 1] \to \mathbb{R}\), with the supremum norm \(\|f\| = \sup_{x \in [0, 1]} |f(x)|\).

abbrev KernelSpace := Set.Icc (0 : ℝ) 1 →ᵇ ℝ

Used by 21

Used byJoint continuity of the kernel integrand · Separable kernels give finite-rank integral operators · Integral operators with continuous kernels are compact · Clamped extension · The clamped extension agrees with the function on \((0, 1)\) · Continuity of the clamped extension · Kernel integrand · Continuity of the kernel integrand in \(t\) · The integral operator with continuous kernel, as a linear map · Sup-norm bound for the integral operator with continuous kernel · Integral operator with a continuous kernel · The integral operator is additive in the kernel · Evaluation formula for the integral operator · The integral operator is homogeneous in the kernel · The zero kernel gives the zero operator · Kernel value · Continuity of the kernel value · The clamped extension is bounded by the supremum norm · Difference bound for the values of a kernel operator · Norm bound for a kernel integral operator · Pointwise bound for a kernel integral

AbbreviationContinuous kernels on the unit square#✓fully proved

A continuous kernel is a bounded continuous function \(k : [0, 1] \times [0, 1] \to \mathbb{R}\). These kernels form a normed space under the supremum norm \(\|k\| = \sup_{x, y \in [0, 1]} |k(x, y)|\).

abbrev KernelType := (Set.Icc (0 : ℝ) 1 × Set.Icc (0 : ℝ) 1) →ᵇ ℝ

Used by 17

Used byJoint continuity of the kernel integrand · Separable kernels give finite-rank integral operators · Integral operators with continuous kernels are compact · Kernel integrand · Continuity of the kernel integrand in \(t\) · The integral operator with continuous kernel, as a linear map · Sup-norm bound for the integral operator with continuous kernel · Integral operator with a continuous kernel · The integral operator is additive in the kernel · Evaluation formula for the integral operator · The integral operator is homogeneous in the kernel · The zero kernel gives the zero operator · Kernel value · Continuity of the kernel value · Difference bound for the values of a kernel operator · Norm bound for a kernel integral operator · Pointwise bound for a kernel integral

DefinitionClamped extension#✓fully proved

For a bounded continuous function \(f\) on \([0, 1]\), its clamped extension is the function \(\tilde f : \mathbb{R} \to \mathbb{R}\) given by \(\tilde f(t) = f(\max(0, \min(1, t)))\). Thus \(\tilde f(t) = f(0)\) for \(t < 0\), \(\tilde f(t) = f(t)\) for \(t \in [0, 1]\), and \(\tilde f(t) = f(1)\) for \(t > 1\).

def kernelExtend (f : KernelSpace) : ℝ → ℝ :=
  fun t => f (Set.projIcc 0 1 zero_le_one t)

Uses 1 · Used by 11

Statement usesContinuous functions on the unit interval

Used byJoint continuity of the kernel integrand · Separable kernels give finite-rank integral operators · The clamped extension agrees with the function on \((0, 1)\) · Continuity of the clamped extension · Kernel integrand · The integral operator is additive in the kernel · The integral operator is homogeneous in the kernel · The zero kernel gives the zero operator · The clamped extension is bounded by the supremum norm · Difference bound for the values of a kernel operator · Pointwise bound for a kernel integral

TheoremContinuity of the clamped extension#✓fully proved

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

theorem kernelExtend_continuous (f : KernelSpace) : Continuous (kernelExtend f)

Uses 2 · Used by 3

Statement usesContinuous functions on the unit interval · Clamped extension

Used byJoint continuity of the kernel integrand · Separable kernels give finite-rank integral operators · Difference bound for the values of a kernel operator

TheoremThe clamped extension agrees with the function on \((0, 1)\)#✓fully proved

Let \(f\) be a bounded continuous function on \([0, 1]\) and let \(\tilde f(s) = f(\max(0, \min(1, s)))\) for real \(s\) be its clamped extension. Then \(\tilde f(t) = f(t)\) for every \(t \in [0, 1]\).

theorem kernelExtend_apply_of_mem {f : KernelSpace} {t : ℝ} (ht : t ∈ Set.Icc (0 : ℝ) 1) :
    kernelExtend f t = f ⟨t, ht⟩

Uses 2

Statement usesContinuous functions on the unit interval · Clamped extension

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

Let \(\pi(t) = \max(0, \min(1, t))\) be the projection of \(\mathbb{R}\) onto \([0, 1]\). For every \(f \in C([0, 1], \mathbb{R})\) and every \(t \in \mathbb{R}\), the clamped extension \(f \circ \pi\) of \(f\) satisfies \(|f(\pi(t))| \le \|f\|\), where \(\|f\|\) is the supremum norm.

theorem norm_kernelExtend_le (f : KernelSpace) (t : ℝ) : ‖kernelExtend f t‖ ≤ ‖f‖

Uses 2 · Used by 2

Statement usesContinuous functions on the unit interval · Clamped extension

Used byDifference bound for the values of a kernel operator · Pointwise bound for a kernel integral

DefinitionKernel integrand#✓fully proved

Let \(\pi(t) = \max(0, \min(1, t))\) clamp a real number \(t\) to \([0, 1]\). For a continuous kernel \(k\) on \([0, 1] \times [0, 1]\), a bounded continuous function \(f\) on \([0, 1]\) and a point \(x \in [0, 1]\), the kernel integrand is the function \(\mathbb{R} \to \mathbb{R}\), \(t \mapsto k(x, \pi(t)) \, f(\pi(t))\).

def kernelIntegrand (k : KernelType) (f : KernelSpace) (x : Set.Icc (0 : ℝ) 1) :
    ℝ → ℝ :=
  fun t => k (x, Set.projIcc 0 1 zero_le_one t) * kernelExtend f t

Uses 3 · Used by 12

Statement usesContinuous functions on the unit interval · Continuous kernels on the unit square · Clamped extension

Used byJoint continuity of the kernel integrand · Separable kernels give finite-rank integral operators · Continuity of the kernel integrand in \(t\) · The integral operator with continuous kernel, as a linear map · The integral operator is additive in the kernel · Evaluation formula for the integral operator · The integral operator is homogeneous in the kernel · The zero kernel gives the zero operator · Kernel value · Continuity of the kernel value · Difference bound for the values of a kernel operator · Pointwise bound for a kernel integral

TheoremJoint continuity of the kernel integrand#✓fully proved

Let \(\pi(t) = \max(0, \min(1, t))\) clamp a real number \(t\) to \([0, 1]\). For every continuous kernel \(k\) on \([0, 1] \times [0, 1]\) and every bounded continuous function \(f\) on \([0, 1]\), the kernel integrand \((x, t) \mapsto k(x, \pi(t)) \, f(\pi(t))\) is jointly continuous on \([0, 1] \times \mathbb{R}\).

theorem continuous_kernelIntegrand_uncurry (k : KernelType) (f : KernelSpace) :
    Continuous (Function.uncurry (kernelIntegrand k f))

Uses 5 · Used by 2

Statement usesContinuous functions on the unit interval · Continuous kernels on the unit square · Kernel integrand

Proof usesClamped extension · Continuity of the clamped extension

Used byContinuity of the kernel integrand in \(t\) · Continuity of the kernel value

TheoremContinuity of the kernel integrand in \(t\)#✓fully proved

Let \(\pi(t) = \max(0, \min(1, t))\) clamp a real number \(t\) to \([0, 1]\). For every continuous kernel \(k\) on \([0, 1] \times [0, 1]\), every bounded continuous function \(f\) on \([0, 1]\) and every \(x \in [0, 1]\), the function \(t \mapsto k(x, \pi(t)) \, f(\pi(t))\) is continuous on \(\mathbb{R}\).

theorem kernelIntegrand_continuous (k : KernelType) (f : KernelSpace)
    (x : Set.Icc (0 : ℝ) 1) : Continuous (kernelIntegrand k f x)

Uses 4 · Used by 4

Statement usesContinuous functions on the unit interval · Continuous kernels on the unit square · Kernel integrand

Proof usesJoint continuity of the kernel integrand

Used byThe integral operator with continuous kernel, as a linear map · The integral operator is additive in the kernel · Difference bound for the values of a kernel operator · Pointwise bound for a kernel integral

DefinitionKernel value#✓fully proved

Let \(\pi(t) = \max(0, \min(1, t))\) be the projection of \(\mathbb{R}\) onto \([0, 1]\). For a continuous kernel \(k\) on \([0, 1] \times [0, 1]\), a function \(f \in C([0, 1], \mathbb{R})\) and a point \(x \in [0, 1]\), the kernel value is the real number

\[\int_0^1 k(x, \pi(t))\, f(\pi(t))\, dt.\]

Since \(\pi(t) = t\) for \(t \in [0, 1]\), it equals \(\int_0^1 k(x, t)\, f(t)\, dt\), the value at \(x\) of the integral operator with kernel \(k\) applied to \(f\).

def kernelValue (k : KernelType) (f : KernelSpace) (x : Set.Icc (0 : ℝ) 1) : ℝ :=
  ∫ t in (0 : ℝ)..1, kernelIntegrand k f x t

Uses 3 · Used by 4

Statement usesContinuous functions on the unit interval · Continuous kernels on the unit square · Kernel integrand

Used byThe integral operator with continuous kernel, as a linear map · Sup-norm bound for the integral operator with continuous kernel · Continuity of the kernel value · Pointwise bound for a kernel integral

TheoremContinuity of the kernel value#✓fully proved

For every continuous kernel \(k\) on \([0, 1] \times [0, 1]\) and every \(f \in C([0, 1], \mathbb{R})\), the kernel value of \(k\) and \(f\), the function \(x \mapsto \int_0^1 k(x, t)\, f(t)\, dt\) on \([0, 1]\), is continuous.

theorem kernelValue_continuous (k : KernelType) (f : KernelSpace) :
    Continuous (kernelValue k f)

Uses 5 · Used by 2

Statement usesContinuous functions on the unit interval · Continuous kernels on the unit square · Kernel value

Proof usesJoint continuity of the kernel integrand · Kernel integrand

Used byThe integral operator with continuous kernel, as a linear map · Sup-norm bound for the integral operator with continuous kernel

TheoremPointwise bound for a kernel integral#✓fully proved

Let \(k\) be a continuous kernel on \([0, 1] \times [0, 1]\) and let \(f \in C([0, 1], \mathbb{R})\). For every \(x \in [0, 1]\), the integral \(\int_0^1 k(x, t) \, f(t) \, dt\) has absolute value at most \(\|k\|_\infty \, \|f\|_\infty\).

theorem norm_kernelValue_le (k : KernelType) (f : KernelSpace)
    (x : Set.Icc (0 : ℝ) 1) : ‖kernelValue k f x‖ ≤ ‖k‖ * ‖f‖

Uses 7 · Used by 2

Statement usesContinuous functions on the unit interval · Continuous kernels on the unit square · Kernel value

Proof usesClamped extension · Kernel integrand · Continuity of the kernel integrand in \(t\) · The clamped extension is bounded by the supremum norm

Used byThe integral operator with continuous kernel, as a linear map · Sup-norm bound for the integral operator with continuous kernel

DefinitionThe integral operator with continuous kernel, as a linear map#✓fully proved

For a continuous kernel \(k\) on \([0, 1] \times [0, 1]\), this is the \(\mathbb{R}\)-linear map \(K\) from the space of bounded continuous real functions on \([0, 1]\) to itself given by \((Kf)(x) = \int_0^1 k(x, t) f(t) \, dt\) for \(x \in [0, 1]\).

MathlibExt.Analysis.FunctionalAnalysis.KernelOperator.kernelLinearMap · 26 lines

noncomputable def kernelLinearMap (k : KernelType) : KernelSpace →ₗ[ℝ] KernelSpace where
  toFun f :=
    BoundedContinuousFunction.ofNormedAddCommGroup (kernelValue k f)
      (kernelValue_continuous k f) (‖k‖ * ‖f‖) (norm_kernelValue_le k f)
  map_add' f g := by
    apply BoundedContinuousFunction.ext
    intro x
    show kernelValue k (f + g) x = kernelValue k f x + kernelValue k g x
    simp only [kernelValue]
    rw [← intervalIntegral.integral_add
      ((kernelIntegrand_continuous k f x).intervalIntegrable _ _)
      ((kernelIntegrand_continuous k g x).intervalIntegrable _ _)]
    congr 1
    funext t
    simp [kernelIntegrand, kernelExtend, mul_add]
  map_smul' c f := by
    apply BoundedContinuousFunction.ext
    intro x
    show kernelValue k (c • f) x = c • kernelValue k f x
    simp only [kernelValue]
    rw [← intervalIntegral.integral_smul]
    congr 1
    funext t
    simp only [kernelIntegrand, kernelExtend, BoundedContinuousFunction.smul_apply,
      smul_eq_mul]
    ring

Uses 7 · Used by 2

Statement usesContinuous functions on the unit interval · Continuous kernels on the unit square · Kernel integrand · Continuity of the kernel integrand in \(t\) · Kernel value · Continuity of the kernel value · Pointwise bound for a kernel integral

Used bySup-norm bound for the integral operator with continuous kernel · Integral operator with a continuous kernel

TheoremSup-norm bound for the integral operator with continuous kernel#✓fully proved

Write \(\|\cdot\|\) for the sup norm. For every continuous kernel \(k\) on \([0, 1] \times [0, 1]\) and every bounded continuous function \(f\) on \([0, 1]\), the function \(Kf\) given by \((Kf)(x) = \int_0^1 k(x, t) f(t) \, dt\) satisfies \(\|Kf\| \le \|k\| \, \|f\|\).

theorem kernelLinearMap_norm_le (k : KernelType) (f : KernelSpace) :
    ‖kernelLinearMap k f‖ ≤ ‖k‖ * ‖f‖

Uses 6 · Used by 3

Statement usesContinuous functions on the unit interval · Continuous kernels on the unit square · The integral operator with continuous kernel, as a linear map

Proof usesKernel value · Continuity of the kernel value · Pointwise bound for a kernel integral

Used byIntegral operators with continuous kernels are compact · Integral operator with a continuous kernel · Norm bound for a kernel integral operator

DefinitionIntegral operator with a continuous kernel#✓fully proved

For a continuous kernel \(k\) on \([0, 1] \times [0, 1]\), the integral operator \(T_k\) with kernel \(k\) is the continuous linear operator on \(C([0, 1], \mathbb{R})\) given, for \(f \in C([0, 1], \mathbb{R})\) and \(x \in [0, 1]\), by \((T_k f)(x) = \int_0^1 k(x, t)\, f(t)\, dt\).

noncomputable def kernelOperator (k : KernelType) : KernelSpace →L[ℝ] KernelSpace :=
  (kernelLinearMap k).mkContinuous ‖k‖ (kernelLinearMap_norm_le k)

Uses 4 · Used by 8

Statement usesContinuous functions on the unit interval · Continuous kernels on the unit square · The integral operator with continuous kernel, as a linear map · Sup-norm bound for the integral operator with continuous kernel

Used bySeparable kernels give finite-rank integral operators · Integral operators with continuous kernels are compact · The integral operator is additive in the kernel · Evaluation formula for the integral operator · The integral operator is homogeneous in the kernel · The zero kernel gives the zero operator · Difference bound for the values of a kernel operator · Norm bound for a kernel integral operator

TheoremEvaluation formula for the integral operator#✓fully proved

Let \(\pi(t) = \max(0, \min(1, t))\) be the projection of \(\mathbb{R}\) onto \([0, 1]\). For a continuous kernel \(k\) on \([0, 1] \times [0, 1]\), write \(T_k\) for the integral operator with kernel \(k\) on \(C([0, 1], \mathbb{R})\). For every \(f \in C([0, 1], \mathbb{R})\) and every \(x \in [0, 1]\),

\[(T_k f)(x) = \int_0^1 k(x, \pi(t))\, f(\pi(t))\, dt,\]

the integral over \([0, 1]\) of the kernel integrand. Since \(\pi(t) = t\) for \(t \in [0, 1]\), this is \(\int_0^1 k(x, t)\, f(t)\, dt\).

theorem kernelOperator_apply (k : KernelType) (f : KernelSpace)
    (x : Set.Icc (0 : ℝ) 1) :
    kernelOperator k f x = ∫ t in (0 : ℝ)..1, kernelIntegrand k f x t

Uses 4 · Used by 5

Statement usesContinuous functions on the unit interval · Continuous kernels on the unit square · Kernel integrand · Integral operator with a continuous kernel

Used bySeparable kernels give finite-rank integral operators · The integral operator is additive in the kernel · The integral operator is homogeneous in the kernel · The zero kernel gives the zero operator · Difference bound for the values of a kernel operator

TheoremNorm bound for a kernel integral operator#✓fully proved

For every continuous kernel \(k\) on \([0, 1] \times [0, 1]\), the integral operator \(K\) with kernel \(k\) on \(C([0, 1], \mathbb{R})\) has operator norm \(\|K\| \le \|k\|_\infty\).

theorem norm_kernelOperator_le (k : KernelType) : ‖kernelOperator k‖ ≤ ‖k‖

Uses 4

Statement usesContinuous functions on the unit interval · Continuous kernels on the unit square · Integral operator with a continuous kernel

Proof usesSup-norm bound for the integral operator with continuous kernel

TheoremDifference bound for the values of a kernel operator#✓fully proved

Let \(k\) be a continuous kernel on \([0, 1] \times [0, 1]\), let \(K\) be the integral operator with kernel \(k\) on \(C([0, 1], \mathbb{R})\), let \(f \in C([0, 1], \mathbb{R})\), and let \(x, x' \in [0, 1]\) and \(\delta \in \mathbb{R}\). If \(|k(x, y) - k(x', y)| \le \delta\) for every \(y \in [0, 1]\), then \(|(Kf)(x) - (Kf)(x')| \le \delta \, \|f\|_\infty\).

theorem norm_kernelOperator_apply_sub_le (k : KernelType) (f : KernelSpace)
    {x x' : Set.Icc (0 : ℝ) 1} {δ : ℝ}
    (h : ∀ y : Set.Icc (0 : ℝ) 1, ‖k (x, y) - k (x', y)‖ ≤ δ) :
    ‖kernelOperator k f x - kernelOperator k f x'‖ ≤ δ * ‖f‖

Uses 9 · Used by 1

Statement usesContinuous functions on the unit interval · Continuous kernels on the unit square · Integral operator with a continuous kernel

Proof usesClamped extension · Continuity of the clamped extension · Kernel integrand · Continuity of the kernel integrand in \(t\) · Evaluation formula for the integral operator · The clamped extension is bounded by the supremum norm

Used byIntegral operators with continuous kernels are compact

TheoremIntegral operators with continuous kernels are compact#✓fully proved

For every continuous kernel \(k\) on \([0, 1] \times [0, 1]\), the integral operator \(K\) on the space of bounded continuous real functions on \([0, 1]\), given by \((Kf)(x) = \int_0^1 k(x, t) f(t) \, dt\), is a compact operator.

The proof uses Arzelà–Ascoli: the image of the unit ball is equicontinuous by uniform continuity of the kernel.

theorem isCompactOperator_kernelOperator (k : KernelType) :
    IsCompactOperator (kernelOperator k)

Uses 5

Statement usesContinuous functions on the unit interval · Continuous kernels on the unit square · Integral operator with a continuous kernel

Proof usesSup-norm bound for the integral operator with continuous kernel · Difference bound for the values of a kernel operator

TheoremSeparable kernels give finite-rank integral operators#✓fully proved

Let \(s\) be a finite set of indices and, for \(i \in s\), let \(\varphi_i\) and \(\psi_i\) be bounded continuous functions on \([0, 1]\). If a continuous kernel \(k\) on \([0, 1] \times [0, 1]\) satisfies \(k(x, y) = \sum_{i \in s} \varphi_i(x) \psi_i(y)\) for all \(x, y \in [0, 1]\), then the range of the integral operator \(K\) on the space of bounded continuous real functions on \([0, 1]\), given by \((Kf)(x) = \int_0^1 k(x, t) f(t) \, dt\), is a finite-dimensional real vector space.

The proof shows that the range lies in the span of the functions \(\varphi_i\), \(i \in s\).

theorem finiteDimensional_range_kernelOperator_of_separable {ι : Type*} (k : KernelType)
    (s : Finset ι) (φ : ι → KernelSpace) (ψ : ι → KernelSpace)
    (hk : ∀ x y : Set.Icc (0 : ℝ) 1, k (x, y) = ∑ i ∈ s, φ i x * ψ i y) :
    FiniteDimensional ℝ ↥(LinearMap.range
      (kernelOperator k : KernelSpace →ₗ[ℝ] KernelSpace))

Uses 7

Statement usesContinuous functions on the unit interval · Continuous kernels on the unit square · Integral operator with a continuous kernel

Proof usesClamped extension · Continuity of the clamped extension · Kernel integrand · Evaluation formula for the integral operator

TheoremThe integral operator is additive in the kernel#✓fully proved

For a continuous kernel \(k\) on \([0, 1] \times [0, 1]\), write \(T_k\) for the integral operator with kernel \(k\) on \(C([0, 1], \mathbb{R})\). For all continuous kernels \(k_1\) and \(k_2\), the operator with the pointwise sum kernel is the sum of the operators: \(T_{k_1 + k_2} = T_{k_1} + T_{k_2}\).

theorem kernelOperator_add (k₁ k₂ : KernelType) :
    kernelOperator (k₁ + k₂) = kernelOperator k₁ + kernelOperator k₂

Uses 7

Statement usesContinuous functions on the unit interval · Continuous kernels on the unit square · Integral operator with a continuous kernel

Proof usesClamped extension · Kernel integrand · Continuity of the kernel integrand in \(t\) · Evaluation formula for the integral operator

TheoremThe integral operator is homogeneous in the kernel#✓fully proved

For a continuous kernel \(k\) on \([0, 1] \times [0, 1]\), write \(T_k\) for the integral operator with kernel \(k\) on \(C([0, 1], \mathbb{R})\). For every real number \(c\) and every continuous kernel \(k\), \(T_{c k} = c\, T_k\).

theorem kernelOperator_smul (c : ℝ) (k : KernelType) :
    kernelOperator (c • k) = c • kernelOperator k

Uses 6

Statement usesContinuous functions on the unit interval · Continuous kernels on the unit square · Integral operator with a continuous kernel

Proof usesClamped extension · Kernel integrand · Evaluation formula for the integral operator

TheoremThe zero kernel gives the zero operator#✓fully proved

The integral operator on \(C([0, 1], \mathbb{R})\) whose kernel is the zero function on \([0, 1] \times [0, 1]\) is the zero operator.

theorem kernelOperator_zero : kernelOperator 0 = 0

Uses 6

Statement usesContinuous functions on the unit interval · Continuous kernels on the unit square · Integral operator with a continuous kernel

Proof usesClamped extension · Kernel integrand · Evaluation formula for the integral operator

23 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.