theorem SchwartzSeminorms.weighted_norm_le_sup_seminorm {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] {K k n : ℕ} (hk : k ≤ K) (hn : n ≤ K) (f : SchwartzMap E F) (x : E) : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ 2 ^ K * ((Finset.Iic (K, K)).sup fun (m : ℕ × ℕ) => SchwartzMap.seminorm 𝕜 m.1 m.2) f

Pointwise weighted derivative bound by Schwartz seminorms: for k, n ≤ K, (1 + ‖x‖)^k · ‖∂^n f(x)‖ ≤ 2^K · sup_{m ≤ (K, K)} (Schwartz seminorm m of f).

theorem SchwartzSeminorms.monomial_norm_le_weighted_norm {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (k n : ℕ) (f : SchwartzMap E F) (x : E) : ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖

Trivial comparison: ‖x‖^k ≤ (1 + ‖x‖)^k pointwise, with the derivative factor common.

theorem SchwartzSeminorms.seminorm_le_two_pow_mul_sup_seminorm {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (K : ℕ) {k n : ℕ} (hk : k ≤ K) (hn : n ≤ K) (f : SchwartzMap E F) : (SchwartzMap.seminorm 𝕜 k n) f ≤ 2 ^ K * ((Finset.Iic (K, K)).sup fun (m : ℕ × ℕ) => SchwartzMap.seminorm 𝕜 m.1 m.2) f

Uniform comparison of individual Schwartz seminorms with the supremum: for k, n ≤ K, ‖f‖_{k,n} ≤ 2^K · sup_{(k',n') ≤ (K, K)} ‖f‖_{k',n'}.

theorem SchwartzSeminorms.individual_le_sup_seminorm {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] {K k n : ℕ} (hk : k ≤ K) (hn : n ≤ K) (f : SchwartzMap E F) : (SchwartzMap.seminorm 𝕜 k n) f ≤ ((Finset.Iic (K, K)).sup fun (m : ℕ × ℕ) => SchwartzMap.seminorm 𝕜 m.1 m.2) f

Each Schwartz seminorm ‖f‖_{k,n} with k, n ≤ K is bounded by the supremum over the finite set Iic (K, K) of such seminorms.

theorem SchwartzSeminorms.monomial_le_one_add_pow_pointwise {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {K p q : ℕ} (hp : p ≤ K) (f : SchwartzMap E F) (x : E) : ‖x‖ ^ p * ‖iteratedFDeriv ℝ q (⇑f) x‖ ≤ (1 + ‖x‖) ^ K * ‖iteratedFDeriv ℝ q (⇑f) x‖

Pointwise monotonicity of weighted derivative bounds: for p ≤ K, ‖x‖^p · ‖∂^q f(x)‖ ≤ (1 + ‖x‖)^K · ‖∂^q f(x)‖.

theorem SchwartzSeminorms.seminorm_le_weighted_via_one_add {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] {K p q : ℕ} (hp : p ≤ K) (hq : q ≤ K) (f : SchwartzMap E F) : (SchwartzMap.seminorm 𝕜 p q) f ≤ 2 ^ K * ((Finset.Iic (K, K)).sup fun (m : ℕ × ℕ) => SchwartzMap.seminorm 𝕜 m.1 m.2) f

Reformulation of the seminorm-supremum bound using the (1 + ‖x‖)^K weight: for p, q ≤ K, ‖f‖_{p,q} ≤ 2^K · sup_{(k, n) ≤ (K, K)} ‖f‖_{k,n}.