Harmonic extension to a half-space

AbbreviationThe Euclidean plane#✓fully proved

The Euclidean plane \(\mathbb{R}^2\) is the space of pairs of real numbers with the Euclidean inner product and norm.

abbrev R2 : Type := EuclideanSpace ℝ (Fin 2)

Used by 2

Used byDecay of bounded harmonic extensions of Schwartz data in a half-space · Appending a third coordinate

AbbreviationEuclidean three-space#✓fully proved

Euclidean three-space \(\mathbb{R}^3\) is the space of triples of real numbers with the Euclidean inner product and norm.

abbrev R3 : Type := EuclideanSpace ℝ (Fin 3)

Used by 4

Used byDecay of bounded harmonic extensions of Schwartz data in a half-space · Closed lower half-space · Open lower half-space · Appending a third coordinate

AbbreviationClosed lower half-space#✓fully proved

The closed lower half-space is the set of points \((p_1, p_2, p_3)\) of Euclidean three-space \(\mathbb{R}^3\) with \(p_3 \le 0\).

abbrev LowerHalfSpace : Set R3 := {p : R3 | p 2 ≤ 0}

Uses 1 · Used by 1

Statement usesEuclidean three-space

Used byDecay of bounded harmonic extensions of Schwartz data in a half-space

AbbreviationOpen lower half-space#✓fully proved

The open lower half-space is the set of points \((p_1, p_2, p_3)\) of Euclidean three-space \(\mathbb{R}^3\) with \(p_3 < 0\).

abbrev OpenLowerHalfSpace : Set R3 := {p : R3 | p 2 < 0}

Uses 1 · Used by 1

Statement usesEuclidean three-space

Used byDecay of bounded harmonic extensions of Schwartz data in a half-space

DefinitionAppending a third coordinate#✓fully proved

For a point \(x = (x_1, x_2)\) of the Euclidean plane \(\mathbb{R}^2\) and a real number \(z\), this is the point \((x_1, x_2, z)\) of Euclidean three-space \(\mathbb{R}^3\).

noncomputable def point3 (x : R2) (z : ℝ) : R3 :=
  EuclideanSpace.single (0 : Fin 3) (x 0) +
    EuclideanSpace.single (1 : Fin 3) (x 1) +
      EuclideanSpace.single (2 : Fin 3) z

Uses 2 · Used by 1

Statement usesThe Euclidean plane · Euclidean three-space

Used byDecay of bounded harmonic extensions of Schwartz data in a half-space

TheoremDecay of bounded harmonic extensions of Schwartz data in a half-space#●ready to prove

Write a point of \(\mathbb{R}^3\) as \((x, z)\) with \(x = (x_1, x_2) \in \mathbb{R}^2\) and \(z \in \mathbb{R}\). Let \(\phi : \mathbb{R}^2 \to \mathbb{R}\) be a Schwartz function and let \(u : \mathbb{R}^3 \to \mathbb{R}\) be harmonic at every point of the open lower half-space \(\{(x, z) : z < 0\}\), continuous on the closed lower half-space \(\{(x, z) : z \le 0\}\) and bounded there, with \(u(x, 0) = \phi(x)\) for every \(x \in \mathbb{R}^2\). Suppose that \(u(x, z) \to 0\) as \(z \to -\infty\) uniformly in \(x\): for every \(\varepsilon > 0\) there is \(z_0\) such that \(|u(x, z)| < \varepsilon\) for all \(z \le z_0\) and all \(x \in \mathbb{R}^2\). Then there is a constant \(C > 0\) such that \(|u(x, z)| \le C (1 + |z|)^{-1}\) for all \(z \le 0\) and all \(x \in \mathbb{R}^2\).

Boundedness of \(u\) is not among the hypotheses of the source problem, but the bound fails without it: adding to the Poisson extension of \(\phi\) the harmonic function \(\operatorname{Im} G(x_1 + iz)\) built from Newman's entire function \(G\), which vanishes on \(z = 0\) and as \(z \to -\infty\) but is unbounded near the boundary, gives a counterexample.

public theorem_wanted exists_abs_le_inv_one_add_abs_of_harmonic_lowerHalfSpace
  (φ : SchwartzMap R2 ℝ)
  (u : R3 → ℝ)
  (hu_harmonic : InnerProductSpace.HarmonicOnNhd u OpenLowerHalfSpace)
  (hu_cont : ContinuousOn u LowerHalfSpace)
  (hu_bdd : ∃ M : ℝ, ∀ p ∈ LowerHalfSpace, |u p| ≤ M)
  (hu_boundary : ∀ x : R2, u (point3 x 0) = φ x)
  (hu_decay :
    ∀ ε : ℝ, 0 < ε →
      ∀ᶠ z : ℝ in Filter.atBot, ∀ x : R2, |u (point3 x z)| < ε) :
  ∃ C : ℝ, 0 < C ∧
    ∀ z : ℝ, z ≤ 0 →
      ∀ x : R2, |u (point3 x z)| ≤ C * (1 + |z|)⁻¹

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Operator theory; Integral, integro-differential, and pseudodifferential operators), problem ma_proofbench_l2_72, with the change above.

Uses 5

Statement usesClosed lower half-space · Open lower half-space · The Euclidean plane · Euclidean three-space · Appending a third coordinate

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.