Radial symmetry for positive semilinear Poisson solutions

semilinear_poisson_radial_symmetry — a formalization challenge from the lean-eval benchmark.

Formal statement

/-- **Radial symmetry theorem.** Let `u ∈ C^2(closedBall 0 1)` be a positive
solution of the semilinear Poisson problem `-Δ u = f(u)` in the open unit ball,
with zero Dirichlet boundary values on the unit sphere. If `f : ℝ → ℝ` is
Lipschitz, then `u` is radial: `u x = v ‖x‖` for a nonnegative strictly
decreasing radial profile `v` on `[0, 1]`. -/
theorem 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‖ := by
  sorry

Informal solution sketch

Use the method of moving planes. Compare u with its reflection across a moving hyperplane.

Source

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.

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: semilinear_poisson_radial_symmetry
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Yongxi Lin.