English
If f satisfies a growth bound with H, then ‖mkContinuousAlternating f C H‖ ≤ max(C,0).
Русский
Если соблюдается верхняя граница роста, норма mkContinuousAlternating не превосходит max(C,0).
LaTeX
$$$\\\\| mkContinuousAlternating f C H \\\\| \\\\le \\\\max(C, 0)$$$
Lean4
/-- Given a continuous alternating map `f` in `n+1` variables, split the first variable to obtain
a continuous linear map into continuous alternating maps in `n` variables,
given by `x ↦ (m ↦ f (Matrix.vecCons x m))`.
It can be thought of as a map $Hom(\bigwedge^{n+1} M, N) \to Hom(M, Hom(\bigwedge^n M, N))$.
This is `ContinuousMultilinearMap.curryLeft` for `AlternatingMap`. See also
`ContinuousAlternatingMap.curryLeftLI`. -/
noncomputable def curryLeft (f : E [⋀^Fin (n + 1)]→L[𝕜] F) : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F :=
AlternatingMap.mkContinuousLinear f.toAlternatingMap.curryLeft ‖f‖ f.toContinuousMultilinearMap.norm_map_cons_le
