Green's operator of the Dirichlet Laplacian on [0, 1]

AbbreviationThe space \(L^2((0, 1))\)#✓fully proved

\(L^2([0, 1])\) is the real Hilbert space of square-integrable real-valued functions on the unit interval, up to equality almost everywhere, with Lebesgue measure restricted to \([0, 1]\).

noncomputable abbrev L2UnitInterval :=
  Lp ℝ 2 (volume.restrict (Set.Icc (0 : ℝ) 1))

Used by 7

Used bySpectral decomposition of the Dirichlet Green's operator · Square root of the Dirichlet Green's operator · The square root of the Green's operator is a diagonal operator · The square root of the Green's operator squares to the Green's operator · Squared Hilbert–Schmidt norm of the Green's operator · The sine Hilbert basis of \(L^2((0, 1))\) · The sine Hilbert basis consists of sine functions

DefinitionSine basis functions on \((0, 1)\)#✓fully proved

For a positive integer \(k\), the \(k\)-th sine basis function is \(u_k : \mathbb{R} \to \mathbb{R}\), \(u_k(x) = \sqrt{2} \sin(k\pi x)\).

Restricted to \([0, 1]\), these functions form an orthonormal eigenbasis of the Green's operator with Dirichlet boundary conditions.

noncomputable def sineBasisFun (k : ℕ+) : ℝ → ℝ :=
  fun x => Real.sqrt 2 * Real.sin (↑k * Real.pi * x)

Used by 16

Used bySmoothness of the Dirichlet sine eigenfunctions · Derivative function of a Dirichlet sine eigenfunction · Pointwise derivative of a Dirichlet sine eigenfunction · Second derivative of a Dirichlet sine eigenfunction · Dirichlet sine eigenfunctions are nonzero · Sine eigenfunctions vanish at the right endpoint · Sine eigenfunctions vanish at the left endpoint · Green's kernel eigenfunction identity for sines · Spectral decomposition of the Dirichlet Green's operator · Square root of the Dirichlet Green's operator · The square root of the Green's operator is a diagonal operator · The square root of the Green's operator squares to the Green's operator · Dirichlet eigenvalue equation in Sturm-Liouville form · The sine Hilbert basis of \(L^2((0, 1))\) · The sine Hilbert basis consists of sine functions · Orthonormality of the sine basis on the unit interval

DefinitionEigenvalues of the Dirichlet Green's operator#✓fully proved

For a positive integer \(k\), the \(k\)-th eigenvalue of the Green's operator of \(-\frac{d^2}{dx^2}\) on \([0, 1]\) with Dirichlet boundary conditions \(u(0) = u(1) = 0\) is \(\lambda_k = \frac{1}{k^2 \pi^2}\).

noncomputable def greensEigenvalue (k : ℕ+) : ℝ := 1 / ((k : ℝ) ^ 2 * Real.pi ^ 2)

Used by 9

Used byThe Green's eigenvalues sum to the diagonal integral of the kernel · Green's kernel eigenfunction identity for sines · Spectral decomposition of the Dirichlet Green's operator · The square root of the Green's operator squares to the Green's operator · Squared Hilbert–Schmidt norm of the Green's operator · The Green's eigenvalues are summable · The Green's eigenvalues tend to zero · Sum of the Green's eigenvalues · Sum of the squared Green's eigenvalues

DefinitionSquare roots of the Green's operator eigenvalues#✓fully proved

For a positive integer \(k\), set \(\mu_k = \frac{1}{k\pi}\). This is the square root of the \(k\)-th eigenvalue \(\frac{1}{k^2\pi^2}\) of the Green's operator of \(-\frac{d^2}{dx^2}\) on \([0, 1]\) with Dirichlet boundary conditions.

noncomputable def greensEigenvalueSqrt (k : ℕ+) : ℝ := 1 / ((k : ℝ) * Real.pi)

Used by 3

Used bySquare root of the Dirichlet Green's operator · The square root of the Green's operator is a diagonal operator · The square root of the Green's operator squares to the Green's operator

DefinitionSquare root of the Dirichlet Green's operator#✓fully proved

Let \(L^2([0, 1])\) be the real Hilbert space of square-integrable functions on \([0, 1]\), and let \((b_k)_{k \ge 1}\) be a Hilbert basis of \(L^2([0, 1])\) indexed by the positive integers with \(b_k(x) = \sqrt{2} \sin(k\pi x)\) for almost every \(x \in [0, 1]\). Define \(A^{1/2} : L^2([0, 1]) \to L^2([0, 1])\) by

\[A^{1/2} f = \sum_{k \ge 1} \frac{1}{k\pi} \langle b_k, f \rangle\, b_k.\]

Since the Green's operator acts on \(b_k\) as multiplication by \(\frac{1}{k^2\pi^2}\), this is its square root.

noncomputable def greensOperatorSqrt (b : HilbertBasis ℕ+ ℝ L2UnitInterval)
    (_hb : ∀ k : ℕ+, (b k : L2UnitInterval) =ᵐ[volume.restrict (Set.Icc (0 : ℝ) 1)]
      (sineBasisFun k : ℝ → ℝ)) :
    L2UnitInterval → L2UnitInterval :=
  fun f => ∑' (k : ℕ+), (greensEigenvalueSqrt k * inner (𝕜 := ℝ) (b k) f) • b k

Uses 3 · Used by 2

Statement usesThe space \(L^2((0, 1))\) · Square roots of the Green's operator eigenvalues · Sine basis functions on \((0, 1)\)

Used byThe square root of the Green's operator is a diagonal operator · The square root of the Green's operator squares to the Green's operator

DefinitionGreen's kernel of the Dirichlet Laplacian on \((0, 1)\)#✓fully proved

For real numbers \(x\) and \(t\), set \(G(x, t) = \min(x, t)\,(1 - \max(x, t))\).

On \([0, 1]\) this is the Green's kernel of \(-\frac{d^2}{dx^2}\) with boundary conditions \(u(0) = u(1) = 0\): the operator \(f \mapsto \int_0^1 G(\cdot, t) f(t)\, dt\) inverts \(-\frac{d^2}{dx^2}\) under these conditions.

noncomputable def greensKernel (x t : ℝ) : ℝ :=
  min x t * (1 - max x t)

Used by 6

Used byThe Green's eigenvalues sum to the diagonal integral of the kernel · Green's kernel eigenfunction identity for sines · Spectral decomposition of the Dirichlet Green's operator · The square root of the Green's operator squares to the Green's operator · Squared Hilbert–Schmidt norm of the Green's operator · Diagonal integral of the Green's kernel

LemmaGreen's kernel eigenfunction identity for sines#✓fully proved

Let \(k\) be a positive integer, let \(G(x, t) = \min(x, t)\,(1 - \max(x, t))\) be the Green's kernel, and let \(u_k(x) = \sqrt{2} \sin(k\pi x)\) and \(\lambda_k = \frac{1}{k^2\pi^2}\). Then for every \(x \in [0, 1]\),

\[\int_0^1 G(x, t)\, u_k(t)\, dt = \lambda_k\, u_k(x).\]

lemma greens_kernel_integral_sine_eq (k : ℕ+) (x : ℝ) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) :
    ∫ t in (0 : ℝ)..1, (greensKernel x t) * (sineBasisFun k t) =
      greensEigenvalue k * sineBasisFun k x

Uses 3 · Used by 1

Statement usesEigenvalues of the Dirichlet Green's operator · Green's kernel of the Dirichlet Laplacian on \((0, 1)\) · Sine basis functions on \((0, 1)\)

Used bySpectral decomposition of the Dirichlet Green's operator

TheoremSpectral decomposition of the Dirichlet Green's operator#✓fully proved

