Theorems · Definition · functional analysis

SchwartzMap.toTemperedDistributionCLM

(E : Type u_3) →
  (F : Type u_4) →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℂ F] →
            [inst_4 : MeasurableSpace E] →
              [BorelSpace E] →
                [SecondCountableTopology E] →
                  (μ : autoParam (MeasureTheory.Measure E) SchwartzMap.toTemperedDistributionCLM._auto_1) →
                    [hμ : μ.HasTemperateGrowth] → SchwartzMap E F →L[ℂ] TemperedDistribution E F

The canonical embedding of 𝓢(E, F) into 𝓢'(E, F) as a continuous linear map.

Defined in

Mathlib.Analysis.Distribution.TemperedDistribution

Cited by

14 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceMeasurableSpaceBorelSpaceSecondCountableTopologyMeasureTheory.Measure.HasTemperateGrowth