English
A bound-of-difference inequality holds for two inputs m1 and m2 of a multilinear map: the norm of f(m1) − f(m2) is bounded by a sum of products involving coordinate differences.
Русский
Существует неравенство для разности значений f(m1) − f(m2), выражающее норму через сумму произведений по координатам и их различиям.
LaTeX
$$‖f(m1) − f(m2)‖ ≤ C * ∑ i ∏ j, (if j = i then ‖m1_i − m2_i‖ else max(‖m1_j‖, ‖m2_j‖))$$
Lean4
/-- If a continuous multilinear map in finitely many variables on normed spaces satisfies
the inequality `‖f m‖ ≤ C * ∏ i, ‖m i‖` on a shell `ε i / ‖c i‖ < ‖m i‖ < ε i` for some positive
numbers `ε i` and elements `c i : 𝕜`, `1 < ‖c i‖`, then it satisfies this inequality for all `m`. -/
theorem bound_of_shell_of_continuous (f : MultilinearMap 𝕜 E G) (hfc : Continuous f) {ε : ι → ℝ} {C : ℝ}
(hε : ∀ i, 0 < ε i) {c : ι → 𝕜} (hc : ∀ i, 1 < ‖c i‖)
(hf : ∀ m : ∀ i, E i, (∀ i, ε i / ‖c i‖ ≤ ‖m i‖) → (∀ i, ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖) (m : ∀ i, E i) :
‖f m‖ ≤ C * ∏ i, ‖m i‖ :=
bound_of_shell_of_norm_map_coord_zero f (norm_map_coord_zero f hfc) hε hc hf m
