Documentation

Mathlib.Analysis.Distribution.SchwartzSpace

Schwartz space #

This file defines the Schwartz space. Usually, the Schwartz space is defined as the set of smooth functions $f : ℝ^n β†’ β„‚$ such that there exists $C_{Ξ±Ξ²} > 0$ with $$|x^Ξ± βˆ‚^Ξ² f(x)| < C_{Ξ±Ξ²}$$ for all $x ∈ ℝ^n$ and for all multiindices $Ξ±, Ξ²$. In mathlib, we use a slightly different approach and define the Schwartz space as all smooth functions f : E β†’ F, where E and F are real normed vector spaces such that for all natural numbers k and n we have uniform bounds β€–xβ€–^k * β€–iteratedFDeriv ℝ n f xβ€– < C. This approach completely avoids using partial derivatives as well as polynomials. We construct the topology on the Schwartz space by a family of seminorms, which are the best constants in the above estimates. The abstract theory of topological vector spaces developed in SeminormFamily.moduleFilterBasis and WithSeminorms.toLocallyConvexSpace turns the Schwartz space into a locally convex topological vector space.

Main definitions #

Main statements #

Implementation details #

The implementation of the seminorms is taken almost literally from ContinuousLinearMap.opNorm.

Notation #

Tags #

Schwartz space, tempered distributions

structure SchwartzMap (E : Type u_4) (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] :
Type (max u_4 u_5)

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

