Radial symmetry for positive semilinear Poisson solutions

Problem statement

Notes: Unavailable.

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.

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

theorem declaration uses `sorry`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 : LeanEval.Analysis.PDE.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‖ := byn:ℕhn:0 < nf:ℝ → ℝu:EuclideanSpace ℝ (Fin n) → ℝhf_lipschitz:∃ K, LipschitzWith K fhu_c2:ContDiffOn ℝ 2 u (closedBall 0 1)hu_solve:SolvesSemilinearPoisson f uhu_positive:∀ x ∈ ball 0 1, 0 < u x⊢ ∃ v, StrictAntiOn v (Set.Icc 0 1) ∧ ∀ x ∈ closedBall 0 1, u x = ↑(v ‖x‖)
  sorryAll goals completed! 🐙