Theorems · Definition · potential theory

InnerProductSpace.HarmonicAt

{E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] →
      [FiniteDimensional ℝ E] → {F : Type u_2} → [inst : NormedAddCommGroup F] → [NormedSpace ℝ F] → (E → F) → E → Prop

Let E be a real, finite-dimensional, inner product space and x be a point of E. A function f on E is harmonic at x if it is two times continuously ℝ-differentiable and if its Laplacian vanishes in a neighborhood of x.

Defined in

Mathlib.Analysis.InnerProductSpace.Harmonic.Basic

Cited by

23 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceFiniteDimensionalNormedAddCommGroupNormedSpace