Write \(L^2([0, 1])\) for the real Hilbert space of square-integrable functions on \([0, 1]\) with Lebesgue measure, let \(G(x, t) = \min(x, t)\,(1 - \max(x, t))\) be the Green's kernel, and for each positive integer \(k\) let \(u_k(x) = \sqrt{2} \sin(k\pi x)\) and \(\lambda_k = \frac{1}{k^2\pi^2}\). Let \(A\) be a linear map from \(L^2([0, 1])\) to itself that is symmetric, \(\langle Af, g \rangle = \langle f, Ag \rangle\) for all \(f, g\), and is given by the Green's kernel, \((Af)(x) = \int_{[0, 1]} G(x, t) f(t)\, dt\) for almost every \(x \in [0, 1]\) and every \(f\). Let \((b_k)_{k \ge 1}\) be a Hilbert basis of \(L^2([0, 1])\) indexed by the positive integers with \(b_k = u_k\) almost everywhere on \([0, 1]\). Then \(A\) is injective, each \(b_k\) is an eigenvector of \(A\) with eigenvalue \(\lambda_k\), and every \(f \in L^2([0, 1])\) satisfies \(Af = \sum_{k \ge 1} \lambda_k \langle b_k, f \rangle\, b_k\).

theorem greens_operator_eigendecomposition
    (A : Module.End ℝ L2UnitInterval)
    (b : HilbertBasis ℕ+ ℝ L2UnitInterval)
    (hA_sa : ∀ f g : L2UnitInterval,
      inner (𝕜 := ℝ) (A f) g = inner (𝕜 := ℝ) f (A g))
    (hb : ∀ k : ℕ+, (b k : L2UnitInterval) =ᵐ[volume.restrict (Set.Icc (0 : ℝ) 1)]
      (sineBasisFun k : ℝ → ℝ))
    (hA_greens : ∀ f : L2UnitInterval,
      (A f : L2UnitInterval) =ᵐ[volume.restrict (Set.Icc (0 : ℝ) 1)]
      (fun x => ∫ t in Set.Icc (0 : ℝ) 1, greensKernel x t * (f : ℝ → ℝ) t)) :
    LinearMap.ker A = ⊥ ∧
    (∀ k : ℕ+, A.HasEigenvector (greensEigenvalue k) (b k)) ∧
    ∀ f : L2UnitInterval,
      A f = ∑' k : ℕ+, (greensEigenvalue k * @inner ℝ _ _ (b k) f) • (b k)

Uses 5 · Used by 2

Statement usesThe space \(L^2((0, 1))\) · Eigenvalues of the Dirichlet Green's operator · Green's kernel of the Dirichlet Laplacian on \((0, 1)\) · Sine basis functions on \((0, 1)\)

Proof usesGreen's kernel eigenfunction identity for sines

Used byThe square root of the Green's operator squares to the Green's operator · Squared Hilbert–Schmidt norm of the Green's operator

LemmaOrthonormality of the sine basis on the unit interval#✓fully proved

The canonical sine basis is orthonormal on the unit interval, in product-integral form.

lemma sine_product_integral (k j : ℕ+) :
    (∫ x in (0 : ℝ)..1, sineBasisFun k x * sineBasisFun j x) =
      if k = j then 1 else 0

Uses 1 · Used by 2

Statement usesSine basis functions on \((0, 1)\)

Used byThe sine Hilbert basis of \(L^2((0, 1))\) · The sine Hilbert basis consists of sine functions

DefinitionThe sine Hilbert basis of \(L^2((0, 1))\)#✓fully proved

The sine Hilbert basis is a Hilbert basis \((b_k)_{k \ge 1}\) of the real Hilbert space \(L^2([0, 1])\), indexed by the positive integers, with \(b_k(x) = \sqrt{2} \sin(k\pi x)\) for almost every \(x \in [0, 1]\). Such a basis exists, and since an element of \(L^2([0, 1])\) is determined by its values almost everywhere, it is unique.

