norm_mkPiAlgebraFin_succ_le — Mathlib

English

When the index n is zero, mkPiAlgebraFin 𝕜 0 A has norm equal to the norm of 1 in A. This gives the base case for recursive Pi-constructions.

Русский

При индексе n=0 норма mkPiAlgebraFin 𝕜 0 A равна норме единицы в A.

LaTeX

$$$\|\mathrm{mkPiAlgebraFin}_{\mathbb{K}}(0, A)\| = \|1\|$$$

Lean4

theorem norm_mkPiAlgebraFin_succ_le : ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A‖ ≤ 1 :=
  by
  refine opNorm_le_bound zero_le_one fun m => ?_
  simp only [ContinuousMultilinearMap.mkPiAlgebraFin_apply, one_mul, List.ofFn_eq_map, Fin.prod_univ_def]
  refine (List.norm_prod_le' ?_).trans_eq ?_
  · rw [Ne, List.map_eq_nil_iff, List.finRange_eq_nil]
    exact Nat.succ_ne_zero _
  rw [List.map_map, Function.comp_def]

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