feat: add differentiation for ContDiffMapSupportedIn (#30201)

Add a wrapper for `iteratedFDeriv` on `ContDiffMapSupportedIn` and related API.

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

Author: 3 people

Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean

@@ -21,7 +21,7 @@ functions `f : E → F` (where `F` is a normed vector space) such that:
 - `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`).
+topology (namely, uniform convergence of `f` and its derivatives 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.
@@ -32,9 +32,11 @@ larger space of test functions.
 
 - `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`.
+- `ContDiffMapSupportedIn.iteratedFDerivWithOrderLM`: wrapper, as a `𝕜`-linear map, for
+  `iteratedFDeriv` from `ContDiffMapSupportedIn E F n K` to
+  `ContDiffMapSupportedIn E (E [×i]→L[ℝ] F) k K`.
+- `ContDiffMapSupportedIn.iteratedFDerivLM`: specialization of the above, giving a `𝕜`-linear map
+  from `ContDiffMapSupportedIn E F ⊤ K` to `ContDiffMapSupportedIn E (E [×i]→L[ℝ] F) ⊤ K`.
 
 ## Main statements
 
@@ -52,21 +54,28 @@ TODO:
 
 ## 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`.
+* 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`.
+* Since the most common case is by far the smooth case, we often reserve the "expected" name
+  of a result/definition to this case, and add `WithOrder` to the declaration applying to
+  any regularity.
+* In `iteratedFDerivWithOrderLM`, we define the `i`-th iterated differentiation operator as
+  a map from `𝓓^{n}_{K}` to `𝓓^{k}_{K}` without imposing relations on `n`, `k` and `i`. Of course
+  this is defined as `0` if `k + i > n`. This creates some verbosity as all of these variables are
+  explicit, but it allows the most flexibility while avoiding DTT hell.
 
 ## Tags
 
 distributions
 -/
 
 open TopologicalSpace SeminormFamily Set Function Seminorm UniformSpace
-open scoped BoundedContinuousFunction Topology NNReal
+open scoped BoundedContinuousFunction Topology NNReal ContDiff
 
 variable (𝕜 E F : Type*) [NontriviallyNormedField 𝕜]
   [NormedAddCommGroup E] [NormedSpace ℝ E]
   [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F]
-  {n : ℕ∞} {K : Compacts E}
+  {n k : ℕ∞} {K : Compacts E}
 
 /-- The type of bundled `n`-times continuously differentiable maps which vanish outside of a fixed
 compact set `K`. -/
@@ -160,8 +169,8 @@ theorem copy_eq (f : 𝓓^{n}_{K}(E, F)) (f' : E → F) (h : f' = f) : f.copy f'
   DFunLike.ext' h
 
 @[simp]
-theorem toBoundedContinuousFunction_apply (f : 𝓓^{n}_{K}(E, F)) (x : E) :
-   (f : BoundedContinuousFunction E F) x = (f x) := rfl
+theorem coe_toBoundedContinuousFunction (f : 𝓓^{n}_{K}(E, F)) :
+   (f : BoundedContinuousFunction E F) = (f : E → F) := rfl
 
 section AddCommGroup
 
@@ -243,4 +252,159 @@ protected def of_support_subset {f : E → F} (hf : ContDiff ℝ n f) (hsupp : s
   contDiff' := hf
   zero_on_compl' := support_subset_iff'.mp hsupp
 
+protected theorem bounded_iteratedFDeriv (f : 𝓓^{n}_{K}(E, F)) {i : ℕ} (hi : i ≤ n) :
+    ∃ C, ∀ x, ‖iteratedFDeriv ℝ i f x‖ ≤ C :=
+  Continuous.bounded_above_of_compact_support
+    (f.contDiff.continuous_iteratedFDeriv <| (WithTop.le_coe rfl).mpr hi)
+    (f.hasCompactSupport.iteratedFDeriv i)
+
+/-- Inclusion of `𝓓^{n}_{K}(E, F)` into the space `E →ᵇ F` of bounded continuous maps
+as a `𝕜`-linear map.
+
+This is subsumed by `toBoundedContinuousFunctionCLM` (not yet in Mathlib), which also bundles the
+continuity. -/
+@[simps -fullyApplied]
+noncomputable def toBoundedContinuousFunctionLM : 𝓓^{n}_{K}(E, F) →ₗ[𝕜] E →ᵇ F where
+  toFun f := f
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+
+-- Workaround for simps' automatic name generation: manually specifying names is not supported yet.
+alias toBoundedContinuousFunctionLM_apply := toBoundedContinuousFunctionLM_apply_apply
+
+lemma toBoundedContinuousFunctionLM_eq_of_scalars (𝕜' : Type*) [NontriviallyNormedField 𝕜']
+    [NormedSpace 𝕜' F] [SMulCommClass ℝ 𝕜' F] :
+    (toBoundedContinuousFunctionLM 𝕜 : 𝓓^{n}_{K}(E, F) → _) = toBoundedContinuousFunctionLM 𝕜' :=
+  rfl
+
+variable (n k) in
+/-- `iteratedFDerivWithOrderLM 𝕜 n k i` is the `𝕜`-linear-map sending `f : 𝓓^{n}_{K}(E, F)` to
+its `i`-th iterated derivative as an element of `𝓓^{k}_{K}(E, E [×i]→L[ℝ] F)`.
+This only makes mathematical sense if `k + i ≤ n`, otherwise we define it as the zero map.
+
+See `iteratedFDerivLM` for the very common case where everything is infinitely differentiable.
+
+This is subsumed by `iteratedFDerivWithOrderCLM` (not yet in Mathlib), which also bundles the
+continuity. -/
+noncomputable def iteratedFDerivWithOrderLM (i : ℕ) :
+    𝓓^{n}_{K}(E, F) →ₗ[𝕜] 𝓓^{k}_{K}(E, E [×i]→L[ℝ] F) where
+  /-
+  Note: it is tempting to define this as some linear map if `k + i ≤ n`,
+  and the zero map otherwise. However, we would lose the definitional equality between
+  `iteratedFDerivWithOrderLM 𝕜 n k i f` and `iteratedFDerivWithOrderLM ℝ n k i f`.
+
+  This is caused by the fact that the equality `f (if p then x else y) = if p then f x else f y`
+  is not definitional.
+  -/
+  toFun f :=
+    if hi : k + i ≤ n then
+      .of_support_subset
+        (f.contDiff.iteratedFDeriv_right <| by exact_mod_cast hi)
+        ((support_iteratedFDeriv_subset i).trans f.tsupport_subset)
+    else 0
+  map_add' f g := by
+    split_ifs with hi
+    · have hi' : (i : WithTop ℕ∞) ≤ n := by exact_mod_cast le_of_add_le_right hi
+      ext
+      simp [iteratedFDeriv_add (f.contDiff.of_le hi') (g.contDiff.of_le hi')]
+    · simp
+  map_smul' c f := by
+    split_ifs with hi
+    · have hi' : (i : WithTop ℕ∞) ≤ n := by exact_mod_cast le_of_add_le_right hi
+      ext
+      simp [iteratedFDeriv_const_smul_apply (f.contDiff.of_le hi').contDiffAt]
+    · simp
+
+@[simp]
+lemma iteratedFDerivWithOrderLM_apply {i : ℕ} (f : 𝓓^{n}_{K}(E, F)) :
+    iteratedFDerivWithOrderLM 𝕜 n k i f = if k + i ≤ n then iteratedFDeriv ℝ i f else 0 := by
+  rw [ContDiffMapSupportedIn.iteratedFDerivWithOrderLM]
+  split_ifs <;> rfl
+
+lemma iteratedFDerivWithOrderLM_apply_of_le {i : ℕ} (f : 𝓓^{n}_{K}(E, F)) (hin : k + i ≤ n) :
+    iteratedFDerivWithOrderLM 𝕜 n k i f = iteratedFDeriv ℝ i f := by
+  simp [hin]
+
+lemma iteratedFDerivWithOrderLM_apply_of_gt {i : ℕ} (f : 𝓓^{n}_{K}(E, F)) (hin : ¬ (k + i ≤ n)) :
+    iteratedFDerivWithOrderLM 𝕜 n k i f = 0 := by
+  ext : 1
+  simp [hin]
+
+lemma iteratedFDerivWithOrderLM_eq_of_scalars {i : ℕ} (𝕜' : Type*) [NontriviallyNormedField 𝕜']
+    [NormedSpace 𝕜' F] [SMulCommClass ℝ 𝕜' F] :
+    (iteratedFDerivWithOrderLM 𝕜 n k i : 𝓓^{n}_{K}(E, F) → _)
+      = iteratedFDerivWithOrderLM 𝕜' n k i :=
+  rfl
+
+/-- `iteratedFDerivLM 𝕜 i` is the `𝕜`-linear-map sending `f : 𝓓_{K}(E, F)` to
+its `i`-th iterated derivative as an element of `𝓓_{K}(E, E [×i]→L[ℝ] F)`.
+
+See also `iteratedFDerivWithOrderLM` if you need more control on the regularities.
+
+This is subsumed by `iteratedFDerivCLM` (not yet in Mathlib), which also bundles the
+continuity. -/
+noncomputable def iteratedFDerivLM (i : ℕ) :
+    𝓓_{K}(E, F) →ₗ[𝕜] 𝓓_{K}(E, E [×i]→L[ℝ] F) where
+  toFun f := .of_support_subset
+    (f.contDiff.iteratedFDeriv_right le_rfl)
+    ((support_iteratedFDeriv_subset i).trans f.tsupport_subset)
+  map_add' f g := by
+    have hi : (i : WithTop ℕ∞) ≤ ∞ := by exact_mod_cast le_top
+    ext
+    simp [iteratedFDeriv_add (f.contDiff.of_le hi) (g.contDiff.of_le hi)]
+  map_smul' c f := by
+    have hi : (i : WithTop ℕ∞) ≤ ∞ := by exact_mod_cast le_top
+    ext
+    simp [iteratedFDeriv_const_smul_apply (f.contDiff.of_le hi).contDiffAt]
+
+@[simp]
+lemma iteratedFDerivLM_apply {i : ℕ} (f : 𝓓_{K}(E, F)) :
+    iteratedFDerivLM 𝕜 i f = iteratedFDeriv ℝ i f :=
+  rfl
+
+/-- Note: this turns out to be a definitional equality thanks to decidablity of the order
+on `ℕ∞`. This means we could have *defined* `iteratedFDerivLM` this way, but we avoid it
+to make sure that `if`s won't appear in the smooth case. -/
+lemma iteratedFDerivLM_eq_withOrder (i : ℕ) :
+    (iteratedFDerivLM 𝕜 i : 𝓓_{K}(E, F) →ₗ[𝕜] _) = iteratedFDerivWithOrderLM 𝕜 ⊤ ⊤ i :=
+  rfl
+
+lemma iteratedFDerivLM_eq_of_scalars {i : ℕ} (𝕜' : Type*) [NontriviallyNormedField 𝕜']
+    [NormedSpace 𝕜' F] [SMulCommClass ℝ 𝕜' F] :
+    (iteratedFDerivLM 𝕜 i : 𝓓_{K}(E, F) → _) = iteratedFDerivLM 𝕜' i :=
+  rfl
+
+variable (n) in
+/-- `structureMapLM 𝕜 n i` is the `𝕜`-linear-map sending `f : 𝓓^{n}_{K}(E, F)` to its
+`i`-th iterated derivative as an element of `E →ᵇ (E [×i]→L[ℝ] F)`. In other words, it
+is the composition of `toBoundedContinuousFunctionLM 𝕜` and `iteratedFDerivWithOrderLM 𝕜 n 0 i`.
+This only makes mathematical sense if `i ≤ n`, otherwise we define it as the zero map.
+
+We call these "structure maps" because they define the topology on `𝓓^{n}_{K}(E, F)`.
+
+This is subsumed by `structureMapCLM` (not yet in Mathlib), which also bundles the
+continuity. -/
+noncomputable def structureMapLM (i : ℕ) :
+    𝓓^{n}_{K}(E, F) →ₗ[𝕜] E →ᵇ (E [×i]→L[ℝ] F) :=
+  toBoundedContinuousFunctionLM 𝕜 ∘ₗ iteratedFDerivWithOrderLM 𝕜 n 0 i
+
+lemma structureMapLM_eq {i : ℕ} :
+    (structureMapLM 𝕜 ⊤ i : 𝓓_{K}(E, F) →ₗ[𝕜] E →ᵇ (E [×i]→L[ℝ] F)) =
+      (toBoundedContinuousFunctionLM 𝕜 : 𝓓_{K}(E, E [×i]→L[ℝ] F) →ₗ[𝕜] E →ᵇ (E [×i]→L[ℝ] F)) ∘ₗ
+      (iteratedFDerivLM 𝕜 i : 𝓓_{K}(E, F) →ₗ[𝕜] 𝓓_{K}(E, E [×i]→L[ℝ] F)) :=
+  rfl
+
+lemma structureMapLM_apply_withOrder {i : ℕ} (f : 𝓓^{n}_{K}(E, F)) :
+    structureMapLM 𝕜 n i f = if i ≤ n then iteratedFDeriv ℝ i f else 0 := by
+  simp [structureMapLM]
+
+lemma structureMapLM_apply {i : ℕ} (f : 𝓓_{K}(E, F)) :
+    structureMapLM 𝕜 ⊤ i f = iteratedFDeriv ℝ i f := by
+  simp [structureMapLM_eq]
+
+lemma structureMapLM_eq_of_scalars {i : ℕ} (𝕜' : Type*) [NontriviallyNormedField 𝕜']
+    [NormedSpace 𝕜' F] [SMulCommClass ℝ 𝕜' F] :
+    (structureMapLM 𝕜 n i : 𝓓^{n}_{K}(E, F) → _) = structureMapLM 𝕜' n i :=
+  rfl
+
 end ContDiffMapSupportedIn

Mathlib/Topology/ContinuousMap/Bounded/Basic.lean

@@ -94,6 +94,11 @@ protected theorem continuous (f : α →ᵇ β) : Continuous f :=
 theorem ext (h : ∀ x, f x = g x) : f = g :=
   DFunLike.ext _ _ h
 
+@[simp]
+theorem coe_mk (f : α → β) (h : _) (h' : _) :
+    BoundedContinuousFunction.mk ⟨f, h⟩ h' = f :=
+  rfl
+
 theorem isBounded_range (f : α →ᵇ β) : IsBounded (range f) :=
   isBounded_range_iff.2 f.bounded
 
@@ -194,7 +199,7 @@ instance instMetricSpace {β} [MetricSpace β] : MetricSpace (α →ᵇ β) wher
 theorem nndist_eq : nndist f g = sInf { C | ∀ x : α, nndist (f x) (g x) ≤ C } :=
   Subtype.ext <| dist_eq.trans <| by
     rw [val_eq_coe, coe_sInf, coe_image]
-    simp_rw [mem_setOf_eq, ← NNReal.coe_le_coe, coe_mk, exists_prop, coe_nndist]
+    simp_rw [mem_setOf_eq, ← NNReal.coe_le_coe, NNReal.coe_mk, exists_prop, coe_nndist]
 
 theorem nndist_set_exists : ∃ C, ∀ x : α, nndist (f x) (g x) ≤ C :=
   Subtype.exists.mpr <| dist_set_exists.imp fun _ ⟨ha, h⟩ => ⟨ha, h⟩