Theorems · Definition · functional analysis

SchwartzMap.toLp

{E : Type u_5} →
  {F : Type u_6} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℝ F] →
            [inst_4 : MeasurableSpace E] →
              [OpensMeasurableSpace E] →
                [SecondCountableTopologyEither E F] →
                  SchwartzMap E F →
                    (p : ENNReal) →
                      (μ : autoParam (MeasureTheory.Measure E) SchwartzMap.toLp._auto_1) →
                        [hμ : μ.HasTemperateGrowth] → ↥(MeasureTheory.Lp F p μ)

Map a Schwartz function to an Lp function for any p.

Defined in

Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Cited by

23 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceMeasurableSpaceOpensMeasurableSpaceSecondCountableTopologyEitherMeasureTheory.Measure.HasTemperateGrowth