Documentation

TauCeti.Analysis.PDE.Ellipticity.ConstantCoefficient

Constant-coefficient elliptic operators as the Laplacian in linear coordinates #

Let A be a constant n × n coefficient matrix whose quadratic form satisfies λ ‖ξ‖² ≤ ξᵀ A ξ ≤ Λ ‖ξ‖² with 0 < λ. This file shows that the operator u ↦ ∑ᵢⱼ Aᵢⱼ ∂ᵢ∂ⱼu is the Laplacian after a linear change of variables whose stretching is controlled by λ and Λ, so that C² solutions of ∑ᵢⱼ Aᵢⱼ ∂ᵢ∂ⱼu = 0 become harmonic functions in the new coordinates. This reduces questions about constant-coefficient elliptic equations, such as decay estimates on balls, to the corresponding questions for harmonic functions. The same holds for the gradient of a solution, so that its decay on balls also follows from that of harmonic functions.

The argument #

Only the symmetric part S of A enters the operator, because the second derivative of u is symmetric. Let T = √S, the positive square root of the positive definite matrix S. By the chain rule Δ (u ∘ T) = (∑ᵢⱼ (T Tᵀ)ᵢⱼ ∂ᵢ∂ⱼu) ∘ T (TauCeti.laplacian_comp_toEuclideanCLE_apply), and T Tᵀ = S. Since ‖T y‖² = yᵀ A y, the map T stretches lengths by at most √Λ and its inverse by at most 1 / √λ.

Main declarations #

References #

theorem TauCeti.PDE.exists_continuousLinearEquiv_laplacian_comp_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {A : Matrix ι ι ℝ} {lam Lam : ℝ} (hlam : 0 < lam) (hA : ∀ (ξ : EuclideanSpace ℝ ι), lam * ‖ξ‖ ^ 2 ≤ A.toQuadraticForm' ξ.ofLp) (hA' : ∀ (ξ : EuclideanSpace ℝ ι), A.toQuadraticForm' ξ.ofLp ≤ Lam * ‖ξ‖ ^ 2) :
∃ (e : EuclideanSpace ℝ ι ≃L[ℝ] EuclideanSpace ℝ ι), (∀ (x : EuclideanSpace ℝ ι), ‖e.symm x‖ ≤ (√lam)⁻¹ * ‖x‖) ∧ (∀ (y : EuclideanSpace ℝ ι), ‖e y‖ ≤ √Lam * ‖y‖) ∧ ∀ (u : EuclideanSpace ℝ ι → F) (y : EuclideanSpace ℝ ι), ContDiffAt ℝ 2 u (e y) → Laplacian.laplacian (u ∘ ⇑e) y = ∑ i : ι, ∑ j : ι, A i j • ((fderiv ℝ (fderiv ℝ u) (e y)) (EuclideanSpace.single i 1)) (EuclideanSpace.single j 1)

A constant-coefficient operator is the Laplacian in suitable linear coordinates. Let A be a square matrix whose quadratic form satisfies λ ‖ξ‖² ≤ ξᵀ A ξ ≤ Λ ‖ξ‖² with 0 < λ. Then there is a continuous linear automorphism e of EuclideanSpace ℝ ι, with ‖e⁻¹ x‖ ≤ ‖x‖ / √λ and ‖e y‖ ≤ √Λ ‖y‖, such that

Δ (u ∘ e) y = ∑ᵢⱼ Aᵢⱼ ∂ᵢ∂ⱼu (e y)

for every u twice continuously differentiable near e y. So u solves ∑ᵢⱼ Aᵢⱼ ∂ᵢ∂ⱼu = 0 exactly when u ∘ e is harmonic. One can take e to be the square root of the symmetric part of A; only the symmetric part matters, since the second derivative of u is symmetric.

theorem TauCeti.PDE.harmonicOnNhd_comp_of_sum_smul_fderiv_fderiv_eq_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {A : Matrix ι ι ℝ} {e : EuclideanSpace ℝ ι ≃L[ℝ] EuclideanSpace ℝ ι} (he : ∀ (u : EuclideanSpace ℝ ι → F) (y : EuclideanSpace ℝ ι), ContDiffAt ℝ 2 u (e y) → Laplacian.laplacian (u ∘ ⇑e) y = ∑ i : ι, ∑ j : ι, A i j • ((fderiv ℝ (fderiv ℝ u) (e y)) (EuclideanSpace.single i 1)) (EuclideanSpace.single j 1)) {s : Set (EuclideanSpace ℝ ι)} (hs : IsOpen s) {u : EuclideanSpace ℝ ι → F} (hu : ContDiffOn ℝ 2 u s) (hLu : ∀ x ∈ s, ∑ i : ι, ∑ j : ι, A i j • ((fderiv ℝ (fderiv ℝ u) x) (EuclideanSpace.single i 1)) (EuclideanSpace.single j 1) = 0) :

Solutions become harmonic after the change of variables. If e is a continuous linear automorphism with Δ (u ∘ e) = (∑ᵢⱼ Aᵢⱼ ∂ᵢ∂ⱼu) ∘ e for every u that is C² at the relevant point, as provided by exists_continuousLinearEquiv_laplacian_comp_eq, then a C² solution of ∑ᵢⱼ Aᵢⱼ ∂ᵢ∂ⱼu = 0 on an open set s becomes harmonic on e ⁻¹' s.

theorem TauCeti.PDE.harmonicOnNhd_gradient_comp_of_sum_smul_fderiv_fderiv_eq_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : Matrix ι ι ℝ} {e : EuclideanSpace ℝ ι ≃L[ℝ] EuclideanSpace ℝ ι} (he : ∀ (u : EuclideanSpace ℝ ι → ℝ) (y : EuclideanSpace ℝ ι), ContDiffAt ℝ 2 u (e y) → Laplacian.laplacian (u ∘ ⇑e) y = ∑ i : ι, ∑ j : ι, A i j • ((fderiv ℝ (fderiv ℝ u) (e y)) (EuclideanSpace.single i 1)) (EuclideanSpace.single j 1)) {s : Set (EuclideanSpace ℝ ι)} (hs : IsOpen s) {u : EuclideanSpace ℝ ι → ℝ} (hu : ContDiffOn ℝ 2 u s) (hLu : ∀ x ∈ s, ∑ i : ι, ∑ j : ι, A i j • ((fderiv ℝ (fderiv ℝ u) x) (EuclideanSpace.single i 1)) (EuclideanSpace.single j 1) = 0) :

The gradient of a solution becomes harmonic after the change of variables. If e is a continuous linear automorphism with Δ (u ∘ e) = (∑ᵢⱼ Aᵢⱼ ∂ᵢ∂ⱼu) ∘ e for every scalar u that is C² at the relevant point, as provided by exists_continuousLinearEquiv_laplacian_comp_eq, and u is a scalar C² solution of ∑ᵢⱼ Aᵢⱼ ∂ᵢ∂ⱼu = 0 on an open set s, then ∇u ∘ e is harmonic on e ⁻¹' s: it is the image of the gradient of the harmonic u ∘ e under the adjoint of e⁻¹.