Commit 2025-07-04 05:47 ed930916

View on Github →

feat: introduce the Laplace operator (#26302) This PR continues the work from #25441. Original PR: https://github.com/leanprover-community/mathlib4/pull/25441

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Calculus/ContDiff/Basic.lean

added theorem ContinuousLinearEquiv.iteratedFDeriv_comp_left

Modified Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean

added theorem Filter.EventuallyEq.iteratedFDeriv

Created Mathlib/Analysis/InnerProductSpace/Laplacian.lean

added theorem ContDiffAt.laplacianWithin_add_nhdsWithin

added theorem ContDiffAt.laplacian_CLM_comp_left

added theorem ContDiffAt.laplacian_add

added theorem ContDiffAt.laplacian_add_nhds

added theorem ContDiffWithinAt.laplacianWithin_CLM_comp_left

added theorem ContDiffWithinAt.laplacianWithin_add

added theorem InnerProductSpace.laplacianWithin_CLE_comp_left

added theorem InnerProductSpace.laplacianWithin_congr_nhdsWithin

added theorem InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_complexPlane

added theorem InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis

added theorem InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis

added theorem InnerProductSpace.laplacianWithin_smul

added theorem InnerProductSpace.laplacianWithin_univ

added theorem InnerProductSpace.laplacian_CLE_comp_left

added theorem InnerProductSpace.laplacian_congr_nhds

added theorem InnerProductSpace.laplacian_eq_iteratedFDeriv_complexPlane

added theorem InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis

added theorem InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis

added theorem InnerProductSpace.laplacian_smul

added theorem bilinearIteratedFDerivTwo_eq_iteratedFDeriv

added theorem bilinearIteratedFDerivWithinTwo_eq_iteratedFDeriv

added theorem tensorIteratedFDerivTwo_eq_iteratedFDeriv

added theorem tensorIteratedFDerivWithinTwo_eq_iteratedFDerivWithin