English
Under a global bound, the difference f(m1) - f(m2) is bounded by a sum of products of coordinates norms.
Русский
При наличии глобального ограничение, разность f(m1) - f(m2) ограничена суммой произведений норм координат.
LaTeX
$$$\|f m_1 - f m_2\| ≤ C \sum_i \prod_j \|m_{1j} - m_{2j}\|$$$
Lean4
/-- If an alternating map `f` satisfies a boundedness property around `0`,
one can deduce a bound on `f m₁ - f m₂` using the multilinearity.
Here, we give a usable but not very precise version.
See `AlternatingMap.norm_image_sub_le_of_bound'` for a more precise but less usable version.
The bound is `‖f m - f m'‖ ≤ C * card ι * ‖m - m'‖ * (max ‖m‖ ‖m'‖) ^ (card ι - 1)`. -/
theorem norm_image_sub_le_of_bound (f : E [⋀^ι]→ₗ[𝕜] F) {C : ℝ} (hC : 0 ≤ C) (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖)
(m₁ m₂ : ι → E) : ‖f m₁ - f m₂‖ ≤ C * (Fintype.card ι) * (max ‖m₁‖ ‖m₂‖) ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖ :=
f.toMultilinearMap.norm_image_sub_le_of_bound hC H m₁ m₂
