English
If a finite-coordinate alternating map sends zero-norm coordinates to zero, a shell-based bound propagates to all vectors.
Русский
Если чередующийся отображатель в конечном числе координат отправляет нулевые компоненты в нулевые, граница на оболочке распространяется на все вектора.
LaTeX
$$$f\,m \le C \prod_i \|m_i\|$ при оболочке условий$$
Lean4
/-- If an alternating map in finitely many variables on seminormed spaces
sends vectors with a component of norm zero to vectors of norm zero
and 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`.
The first assumption is automatically satisfied on normed spaces, see `bound_of_shell` below.
For seminormed spaces, it follows from continuity of `f`,
see lemma `bound_of_shell_of_continuous` below. -/
theorem bound_of_shell_of_norm_map_coord_zero (f : E [⋀^ι]→ₗ[𝕜] F) (hf₀ : ∀ {m i}, ‖m i‖ = 0 → ‖f m‖ = 0) {ε : ι → ℝ}
{C : ℝ} (hε : ∀ i, 0 < ε i) {c : ι → 𝕜} (hc : ∀ i, 1 < ‖c i‖)
(hf : ∀ m : ι → E, (∀ i, ε i / ‖c i‖ ≤ ‖m i‖) → (∀ i, ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖) (m : ι → E) :
‖f m‖ ≤ C * ∏ i, ‖m i‖ :=
f.1.bound_of_shell_of_norm_map_coord_zero hf₀ hε hc hf m