Instances For
    instance SchwartzMap.instCoeFun {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] :
    CoeFun (SchwartzMap E F) fun x => E β†’ F

    Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun.

    theorem SchwartzMap.decay {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : SchwartzMap E F) (k : β„•) (n : β„•) :
    βˆƒ C, 0 < C ∧ βˆ€ (x : E), β€–xβ€– ^ k * β€–iteratedFDeriv ℝ n (↑f) xβ€– ≀ C

    All derivatives of a Schwartz function are rapidly decaying.

    Every Schwartz function is smooth.

    Every Schwartz function is continuous.

    Every Schwartz function is differentiable.

    Every Schwartz function is differentiable at any point.

    theorem SchwartzMap.ext {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : SchwartzMap E F} {g : SchwartzMap E F} (h : βˆ€ (x : E), ↑f x = ↑g x) :
    f = g

    Auxiliary lemma, used in proving the more general result isBigO_cocompact_rpow.

    theorem SchwartzMap.bounds_nonempty {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (k : β„•) (n : β„•) (f : SchwartzMap E F) :
    βˆƒ c, c ∈ {c | 0 ≀ c ∧ βˆ€ (x : E), β€–xβ€– ^ k * β€–iteratedFDeriv ℝ n (↑f) xβ€– ≀ c}
    theorem SchwartzMap.decay_smul_aux {π•œ : Type u_1} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] (k : β„•) (n : β„•) (f : SchwartzMap E F) (c : π•œ) (x : E) :

    Helper definition for the seminorms of the Schwartz space.

    Instances For
      theorem SchwartzMap.seminormAux_le_bound {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (k : β„•) (n : β„•) (f : SchwartzMap E F) {M : ℝ} (hMp : 0 ≀ M) (hM : βˆ€ (x : E), β€–xβ€– ^ k * β€–iteratedFDeriv ℝ n (↑f) xβ€– ≀ M) :

      If one controls the norm of every A x, then one controls the norm of A.

      Algebraic properties #

      instance SchwartzMap.instSMul {π•œ : Type u_1} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] :
      SMul π•œ (SchwartzMap E F)
      @[simp]
      theorem SchwartzMap.smul_apply {π•œ : Type u_1} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] {f : SchwartzMap E F} {c : π•œ} {x : E} :
      ↑(c β€’ f) x = c β€’ ↑f x
      instance SchwartzMap.instIsScalarTower {π•œ : Type u_1} {π•œ' : Type u_2} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] [NormedField π•œ'] [NormedSpace π•œ' F] [SMulCommClass ℝ π•œ' F] [SMul π•œ π•œ'] [IsScalarTower π•œ π•œ' F] :
      IsScalarTower π•œ π•œ' (SchwartzMap E F)
      instance SchwartzMap.instSMulCommClass {π•œ : Type u_1} {π•œ' : Type u_2} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] [NormedField π•œ'] [NormedSpace π•œ' F] [SMulCommClass ℝ π•œ' F] [SMulCommClass π•œ π•œ' F] :
      SMulCommClass π•œ π•œ' (SchwartzMap E F)
      theorem SchwartzMap.seminormAux_smul_le {π•œ : Type u_1} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] (k : β„•) (n : β„•) (c : π•œ) (f : SchwartzMap E F) :
      @[simp]
      @[simp]
      theorem SchwartzMap.zero_apply {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {x : E} :
      ↑0 x = 0
      @[simp]
      theorem SchwartzMap.add_apply {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : SchwartzMap E F} {g : SchwartzMap E F} {x : E} :
      ↑(f + g) x = ↑f x + ↑g x
      @[simp]
      theorem SchwartzMap.sub_apply {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : SchwartzMap E F} {g : SchwartzMap E F} {x : E} :
      ↑(f - g) x = ↑f x - ↑g x

      Coercion as an additive homomorphism.

      Instances For
        instance SchwartzMap.instModule {π•œ : Type u_1} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] :
        Module π•œ (SchwartzMap E F)

        Seminorms on Schwartz space #

        def SchwartzMap.seminorm (π•œ : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] (k : β„•) (n : β„•) :
        Seminorm π•œ (SchwartzMap E F)

        The seminorms of the Schwartz space given by the best constants in the definition of 𝓒(E, F).

        Instances For
          theorem SchwartzMap.seminorm_le_bound (π•œ : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] (k : β„•) (n : β„•) (f : SchwartzMap E F) {M : ℝ} (hMp : 0 ≀ M) (hM : βˆ€ (x : E), β€–xβ€– ^ k * β€–iteratedFDeriv ℝ n (↑f) xβ€– ≀ M) :
          ↑(SchwartzMap.seminorm π•œ k n) f ≀ M

          If one controls the seminorm for every x, then one controls the seminorm.

          theorem SchwartzMap.seminorm_le_bound' (π•œ : Type u_1) {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] (k : β„•) (n : β„•) (f : SchwartzMap ℝ F) {M : ℝ} (hMp : 0 ≀ M) (hM : βˆ€ (x : ℝ), |x| ^ k * β€–iteratedDeriv n (↑f) xβ€– ≀ M) :
          ↑(SchwartzMap.seminorm π•œ k n) f ≀ M

          If one controls the seminorm for every x, then one controls the seminorm.

          Variant for functions 𝓒(ℝ, F).

          theorem SchwartzMap.le_seminorm (π•œ : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] (k : β„•) (n : β„•) (f : SchwartzMap E F) (x : E) :

          The seminorm controls the Schwartz estimate for any fixed x.

          theorem SchwartzMap.le_seminorm' (π•œ : Type u_1) {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] (k : β„•) (n : β„•) (f : SchwartzMap ℝ F) (x : ℝ) :
          |x| ^ k * β€–iteratedDeriv n (↑f) xβ€– ≀ ↑(SchwartzMap.seminorm π•œ k n) f

          The seminorm controls the Schwartz estimate for any fixed x.

          Variant for functions 𝓒(ℝ, F).

          theorem SchwartzMap.norm_iteratedFDeriv_le_seminorm (π•œ : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] (f : SchwartzMap E F) (n : β„•) (xβ‚€ : E) :
          β€–iteratedFDeriv ℝ n (↑f) xβ‚€β€– ≀ ↑(SchwartzMap.seminorm π•œ 0 n) f
          theorem SchwartzMap.norm_pow_mul_le_seminorm (π•œ : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] (f : SchwartzMap E F) (k : β„•) (xβ‚€ : E) :
          β€–xβ‚€β€– ^ k * ‖↑f xβ‚€β€– ≀ ↑(SchwartzMap.seminorm π•œ k 0) f
          theorem SchwartzMap.norm_le_seminorm (π•œ : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] (f : SchwartzMap E F) (xβ‚€ : E) :
          ‖↑f xβ‚€β€– ≀ ↑(SchwartzMap.seminorm π•œ 0 0) f
          def schwartzSeminormFamily (π•œ : Type u_1) (E : Type u_4) (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] :

          The family of Schwartz seminorms.

          Instances For
            @[simp]
            theorem SchwartzMap.schwartzSeminormFamily_apply (π•œ : Type u_1) (E : Type u_4) (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] (n : β„•) (k : β„•) :
            schwartzSeminormFamily π•œ E F (n, k) = SchwartzMap.seminorm π•œ n k
            @[simp]
            theorem SchwartzMap.schwartzSeminormFamily_apply_zero (π•œ : Type u_1) (E : Type u_4) (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] :
            schwartzSeminormFamily π•œ E F 0 = SchwartzMap.seminorm π•œ 0 0
            theorem SchwartzMap.one_add_le_sup_seminorm_apply {π•œ : Type u_1} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] {m : β„• Γ— β„•} {k : β„•} {n : β„•} (hk : k ≀ m.fst) (hn : n ≀ m.snd) (f : SchwartzMap E F) (x : E) :
            (1 + β€–xβ€–) ^ k * β€–iteratedFDeriv ℝ n (↑f) xβ€– ≀ ↑(2 ^ m.fst) * ↑(Finset.sup (Finset.Iic m) fun m => SchwartzMap.seminorm π•œ m.fst m.snd) f

            A more convenient version of le_sup_seminorm_apply.

            The set Finset.Iic m is the set of all pairs (k', n') with k' ≀ m.1 and n' ≀ m.2. Note that the constant is far from optimal.

            The topology on the Schwartz space #

            theorem schwartz_withSeminorms (π•œ : Type u_1) (E : Type u_4) (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] :
            instance SchwartzMap.instContinuousSMul {π•œ : Type u_1} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] :

            Functions of temperate growth #

            A function is called of temperate growth if it is smooth and all iterated derivatives are polynomially bounded.

            Instances For
              theorem Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform_aux {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E β†’ F} (hf_temperate : Function.HasTemperateGrowth f) (n : β„•) :
              βˆƒ k C x, βˆ€ (N : β„•), N ≀ n β†’ βˆ€ (x : E), β€–iteratedFDeriv ℝ N f xβ€– ≀ C * (1 + β€–xβ€–) ^ k

              Construction of continuous linear maps between Schwartz spaces #

              def SchwartzMap.mkLM {π•œ : Type u_1} {π•œ' : Type u_2} {D : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedField π•œ'] [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedSpace π•œ E] [SMulCommClass ℝ π•œ E] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace π•œ' G] [SMulCommClass ℝ π•œ' G] {Οƒ : π•œ β†’+* π•œ'} (A : (D β†’ E) β†’ F β†’ G) (hadd : βˆ€ (f g : SchwartzMap D E) (x : F), A (↑f + ↑g) x = A (↑f) x + A (↑g) x) (hsmul : βˆ€ (a : π•œ) (f : SchwartzMap D E) (x : F), A (↑(a β€’ f)) x = ↑σ a β€’ A (↑f) x) (hsmooth : βˆ€ (f : SchwartzMap D E), ContDiff ℝ ⊀ (A ↑f)) (hbound : βˆ€ (n : β„• Γ— β„•), βˆƒ s C, 0 ≀ C ∧ βˆ€ (f : SchwartzMap D E) (x : F), β€–xβ€– ^ n.fst * β€–iteratedFDeriv ℝ n.snd (A ↑f) xβ€– ≀ C * ↑(Finset.sup s (schwartzSeminormFamily π•œ D E)) f) :

              Create a semilinear map between Schwartz spaces.

              Note: This is a helper definition for mkCLM.

              Instances For
                def SchwartzMap.mkCLM {π•œ : Type u_1} {π•œ' : Type u_2} {D : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedField π•œ'] [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedSpace π•œ E] [SMulCommClass ℝ π•œ E] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace π•œ' G] [SMulCommClass ℝ π•œ' G] {Οƒ : π•œ β†’+* π•œ'} [RingHomIsometric Οƒ] (A : (D β†’ E) β†’ F β†’ G) (hadd : βˆ€ (f g : SchwartzMap D E) (x : F), A (↑f + ↑g) x = A (↑f) x + A (↑g) x) (hsmul : βˆ€ (a : π•œ) (f : SchwartzMap D E) (x : F), A (↑(a β€’ f)) x = ↑σ a β€’ A (↑f) x) (hsmooth : βˆ€ (f : SchwartzMap D E), ContDiff ℝ ⊀ (A ↑f)) (hbound : βˆ€ (n : β„• Γ— β„•), βˆƒ s C, 0 ≀ C ∧ βˆ€ (f : SchwartzMap D E) (x : F), β€–xβ€– ^ n.fst * β€–iteratedFDeriv ℝ n.snd (A ↑f) xβ€– ≀ C * ↑(Finset.sup s (schwartzSeminormFamily π•œ D E)) f) :

                Create a continuous semilinear map between Schwartz spaces.

                For an example of using this definition, see fderivCLM.

                Instances For
                  def SchwartzMap.evalCLM {π•œ : Type u_1} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] (m : E) :

                  The map applying a vector to Hom-valued Schwartz function as a continuous linear map.

                  Instances For

                    The map f ↦ (x ↦ B (f x) (g x)) as a continuous π•œ-linear map on Schwartz space, where B is a continuous π•œ-linear map and g is a function of temperate growth.

                    Instances For
                      def SchwartzMap.compCLM (π•œ : Type u_1) {D : Type u_3} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC π•œ] [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] {g : D β†’ E} (hg : Function.HasTemperateGrowth g) (hg_upper : βˆƒ k C, βˆ€ (x : D), β€–xβ€– ≀ C * (1 + β€–g xβ€–) ^ k) :

                      Composition with a function on the right is a continuous linear map on Schwartz space provided that the function is temperate and growths polynomially near infinity.

                      Instances For

                        Derivatives of Schwartz functions #

                        def SchwartzMap.fderivCLM (π•œ : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] :

                        The FrΓ©chet derivative on Schwartz space as a continuous π•œ-linear map.

                        Instances For
                          @[simp]
                          theorem SchwartzMap.fderivCLM_apply (π•œ : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] (f : SchwartzMap E F) (x : E) :
                          ↑(↑(SchwartzMap.fderivCLM π•œ) f) x = fderiv ℝ (↑f) x
                          def SchwartzMap.derivCLM (π•œ : Type u_1) {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] :

                          The 1-dimensional derivative on Schwartz space as a continuous π•œ-linear map.

                          Instances For
                            @[simp]
                            theorem SchwartzMap.derivCLM_apply (π•œ : Type u_1) {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] (f : SchwartzMap ℝ F) (x : ℝ) :
                            ↑(↑(SchwartzMap.derivCLM π•œ) f) x = deriv (↑f) x
                            def SchwartzMap.pderivCLM (π•œ : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] (m : E) :

                            The partial derivative (or directional derivative) in the direction m : E as a continuous linear map on Schwartz space.

                            Instances For
                              @[simp]
                              theorem SchwartzMap.pderivCLM_apply (π•œ : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] (m : E) (f : SchwartzMap E F) (x : E) :
                              ↑(↑(SchwartzMap.pderivCLM π•œ m) f) x = ↑(fderiv ℝ (↑f) x) m
                              def SchwartzMap.iteratedPDeriv (π•œ : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] {n : β„•} :
                              (Fin n β†’ E) β†’ SchwartzMap E F β†’L[π•œ] SchwartzMap E F

                              The iterated partial derivative (or directional derivative) as a continuous linear map on Schwartz space.

                              Instances For
                                @[simp]
                                theorem SchwartzMap.iteratedPDeriv_zero (π•œ : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] (m : Fin 0 β†’ E) (f : SchwartzMap E F) :
                                ↑(SchwartzMap.iteratedPDeriv π•œ m) f = f
                                @[simp]
                                theorem SchwartzMap.iteratedPDeriv_one (π•œ : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] (m : Fin 1 β†’ E) (f : SchwartzMap E F) :
                                ↑(SchwartzMap.iteratedPDeriv π•œ m) f = ↑(SchwartzMap.pderivCLM π•œ (m 0)) f
                                theorem SchwartzMap.iteratedPDeriv_succ_left (π•œ : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] {n : β„•} (m : Fin (n + 1) β†’ E) (f : SchwartzMap E F) :
                                ↑(SchwartzMap.iteratedPDeriv π•œ m) f = ↑(SchwartzMap.pderivCLM π•œ (m 0)) (↑(SchwartzMap.iteratedPDeriv π•œ (Fin.tail m)) f)
                                theorem SchwartzMap.iteratedPDeriv_succ_right (π•œ : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] {n : β„•} (m : Fin (n + 1) β†’ E) (f : SchwartzMap E F) :
                                ↑(SchwartzMap.iteratedPDeriv π•œ m) f = ↑(SchwartzMap.iteratedPDeriv π•œ (Fin.init m)) (↑(SchwartzMap.pderivCLM π•œ (m (Fin.last n))) f)

                                Inclusion into the space of bounded continuous functions #

                                Schwartz functions as bounded continuous functions

                                Instances For

                                  Schwartz functions as continuous functions

                                  Instances For

                                    The inclusion map from Schwartz functions to bounded continuous functions as a linear map.

                                    Instances For
                                      @[simp]
                                      theorem SchwartzMap.toBoundedContinuousFunctionLM_apply (π•œ : Type u_1) (E : Type u_4) (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] (f : SchwartzMap E F) (x : E) :
                                      ↑(↑(SchwartzMap.toBoundedContinuousFunctionLM π•œ E F) f) x = ↑f x

                                      The inclusion map from Schwartz functions to bounded continuous functions as a continuous linear map.

                                      Instances For
                                        @[simp]
                                        theorem SchwartzMap.toBoundedContinuousFunctionCLM_apply (π•œ : Type u_1) (E : Type u_4) (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] (f : SchwartzMap E F) (x : E) :
                                        ↑(↑(SchwartzMap.toBoundedContinuousFunctionCLM π•œ E F) f) x = ↑f x
                                        def SchwartzMap.delta (π•œ : Type u_1) {E : Type u_4} (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] (x : E) :
                                        SchwartzMap E F β†’L[π•œ] F

                                        The Dirac delta distribution

                                        Instances For
                                          @[simp]
                                          theorem SchwartzMap.delta_apply (π•œ : Type u_1) {E : Type u_4} (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC π•œ] [NormedSpace π•œ F] [SMulCommClass ℝ π•œ F] (xβ‚€ : E) (f : SchwartzMap E F) :
                                          ↑(SchwartzMap.delta π•œ F xβ‚€) f = ↑f xβ‚€