Theorems · Definition · functional analysis

TemperedDistribution.besselPotential

(E : Type u_1) →
  (F : Type u_2) →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedAddCommGroup F] →
        [inst_2 : InnerProductSpace ℝ E] →
          [FiniteDimensional ℝ E] →
            [inst_4 : MeasurableSpace E] →
              [BorelSpace E] → [inst_6 : NormedSpace ℂ F] → ℝ → TemperedDistribution E F →L[ℂ] TemperedDistribution E F

The Bessel potential operator is the Fourier multiplier with the function (1 + ‖x‖ ^ 2) ^ (s / 2). Note that due to the convention of the Fourier transform, this is the operator (1 - (2 * π) ^ (-2) • Δ) ^ (s / 2) not (1 - Δ) ^ (s / 2).

Defined in

Mathlib.Analysis.Distribution.Sobolev

Cited by

15 results in Mathlib

Foundations

Depth 304 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedAddCommGroupInnerProductSpaceFiniteDimensionalMeasurableSpaceBorelSpaceNormedSpace