Skip to content

Commit 993928b

Browse files
mcdollmcdoll
committed
feat(Analysis/Distribution): definition of tempered distributions (#31757)
Define the space of tempered distributions as an abbreviation. We also prove the abstract convergence results for `PointwiseConvergenceCLM` and define the Fourier transform on tempered distributions. There is a bit of disagreement in the literature about which is the correct topology on tempered distributions. For practical reasons, we will use the pointwise topology, but we might switch later to the bounded topology, if the abstract functional analysis is developed enough to prove the same statements.
1 parent c671bc4 commit 993928b

File tree

6 files changed

+208
-9
lines changed

6 files changed

+208
-9
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1771,6 +1771,7 @@ public import Mathlib.Analysis.Distribution.Distribution
17711771
public import Mathlib.Analysis.Distribution.FourierSchwartz
17721772
public import Mathlib.Analysis.Distribution.SchwartzSpace
17731773
public import Mathlib.Analysis.Distribution.TemperateGrowth
1774+
public import Mathlib.Analysis.Distribution.TemperedDistribution
17741775
public import Mathlib.Analysis.Distribution.TestFunction
17751776
public import Mathlib.Analysis.Fourier.AddCircle
17761777
public import Mathlib.Analysis.Fourier.AddCircleMulti

‎Mathlib/Analysis/Distribution/TemperedDistribution.lean‎

Lines changed: 130 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,130 @@
1+
/-
2+
Copyright (c) 2025 Moritz Doll. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Moritz Doll
5+
-/
6+
module
7+
8+
public import Mathlib.Analysis.Distribution.FourierSchwartz
9+
public import Mathlib.Analysis.LocallyConvex.PointwiseConvergence
10+
11+
/-!
12+
# TemperedDistribution
13+
14+
## Main definitions
15+
16+
* `TemperedDistribution E F`: The space `𝓢(E, ℂ) →L[ℂ] F` equipped with the pointwise
17+
convergence topology.
18+
* `MeasureTheory.Measure.toTemperedDistribution`: Every measure of temperate growth is a tempered
19+
distribution.
20+
* `TemperedDistribution.fourierTransformCLM`: The Fourier transform on tempered distributions.
21+
22+
## Notation
23+
* `𝓢'(E, F)`: The space of tempered distributions `TemperedDistribution E F` scoped in
24+
`SchwartzMap`
25+
-/
26+
27+
@[expose] public noncomputable section
28+
29+
noncomputable section
30+
31+
open SchwartzMap ContinuousLinearMap
32+
33+
open scoped Nat NNReal ContDiff
34+
35+
variable {E F : Type*}
36+
37+
section definition
38+
39+
variable [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F]
40+
41+
variable (E F) in
42+
/-- The space of tempered distribution is the space of continuous linear maps from the Schwartz to
43+
a normed space, equipped with the topology of pointwise convergence. -/
44+
abbrev TemperedDistribution := 𝓢(E, ℂ) →Lₚₜ[ℂ] F
45+
/- Since mathlib is missing quite a few results that show that continuity of linear maps and
46+
convergence of sequences can be checked for strong duals of Fréchet-Montel spaces pointwise, we
47+
use the pointwise topology for now and not the strong topology. The pointwise topology is
48+
conventially used in PDE texts, but has the downside that it is not barrelled, hence the uniform
49+
boundedness principle does not hold. -/
50+
51+
@[inherit_doc]
52+
scoped[SchwartzMap] notation "𝓢'(" E ", " F ")" => TemperedDistribution E F
53+
54+
end definition
55+
56+
/-! ### Embeddings into tempered distributions -/
57+
58+
section Embeddings
59+
60+
variable [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F]
61+
62+
namespace MeasureTheory.Measure
63+
64+
variable [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
65+
(μ : Measure E := by volume_tac) [hμ : μ.HasTemperateGrowth]
66+
67+
/-- Every temperate growth measure defines a tempered distribution. -/
68+
def toTemperedDistribution : 𝓢'(E, ℂ) :=
69+
toPointwiseConvergenceCLM _ _ _ _ (integralCLM ℂ μ)
70+
71+
@[simp]
72+
theorem toTemperedDistribution_apply (g : 𝓢(E, ℂ)) :
73+
μ.toTemperedDistribution g = ∫ (x : E), g x ∂μ := by
74+
rfl
75+
76+
end MeasureTheory.Measure
77+
78+
end Embeddings
79+
80+
namespace TemperedDistribution
81+
82+
/-! ### Fourier transform -/
83+
84+
section Fourier
85+
86+
open FourierTransform
87+
88+
variable [NormedAddCommGroup E] [NormedAddCommGroup F]
89+
[InnerProductSpace ℝ E] [NormedSpace ℂ F]
90+
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
91+
92+
variable (E F) in
93+
/-- The Fourier transform on tempered distributions as a continuous linear map. -/
94+
def fourierTransformCLM : 𝓢'(E, F) →L[ℂ] 𝓢'(E, F) :=
95+
PointwiseConvergenceCLM.precomp F (SchwartzMap.fourierTransformCLM ℂ)
96+
97+
instance instFourierTransform : FourierTransform 𝓢'(E, F) 𝓢'(E, F) where
98+
fourier := fourierTransformCLM E F
99+
100+
@[simp]
101+
theorem fourierTransformCLM_apply (f : 𝓢'(E, F)) :
102+
fourierTransformCLM E F f = 𝓕 f := rfl
103+
104+
@[simp]
105+
theorem fourierTransform_apply (f : 𝓢'(E, F)) (g : 𝓢(E, ℂ)) : 𝓕 f g = f (𝓕 g) := rfl
106+
107+
variable (E F) in
108+
/-- The inverse Fourier transform on tempered distributions as a continuous linear map. -/
109+
def fourierTransformInvCLM : 𝓢'(E, F) →L[ℂ] 𝓢'(E, F) :=
110+
PointwiseConvergenceCLM.precomp F (SchwartzMap.fourierTransformCLE ℂ).symm.toContinuousLinearMap
111+
112+
instance instFourierTransformInv : FourierTransformInv 𝓢'(E, F) 𝓢'(E, F) where
113+
fourierInv := fourierTransformInvCLM E F
114+
115+
@[simp]
116+
theorem fourierTransformInvCLM_apply (f : 𝓢'(E, F)) :
117+
fourierTransformInvCLM E F f = 𝓕⁻ f := rfl
118+
119+
@[simp]
120+
theorem fourierTransformInv_apply (f : 𝓢'(E, F)) (g : 𝓢(E, ℂ)) : 𝓕⁻ f g = f (𝓕⁻ g) := rfl
121+
122+
instance instFourierPair : FourierPair 𝓢'(E, F) 𝓢'(E, F) where
123+
fourierInv_fourier_eq f := by ext; simp
124+
125+
instance instFourierPairInv : FourierInvPair 𝓢'(E, F) 𝓢'(E, F) where
126+
fourier_fourierInv_eq f := by ext; simp
127+
128+
end Fourier
129+
130+
end TemperedDistribution

‎Mathlib/Analysis/LocallyConvex/PointwiseConvergence.lean‎

Lines changed: 49 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -24,8 +24,8 @@ that it is locally convex in the topological sense
2424

2525
@[expose] public section
2626

27-
variable {R 𝕜₁ 𝕜₂ : Type*} [NormedField 𝕜₁] [NormedField 𝕜₂]
28-
{σ : 𝕜₁ →+* 𝕜₂} {E F : Type*}
27+
variable {α R 𝕜₁ 𝕜₂ 𝕜₃ : Type*} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃]
28+
{σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₃ →+* 𝕜₂} {D E F G : Type*}
2929
[AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E]
3030

3131
namespace PointwiseConvergenceCLM
@@ -67,6 +67,53 @@ lemma withSeminorms : WithSeminorms (PointwiseConvergenceCLM.seminormFamily σ E
6767
(isInducing_inducingFn σ E F).withSeminorms <| withSeminorms_pi (fun _ ↦ norm_withSeminorms 𝕜₂ F)
6868
|>.congr_equiv e
6969

70+
section Tendsto
71+
72+
open Filter
73+
open scoped Topology
74+
75+
theorem tendsto_nhds {f : Filter α} (u : α → E →SLₚₜ[σ] F) (y₀ : E →SLₚₜ[σ] F) :
76+
Tendsto u f (𝓝 y₀) ↔ ∀ (x : E) (ε : ℝ), 0 < ε → ∀ᶠ (k : α) in f, ‖u k x - y₀ x‖ < ε :=
77+
PointwiseConvergenceCLM.withSeminorms.tendsto_nhds _ _
78+
79+
theorem tendsto_nhds_atTop [SemilatticeSup α] [Nonempty α] (u : α → E →SLₚₜ[σ] F)
80+
(y₀ : E →SLₚₜ[σ] F) :
81+
Tendsto u atTop (𝓝 y₀) ↔ ∀ (x : E) (ε : ℝ), 0 < ε → ∃ (k₀ : α), ∀ (k : α), k₀ ≤ k →
82+
‖u k x - y₀ x‖ < ε :=
83+
PointwiseConvergenceCLM.withSeminorms.tendsto_nhds_atTop _ _
84+
85+
end Tendsto
86+
87+
section ContinuousLinearMap
88+
89+
variable [AddCommGroup D] [TopologicalSpace D] [Module 𝕜₃ D]
90+
[NormedAddCommGroup F] [NormedSpace 𝕜₂ F] [NormedAddCommGroup G] [NormedSpace 𝕜₂ G]
91+
92+
open NNReal ContinuousLinearMap
93+
94+
variable (F G) in
95+
/-- Define a continuous linear map between `E →SLₚₜ[σ] F` and `D →SLₚₜ[τ] G`.
96+
97+
Use `PointwiseConvergenceCLM.precomp` for the special case of the adjoint operator. -/
98+
def mkCLM (A : (E →SL[σ] F) →ₗ[𝕜₂] D →SL[τ] G) (hbound : ∀ (f : D), ∃ (s : Finset E) (C : ℝ≥0),
99+
∀ (B : E →SL[σ] F), ∃ (g : E) (_hb : g ∈ s), ‖(A B) f‖ ≤ C • ‖B g‖) :
100+
(E →SLₚₜ[σ] F) →L[𝕜₂] D →SLₚₜ[τ] G where
101+
__ := (toUniformConvergenceCLM _ _ _).toLinearMap.comp
102+
(A.comp (toUniformConvergenceCLM _ _ _).symm.toLinearMap)
103+
cont := by
104+
apply Seminorm.continuous_from_bounded PointwiseConvergenceCLM.withSeminorms
105+
PointwiseConvergenceCLM.withSeminorms A
106+
intro f
107+
obtain ⟨s, C, h⟩ := hbound f
108+
use s, C
109+
rw [← Seminorm.finset_sup_smul]
110+
intro B
111+
obtain ⟨g, h₁, h₂⟩ := h ((toUniformConvergenceCLM _ _ _).symm B)
112+
refine le_trans ?_ (Seminorm.le_finset_sup_apply h₁)
113+
exact h₂
114+
115+
end ContinuousLinearMap
116+
70117
end NormedSpace
71118

72119
section IsTopologicalAddGroup

‎Mathlib/Topology/Algebra/Module/PointwiseConvergence.lean‎

Lines changed: 24 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -41,12 +41,13 @@ continuous if for every `x : E` the evaluation `g · x` is continuous.
4141
/-! ### Topology of pointwise convergence -/
4242

4343
variable {α ι : Type*} [TopologicalSpace α]
44-
variable {𝕜 𝕜₁ 𝕜₂ : Type*} [NormedField 𝕜] [NormedField 𝕜₁] [NormedField 𝕜₂]
45-
variable {σ : 𝕜₁ →+* 𝕜₂}
46-
variable {E F Fᵤ : Type*} [AddCommGroup E] [TopologicalSpace E]
44+
variable {𝕜 𝕜₁ 𝕜₂ 𝕜₃ : Type*} [NormedField 𝕜] [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃]
45+
variable {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ]
46+
variable {E F Fᵤ G : Type*} [AddCommGroup E] [TopologicalSpace E]
4747
[AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F]
48+
[AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G]
4849
[AddCommGroup Fᵤ] [UniformSpace Fᵤ] [IsUniformAddGroup Fᵤ]
49-
[Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 Fᵤ] [Module 𝕜₁ E] [Module 𝕜₂ F] [Module 𝕜₂ Fᵤ]
50+
[Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 Fᵤ] [Module 𝕜₁ E] [Module 𝕜₂ F] [Module 𝕜₂ Fᵤ] [Module 𝕜₃ G]
5051

5152
open Set Topology
5253

@@ -127,6 +128,25 @@ theorem continuous_of_continuous_eval {g : α → E →SLₚₜ[σ] F}
127128
(h : ∀ x, Continuous (g · x)) : Continuous g := by
128129
simp [(PointwiseConvergenceCLM.isEmbedding_coeFn σ E F).continuous_iff, continuous_pi_iff, h]
129130

131+
variable (G) in
132+
/-- Pre-composition by a *fixed* continuous linear map as a continuous linear map for the pointwise
133+
convergence topology. -/
134+
@[simps! apply]
135+
def precomp [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] (L : E →SL[σ] F) :
136+
(F →SLₚₜ[τ] G) →L[𝕜₃] E →SLₚₜ[ρ] G where
137+
toFun f := f.comp L
138+
__ := ContinuousLinearMap.precomp_uniformConvergenceCLM G { (S : Set E) | Finite S }
139+
{ (S : Set F) | Finite S } L (fun S hS ↦ letI : Finite S := hS; Finite.Set.finite_image _ _)
140+
141+
variable (E) in
142+
/-- Post-composition by a *fixed* continuous linear map as a continuous linear map for the pointwise
143+
convergence topology. -/
144+
@[simps! apply]
145+
def postcomp [ContinuousConstSMul 𝕜₂ F] [ContinuousConstSMul 𝕜₃ G] (L : F →SL[τ] G) :
146+
(E →SLₚₜ[σ] F) →SL[τ] E →SLₚₜ[ρ] G where
147+
toFun f := L.comp f
148+
__ := ContinuousLinearMap.postcomp_uniformConvergenceCLM { (S : Set E) | Finite S } L
149+
130150
variable (𝕜₂ σ E F) in
131151
/-- The topology of bounded convergence is stronger than the topology of pointwise convergence. -/
132152
@[simps!]

‎docs/overview.yaml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -376,6 +376,7 @@ Analysis:
376376
Test functions: 'TestFunction'
377377
Schwartz space: 'SchwartzMap'
378378
Distributions: 'Distribution'
379+
tempered distributions: 'TemperedDistribution'
379380

380381
Fourier analysis:
381382
Fourier transform as an integral: 'Real.fourier_eq'

‎docs/undergrad.yaml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -610,15 +610,15 @@ Distribution calculus:
610610
Fourier transforms on $\mathcal{S}(\R^d)$: 'SchwartzMap.fourierTransformCLM'
611611
convolution of two functions of $\mathcal{S}(\R^d)$: ''
612612
Tempered distributions:
613-
definition: ''
613+
definition: 'TemperedDistribution'
614614
derivation of tempered distributions: ''
615615
multiplication by a function $C^\infty$ of slow growth: ''
616616
$L^2$ functions and Riesz representation: ''
617617
$L^p$ functions: ''
618618
periodic functions: ''
619619
Dirac comb: ''
620-
Fourier transforms: ''
621-
inverse Fourier transform: ''
620+
Fourier transforms: 'TemperedDistribution.fourierTransformCLM'
621+
inverse Fourier transform: 'TemperedDistribution.fourierTransformInvCLM'
622622
Fourier transform and derivation: ''
623623
Fourier transform and convolution product: ''
624624
Applications:

0 commit comments

Comments
 (0)