feat: bundled C^n maps supported in a fixed compact set (#30197)

Add a type of n-times continuously differentiable maps supported in a fixed compact set and related notation.
Co-authored by: @ADedecker

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

Author: 3 people

Mathlib.lean

@@ -1679,6 +1679,7 @@ import Mathlib.Analysis.Convex.Uniform
 import Mathlib.Analysis.Convex.Visible
 import Mathlib.Analysis.Convolution
 import Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
+import Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
 import Mathlib.Analysis.Distribution.FourierSchwartz
 import Mathlib.Analysis.Distribution.SchwartzSpace
 import Mathlib.Analysis.Fourier.AddCircle

Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean

@@ -0,0 +1,162 @@
+/-
+Copyright (c) 2023 Anatole Dedecker. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anatole Dedecker, Luigi Massacci
+-/
+
+import Mathlib.Analysis.Calculus.ContDiff.Defs
+import Mathlib.Topology.ContinuousMap.Bounded.Normed
+import Mathlib.Topology.Sets.Compacts
+
+/-!
+# Continuously differentiable functions supported in a given compact set
+
+This file develops the basic theory of bundled `n`-times continuously differentiable functions
+with support contained in a given compact set.
+
+Given `n : ℕ∞` and a compact subset `K` of a normed space `E`, we consider the type of bundled
+functions `f : E → F` (where `F` is a normed vector space) such that:
+
+- `f` is `n`-times continuously differentiable: `ContDiff ℝ n f`.
+- `f` vanishes outside of a compact set: `EqOn f 0 Kᶜ`.
+
+The main reason this exists as a bundled type is to be endowed with its natural locally convex
+topology (namely, uniform convergence of `f` and its derivative up to order `n`).
+Taking the locally convex inductive limit of these as `K` varies yields the natural topology on test
+functions, used to define distributions. While most of distribution theory cares only about `C^∞`
+functions, we also want to endow the space of `C^n` test functions with its natural topology.
+Indeed, distributions of order less than `n` are precisely those which extend continuously to this
+larger space of test functions.
+
+## Main definitions
+
+- `ContDiffMapSupportedIn E F n K`: the type of bundled `n`-times continuously differentiable
+  functions `E → F` which vanish outside of `K`.
+- `ContDiffMapSupportedIn.iteratedFDerivₗ'`: wraps `iteratedFDeriv` into a `𝕜`-linear map on
+  `ContDiffMapSupportedIn E F n K`, as a map into
+  `ContDiffMapSupportedIn E (E [×i]→L[ℝ] F) (n-i) K`.
+
+## Main statements
+
+TODO:
+- `ContDiffMapSupportedIn.instIsUniformAddGroup` and
+  `ContDiffMapSupportedIn.instLocallyConvexSpace`: `ContDiffMapSupportedIn` is a locally convex
+  topological vector space.
+
+## Notation
+
+- `𝓓^{n}_{K}(E, F)`:  the space of `n`-times continuously differentiable functions `E → F`
+  which vanish outside of `K`.
+- `𝓓_{K}(E, F)`:  the space of smooth (infinitely differentiable) functions `E → F`
+  which vanish outside of `K`, i.e. `𝓓^{⊤}_{K}(E, F)`.
+
+## Implementation details
+
+The technical choice of spelling `EqOn f 0 Kᶜ` in the definition, as opposed to `tsupport f ⊆ K`
+is to make rewriting `f x` to `0` easier when `x ∉ K`.
+
+## Tags
+
+distributions
+-/
+
+open TopologicalSpace SeminormFamily Set Function Seminorm UniformSpace
+open scoped BoundedContinuousFunction Topology NNReal
+
+variable (𝕜 E F : Type*) [NontriviallyNormedField 𝕜]
+  [NormedAddCommGroup E] [NormedSpace ℝ E]
+  [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F]
+  {n : ℕ∞} {K : Compacts E}
+
+/-- The type of bundled `n`-times continuously differentiable maps which vanish outside of a fixed
+compact set `K`. -/
+structure ContDiffMapSupportedIn (n : ℕ∞) (K : Compacts E) : Type _ where
+  /-- The underlying function. Use coercion instead. -/
+  protected toFun : E → F
+  protected contDiff' : ContDiff ℝ n toFun
+  protected zero_on_compl' : EqOn toFun 0 Kᶜ
+
+/-- Notation for the space of bundled `n`-times continuously differentiable
+functions with support in a compact set `K`. -/
+scoped[Distributions] notation "𝓓^{" n "}_{"K"}(" E ", " F ")" =>
+  ContDiffMapSupportedIn E F n K
+
+/-- Notation for the space of bundled smooth (inifinitely differentiable)
+functions with support in a compact set `K`. -/
+scoped[Distributions] notation "𝓓_{"K"}(" E ", " F ")" =>
+  ContDiffMapSupportedIn E F ⊤ K
+
+open Distributions
+
+/-- `ContDiffMapSupportedInClass B E F n K` states that `B` is a type of bundled `n`-times
+continously differentiable functions with support in the compact set `K`. -/
+class ContDiffMapSupportedInClass (B : Type*) (E F : outParam <| Type*)
+    [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F]
+    (n : outParam ℕ∞) (K : outParam <| Compacts E)
+    extends FunLike B E F where
+  map_contDiff (f : B) : ContDiff ℝ n f
+  map_zero_on_compl (f : B) : EqOn f 0 Kᶜ
+
+open ContDiffMapSupportedInClass
+
+instance (B : Type*) (E F : outParam <| Type*)
+    [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F]
+    (n : outParam ℕ∞) (K : outParam <| Compacts E)
+    [ContDiffMapSupportedInClass B E F n K] :
+    ContinuousMapClass B E F where
+  map_continuous f := (map_contDiff f).continuous
+
+instance (B : Type*) (E F : outParam <| Type*)
+    [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F]
+    (n : outParam ℕ∞) (K : outParam <| Compacts E)
+    [ContDiffMapSupportedInClass B E F n K] :
+    BoundedContinuousMapClass B E F where
+  map_bounded f := by
+    have := HasCompactSupport.intro K.isCompact (map_zero_on_compl f)
+    rcases (map_continuous f).bounded_above_of_compact_support this with ⟨C, hC⟩
+    exact map_bounded (BoundedContinuousFunction.ofNormedAddCommGroup f (map_continuous f) C hC)
+
+namespace ContDiffMapSupportedIn
+
+instance toContDiffMapSupportedInClass :
+    ContDiffMapSupportedInClass 𝓓^{n}_{K}(E, F) E F n K where
+  coe f := f.toFun
+  coe_injective' f g h := by cases f; cases g; congr
+  map_contDiff f := f.contDiff'
+  map_zero_on_compl f := f.zero_on_compl'
+
+variable {E F}
+
+protected theorem contDiff (f : 𝓓^{n}_{K}(E, F)) : ContDiff ℝ n f := map_contDiff f
+protected theorem zero_on_compl (f : 𝓓^{n}_{K}(E, F)) : EqOn f 0 Kᶜ := map_zero_on_compl f
+protected theorem compact_supp (f : 𝓓^{n}_{K}(E, F)) : HasCompactSupport f :=
+  .intro K.isCompact (map_zero_on_compl f)
+
+@[simp]
+theorem toFun_eq_coe {f : 𝓓^{n}_{K}(E, F)} : f.toFun = (f : E → F) :=
+  rfl
+
+/-- See note [custom simps projection]. -/
+def Simps.apply (f : 𝓓^{n}_{K}(E, F)) : E → F := f
+
+initialize_simps_projections ContDiffMapSupportedIn (toFun → apply)
+
+@[ext]
+theorem ext {f g : 𝓓^{n}_{K}(E, F)} (h : ∀ a, f a = g a) : f = g :=
+  DFunLike.ext _ _ h
+
+/-- Copy of a `ContDiffMapSupportedIn` with a new `toFun` equal to the old one. Useful to fix
+definitional equalities. -/
+protected def copy (f : 𝓓^{n}_{K}(E, F)) (f' : E → F) (h : f' = f) : 𝓓^{n}_{K}(E, F) where
+  toFun := f'
+  contDiff' := h.symm ▸ f.contDiff
+  zero_on_compl' := h.symm ▸ f.zero_on_compl
+
+@[simp]
+theorem coe_copy (f : 𝓓^{n}_{K}(E, F)) (f' : E → F) (h : f' = f) : ⇑(f.copy f' h) = f' :=
+  rfl
+
+theorem copy_eq (f : 𝓓^{n}_{K}(E, F)) (f' : E → F) (h : f' = f) : f.copy f' h = f :=
+  DFunLike.ext' h
+
+end ContDiffMapSupportedIn