WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Sturm–Liouville theory

Revision #1604 → #2472 · back to history

modifiedSturm–Liouville problem92db065a49f4
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Grep for `Sturm` in `Mathlib/` returns no Sturm–Liouville definitions.
status—not_formalized
modifiedEigenvalues of a Sturm–Liouville problem5e5dca356cd6
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has general `Module.End.HasEigenvalue`, but no Sturm–Liouville eigenvalue definition.
status—not_formalized
modifiedEigenfunctions of a Sturm–Liouville problema13a618cdee8
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Sturm–Liouville eigenfunction definition appears in Mathlib.
status—not_formalized
modifiedSturm–Liouville theory4456c23324aa
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The topic itself is absent from Mathlib.
status—not_formalized
modifiedRegular Sturm–Liouville problemf59e2b3ade25
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No regularity definition for Sturm–Liouville problems is present.
status—not_formalized
modifiedWeight (density) functiond8f10ba24673
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No SL weight-function concept present in Mathlib.
status—not_formalized
modifiedSolution of a regular Sturm–Liouville problemea417323475b
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No SL solution notion present.
status—not_formalized
modifiedMain theorem of Sturm–Liouville theorybdec88e9fcb8
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The SL main theorem is not stated in Mathlib; only a finite-dimensional symmetric-operator spectral theorem exists in `Mathlib/Analysis/InnerProductSpace/Spectrum.lean`.
status—not_formalized
modifiedNo nontrivial solution has infinitely many zeros on a closed interval4b8d7eec3f28
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Mathlib statement about zeros of ODE solutions.
status—not_formalized
modifiedSturm's Separation Theorema617af2461fd
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Sturm's separation theorem is not present in Mathlib.
status—not_formalized
modifiedSturm's Fundamental Theorem90b6eece54d0
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Sturm's comparison/fundamental theorem is not present in Mathlib.
status—not_formalized
modifiedSturm–Liouville form (self-adjoint form)59576227c2e1
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Sturm–Liouville canonical form of a second-order ODE is not defined in Mathlib.
status—not_formalized
modifiedEvery second-order linear homogeneous ODE can be recast in Sturm–Liouville formb86bb55f9420
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The reduction lemma is not formalized in Mathlib.
status—not_formalized
modifiedBessel equation in Sturm–Liouville form484ccedcc0ff
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Bessel equation itself is not in Mathlib, let alone its SL form.
status—not_formalized
modifiedLegendre equation in Sturm–Liouville formd234c2a7c60d
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Legendre differential equation is not present in Mathlib (only Legendre symbols/polynomials in algebraic contexts).
status—not_formalized
modifiedReduction via integrating factor8b05257d56d8
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Integrating-factor SL reduction examples are not in Mathlib.
status—not_formalized
modifiedIntegrating factor for general second-order homogeneous equation40eb37e41643
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Integrating-factor construction for second-order ODEs is not present.
status—not_formalized
modifiedSturm–Liouville operator La3c85b0c75a7
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No SL operator is defined in Mathlib.
status—not_formalized
modifiedL is a self-adjoint operatorbf40e7e5b5ab
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The specific self-adjointness of the SL operator is not stated in Mathlib.
status—not_formalized
addedEigenvalues of L are real; eigenfunctions with different eigenvalues are orthogonald65f61228718
modifiedResolvent is a compact integral operator; spectral theorem yields orthonormal basis of eigenfunctionsce89df9d113e
FieldFrom #1604To #2472
mathlib.decl—LinearMap.IsSymmetric.eigenvectorBasis
mathlib.match_kind—generalization
mathlib.module—Mathlib.Analysis.InnerProductSpace.Spectrum
note—Mathlib has a finite-dimensional symmetric-operator eigenbasis; the compact-resolvent Sturm–Liouville argument itself is not formalized.
status—partial
modifiedSingular Sturm–Liouville operatorecce5e6f7aff
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The singular-vs-regular SL distinction is not defined in Mathlib.
status—not_formalized
modifiedReduction of inhomogeneous second-order linear ODE to Sturm–Liouville form40f8a0760c6c
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not present in Mathlib.
status—not_formalized
modifiedPicard–Lindelöf existence and uniqueness for initial value problems2fcef97e039c
FieldFrom #1604To #2472
mathlib.decl—IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.ODE.ExistUnique
note—Picard–Lindelöf existence (plus uniqueness via `ODE_solution_unique`) is formalized in `Mathlib.Analysis.ODE`.
status—formalized
modifiedSolution of inhomogeneous problem via eigenfunction expansionde0745055f62
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Eigenfunction-expansion solution of an inhomogeneous SL BVP is not in Mathlib.
status—not_formalized
modifiedFourier series as a Sturm–Liouville problema2c6ffc6999d
FieldFrom #1604To #2472
mathlib.decl—fourierBasis
mathlib.match_kind—generalization
mathlib.module—Mathlib.Analysis.Fourier.AddCircle
note—Mathlib has the Fourier series/orthonormal basis `fourierBasis` on `AddCircle`, but it is not derived via a Sturm–Liouville eigenvalue problem.
status—partial
modifiedNormal modes of a rectangular membrane003d3b56099d
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Membrane vibrational modes / 2D wave-equation eigenvalue problem are not formalized.
status—not_formalized
modifiedSeparation of variables for a linear second-order equation88b9bb46e1e1
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Separation of variables for PDEs is not a formalized technique in Mathlib.
status—not_formalized
modifiedShooting method for Sturm–Liouville problems944086f8956c
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—This numerical method is not in Mathlib.
status—not_formalized
modifiedSpectral parameter power series (SPPS) representation of solutions26e299923124
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The SPPS method is not formalized.
status—not_formalized
modifiedConstruction of a nonvanishing solution via SPPSd2303a984011
FieldFrom #1604To #2472
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not present in Mathlib.
status—not_formalized