Derivatives of harmonic functions are harmonic

Let E be a finite-dimensional real inner product space. If f : E → ℝ is harmonic at x, then so is each of its directional derivatives y ↦ Df(y) v (InnerProductSpace.HarmonicAt.fderiv_apply), and so is its gradient ∇f, whose coordinates in an orthonormal basis are directional derivatives (InnerProductSpace.HarmonicAt.gradient). Consequently every estimate proved for harmonic functions, such as the decay of their oscillation and of their integrals on shrinking balls, applies verbatim to the partial derivatives and to the gradient of a harmonic function. This is how gradient decay estimates for solutions of constant-coefficient elliptic equations are reduced to the harmonic case.

Main declarations

• InnerProductSpace.HarmonicAt.fderiv_apply: a directional derivative of a function harmonic at x is harmonic at x.
• InnerProductSpace.HarmonicOnNhd.fderiv_apply: the same on a set.
• InnerProductSpace.HarmonicAt.gradient and InnerProductSpace.HarmonicOnNhd.gradient: the gradient of a harmonic function is harmonic.

Implementation notes

Since harmonicity only asks for two continuous derivatives, the identity Δ (∂ᵥf) = ∂ᵥ(Δf) is not available classically. Instead, ∂ᵥf is a weak derivative of the weakly harmonic function f, hence weakly harmonic (TauCeti.HasWeakLineDerivOn.weaklyHarmonicOn), and being continuous it is harmonic by Weyl's lemma (TauCeti.harmonicOnNhd_iff_weaklyHarmonicOn).

References

• L. C. Evans, Partial Differential Equations, 2nd ed., §2.2.3, Theorem 6 (smoothness of harmonic functions).

theorem InnerProductSpace.HarmonicAt.fderiv_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (hf : HarmonicAt f x) (v : E) : HarmonicAt (fun (y : E) => (fderiv ℝ f y) v) x

Derivatives of harmonic functions are harmonic. If f is harmonic at x, then so is the directional derivative y ↦ Df(y) v, for every direction v.

theorem InnerProductSpace.HarmonicOnNhd.fderiv_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {s : Set E} (hf : HarmonicOnNhd f s) (v : E) : HarmonicOnNhd (fun (y : E) => (fderiv ℝ f y) v) s

Derivatives of harmonic functions are harmonic. If f is harmonic on s, then so is the directional derivative y ↦ Df(y) v, for every direction v.

theorem InnerProductSpace.HarmonicAt.gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (hf : HarmonicAt f x) : HarmonicAt (_root_.gradient f) x

The gradient of a harmonic function is harmonic. If f is harmonic at x, then so is its gradient ∇f, as a vector-valued function: in an orthonormal basis its coordinates are the directional derivatives of f.

theorem InnerProductSpace.HarmonicOnNhd.gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {s : Set E} (hf : HarmonicOnNhd f s) : HarmonicOnNhd (_root_.gradient f) s

The gradient of a harmonic function is harmonic. If f is harmonic on s, then so is its gradient ∇f.