English
If a multilinear map is continuous, then there exists a bound as above; conversely, a bound implies continuity.
Русский
Если карта непрерывна, существует граница; напр., ограничение порождает непрерывность.
LaTeX
$$continuous_of_bound and bound_of_continuous$$
Lean4
/-- Given a multilinear map in `n` variables, if one restricts it to `k` variables putting `z` on
the other coordinates, then the resulting restricted function satisfies an inequality
`‖f.restr v‖ ≤ C * ‖z‖^(n-k) * Π ‖v i‖` if the original function satisfies `‖f v‖ ≤ C * Π ‖v i‖`. -/
theorem restr_norm_le {k n : ℕ} (f : MultilinearMap 𝕜 (fun _ : Fin n => G) G') (s : Finset (Fin n)) (hk : #s = k)
(z : G) {C : ℝ} (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) (v : Fin k → G) :
‖f.restr s hk z v‖ ≤ C * ‖z‖ ^ (n - k) * ∏ i, ‖v i‖ :=
by
rw [mul_right_comm, mul_assoc]
convert H _ using 2
simp only [apply_dite norm, Fintype.prod_dite, prod_const ‖z‖, Finset.card_univ,
Fintype.card_of_subtype sᶜ fun _ => mem_compl, card_compl, Fintype.card_fin, hk,
← (s.orderIsoOfFin hk).symm.bijective.prod_comp fun x => ‖v x‖]
convert rfl
