English
A refined bound holds for all m with a supremum over a finite index set, linking to Schwartz seminorms.
Русский
Существует уточнённое неравенство для всех m, где применяется супремум по конечному множеству индексов и связывается с семинормами SchwartzMap.
LaTeX
$$$\forall m\in \mathbb{N}^2, \; \forall f, x: \; \text{bound}(m,f,x) \le 2^{m_1} \sup_{i\le m_1,j\le m_2} \mathrm{seminorm}(i,j)(f)$$$
Lean4
/-- 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. -/
theorem 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 * ‖iteratedFDeriv ℝ n f x‖ ≤
2 ^ m.1 * (Finset.Iic m).sup (fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f :=
by
rw [add_comm, add_pow]
simp only [one_pow, mul_one, 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 grind
grw [hk']
gcongr ∑ _i ∈ Finset.range (m.1 + 1), ?_ with i hi
move_mul [(Nat.choose k i : ℝ), (Nat.choose m.1 i : ℝ)]
gcongr
· apply (le_seminorm 𝕜 i n f x).trans
apply Seminorm.le_def.1
exact Finset.le_sup_of_le (Finset.mem_Iic.2 <| Prod.mk_le_mk.2 ⟨Finset.mem_range_succ_iff.mp hi, hn⟩) le_rfl
· exact mod_cast Nat.choose_le_choose i hk
