fin0_apply_norm — Mathlib

English

The operator norm of the curryMid transform equals the original operator norm: ∥f.curryMid p∥ = ∥f∥.

Русский

Норма оператора для каррирования curryMid равна исходной норме: ∥f.curryMid p∥ = ∥f∥.

LaTeX

$$$\\|f.curryMid\\,p\\| = \\|f\\|$$$

Lean4

@[simp]
theorem fin0_apply_norm (f : G [×0]→L[𝕜] G') {x : Fin 0 → G} : ‖f x‖ = ‖f‖ :=
  by
  obtain rfl : x = 0 := Subsingleton.elim _ _
  refine le_antisymm (by simpa using f.le_opNorm 0) ?_
  have : ‖ContinuousMultilinearMap.uncurry0 𝕜 G f.curry0‖ ≤ ‖f.curry0‖ :=
    ContinuousMultilinearMap.opNorm_le_bound (norm_nonneg _) fun m => by
      simp [-ContinuousMultilinearMap.apply_zero_uncurry0]
  simpa [-Matrix.zero_empty] using this

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