Theorems · Theorem · potential theory

InnerProductSpace.laplacianWithin_eq_iteratedDerivWithin_real

∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {e : ℝ} {s : Set ℝ} (f : ℝ → F),
  UniqueDiffOn ℝ s → e ∈ s → InnerProductSpace.laplacianWithin f s e = iteratedDerivWithin 2 f s e

For a function on ℝ, the Laplacian is the second derivative: version within a set.

Defined in

Mathlib.Analysis.InnerProductSpace.Laplacian

Cited by

1 results in Mathlib

Foundations

Depth 244 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace