Subharmonic functions

DefinitionSubharmonic functions on the plane#✓fully proved

A function \(\varphi : \mathbb{R} \times \mathbb{R} \to \mathbb{R}\) is subharmonic if it is upper semicontinuous and, for every point \((a, b)\) of the plane and every radius \(r > 0\),

\[ \varphi(a, b) \le \frac{1}{2\pi} \int_0^{2\pi} \varphi(a + r\cos\theta, b + r\sin\theta)\, d\theta. \]

The integral is taken to be \(0\) when the integrand is not integrable over \([0, 2\pi]\), so for such a circle the condition only says \(\varphi(a, b) \le 0\).

def IsSubharmonic (φ : ℝ × ℝ → ℝ) : Prop :=
  UpperSemicontinuous φ ∧ ∀ (p : ℝ × ℝ) (r : ℝ), 0 < r →
    φ p ≤ (1 / (2 * Real.pi)) * ∫ θ in (0 : ℝ)..(2 * Real.pi),
      φ (p.1 + r * Real.cos θ, p.2 + r * Real.sin θ)

Used by 1

Used bySubharmonic functions with second partial derivatives have nonnegative Laplacian

DefinitionExistence of the pure second partial derivatives#✓fully proved

A function \(\varphi : \mathbb{R} \times \mathbb{R} \to \mathbb{R}\) has second partial derivatives if at every point of the plane the partial derivatives \(\varphi_x\) and \(\varphi_y\) exist, and the partial derivatives \(\varphi_{xx} = (\varphi_x)_x\) and \(\varphi_{yy} = (\varphi_y)_y\) also exist.

def HasSecondPartialDerivatives (φ : ℝ × ℝ → ℝ) : Prop :=
  ∀ p : ℝ × ℝ,
    DifferentiableAt ℝ (fun s => φ (s, p.2)) p.1 ∧
    DifferentiableAt ℝ (fun t => deriv (fun s => φ (s, p.2)) t) p.1 ∧
    DifferentiableAt ℝ (fun s => φ (p.1, s)) p.2 ∧
    DifferentiableAt ℝ (fun t => deriv (fun s => φ (p.1, s)) t) p.2

Used by 1

Used bySubharmonic functions with second partial derivatives have nonnegative Laplacian

TheoremSubharmonic functions with second partial derivatives have nonnegative Laplacian#●ready to prove

Let \(\varphi : \mathbb{R} \times \mathbb{R} \to \mathbb{R}\) be subharmonic, and suppose that its partial derivatives \(\varphi_x\), \(\varphi_{xx}\), \(\varphi_y\) and \(\varphi_{yy}\) exist at every point of the plane. Then \(\varphi_{xx}(p) + \varphi_{yy}(p) \ge 0\) for every point \(p\) of the plane.

The point is that this is not immediate outside the (dense) set where the second derivatives are continuous.

theorem_wanted saks184_subharmonic_laplacian_nonneg :
    ∀ φ : ℝ × ℝ → ℝ, IsSubharmonic φ → HasSecondPartialDerivatives φ →
      ∀ p : ℝ × ℝ, 0 ≤ deriv (fun t => deriv (fun s => φ (s, p.2)) t) p.1 +
        deriv (fun t => deriv (fun s => φ (p.1, s)) t) p.2

Sources

• S. Saks, Problem 184 of the Scottish Book; solved by A. Eremenko, "A problem of Stanislaw Saks", Mat. Stud. 52 (2019), 173-175 (arXiv:1911.09530). See the commentary in R. D. Mauldin (ed.), The Scottish Book, 2nd ed. (Birkhäuser, 2015).

Uses 2

Statement usesExistence of the pure second partial derivatives · Subharmonic functions on the plane

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.