noncomputable def sineHilbertBasis : HilbertBasis ℕ+ ℝ L2UnitInterval :=
  Classical.choose (p := fun b : HilbertBasis ℕ+ ℝ L2UnitInterval =>
    ∀ k : ℕ+, (b k : L2UnitInterval) =ᵐ[volume.restrict (Set.Icc (0 : ℝ) 1)]
      (sineBasisFun k : ℝ → ℝ)) (by exact exists_sineHilbertBasis)

Uses 3 · Used by 2

Statement usesThe space \(L^2((0, 1))\) · Sine basis functions on \((0, 1)\) · Orthonormality of the sine basis on the unit interval

Used bySquared Hilbert–Schmidt norm of the Green's operator · The sine Hilbert basis consists of sine functions

LemmaThe sine Hilbert basis consists of sine functions#✓fully proved

For every positive integer \(k\), the \(k\)-th element \(b_k\) of the sine Hilbert basis of \(L^2([0, 1])\) satisfies \(b_k(x) = \sqrt{2} \sin(k\pi x)\) for almost every \(x \in [0, 1]\).

lemma sineHilbertBasis_coe (k : ℕ+) :
    (sineHilbertBasis k : L2UnitInterval) =ᵐ[volume.restrict (Set.Icc (0 : ℝ) 1)]
      (sineBasisFun k : ℝ → ℝ)

Uses 4 · Used by 1

Statement usesThe space \(L^2((0, 1))\) · Sine basis functions on \((0, 1)\) · The sine Hilbert basis of \(L^2((0, 1))\)

Proof usesOrthonormality of the sine basis on the unit interval

Used bySquared Hilbert–Schmidt norm of the Green's operator

DefinitionDirichlet eigenvalues of the Laplacian on the unit interval#✓fully proved

The k-th Dirichlet eigenvalue: λ_k = (kπ)², the eigenvalue of -d²/dx² for the eigenfunction sineBasisFun k.

noncomputable def dirichletLaplacianEigenvalue (k : ℕ+) : ℝ :=
  ((k : ℝ) * Real.pi) ^ 2

Used by 2

Used bySecond derivative of a Dirichlet sine eigenfunction · Dirichlet eigenvalue equation in Sturm-Liouville form

TheoremPointwise derivative of a Dirichlet sine eigenfunction#✓fully proved

First derivative of the k-th sine eigenfunction.

theorem dirichletSine_hasDerivAt (k : ℕ+) (x : ℝ) :
    HasDerivAt (sineBasisFun k)
      (Real.sqrt 2 * ((k : ℝ) * Real.pi) * Real.cos ((k : ℝ) * Real.pi * x)) x

Uses 1 · Used by 1

Statement usesSine basis functions on \((0, 1)\)

Used byDerivative function of a Dirichlet sine eigenfunction

TheoremDerivative function of a Dirichlet sine eigenfunction#✓fully proved

The derivative of the k-th sine eigenfunction, as a function.

theorem dirichletSine_deriv (k : ℕ+) (x : ℝ) :
    deriv (sineBasisFun k) x =
      Real.sqrt 2 * ((k : ℝ) * Real.pi) * Real.cos ((k : ℝ) * Real.pi * x)

Uses 2 · Used by 1

Statement usesSine basis functions on \((0, 1)\)

Proof usesPointwise derivative of a Dirichlet sine eigenfunction

Used bySecond derivative of a Dirichlet sine eigenfunction

TheoremSecond derivative of a Dirichlet sine eigenfunction#✓fully proved

Second-derivative (eigenvalue) equation for the k-th sine eigenfunction: u_k'' = -(kπ)² u_k.

theorem dirichletSine_iteratedDeriv_two (k : ℕ+) (x : ℝ) :
    iteratedDeriv 2 (sineBasisFun k) x =
      -dirichletLaplacianEigenvalue k * sineBasisFun k x

Uses 3 · Used by 1

Statement usesDirichlet eigenvalues of the Laplacian on the unit interval · Sine basis functions on \((0, 1)\)

Proof usesDerivative function of a Dirichlet sine eigenfunction

Used byDirichlet eigenvalue equation in Sturm-Liouville form

