English
For a continuous multilinear map f on E, if a coordinate component m_i has zero norm, then the evaluation f(m) has zero norm.
Русский
Для непрерывной многообразной карты f на E, если какой-либо компонент м_i имеет нулевую норму, то f(m) имеет ноль нормы.
LaTeX
$$‖f m‖ = 0 whenever ‖m_i‖ = 0 for some i$$
Lean4
/-- If a multilinear 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 next lemma,
see `bound_of_shell_of_continuous` below. -/
theorem bound_of_shell_of_norm_map_coord_zero (f : MultilinearMap 𝕜 E G) (hf₀ : ∀ {m i}, ‖m i‖ = 0 → ‖f m‖ = 0)
{ε : ι → ℝ} {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‖ := by
rcases em (∃ i, ‖m i‖ = 0) with (⟨i, hi⟩ | hm)
· rw [hf₀ hi, prod_eq_zero (mem_univ i) hi, mul_zero]
push_neg at hm
choose δ hδ0 hδm_lt hle_δm _ using fun i => rescale_to_shell_semi_normed (hc i) (hε i) (hm i)
have hδ0 : 0 < ∏ i, ‖δ i‖ := prod_pos fun i _ => norm_pos_iff.2 (hδ0 i)
simpa [map_smul_univ, norm_smul, prod_mul_distrib, mul_left_comm C, hδ0] using hf (fun i => δ i • m i) hle_δm hδm_lt
