norm_compContinuousLinearMap_le — Mathlib

English

If a bound holds for the multilinear map f, then the norm of the composed continuous multilinear map is at most the bound C when the lower bound is non-positive, i.e., ∥mkContinuousLinear f C H∥ ≤ C.

Русский

Если ограничение выполнено для отображения f, то норма композиции не превышает C при условии 0 ≤ C.

LaTeX

$$$ \|mkContinuousLinear f C H\| ≤ C $ (when 0 ≤ C and H bound is satisfied)$$

Lean4

theorem norm_compContinuousLinearMap_le (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : ∀ i, E i →L[𝕜] E₁ i) :
    ‖g.compContinuousLinearMap f‖ ≤ ‖g‖ * ∏ i, ‖f i‖ :=
  opNorm_le_bound (by positivity) fun m =>
    calc
      ‖g fun i => f i (m i)‖ ≤ ‖g‖ * ∏ i, ‖f i (m i)‖ := g.le_opNorm _
      _ ≤ ‖g‖ * ∏ i, ‖f i‖ * ‖m i‖ := by gcongr with i; exact (f i).le_opNorm (m i)
      _ = (‖g‖ * ∏ i, ‖f i‖) * ∏ i, ‖m i‖ := by rw [prod_mul_distrib, mul_assoc]

Похожие утверждения