TheoremDirichlet eigenvalue equation in Sturm-Liouville form#✓fully proved

The Dirichlet eigenvalue equation in Sturm-Liouville form: -u_k'' = λ_k u_k with λ_k = (kπ)².

theorem neg_iteratedDeriv_two_eq (k : ℕ+) (x : ℝ) :
    -iteratedDeriv 2 (sineBasisFun k) x =
      dirichletLaplacianEigenvalue k * sineBasisFun k x

Uses 3

Statement usesDirichlet eigenvalues of the Laplacian on the unit interval · Sine basis functions on \((0, 1)\)

Proof usesSecond derivative of a Dirichlet sine eigenfunction

TheoremSine eigenfunctions vanish at the left endpoint#✓fully proved

Left Dirichlet boundary value: u_k(0) = 0.

theorem dirichletSine_zero (k : ℕ+) : sineBasisFun k 0 = 0

Uses 1

Statement usesSine basis functions on \((0, 1)\)

TheoremSine eigenfunctions vanish at the right endpoint#✓fully proved

Right Dirichlet boundary value: u_k(1) = 0.

theorem dirichletSine_one (k : ℕ+) : sineBasisFun k 1 = 0

Uses 1

Statement usesSine basis functions on \((0, 1)\)

TheoremSmoothness of the Dirichlet sine eigenfunctions#✓fully proved

The sine eigenfunctions are smooth.

theorem dirichletSine_contDiff (k : ℕ+) : ContDiff ℝ ⊤ (sineBasisFun k)

Uses 1

Statement usesSine basis functions on \((0, 1)\)

TheoremDirichlet sine eigenfunctions are nonzero#✓fully proved

The sine eigenfunctions are nonzero (so they are genuine eigenfunctions, not the trivial solution). The witness point is x = 1 / (2k), where u_k = √2.

theorem dirichletSine_ne_zero (k : ℕ+) : sineBasisFun k ≠ 0

Uses 1

Statement usesSine basis functions on \((0, 1)\)

TheoremThe square root of the Green's operator is a diagonal operator#✓fully proved

Let \((b_k)_{k \ge 1}\) be a Hilbert basis of \(L^2([0, 1])\) indexed by the positive integers with \(b_k(x) = \sqrt{2} \sin(k\pi x)\) for almost every \(x \in [0, 1]\), let \(\mu_k = \frac{1}{k\pi}\), and let \(C\) be a real number with \(|\mu_k| \le C\) for every \(k\). Then for every \(f \in L^2([0, 1])\), the square root \(A^{1/2} f\) of the Green's operator defined from \((b_k)\) equals \(D f\), where \(D\) is the bounded diagonal operator with coefficients \((\mu_k)\) in the basis \((b_k)\) and coefficient bound \(C\).

theorem greensOperatorSqrt_eq_diagonal
    (b : HilbertBasis ℕ+ ℝ L2UnitInterval)
    (hb : ∀ k : ℕ+, (b k : L2UnitInterval) =ᵐ[volume.restrict (Set.Icc (0 : ℝ) 1)]
      (sineBasisFun k : ℝ → ℝ)) {C : ℝ}
    (hC : ∀ k : ℕ+, ‖greensEigenvalueSqrt k‖ ≤ C) (f : L2UnitInterval) :
    greensOperatorSqrt b hb f = diagonalOperator b greensEigenvalueSqrt
      hC f

Uses 6 · Used by 1

Statement usesBounded diagonal operator on a Hilbert basis · The space \(L^2((0, 1))\) · Square roots of the Green's operator eigenvalues · Square root of the Dirichlet Green's operator · Sine basis functions on \((0, 1)\)

Proof usesSeries formula for a diagonal operator

Used byThe square root of the Green's operator squares to the Green's operator

TheoremThe square root of the Green's operator squares to the Green's operator#✓fully proved

