Harmonicity of actual coordinate derivatives on an open subset of R³.

theorem EulerMeanHarmonic.partialDerivative_sum (f : Fin 3 → EulerSmoothLimit.Space → ℝ) (hf : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (f i)) (j : Fin 3) (x : EulerSmoothLimit.Space) : EulerVectorCalculus.partialDerivative (fun (y : EulerSmoothLimit.Space) => ∑ i : Fin 3, f i y) j x = ∑ i : Fin 3, EulerVectorCalculus.partialDerivative (f i) j x

theorem EulerMeanHarmonic.laplacian_partialDerivative (f : EulerSmoothLimit.Space → ℝ) (hf : ContDiff ℝ (↑⊤) f) (i : Fin 3) (x : EulerSmoothLimit.Space) : Laplacian.laplacian (EulerVectorCalculus.partialDerivative f i) x = EulerVectorCalculus.partialDerivative (Laplacian.laplacian f) i x

theorem EulerMeanHarmonic.partialDerivative_harmonic_on (f : EulerSmoothLimit.Space → ℝ) (hf : ContDiff ℝ (↑⊤) f) (U : Set EulerSmoothLimit.Space) (hU : IsOpen U) (hh : ∀ x ∈ U, Laplacian.laplacian f x = 0) (i : Fin 3) (x : EulerSmoothLimit.Space) : x ∈ U → Laplacian.laplacian (EulerVectorCalculus.partialDerivative f i) x = 0

Differentiating a harmonic function preserves harmonicity on the same open set.

def EulerMeanHarmonic.wordDerivative : List (Fin 3) → (EulerSmoothLimit.Space → ℝ) → EulerSmoothLimit.Space → ℝ

Word derivative as an element of word, f => partialDerivative (wordDerivative word f) i.

Equations

• EulerMeanHarmonic.wordDerivative [] x✝ = x✝
• EulerMeanHarmonic.wordDerivative (i :: word) x✝ = EulerVectorCalculus.partialDerivative (EulerMeanHarmonic.wordDerivative word x✝) i

theorem EulerMeanHarmonic.wordDerivative_smooth (word : List (Fin 3)) (f : EulerSmoothLimit.Space → ℝ) (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (wordDerivative word f)

theorem EulerMeanHarmonic.wordDerivative_harmonic_on (word : List (Fin 3)) (f : EulerSmoothLimit.Space → ℝ) (hf : ContDiff ℝ (↑⊤) f) (U : Set EulerSmoothLimit.Space) (hU : IsOpen U) (hh : ∀ x ∈ U, Laplacian.laplacian f x = 0) (x : EulerSmoothLimit.Space) : x ∈ U → Laplacian.laplacian (wordDerivative word f) x = 0