Determining tempered distributions by real test functions #
Two complex-linear tempered distributions agree if they agree on real-valued smooth, compactly supported functions, embedded in complex Schwartz space. This connects the real test functions used to define weak derivatives with the complex tests used in Fourier analysis.
The density input is SchwartzMap.dense_hasCompactSupport. See L. Hörmander,
The Analysis of Linear Partial Differential Operators I, Section 7.1.
theorem
TauCeti.temperedDistribution_ext_real
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℂ F]
{u v : TemperedDistribution E F}
(h :
∀ (φ : SchwartzMap E ℝ),
HasCompactSupport ⇑φ →
u ((SchwartzMap.postcompCLM Complex.ofRealCLM) φ) = v ((SchwartzMap.postcompCLM Complex.ofRealCLM) φ))
:
Real-valued compactly supported Schwartz functions determine a complex-linear tempered
distribution. The real functions are embedded in complex Schwartz space by Complex.ofRealCLM.