Let \(G(x, t) = \min(x, t)\,(1 - \max(x, t))\) be the Green's kernel and let \(A\) be a linear map from \(L^2([0, 1])\) to itself that is symmetric, \(\langle Af, g \rangle = \langle f, Ag \rangle\) for all \(f, g\), and is given by the Green's kernel, \((Af)(x) = \int_{[0, 1]} G(x, t) f(t)\, dt\) for almost every \(x \in [0, 1]\) and every \(f\). Let \((b_k)_{k \ge 1}\) be a Hilbert basis of \(L^2([0, 1])\) indexed by the positive integers with \(b_k(x) = \sqrt{2} \sin(k\pi x)\) for almost every \(x \in [0, 1]\), and let \(A^{1/2}\) be the square root of the Green's operator defined from \((b_k)\). Then \(A^{1/2}(A^{1/2} f) = Af\) for every \(f \in L^2([0, 1])\).

theorem greensOperatorSqrt_sq
    (A : Module.End ℝ L2UnitInterval)
    (b : HilbertBasis ℕ+ ℝ L2UnitInterval)
    (hA_sa : ∀ f g : L2UnitInterval,
      inner (𝕜 := ℝ) (A f) g = inner (𝕜 := ℝ) f (A g))
    (hb : ∀ k : ℕ+, (b k : L2UnitInterval) =ᵐ[volume.restrict (Set.Icc (0 : ℝ) 1)]
      (sineBasisFun k : ℝ → ℝ))
    (hA_greens : ∀ f : L2UnitInterval,
      (A f : L2UnitInterval) =ᵐ[volume.restrict (Set.Icc (0 : ℝ) 1)]
      (fun x => ∫ t in Set.Icc (0 : ℝ) 1, greensKernel x t * (f : ℝ → ℝ) t))
    (f : L2UnitInterval) :
    greensOperatorSqrt b hb (greensOperatorSqrt b hb f) = A f

Uses 11

Statement usesThe space \(L^2((0, 1))\) · Green's kernel of the Dirichlet Laplacian on \((0, 1)\) · Square root of the Dirichlet Green's operator · Sine basis functions on \((0, 1)\)

Proof usesBounded diagonal operator on a Hilbert basis · Series formula for a diagonal operator · Square of a diagonal operator · Eigenvalues of the Dirichlet Green's operator · Square roots of the Green's operator eigenvalues · Spectral decomposition of the Dirichlet Green's operator · The square root of the Green's operator is a diagonal operator

TheoremThe Green's eigenvalues are summable#✓fully proved

The Green's eigenvalues \(\lambda_k = 1/(k^2\pi^2)\), indexed by the positive integers \(k\), form a summable family of real numbers.

theorem summable_greensEigenvalues : Summable greensEigenvalue

Uses 1 · Used by 1

Statement usesEigenvalues of the Dirichlet Green's operator

Used byThe Green's eigenvalues tend to zero

TheoremThe Green's eigenvalues tend to zero#✓fully proved

The Green's eigenvalues \(\lambda_k = 1/(k^2\pi^2)\) tend to \(0\) along the cofinite filter on the positive integers, that is, \(\lambda_k \to 0\) as \(k \to \infty\).

theorem tendsto_cofinite_greensEigenvalues :
    Filter.Tendsto greensEigenvalue Filter.cofinite (nhds 0)

Uses 2

Statement usesEigenvalues of the Dirichlet Green's operator

Proof usesThe Green's eigenvalues are summable

TheoremSum of the Green's eigenvalues#✓fully proved

For the Green's eigenvalues \(\lambda_k = 1/(k^2\pi^2)\), indexed by the positive integers \(k\), we have \(\sum_{k \ge 1} \lambda_k = 1/6\).

