English
If a bilinear-like bound holds for f, then the induced continuous linear map mkContinuousLinear f C H has operator norm bounded by max{C, 0}.
Русский
Если для отображения f выполняется соответствующее двумерное ограничение, то нормa соответствующего линейного отображения mkContinuousLinear f C H удовлетворяет неравенству ∥mkContinuousLinear f C H∥ ≤ max{C,0}.
LaTeX
$$$ \|mkContinuousLinear f C H\| \le \max\{C,0\} $$$
Lean4
/-- Continuous multilinear maps on `𝕜^n` with values in `G` are in bijection with `G`, as such a
continuous multilinear map is completely determined by its value on the constant vector made of
ones. We register this bijection as a linear isometry in
`ContinuousMultilinearMap.piFieldEquiv`. -/
protected def piFieldEquiv : G ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun _ : ι => 𝕜) G
where
toFun z := ContinuousMultilinearMap.mkPiRing 𝕜 ι z
invFun f := f fun _ => 1
map_add' z
z' := by
ext
simp [smul_add]
map_smul' c
z := by
ext
simp [smul_smul, mul_comm]
left_inv z := by simp
right_inv f := f.mkPiRing_apply_one_eq_self
norm_map' := norm_mkPiRing
