WikiLean Articles · Brain · Recent changes · Proposals · Flags · Stats · About

Diff — Laplace operator

Revision #1345 → #2462 · back to history

modifiedLaplace operator (informal)3eba00eef616
FieldFrom #1345To #2462
mathlib.decl—Laplacian.laplacian
mathlib.match_kind—generalization
mathlib.module—Mathlib.Analysis.Distribution.DerivNotation
note—Mathlib defines a `Laplacian` typeclass with notation `Δ`, instantiated on `E → F` for real inner product spaces via `InnerProductSpace.instLaplacian`.
status—formalized
modifiedHarmonic function3b9be979cfe9
FieldFrom #1345To #2462
mathlib.decl—InnerProductSpace.HarmonicAt
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
note—Defined as being C^2 with `Δ f =ᶠ[𝓝 x] 0`; `HarmonicOnNhd` handles the on-a-set version.
status—formalized
modifiedLaplacian as divergence of gradient84143a3739a7
FieldFrom #1345To #2462
mathlib.decl—InnerProductSpace.laplacianWithin
mathlib.match_kind—generalization
mathlib.module—Mathlib.Analysis.InnerProductSpace.Laplacian
note—Mathlib's Laplacian is defined via the second iterated derivative applied to the canonical covariant tensor, not literally as `div ∘ grad` — divergence is not defined in Mathlib.
status—partial
modifiedLaplacian as sum of unmixed second partialse8cc2ed3d38c
FieldFrom #1345To #2462
mathlib.decl—InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.InnerProductSpace.Laplacian
note—States `Δ f = fun x ↦ ∑ i, iteratedFDeriv ℝ 2 f x ![v i, v i]` for any orthonormal basis `v`.
status—formalized
modifiedLaplacian maps C^k to C^{k-2}7ca1698464db
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No lemma of the form `ContDiff k → ContDiff (k-2) (Δ f)` on the Laplacian was found.
status—not_formalized
modifiedLaplacian via sphere averages83cfdd00c9fc
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No definition of the Laplacian as a limit of the sphere-average deviation was found.
status—not_formalized
modifiedNegative semidefinite sign conventionb70b0be55152
FieldFrom #1345To #2462
mathlib.decl—Laplacian.laplacian
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Distribution.DerivNotation
note—Mathlib's `Δ` uses the sum-of-second-partials sign (the negative-semidefinite convention), matching this Wikipedia convention.
status—formalized
modifiedNonnegative sign convention4929b201aa6a
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No `-Δ` convention operator is defined in Mathlib.
status—not_formalized
modifiedDiffusion equilibrium and Laplace's equation31fc66f52eb8
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Physics motivation, not formalized.
status—not_formalized
modifiedDiffusion implies Laplace's equationb4626012f5a0
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No formalization of a diffusion PDE / Fick-law derivation of Laplace's equation.
status—not_formalized
modifiedAverage over a ball811379d0b5be
FieldFrom #1345To #2462
mathlib.decl—MeasureTheory.average
mathlib.match_kind—generalization
mathlib.module—Mathlib.MeasureTheory.Integral.Average
note—General measure-theoretic average is present, but a dedicated `ballAverage` for the Laplace/harmonic setting is not.
status—partial
modifiedAverage over a sphere2ec46e8bc097
FieldFrom #1345To #2462
mathlib.decl—circleAverage
mathlib.match_kind—special_case
mathlib.module—Mathlib.MeasureTheory.Integral.CircleAverage
note—Circle (2D sphere) average is formalized; the higher-dimensional sphere-average operator specific to harmonic analysis is not.
status—partial
modifiedCharge density from electrostatic potential20527fb4d0ff
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Physics application; no electrostatics API in Mathlib.
status—not_formalized
modifiedGauss's law derivation2b75cd3d2ade
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Gauss's law is not formalized in Mathlib.
status—not_formalized
modifiedMass distribution from gravitational potential3c2ec2267625
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Physics application; not formalized.
status—not_formalized
addedPoisson's equation17fb8cb7d0ef
modifiedHarmonic functions minimize Dirichlet energy583a70c7c634
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Dirichlet energy is not defined in Mathlib.
status—not_formalized
modifiedDirichlet stationary iff harmonic733a31f83770
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Dirichlet-energy variational characterization of harmonicity is not formalized.
status—not_formalized
modifiedLaplacian in 2D Cartesian coordinates56a27caa553b
FieldFrom #1345To #2462
mathlib.decl—InnerProductSpace.laplacian_eq_iteratedFDeriv_complexPlane
mathlib.match_kind—special_case
mathlib.module—Mathlib.Analysis.InnerProductSpace.Laplacian
note—Gives the 2D formula for `Δ f` on `ℂ` in the `(1, I)` basis, i.e. `∂²/∂x² + ∂²/∂y²`.
status—formalized
modifiedLaplacian in polar coordinates783f4fe3543b
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No explicit polar-coordinate expression for the Laplacian was found.
status—not_formalized
modifiedLaplacian in 3D Cartesian coordinates1598dc9a3bb5
FieldFrom #1345To #2462
mathlib.decl—InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis
mathlib.match_kind—generalization
mathlib.module—Mathlib.Analysis.InnerProductSpace.Laplacian
note—General `n`-D Cartesian formula for `Δ f` via the standard orthonormal basis, which specialises to 3D.
status—formalized
modifiedLaplacian in cylindrical coordinateseea1b0b981cb
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No cylindrical-coordinate Laplacian formula was found.
status—not_formalized
modifiedLaplacian in spherical coordinates5b26ce8822c6
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No spherical-coordinate Laplacian formula was found.
status—not_formalized
modifiedLaplacian in general curvilinear coordinates (3D)c51827e78731
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No curvilinear-coordinate Laplacian formula was found.
status—not_formalized
modifiedLaplacian in N-dim curvilinear coordinatesc4c623dcb09f
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized.
status—not_formalized
modifiedRadial/angular decomposition of Laplacian5c68f003ded0
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No radial/angular decomposition of the Laplacian is present.
status—not_formalized
modifiedSpherical harmonic eigenvalue equationc7e9df6c61db
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Spherical harmonics are not formalized in Mathlib.
status—not_formalized
modifiedRadial equation and solid harmonics0352b1eea21d
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Solid harmonics not formalized.
status—not_formalized
modifiedRadial harmonic functions on annulusa80963ccc12d
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized.
status—not_formalized
modifiedSpherical Laplacian via homogeneous extensiond2bd6d4e8586
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Spherical Laplacian and homogeneous-extension characterization not formalized.
status—not_formalized
modifiedEuclidean equivariance of Laplacianb303304fd03f
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No `laplacian_comp_isometry` / pullback-equivariance lemma was found; `laplacian_CLE_comp_left` covers left composition only.
status—not_formalized
modifiedRotation/translation invariance in 2D98a195137c9d
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Rotation/translation invariance of `Δ` is not stated.
status—not_formalized
modifiedEuclidean group invarianceb34290fb155a
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized.
status—not_formalized
modifiedCharacterization of Euclidean-invariant operatorsf94d0d19eeb6
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized.
status—not_formalized
modifiedAngular Laplacian as Casimire1a924730772
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No quadratic Casimir operator formalized; angular Laplacian not present.
status—not_formalized
modifiedLaplace–Beltrami from Casimir on homogeneous spaces1279e7039d48
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized.
status—not_formalized
modifiedLinearity of the Laplacian6f0f9d14d1dc
FieldFrom #1345To #2462
mathlib.decl—ContDiffAt.laplacian_add
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.InnerProductSpace.Laplacian
note—Additivity, negation, and scalar multiplication are proven under C^2 hypotheses (`laplacian_add`, `laplacian_neg`, `laplacian_smul`).
status—formalized
modifiedEllipticity of the Laplacian80ee10b356ed
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No abstract notion of elliptic differential operator is present in Mathlib.
status—not_formalized
modifiedGreen's identities for the Laplaciancb675e5ae9d7
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Green's identities are not formalized in Mathlib.
status—not_formalized
modifiedFormal self-adjointnessb911f0ef8c79
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized.
status—not_formalized
modifiedEnergy identity6edc136b2269
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized.
status—not_formalized
modifiedHarmonic, subharmonic, superharmonic6b5dff3fa0a7
FieldFrom #1345To #2462
mathlib.decl—InnerProductSpace.HarmonicAt
mathlib.match_kind—special_case
mathlib.module—Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
note—Harmonic functions are formalized; subharmonic and superharmonic are not.
status—partial
modifiedMean value property8dfe8c96a16d
FieldFrom #1345To #2462
mathlib.decl—HarmonicOnNhd.circleAverage_eq
mathlib.match_kind—special_case
mathlib.module—Mathlib.Analysis.Complex.Harmonic.MeanValue
note—The circle-average mean-value property is proven for real-valued harmonic functions on `ℂ`; the higher-dimensional sphere/ball version is not.
status—partial
modifiedMaximum and minimum principles5f5be9e5fc6c
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—A maximum principle for harmonic (as opposed to holomorphic) functions was not found.
status—not_formalized
modifiedElliptic regularity for the Laplacian063064ec989a
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—General elliptic regularity is not formalized.
status—not_formalized
modifiedSmoothness/analyticity of harmonic functions2c33cc8cbd84
FieldFrom #1345To #2462
mathlib.decl—HarmonicAt.analyticAt
mathlib.match_kind—special_case
mathlib.module—Mathlib.Analysis.Complex.Harmonic.Analytic
note—Proven for real-valued harmonic functions on `ℂ`; the general n-dimensional result is not formalized.
status—partial
modifiedWeyl's lemma15f834a7a9d1
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Weyl's lemma (distributional harmonicity ⇒ smoothness) is not formalized.
status—not_formalized
modifiedLaplacian as Fourier multiplier464f44cd940d
FieldFrom #1345To #2462
mathlib.decl—SchwartzMap.laplacian_eq_fourierMultiplierCLM
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Distribution.FourierMultiplier
note—States `Δ f = -(2π)^2 • fourierMultiplierCLM F (‖·‖^2) f` on Schwartz functions; a distributional version is also proven.
status—formalized
modifiedHeat semigroup and fractional powers via Fourierc070bd89a4ec
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Heat semigroup and fractional Laplacian are not formalized.
status—not_formalized
modifiedContinuous spectrum on R^n495c16f17a42
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Spectrum of `-Δ` on `L²(ℝⁿ)` is not formalized.
status—not_formalized
modifiedDiscrete spectrum on bounded domainsbb1898f46d22
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized.
status—not_formalized
modifiedHelmholtz equation2990a0bcd98e
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Helmholtz equation defined.
status—not_formalized
modifiedSpectrum of Laplace–Beltrami on compact manifold32b59f5d6b97
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Laplace–Beltrami on manifolds is not formalized.
status—not_formalized
modifiedFractional Laplacian (Fourier definition)5a5769f04fbf
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No fractional Laplacian is defined.
status—not_formalized
modifiedFractional Laplacian (singular integral)8d8f241db241
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized.
status—not_formalized
modifiedRiesz potential59115628c3ed
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Riesz potential is defined in Mathlib.
status—not_formalized
addedRiesz potential inverts fractional Laplacian68a933552673
modifiedBessel potential0e0118fbce3e
FieldFrom #1345To #2462
mathlib.decl—TemperedDistribution.besselPotential
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Distribution.Sobolev
note—Defined as the Fourier multiplier with symbol `(1 + ‖x‖²)^(s/2)` on tempered distributions.
status—formalized
addedBessel potential spaces12d738aec56f
modifiedVector Laplaciane47a2cfce7a0
FieldFrom #1345To #2462
mathlib.decl—InnerProductSpace.laplacianWithin
mathlib.match_kind—generalization
mathlib.module—Mathlib.Analysis.InnerProductSpace.Laplacian
note—Mathlib's `Δ` is defined for `f : E → F` with `F` an arbitrary normed vector space, so the vector-valued case is subsumed.
status—formalized
modifiedVector Laplacian via Helmholtz decompositionf6751cc2cb10
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No `grad(div F) - curl(curl F)` decomposition or Helmholtz decomposition in Mathlib.
status—not_formalized
modifiedVector Laplacian in Cartesian coordinatesb47ce7de8181
FieldFrom #1345To #2462
mathlib.decl—InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis
mathlib.match_kind—generalization
mathlib.module—Mathlib.Analysis.InnerProductSpace.Laplacian
note—The general orthonormal-basis formula applied to vector-valued `f` gives the componentwise Cartesian form.
status—formalized
modifiedTensor Laplacian2d7fb6705846
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized (no tensor-field Laplacian).
status—not_formalized
modifiedNavier–Stokes equation3413fc99101c
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Navier–Stokes equations are not formalized in Mathlib.
status—not_formalized
modifiedWave equation for electric field824479c1357d
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Maxwell/wave equations for E are not formalized.
status—not_formalized
modifiedHeat semigroupdf768dde4edb
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Heat semigroup not formalized.
status—not_formalized
modifiedSmoothing effect of heat semigroupe1308eec9394
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized.
status—not_formalized
modifiedHeat kernel on manifolds4ad4b3e625d3
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized.
status—not_formalized
modifiedLaplace–Beltrami operator1f51d2124abb
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Laplace–Beltrami operator on Riemannian manifolds is defined.
status—not_formalized
modifiedGeometer's Laplacian8d58f9539548
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized.
status—not_formalized
modifiedHodge Laplacian / Laplace–de Rhamf6e091c5f8ec
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Hodge/Laplace–de Rham operator on differential forms is defined.
status—not_formalized
addedWeitzenböck identityabcd63bd7db8
modifiedD'Alembert operator5755f26a9ad4
FieldFrom #1345To #2462
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—D'Alembertian on Minkowski space is not defined in Mathlib.
status—not_formalized