Documentation

TauCeti.Analysis.PDE.Spectrum.Interval

The Dirichlet spectrum of -Δ on an interval #

On a bounded open interval (a, b) the Dirichlet eigenvalue problem for -Δ = -d²/dx² can be solved explicitly: its eigenvalues are exactly the numbers (k π / (b - a))², k ≥ 1, with eigenfunctions x ↦ sin (k π (x - a) / (b - a)). This is the model Sturm--Liouville problem, the case of the general Dirichlet spectral theory of TauCeti.PDE.IsDirichletEigenvalue in which the whole spectrum is explicit. In particular the first Dirichlet eigenvalue is (π / (b - a))², and by the Rayleigh principle this is the optimal constant in the Poincaré inequality C ∫_a^b u² ≤ ∫_a^b |u'|² on H¹₀(a, b).

The interval is realized as the open subset TauCeti.PDE.intervalDomain a b of the Euclidean line EuclideanSpace ℝ (Fin 1), the setting of the Sobolev spaces and the energy forms.

Each sine mode is C^∞, vanishes at a and b and satisfies -Δw = (k π / (b - a))² w classically, so it is a weak Dirichlet eigenfunction (TauCeti.PDE.exists_value_ae_eq_and_energyFormH1_eq_of_laplacian_eq). Conversely, the energy form is symmetric, so an eigenfunction for any other κ is orthogonal in L²(a, b) to every sine mode, and it vanishes by completeness of the sine system (TauCeti.ae_eq_zero_of_forall_integral_mul_sin_eq_zero).

Main declarations #

References #

source
def TauCeti.PDE.intervalDomain (a b : ℝ) :
TopologicalSpace.Opens (EuclideanSpace ℝ (Fin 1))

The open interval (a, b), as an open subset of the Euclidean line EuclideanSpace ℝ (Fin 1).

