Radial symmetry of semilinear elliptic equations

DefinitionSemilinear Poisson problem on the unit ball#✓fully proved

Let \(n\) be a natural number, let \(f : \mathbb{R} \to \mathbb{R}\), and let \(u : \mathbb{R}^n \to \mathbb{R}\) be a function on Euclidean space. Then \(u\) solves the semilinear Poisson problem for \(f\) if \(-\Delta u(x) = f(u(x))\) for every \(x\) in the open unit ball and \(u(x) = 0\) for every \(x\) on the unit sphere.

The definition imposes no differentiability on \(u\); regularity is assumed separately where it is needed.

def SolvesSemilinearPoisson {n : ℕ} (f : ℝ → ℝ) (u : EuclideanSpace ℝ (Fin n) → ℝ) : Prop :=
  (∀ x ∈ ball 0 1, -Laplacian.laplacian u x = f (u x)) ∧ ∀ x ∈ sphere 0 1, u x = 0

Used by 1

Used byRadial symmetry of positive solutions of the semilinear Poisson problem

TheoremRadial symmetry of positive solutions of the semilinear Poisson problem#●ready to prove

Let \(n \ge 1\), let \(f : \mathbb{R} \to \mathbb{R}\) be Lipschitz, and let \(u : \mathbb{R}^n \to \mathbb{R}\) be a function on Euclidean space that is \(C^2\) on the closed unit ball \(\overline{B}\). Suppose that \(u\) solves the semilinear Poisson problem for \(f\), that is, \(-\Delta u = f(u)\) on the open unit ball \(B\) and \(u = 0\) on the unit sphere, and that \(u > 0\) on \(B\). Then there is a function \(v : \mathbb{R} \to [0, \infty)\) that is strictly decreasing on \([0, 1]\) and satisfies \(u(x) = v(\|x\|)\) for every \(x \in \overline{B}\).

public theorem_wanted semilinear_poisson_radial_symmetry {n : ℕ} (hn : 0 < n)
    {f : ℝ → ℝ} (u : EuclideanSpace ℝ (Fin n) → ℝ)
    (hf_lipschitz : ∃ K : ℝ≥0, LipschitzWith K f)
    (hu_c2 : ContDiffOn ℝ 2 u (closedBall 0 1))
    (hu_solve : SolvesSemilinearPoisson f u)
    (hu_positive : ∀ x ∈ ball 0 1, 0 < u x) :
    ∃ v : ℝ → ℝ≥0,
      StrictAntiOn v (Set.Icc (0 : ℝ) 1) ∧
        ∀ x ∈ closedBall 0 1, u x = v ‖x‖

Sources

• B. Gidas, W. M. Ni, and L. Nirenberg, Symmetry and related properties via the maximum principle, Comm. Math. Phys. 68 (1979), 209-243. Also stated as Theorem 2 (Radial symmetry) in L. C. Evans, Partial Differential Equations, Section 9 on nonvariational techniques. Problem semilinear_poisson_radial_symmetry of the lean-eval benchmark.

Uses 1

Statement usesSemilinear Poisson problem on the unit ball

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.