English
Let alternatizeUncurryFinCLM be the continuous linear map realizing alternatization of uncurry Fin; it provides a continuous linear map from E →L[𝕜] E [⋀^Fin n]→L[𝕜] F to the Fin(n+1) level.
Русский
Пусть alternatizeUncurryFinCLM реализует чередование конверсии развёртки Fin; он задаёт непрерывное линейное отображение между уровнями.
LaTeX
$$$\\text{alternatizeUncurryFinCLM} : (E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) →L[𝕜] E [⋀^Fin (n+1)]→L[𝕜] F$$$
Lean4
/-- `AlternaringMap.alternatizeUncurryFin` as a continuous linear map. -/
@[irreducible]
noncomputable def alternatizeUncurryFinCLM : (E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) →L[𝕜] E [⋀^Fin (n + 1)]→L[𝕜] F :=
AlternatingMap.mkContinuousLinear alternatizeUncurryFinCLM.aux (n + 1) fun f v ↦
calc
‖alternatizeUncurryFinCLM.aux f v‖ ≤ ∑ i : Fin (n + 1), ‖f‖ * ∏ i, ‖v i‖ :=
by
rw [alternatizeUncurryFinCLM.aux_apply]
refine norm_sum_le_of_le _ fun i hi ↦ ?_
rw [norm_isUnit_zsmul _ (.pow _ isUnit_one.neg), i.prod_univ_succAbove, ← mul_assoc]
apply (f (v i)).le_of_opNorm_le
apply f.le_opNorm
_ = (n + 1) * ‖f‖ * ∏ i, ‖v i‖ := by simp [mul_assoc]