Instances For
    source
    @[simp]
    theorem TauCeti.PDE.mem_intervalDomain {a b : ℝ} {x : EuclideanSpace ℝ (Fin 1)} :
    x ∈ intervalDomain a b ↔ x.ofLp 0 ∈ Set.Ioo a b
    source
    theorem TauCeti.PDE.coe_intervalDomain (a b : ℝ) :
    ↑(intervalDomain a b) = {x : EuclideanSpace ℝ (Fin 1) | x.ofLp 0 ∈ Set.Ioo a b}

    As a set, the interval domain consists of the points of the line whose coordinate lies in (a, b).

    source
    theorem TauCeti.PDE.isBounded_intervalDomain {a b : ℝ} :
    Bornology.IsBounded ↑(intervalDomain a b)

    The interval domain (a, b) is bounded.

    source
    theorem TauCeti.PDE.exists_value_ae_eq_sin_and_energyFormH1_eq {a b : ℝ} (hab : a < b) (k : ℕ) :
    ∃ (u : ↥(W1p0 MeasureTheory.volume (intervalDomain a b) 2)), (↑↑(W1p.value ↑u) =ᵐ[MeasureTheory.volume.restrict ↑(intervalDomain a b)] fun (x : EuclideanSpace ℝ (Fin 1)) => Real.sin (↑k * Real.pi * (x.ofLp 0 - a) / (b - a))) ∧ ∀ (v : ↥(W1p0 MeasureTheory.volume (intervalDomain a b) 2)), energyFormH1 (fun (x : EuclideanSpace ℝ (Fin 1)) => 1) 0 0 ↑u ↑v = (↑k * Real.pi / (b - a)) ^ 2 * inner ℝ (W1p.value ↑u) (W1p.value ↑v)

    The sine modes are weak Dirichlet eigenfunctions of -Δ on an interval. For every k : ℕ, the function x ↦ sin (k π (x - a) / (b - a)) is the value of some u ∈ H¹₀(a, b) with

    ∫ ∇u · ∇v = (k π / (b - a))² ∫ u v for every v ∈ H¹₀(a, b).

    source
    theorem TauCeti.PDE.isDirichletEigenvalue_laplacian_intervalDomain {a b : ℝ} (hab : a < b) {k : ℕ} (hk : 0 < k) :
    IsDirichletEigenvalue MeasureTheory.volume (intervalDomain a b) (fun (x : EuclideanSpace ℝ (Fin 1)) => 1) 0 0 ((↑k * Real.pi / (b - a)) ^ 2)

    (k π / (b - a))² is a Dirichlet eigenvalue of -Δ on (a, b) for every k ≥ 1, with eigenfunction x ↦ sin (k π (x - a) / (b - a)).

    source
    theorem TauCeti.PDE.isDirichletEigenvalue_laplacian_intervalDomain_iff {a b : ℝ} (hab : a < b) {kappa : ℝ} :
    IsDirichletEigenvalue MeasureTheory.volume (intervalDomain a b) (fun (x : EuclideanSpace ℝ (Fin 1)) => 1) 0 0 kappa ↔ ∃ (k : ℕ), 0 < k ∧ kappa = (↑k * Real.pi / (b - a)) ^ 2

    The Dirichlet spectrum of -Δ on an interval. The Dirichlet eigenvalues of -Δ on (a, b) are exactly the numbers (k π / (b - a))² with k ≥ 1: the homogeneous Dirichlet problem -Δu = κ u in (a, b), u = 0 at a and b, has a nonzero weak solution in H¹₀(a, b) exactly for these κ.

    source
    theorem TauCeti.PDE.isLeast_isDirichletEigenvalue_laplacian_intervalDomain {a b : ℝ} (hab : a < b) :
    IsLeast {kappa : ℝ | IsDirichletEigenvalue MeasureTheory.volume (intervalDomain a b) (fun (x : EuclideanSpace ℝ (Fin 1)) => 1) 0 0 kappa} ((Real.pi / (b - a)) ^ 2)

    The first Dirichlet eigenvalue of -Δ on (a, b) is (π / (b - a))², the least element of the Dirichlet spectrum.

    source
    theorem TauCeti.PDE.nonempty_intervalDomain_iff {a b : ℝ} :
    (↑(intervalDomain a b)).Nonempty ↔ a < b

    The interval domain (a, b) is nonempty exactly when a < b.

    source
    theorem TauCeti.PDE.firstDirichletEigenvalue_laplacian_intervalDomain {a b : ℝ} (hab : a < b) (hcoeff : MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ (Fin 1)) => energyIntegrand ((fun (x : EuclideanSpace ℝ (Fin 1)) => 1) x) (0 x) (0 x)) ⊤ (MeasureTheory.volume.restrict ↑(intervalDomain a b))) (hcoercive : IsCoercive (energyFormH1L0 hcoeff)) :
    firstDirichletEigenvalue hcoeff hcoercive = (Real.pi / (b - a)) ^ 2

    The first Dirichlet eigenvalue of -Δ on an interval (a, b) is (π / (b - a))², for any choice of the boundedness and coercivity data defining it.

    source
    theorem TauCeti.PDE.isGreatest_mul_norm_value_sq_le_energyFormH1_intervalDomain {a b : ℝ} (hab : a < b) :
    IsGreatest {C : ℝ | ∀ (u : ↥(W1p0 MeasureTheory.volume (intervalDomain a b) 2)), C * ‖W1p.value ↑u‖ ^ 2 ≤ energyFormH1 (fun (x : EuclideanSpace ℝ (Fin 1)) => 1) 0 0 ↑u ↑u} ((Real.pi / (b - a)) ^ 2)

    The sharp Poincaré inequality on an interval. For every u ∈ H¹₀(a, b),

    (π / (b - a))² ∫_a^b u² ≤ ∫_a^b |u'|²,

    and (π / (b - a))² is the largest constant for which this holds: it is the first Dirichlet eigenvalue (TauCeti.PDE.firstDirichletEigenvalue_laplacian_intervalDomain).