theorem tsum_greensEigenvalues : (∑' k : ℕ+, greensEigenvalue k) = 1 / 6

Uses 1 · Used by 1

Statement usesEigenvalues of the Dirichlet Green's operator

Used byThe Green's eigenvalues sum to the diagonal integral of the kernel

TheoremSum of the squared Green's eigenvalues#✓fully proved

For the Green's eigenvalues \(\lambda_k = 1/(k^2\pi^2)\), indexed by the positive integers \(k\), we have \(\sum_{k \ge 1} \lambda_k^2 = 1/90\).

theorem tsum_greensEigenvalues_sq :
    (∑' k : ℕ+, (greensEigenvalue k) ^ 2) = 1 / 90

Uses 1

Statement usesEigenvalues of the Dirichlet Green's operator

TheoremDiagonal integral of the Green's kernel#✓fully proved

The Green's kernel \(G\) on \([0, 1]\) satisfies \(\int_0^1 G(x, x)\,dx = 1/6\), since \(G(x, x) = x(1 - x)\).

theorem integral_greensKernel_diag :
    ∫ x in (0 : ℝ)..1, greensKernel x x = 1 / 6

Uses 1 · Used by 1

Statement usesGreen's kernel of the Dirichlet Laplacian on \((0, 1)\)

Used byThe Green's eigenvalues sum to the diagonal integral of the kernel

TheoremThe Green's eigenvalues sum to the diagonal integral of the kernel#✓fully proved

The sum of the Green's eigenvalues \(\lambda_k = 1/(k^2\pi^2)\) over the positive integers \(k\) equals the integral of the Green's kernel \(G\) along the diagonal: \(\sum_{k \ge 1} \lambda_k = \int_0^1 G(x, x)\,dx\).

theorem greens_eigenvalue_sum_eq_kernel_diagonal_integral :
    (∑' k : ℕ+, greensEigenvalue k) =
      ∫ x in (0 : ℝ)..1, greensKernel x x

Uses 4

Statement usesEigenvalues of the Dirichlet Green's operator · Green's kernel of the Dirichlet Laplacian on \((0, 1)\)

Proof usesDiagonal integral of the Green's kernel · Sum of the Green's eigenvalues

TheoremSquared Hilbert–Schmidt norm of the Green's operator#✓fully proved

Let \(G(x, t) = \min(x, t)\,(1 - \max(x, t))\) be the Green's kernel and let \(A\) be a continuous linear operator on \(L^2([0, 1])\) that is symmetric, \(\langle Af, g \rangle = \langle f, Ag \rangle\) for all \(f, g\), and is given by the Green's kernel, \((Af)(x) = \int_{[0, 1]} G(x, t) f(t)\, dt\) for almost every \(x \in [0, 1]\) and every \(f\). Let \((b_k)_{k \ge 1}\) be the sine Hilbert basis of \(L^2([0, 1])\). Then the squared Hilbert–Schmidt norm of \(A\) in the family \((b_{n+1})_{n \ge 0}\) equals \(1/90\), that is, \(\sum_{n \ge 0} \|A b_{n+1}\|^2 = 1/90\), the sum being taken in \([0, \infty]\).

theorem hsNormSq_greensOperator
    (A : L2UnitInterval →L[ℝ] L2UnitInterval)
    (hA_sa : ∀ f g : L2UnitInterval,
      inner (𝕜 := ℝ) (A f) g = inner (𝕜 := ℝ) f (A g))
    (hA_greens : ∀ f : L2UnitInterval,
      (A f : L2UnitInterval) =ᵐ[volume.restrict (Set.Icc (0 : ℝ) 1)]
      (fun x => ∫ t in Set.Icc (0 : ℝ) 1, greensKernel x t * (f : ℝ → ℝ) t)) :
    hsNormSq A (fun n : ℕ => sineHilbertBasis ⟨n + 1, Nat.succ_pos n⟩) =
      ENNReal.ofReal (1 / 90 : ℝ)

Uses 7

Statement usesThe space \(L^2((0, 1))\) · Green's kernel of the Dirichlet Laplacian on \((0, 1)\) · The sine Hilbert basis of \(L^2((0, 1))\) · Squared Hilbert–Schmidt norm in a family

Proof usesEigenvalues of the Dirichlet Green's operator · Spectral decomposition of the Dirichlet Green's operator · The sine Hilbert basis consists of sine functions

29 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.