Distributions

Test functions, Schwartz functions, tempered distributions and distributional derivatives: principal values, Plemelj limits, Dirac comb, partitions of unity.

• Distributional derivatives
• Schwartz space
• Sokhotski–Plemelj formula

TheoremExistence of the Cauchy principal value of \(\varphi(x)/x\)#●ready to prove

For every real-valued Schwartz function \(\varphi\) on \(\mathbb{R}\) there is a real number \(L\) such that \(\int_{\{x \in \mathbb{R} \,:\, |x| \ge \varepsilon\}} \varphi(x)/x \, dx \to L\) as \(\varepsilon \to 0^+\), the integrals being taken with respect to Lebesgue measure.

public theorem_wanted cauchyPrincipalValue_exists (φ : 𝓢(ℝ, ℝ)) :
    ∃ L : ℝ, Filter.Tendsto (fun ε : ℝ => ∫ x in {x : ℝ | ε ≤ |x|}, φ x / x ∂volume)
      (nhdsWithin 0 (Set.Ioi 0)) (nhds L)

Sources

• F. Friedlander and M. Joshi, Introduction to the Theory of Distributions, Ch. 2.

TheoremSmooth partitions of unity subordinate to a finite open cover#●ready to prove

Let \(E\) be a finite-dimensional real normed space, \(K \subseteq E\) a compact set, and \((U_i)_{i \in \iota}\) a finite family of open subsets of \(E\) with \(K \subseteq \bigcup_i U_i\). Then there are smooth compactly supported functions \(\varphi_i : E \to \mathbb{R}\), one for each \(i \in \iota\), such that \(\varphi_i(x) \ge 0\) for all \(i\) and all \(x \in E\), the closed support of each \(\varphi_i\) is contained in \(U_i\), and \(\sum_{i \in \iota} \varphi_i(x) = 1\) for every \(x \in K\).

public theorem_wanted testFunction_partitionOfUnity
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {ι : Type*} [Fintype ι] {K : Set E} (hK : IsCompact K)
    {U : ι → Opens E} (hKU : K ⊆ ⋃ i, ↑(U i)) :
    ∃ φ : ι → 𝓓(⊤, ℝ),
      (∀ i x, 0 ≤ φ i x) ∧ (∀ i, tsupport (φ i) ⊆ ↑(U i)) ∧ ∀ x ∈ K, ∑ i, φ i x = 1

Sources

• https://en.wikipedia.org/wiki/Partition_of_unity.

TheoremThe Dirac comb is a tempered distribution#●ready to prove

There is a tempered distribution \(T\) on \(\mathbb{R}\), that is, a continuous \(\mathbb{C}\)-linear functional on the space of complex-valued Schwartz functions on \(\mathbb{R}\), such that \(T(g)=\sum_{n\in\mathbb{Z}} g(n)\) for every complex-valued Schwartz function \(g\) on \(\mathbb{R}\).

public theorem_wanted diracComb_toTemperedDistribution :
    ∃ T : 𝓢'(ℝ, ℂ), ∀ g : 𝓢(ℝ, ℂ), T g = ∑' n : ℤ, g (n : ℝ)

Sources

• https://en.wikipedia.org/wiki/Dirac_comb.

3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.