Sokhotski–Plemelj formula

DefinitionThe pairing with \((x + i\varepsilon)^{-1}\)#✓fully proved

For a real number \(\varepsilon\) and a Schwartz function \(\phi : \mathbb{R} \to \mathbb{C}\), \(u_{+,\varepsilon}(\phi)\) is the complex number \(\int_{\mathbb{R}} (x + i\varepsilon)^{-1}\phi(x)\, dx\).

The integral is the Lebesgue integral, taken to be \(0\) when the integrand is not integrable; this can happen only for \(\varepsilon = 0\).

def uPlusEps (ε : ℝ) (φ : SchwartzMap ℝ ℂ) : ℂ :=
  ∫ x : ℝ, (((x : ℂ) + (ε : ℂ) * Complex.I)⁻¹) * φ x

Used by 1

Used byThe tempered distributions \((x \pm i\varepsilon)^{-1}\) converge as \(\varepsilon \to 0^+\)

DefinitionThe pairing with \((x - i\varepsilon)^{-1}\)#✓fully proved

For a real number \(\varepsilon\) and a Schwartz function \(\phi : \mathbb{R} \to \mathbb{C}\), \(u_{-,\varepsilon}(\phi)\) is the complex number \(\int_{\mathbb{R}} (x - i\varepsilon)^{-1}\phi(x)\, dx\).

The integral is the Lebesgue integral, taken to be \(0\) when the integrand is not integrable; this can happen only for \(\varepsilon = 0\).

def uMinusEps (ε : ℝ) (φ : SchwartzMap ℝ ℂ) : ℂ :=
  ∫ x : ℝ, (((x : ℂ) - (ε : ℂ) * Complex.I)⁻¹) * φ x

Used by 1

Used byThe tempered distributions \((x \pm i\varepsilon)^{-1}\) converge as \(\varepsilon \to 0^+\)

TheoremThe tempered distributions \((x \pm i\varepsilon)^{-1}\) converge as \(\varepsilon \to 0^+\)#●ready to prove

Write \(S(\mathbb{R})\) for the space of complex-valued Schwartz functions on \(\mathbb{R}\), and for \(\varepsilon > 0\) and \(\phi \in S(\mathbb{R})\) let \(u_{\pm,\varepsilon}(\phi) = \int_{\mathbb{R}} (x \pm i\varepsilon)^{-1}\phi(x)\, dx\). Then for every \(\varepsilon > 0\) both \(u_{+,\varepsilon}\) and \(u_{-,\varepsilon}\) are tempered distributions, that is, continuous \(\mathbb{C}\)-linear functionals on \(S(\mathbb{R})\), and there are tempered distributions \(u_+\) and \(u_-\) such that \(u_{+,\varepsilon}(\phi) \to u_+(\phi)\) and \(u_{-,\varepsilon}(\phi) \to u_-(\phi)\) as \(\varepsilon \to 0^+\) for every \(\phi \in S(\mathbb{R})\).

public theorem_wanted exists_temperedDistribution_tendsto_inv_add_mul_I :
    (∀ ε > 0,
      ∃ uPlus_eps uMinus_eps : TemperedDistribution ℝ ℂ,
        (∀ φ : SchwartzMap ℝ ℂ, uPlus_eps φ = uPlusEps ε φ) ∧
          (∀ φ : SchwartzMap ℝ ℂ, uMinus_eps φ = uMinusEps ε φ)) ∧
    (∃ uPlus uMinus : TemperedDistribution ℝ ℂ,
      (∀ φ : SchwartzMap ℝ ℂ,
        Filter.Tendsto (fun ε : ℝ => uPlusEps ε φ)
          (nhdsWithin 0 (Set.Ioi (0 : ℝ))) (nhds (uPlus φ))) ∧
      (∀ φ : SchwartzMap ℝ ℂ,
        Filter.Tendsto (fun ε : ℝ => uMinusEps ε φ)
          (nhdsWithin 0 (Set.Ioi (0 : ℝ))) (nhds (uMinus φ))))

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functional analysis; Distributions, generalized functions, distribution spaces), problem ma_proofbench_l2_15.

Uses 2

Statement usesThe pairing with \((x - i\varepsilon)^{-1}\) · The pairing with \((x + i\varepsilon)^{-1}\)

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.