Distribution theory

StructureTest functions#

The type of bundled n-times continuously differentiable maps with compact support

TestFunction.{u_3, u_4} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E]
  (Ω : TopologicalSpace.Opens E) (F : Type u_4) [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ∞) :
  Type (max u_3 u_4)

Sources

• Mathlib documentation: TestFunction
• Source of TestFunction in Mathlib/Analysis/Distribution/TestFunction.lean
• Mathlib overview: Analysis › Distribution theory
• Mathlib undergraduate list: Distribution calculus › Spaces \(\mathcal{D}(\R^d)\)

MathlibTestFunction

Uses 3 · Used by 1

Statement uses\(C^k\) function · Closure · Compactness in terms of filters

Used byDistributions

StructureSchwartz space#

A function is a Schwartz function if it is smooth and all derivatives decay faster than any power of ‖x‖.

SchwartzMap.{u_5, u_6} (E : Type u_5) (F : Type u_6) [NormedAddCommGroup E] [NormedSpace ℝ E]
  [NormedAddCommGroup F] [NormedSpace ℝ F] : Type (max u_5 u_6)

Sources

• Mathlib documentation: SchwartzMap
• Source of SchwartzMap in Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean
• Mathlib overview: Analysis › Distribution theory
• Mathlib undergraduate list: Distribution calculus › Spaces \(\mathcal{S}(\R^d)\)

MathlibSchwartzMap

Uses 2 · Used by 7

Statement uses\(C^k\) function · Differentials (linear tangent functions)

Used byTempered distributions · Poisson’s formula · Fourier transforms on \(\mathcal{S}(\R^d)\) · Stability by derivation · Stability by multiplication by a slowly growing smooth function · Fourier transform on \(\mathrm{L}^2(\R^d)\) · Plancherel’s theorem

AbbreviationDistributions#

𝓓'^{n}(Ω, F) = Distribution Ω F n is the space of F-valued distributions on Ω with order at most n.

In most cases you want to use the space 𝓓'(Ω, F) = Distribution Ω F ⊤.

Distribution.{u_1, u_2} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  (Ω : TopologicalSpace.Opens E) (F : Type u_2) [AddCommGroup F] [_root_.Module ℝ F]
  [TopologicalSpace F] (n : ℕ∞) : Type (max u_1 u_2)

Sources

• Mathlib documentation: Distribution
• Source of Distribution in Mathlib/Analysis/Distribution/Distribution.lean
• Mathlib overview: Analysis › Distribution theory
• Mathlib undergraduate list: Distribution calculus › Distributions on \(\R^d\)

MathlibDistribution

Uses 2

Statement usesInner product space, over \(R\) or \(C\) · Test functions

AbbreviationTempered distributions#

The space of tempered distribution is the space of continuous linear maps from the Schwartz to a normed space, equipped with the topology of pointwise convergence.

TemperedDistribution.{u_3, u_4} (E : Type u_3) (F : Type u_4) [NormedAddCommGroup E]
  [NormedSpace ℝ E] [TopologicalSpace F] [AddCommGroup F] [_root_.Module ℂ F] : Type (max u_3 u_4)

Sources

• Mathlib documentation: TemperedDistribution
• Source of TemperedDistribution in Mathlib/Analysis/Distribution/TemperedDistribution.lean
• Mathlib overview: Analysis › Distribution theory
• Mathlib undergraduate list: Distribution calculus › Tempered distributions

MathlibTemperedDistribution

Uses 3 · Used by 3

Statement usesComplex number · Inner product space, over \(R\) or \(C\) · Schwartz space

Used byDerivation of tempered distributions · \(L^p\) functions · Multiplication by a function \(C^\infty\) of slow growth

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.