Theorems · Definition · functional analysis

TemperedDistribution.MemSobolev

{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] →
                  [CompleteSpace F] → ℝ → (p : ENNReal) → [hp : Fact (1 ≤ p)] → TemperedDistribution E F → Prop

A tempered distribution f is a Sobolev function of order s if there exists an Lp function f' such that 𝓕⁻ (1 + ‖x‖ ^ 2) ^ (s / 2) 𝓕 f = f'.

Defined in

Mathlib.Analysis.Distribution.Sobolev

Cited by

16 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedAddCommGroupInnerProductSpaceFiniteDimensionalMeasurableSpaceBorelSpaceNormedSpaceCompleteSpaceFact