compAlongOrderedFinpartitionL — Mathlib

English

Bundled version: compAlongOrderedFinpartitionL f p equals compAlongOrderedFinpartition f p when evaluated on arguments.

Русский

Упакованная версия: compAlongOrderedFinpartitionL f p эквивалентна compAlongOrderedFinpartition f p на аргументах.

LaTeX

$$c.compAlongOrderedFinpartitionL 𝕜 E F G f p = c.compAlongOrderedFinpartition f p$$

Lean4

/-- Bundled version of `compAlongOrderedFinpartition`, depending continuously linearly on `f`
and continuously multilinearly on `p`. -/
noncomputable def compAlongOrderedFinpartitionL :
    (F [×c.length]→L[𝕜] G) →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i ↦ E [×c.partSize i]→L[𝕜] F) (E [×n]→L[𝕜] G) :=
  by
  refine MultilinearMap.mkContinuousLinear c.compAlongOrderedFinpartitionₗ 1 fun f p ↦ ?_
  simp only [one_mul, compAlongOrderedFinpartitionₗ_apply_apply]
  apply norm_compAlongOrderedFinpartition_le

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