feat(analysis/schwartz_space): lemmas for supremum of seminorms (#18648)

The main result is the bound `one_add_le_seminorm_sup_apply`, which is sometimes in the literature used as the definition of the Schwartz space.

We don't really care about the `2^k` factor, since this result is usually used to prove that certain operators are bounded on Schwartz space and hence finiteness of the right hand side is all that matters.

One application is to show that the product of a Schwartz function and a smooth polynomially growing function is again Schwartz.



Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

src/analysis/schwartz_space.lean

@@ -23,7 +23,7 @@ smooth functions `f : E → F`, where `E` and `F` are real normed vector spaces
 natural numbers `k` and `n` we have uniform bounds `‖x‖^k * ‖iterated_fderiv ℝ 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, which is by abstract theory from
+constants in the above estimates. The abstract theory of topological vector spaces developed in
 `seminorm_family.module_filter_basis` and `with_seminorms.to_locally_convex_space` turns the
 Schwartz space into a locally convex topological vector space.
 
@@ -41,6 +41,8 @@ decay faster than any power of `‖x‖`.
 
 * `schwartz_map.uniform_add_group` and `schwartz_map.locally_convex`: The Schwartz space is a
 locally convex topological vector space.
+* `schwartz_map.one_add_le_sup_seminorm_apply`: For a Schwartz function `f` there is a uniform bound
+on `(1 + ‖x‖) ^ k * ‖iterated_fderiv ℝ n f x‖`.
 
 ## Implementation details
 
@@ -430,25 +432,56 @@ begin
   rwa [pow_zero, one_mul] at this,
 end
 
-end seminorms
-
-section topology
-
-/-! ### The topology on the Schwartz space-/
-
-variables [normed_field 𝕜] [normed_space 𝕜 F] [smul_comm_class ℝ 𝕜 F]
 variables (𝕜 E F)
 
 /-- The family of Schwartz seminorms. -/
 def _root_.schwartz_seminorm_family : seminorm_family 𝕜 𝓢(E, F) (ℕ × ℕ) :=
-λ n, seminorm 𝕜 n.1 n.2
+λ m, seminorm 𝕜 m.1 m.2
 
 @[simp] lemma schwartz_seminorm_family_apply (n k : ℕ) :
   schwartz_seminorm_family 𝕜 E F (n,k) = schwartz_map.seminorm 𝕜 n k := rfl
 
 @[simp] lemma schwartz_seminorm_family_apply_zero :
   schwartz_seminorm_family 𝕜 E F 0 = schwartz_map.seminorm 𝕜 0 0 := rfl
 
+variables {𝕜 E 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. -/
+lemma one_add_le_sup_seminorm_apply {m : ℕ × ℕ} {k n : ℕ} (hk : k ≤ m.1) (hn : n ≤ m.2)
+  (f : 𝓢(E, F)) (x : E) :
+  (1 + ‖x‖) ^ k * ‖iterated_fderiv ℝ n f x‖
+    ≤ 2^m.1 * (finset.Iic m).sup (λ m, seminorm 𝕜 m.1 m.2) f :=
+begin
+  rw [add_comm, add_pow],
+  simp only [one_pow, mul_one, finset.sum_congr, finset.sum_mul],
+  norm_cast,
+  rw ← nat.sum_range_choose m.1,
+  push_cast,
+  rw [finset.sum_mul],
+  have hk' : finset.range (k + 1) ⊆ finset.range (m.1 + 1) :=
+  by rwa [finset.range_subset, add_le_add_iff_right],
+  refine le_trans (finset.sum_le_sum_of_subset_of_nonneg hk' (λ _ _ _, by positivity)) _,
+  refine finset.sum_le_sum (λ i hi, _),
+  rw [mul_comm (‖x‖^i), mul_assoc],
+  refine mul_le_mul _ _ (by positivity) (by positivity),
+  { norm_cast,
+    exact i.choose_le_choose hk },
+  exact (le_seminorm 𝕜 i n f x).trans (seminorm.le_def.1 (finset.le_sup_of_le
+    (finset.mem_Iic.2 $ prod.mk_le_mk.2 ⟨finset.mem_range_succ_iff.mp hi, hn⟩) le_rfl) _),
+end
+
+end seminorms
+
+section topology
+
+/-! ### The topology on the Schwartz space-/
+
+variables [normed_field 𝕜] [normed_space 𝕜 F] [smul_comm_class ℝ 𝕜 F]
+variables (𝕜 E F)
+
 instance : topological_space 𝓢(E, F) :=
 (schwartz_seminorm_family ℝ E F).module_filter_basis.topology'
 

src/data/finset/lattice.lean

@@ -83,6 +83,8 @@ lemma sup_const_le : s.sup (λ _, a) ≤ a := finset.sup_le $ λ _ _, le_rfl
 
 lemma le_sup {b : β} (hb : b ∈ s) : f b ≤ s.sup f := finset.sup_le_iff.1 le_rfl _ hb
 
+lemma le_sup_of_le {b : β} (hb : b ∈ s) (h : a ≤ f b) : a ≤ s.sup f := h.trans $ le_sup hb
+
 @[simp] lemma sup_bUnion [decidable_eq β] (s : finset γ) (t : γ → finset β) :
   (s.bUnion t).sup f = s.sup (λ x, (t x).sup f) :=
 eq_of_forall_ge_iff $ λ c, by simp [@forall_swap _ β]
@@ -310,6 +312,8 @@ lemma le_inf_const_le : a ≤ s.inf (λ _, a) := finset.le_inf $ λ _ _, le_rfl
 
 lemma inf_le {b : β} (hb : b ∈ s) : s.inf f ≤ f b := finset.le_inf_iff.1 le_rfl _ hb
 
+lemma inf_le_of_le {b : β} (hb : b ∈ s) (h : f b ≤ a) : s.inf f ≤ a := (inf_le hb).trans h
+
 lemma inf_mono_fun {g : β → α} (h : ∀ b ∈ s, f b ≤ g b) : s.inf f ≤ s.inf g :=
 finset.le_inf (λ b hb, le_trans (inf_le hb) (h b hb))
 
@@ -542,6 +546,9 @@ by { rw [←with_bot.coe_le_coe, coe_sup'],
 lemma le_sup' {b : β} (h : b ∈ s) : f b ≤ s.sup' ⟨b, h⟩ f :=
 by { rw [←with_bot.coe_le_coe, coe_sup'], exact le_sup h, }
 
+lemma le_sup'_of_le {a : α} {b : β} (hb : b ∈ s) (h : a ≤ f b) : a ≤ s.sup' ⟨b, hb⟩ f :=
+h.trans $ le_sup' _ hb
+
 @[simp] lemma sup'_const (a : α) : s.sup' H (λ b, a) = a :=
 begin
   apply le_antisymm,
@@ -637,6 +644,7 @@ variables {s : finset β} (H : s.nonempty) (f : β → α) {a : α} {b : β}
 
 lemma le_inf' (hs : ∀ b ∈ s, a ≤ f b) : a ≤ s.inf' H f := @sup'_le αᵒᵈ _ _ _ H f _ hs
 lemma inf'_le (h : b ∈ s) : s.inf' ⟨b, h⟩ f ≤ f b := @le_sup' αᵒᵈ _ _ _ f _ h
+lemma inf'_le_of_le (hb : b ∈ s) (h : f b ≤ a) : s.inf' ⟨b, hb⟩ f ≤ a := (inf'_le _ hb).trans h
 
 @[simp] lemma inf'_const (a : α) : s.inf' H (λ b, a) = a := @sup'_const αᵒᵈ _ _ _ H _