Constant-direction derivatives preserve harmonicity on open sets

Proved

HunterPDE.Harmonic.harmonic_directional_derivative

by Mazecto · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

derivative-estimatesharmonic-functionspde

Let $n\ge1$ , let $\Omega\subseteq\mathbb R^n$ be open, and let $u:\mathbb R^n\to\mathbb R$ be harmonic near every point of $\Omega$ . For every constant vector $v\in\mathbb R^n$ , the directional derivative is harmonic on the same open set:

D_vu(y)=Du(y)[v],\qquad \Delta(D_vu)=0\quad\text{on }\Omega.

This closure property allows interior estimates to be applied repeatedly to derivatives of harmonic functions.

Preamble

import Theorems.Thm_HunterPDE_Harmonic_mean_value_property
import Theorems.Thm_HunterPDE_Harmonic_smooth_of_mean_value_property
import Theorems.Thm_HunterPDE_Harmonic_directional_derivative_mean_value
import Mathlib.Analysis.Calculus.ContDiff.Comp

open HunterPDE.Harmonic Filter Topology Laplacian
open scoped ContDiff
set_option autoImplicit false

Formal statement

theorem HunterPDE.Harmonic.harmonic_directional_derivative {n : ℕ} (hn : 0 < n)
    {Ω : Set (EuclideanSpace ℝ (Fin n))} {u : EuclideanSpace ℝ (Fin n) → ℝ}
    (hΩ : IsOpen Ω) (hu : InnerProductSpace.HarmonicOnNhd u Ω)
    (v : EuclideanSpace ℝ (Fin n)) :
    InnerProductSpace.HarmonicOnNhd (fun y => fderiv ℝ u y v) Ω := by sorry

Source

Hunter, Notes on Partial Differential Equations (revised 6/18/2014), https://www.math.ucdavis.edu/~hunter/pdes/ch2.pdf, pp. 21 and 23–24, Theorems 2.1–2.2 and proof of Theorem 2.9; generalized to constant directions / families satisfying first-derivative estimates.

View graph