Theorems · Theorem · potential theory

InnerProductSpace.laplacianWithin_smul

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra ℝ 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : InnerProductSpace ℝ E] [inst_4 : FiniteDimensional ℝ E] {F : Type u_3}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F] [inst_7 : NormedSpace 𝕜 F] [IsScalarTower ℝ 𝕜 F]
  {f : E → F} {x : E} {s : Set E} (v : 𝕜),
  ContDiffWithinAt ℝ 2 f s x →
    UniqueDiffOn ℝ s →
      x ∈ s → InnerProductSpace.laplacianWithin (v • f) s x = v • InnerProductSpace.laplacianWithin f s x

The Laplacian commutes with scalar multiplication.

Defined in

Mathlib.Analysis.InnerProductSpace.Laplacian

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAlgebraNormedAddCommGroupInnerProductSpaceFiniteDimensionalNormedAddCommGroupNormedSpaceNormedSpaceIsScalarTower