Currying and uncurrying continuous multilinear maps

We associate to a continuous multilinear map in n+1 variables (i.e., based on Fin n.succ) two curried functions, named f.curryLeft (which is a continuous linear map on E 0 taking values in continuous multilinear maps in n variables) and f.curryRight (which is a continuous multilinear map in n variables taking values in continuous linear maps on E (last n)). The inverse operations are called uncurryLeft and uncurryRight.

We also register continuous linear equiv versions of these correspondences, in continuousMultilinearCurryLeftEquiv and continuousMultilinearCurryRightEquiv.

Main results

• ContinuousMultilinearMap.curryLeft, ContinuousLinearMap.uncurryLeft and continuousMultilinearCurryLeftEquiv
• ContinuousMultilinearMap.curryRight, ContinuousMultilinearMap.uncurryRight and continuousMultilinearCurryRightEquiv.

Type variables

We use the following type variables in this file:

• 𝕜 : a NontriviallyNormedField;
• ι, ι' : finite index types with decidable equality;
• E, E₁ : families of normed vector spaces over 𝕜 indexed by i : ι;
• E' : a family of normed vector spaces over 𝕜 indexed by i' : ι';
• Ei : a family of normed vector spaces over 𝕜 indexed by i : Fin (Nat.succ n);
• G, G' : normed vector spaces over 𝕜.

theorem ContinuousLinearMap.norm_map_tail_le {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => Ei i.succ) G) (m : (i : Fin n.succ) → Ei i) : ‖(f (m 0)) (Fin.tail m)‖ ≤ ‖f‖ * ∏ i : Fin n.succ, ‖m i‖

theorem ContinuousMultilinearMap.norm_map_init_le {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => Ei i.castSucc) (Ei (Fin.last n) →L[𝕜] G)) (m : (i : Fin n.succ) → Ei i) : ‖(f (Fin.init m)) (m (Fin.last n))‖ ≤ ‖f‖ * ∏ i : Fin n.succ, ‖m i‖

theorem ContinuousMultilinearMap.norm_map_cons_le {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G) (x : Ei 0) (m : (i : Fin n) → Ei i.succ) : ‖f (Fin.cons x m)‖ ≤ ‖f‖ * ‖x‖ * ∏ i : Fin n, ‖m i‖

theorem ContinuousMultilinearMap.norm_map_snoc_le {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G) (m : (i : Fin n) → Ei i.castSucc) (x : Ei (Fin.last n)) : ‖f (Fin.snoc m x)‖ ≤ (‖f‖ * ∏ i : Fin n, ‖m i‖) * ‖x‖

Left currying

noncomputable def ContinuousLinearMap.uncurryLeft {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => Ei i.succ) G) : ContinuousMultilinearMap 𝕜 Ei G

Given a continuous linear map f from E 0 to continuous multilinear maps on n variables, construct the corresponding continuous multilinear map on n+1 variables obtained by concatenating the variables, given by m ↦ f (m 0) (tail m)

Equations

• f.uncurryLeft = (ContinuousMultilinearMap.toMultilinearMapLinear ∘ₗ ↑f).uncurryLeft.mkContinuous ‖f‖ ⋯

@[simp]

theorem ContinuousLinearMap.uncurryLeft_apply {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => Ei i.succ) G) (m : (i : Fin n.succ) → Ei i) : f.uncurryLeft m = (f (m 0)) (Fin.tail m)

noncomputable def ContinuousMultilinearMap.curryLeft {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G) : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => Ei i.succ) G

Given a continuous multilinear map f in n+1 variables, split the first variable to obtain a continuous linear map into continuous multilinear maps in n variables, given by x ↦ (m ↦ f (cons x m)).

Equations

• f.curryLeft = { toFun := fun (x : Ei 0) => (f.curryLeft x).mkContinuous (‖f‖ * ‖x‖) ⋯, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous ‖f‖ ⋯

@[simp]

theorem ContinuousMultilinearMap.curryLeft_apply {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G) (x : Ei 0) (m : (i : Fin n) → Ei i.succ) : (f.curryLeft x) m = f (Fin.cons x m)

@[simp]

theorem ContinuousLinearMap.curry_uncurryLeft {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => Ei i.succ) G) : f.uncurryLeft.curryLeft = f

@[simp]

theorem ContinuousMultilinearMap.uncurry_curryLeft {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G) : f.curryLeft.uncurryLeft = f

noncomputable def continuousMultilinearCurryLeftEquiv (𝕜 : Type u) {n : ℕ} (Ei : Fin n.succ → Type wEi) (G : Type wG) [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] : ContinuousMultilinearMap 𝕜 Ei G ≃ₗᵢ[𝕜] Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => Ei i.succ) G

The space of continuous multilinear maps on Π(i : Fin (n+1)), E i is canonically isomorphic to the space of continuous linear maps from E 0 to the space of continuous multilinear maps on Π(i : Fin n), E i.succ, by separating the first variable. We register this isomorphism in continuousMultilinearCurryLeftEquiv 𝕜 E E₂. The algebraic version (without topology) is given in multilinearCurryLeftEquiv 𝕜 E E₂.

The direct and inverse maps are given by f.curryLeft and f.uncurryLeft. Use these unless you need the full framework of linear isometric equivs.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem continuousMultilinearCurryLeftEquiv_apply {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G) (x : Ei 0) (v : (i : Fin n) → Ei i.succ) : (((continuousMultilinearCurryLeftEquiv 𝕜 Ei G) f) x) v = f (Fin.cons x v)

@[simp]

theorem continuousMultilinearCurryLeftEquiv_symm_apply {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => Ei i.succ) G) (v : (i : Fin n.succ) → Ei i) : ((continuousMultilinearCurryLeftEquiv 𝕜 Ei G).symm f) v = (f (v 0)) (Fin.tail v)

@[simp]

theorem ContinuousMultilinearMap.curryLeft_norm {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G) : ‖f.curryLeft‖ = ‖f‖

@[simp]

theorem ContinuousLinearMap.uncurryLeft_norm {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => Ei i.succ) G) : ‖f.uncurryLeft‖ = ‖f‖

Right currying

noncomputable def ContinuousMultilinearMap.uncurryRight {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => Ei i.castSucc) (Ei (Fin.last n) →L[𝕜] G)) : ContinuousMultilinearMap 𝕜 Ei G

Given a continuous linear map f from continuous multilinear maps on n variables to continuous linear maps on E 0, construct the corresponding continuous multilinear map on n+1 variables obtained by concatenating the variables, given by m ↦ f (init m) (m (last n)).

Equations

• f.uncurryRight = { toFun := fun (m : (i : Fin n) → Ei i.castSucc) => ↑(f m), map_add' := ⋯, map_smul' := ⋯ }.uncurryRight.mkContinuous ‖f‖ ⋯

@[simp]

theorem ContinuousMultilinearMap.uncurryRight_apply {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => Ei i.castSucc) (Ei (Fin.last n) →L[𝕜] G)) (m : (i : Fin n.succ) → Ei i) : f.uncurryRight m = (f (Fin.init m)) (m (Fin.last n))

noncomputable def ContinuousMultilinearMap.curryRight {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G) : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => Ei i.castSucc) (Ei (Fin.last n) →L[𝕜] G)

Given a continuous multilinear map f in n+1 variables, split the last variable to obtain a continuous multilinear map in n variables into continuous linear maps, given by m ↦ (x ↦ f (snoc m x)).

Equations

• f.curryRight = { toFun := fun (m : (i : Fin n) → Ei i.castSucc) => (f.curryRight m).mkContinuous (‖f‖ * ∏ i : Fin n, ‖m i‖) ⋯, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous ‖f‖ ⋯

@[simp]

theorem ContinuousMultilinearMap.curryRight_apply {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G) (m : (i : Fin n) → Ei i.castSucc) (x : Ei (Fin.last n)) : (f.curryRight m) x = f (Fin.snoc m x)

@[simp]

theorem ContinuousMultilinearMap.curry_uncurryRight {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => Ei i.castSucc) (Ei (Fin.last n) →L[𝕜] G)) : f.uncurryRight.curryRight = f

@[simp]

theorem ContinuousMultilinearMap.uncurry_curryRight {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G) : f.curryRight.uncurryRight = f

noncomputable def continuousMultilinearCurryRightEquiv (𝕜 : Type u) {n : ℕ} (Ei : Fin n.succ → Type wEi) (G : Type wG) [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] : ContinuousMultilinearMap 𝕜 Ei G ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => Ei i.castSucc) (Ei (Fin.last n) →L[𝕜] G)

The space of continuous multilinear maps on Π(i : Fin (n+1)), Ei i is canonically isomorphic to the space of continuous multilinear maps on Π(i : Fin n), Ei <| castSucc i with values in the space of continuous linear maps on Ei (last n), by separating the last variable. We register this isomorphism as a continuous linear equiv in continuousMultilinearCurryRightEquiv 𝕜 Ei G. The algebraic version (without topology) is given in multilinearCurryRightEquiv 𝕜 Ei G.

The direct and inverse maps are given by f.curryRight and f.uncurryRight. Use these unless you need the full framework of linear isometric equivs.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def continuousMultilinearCurryRightEquiv' (𝕜 : Type u) (n : ℕ) (G : Type wG) (G' : Type wG') [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] : ContinuousMultilinearMap 𝕜 (fun (i : Fin n.succ) => G) G' ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => G) (G →L[𝕜] G')

The space of continuous multilinear maps on Π(i : Fin (n+1)), G is canonically isomorphic to the space of continuous multilinear maps on Π(i : Fin n), G with values in the space of continuous linear maps on G, by separating the last variable. We register this isomorphism as a continuous linear equiv in continuousMultilinearCurryRightEquiv' 𝕜 n G G'. For a version allowing dependent types, see continuousMultilinearCurryRightEquiv. When there are no dependent types, use the primed version as it helps Lean a lot for unification.

The direct and inverse maps are given by f.curryRight and f.uncurryRight. Use these unless you need the full framework of linear isometric equivs.

Equations

• continuousMultilinearCurryRightEquiv' 𝕜 n G G' = continuousMultilinearCurryRightEquiv 𝕜 (fun (x : Fin n.succ) => G) G'

@[simp]

theorem continuousMultilinearCurryRightEquiv_apply {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G) (v : (i : Fin n) → Ei i.castSucc) (x : Ei (Fin.last n)) : (((continuousMultilinearCurryRightEquiv 𝕜 Ei G) f) v) x = f (Fin.snoc v x)

@[simp]

theorem continuousMultilinearCurryRightEquiv_symm_apply {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => Ei i.castSucc) (Ei (Fin.last n) →L[𝕜] G)) (v : (i : Fin n.succ) → Ei i) : ((continuousMultilinearCurryRightEquiv 𝕜 Ei G).symm f) v = (f (Fin.init v)) (v (Fin.last n))

@[simp]

theorem continuousMultilinearCurryRightEquiv_apply' {𝕜 : Type u} {n : ℕ} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin n.succ) => G) G') (v : Fin n → G) (x : G) : (((continuousMultilinearCurryRightEquiv' 𝕜 n G G') f) v) x = f (Fin.snoc v x)

@[simp]

theorem continuousMultilinearCurryRightEquiv_symm_apply' {𝕜 : Type u} {n : ℕ} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => G) (G →L[𝕜] G')) (v : Fin (n + 1) → G) : ((continuousMultilinearCurryRightEquiv' 𝕜 n G G').symm f) v = (f (Fin.init v)) (v (Fin.last n))

@[simp]

theorem ContinuousMultilinearMap.curryRight_norm {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G) : ‖f.curryRight‖ = ‖f‖

@[simp]

theorem ContinuousMultilinearMap.uncurryRight_norm {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : Fin n.succ) → NormedAddCommGroup (Ei i)] [(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => Ei i.castSucc) (Ei (Fin.last n) →L[𝕜] G)) : ‖f.uncurryRight‖ = ‖f‖

Currying with 0 variables

The space of multilinear maps with 0 variables is trivial: such a multilinear map is just an arbitrary constant (note that multilinear maps in 0 variables need not map 0 to 0!). Therefore, the space of continuous multilinear maps on (Fin 0) → G with values in E₂ is isomorphic (and even isometric) to E₂. As this is the zeroth step in the construction of iterated derivatives, we register this isomorphism.

noncomputable def ContinuousMultilinearMap.curry0 {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : ContinuousMultilinearMap 𝕜 (fun (x : Fin 0) => G) G') : G'

Associating to a continuous multilinear map in 0 variables the unique value it takes.

Equations

• f.curry0 = f 0

noncomputable def ContinuousMultilinearMap.uncurry0 (𝕜 : Type u) (G : Type wG) {G' : Type wG'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (x : G') : ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) => G) G'

Associating to an element x of a vector space E₂ the continuous multilinear map in 0 variables taking the (unique) value x

Equations

• ContinuousMultilinearMap.uncurry0 𝕜 G x = ContinuousMultilinearMap.constOfIsEmpty 𝕜 (fun (i : Fin 0) => G) x

@[simp]

theorem ContinuousMultilinearMap.uncurry0_apply (𝕜 : Type u) {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (x : G') (m : Fin 0 → G) : (ContinuousMultilinearMap.uncurry0 𝕜 G x) m = x

@[simp]

theorem ContinuousMultilinearMap.curry0_apply {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) => G) G') : f.curry0 = f 0

@[simp]

theorem ContinuousMultilinearMap.apply_zero_uncurry0 {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) => G) G') {x : Fin 0 → G} : ContinuousMultilinearMap.uncurry0 𝕜 G (f x) = f

theorem ContinuousMultilinearMap.uncurry0_curry0 {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) => G) G') : ContinuousMultilinearMap.uncurry0 𝕜 G f.curry0 = f

theorem ContinuousMultilinearMap.curry0_uncurry0 (𝕜 : Type u) (G : Type wG) {G' : Type wG'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (x : G') : (ContinuousMultilinearMap.uncurry0 𝕜 G x).curry0 = x

@[simp]

theorem ContinuousMultilinearMap.uncurry0_norm (𝕜 : Type u) (G : Type wG) {G' : Type wG'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (x : G') : ‖ContinuousMultilinearMap.uncurry0 𝕜 G x‖ = ‖x‖

@[simp]

theorem ContinuousMultilinearMap.fin0_apply_norm {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) => G) G') {x : Fin 0 → G} : ‖f x‖ = ‖f‖

theorem ContinuousMultilinearMap.curry0_norm {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) => G) G') : ‖f.curry0‖ = ‖f‖

noncomputable def continuousMultilinearCurryFin0 (𝕜 : Type u) (G : Type wG) (G' : Type wG') [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] : ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) => G) G' ≃ₗᵢ[𝕜] G'

The continuous linear isomorphism between elements of a normed space, and continuous multilinear maps in 0 variables with values in this normed space.

The direct and inverse maps are uncurry0 and curry0. Use these unless you need the full framework of linear isometric equivs.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem continuousMultilinearCurryFin0_apply {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) => G) G') : (continuousMultilinearCurryFin0 𝕜 G G') f = f 0

@[simp]

theorem continuousMultilinearCurryFin0_symm_apply {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (x : G') (v : Fin 0 → G) : ((continuousMultilinearCurryFin0 𝕜 G G').symm x) v = x

With 1 variable

noncomputable def continuousMultilinearCurryFin1 (𝕜 : Type u) (G : Type wG) (G' : Type wG') [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) => G) G' ≃ₗᵢ[𝕜] G →L[𝕜] G'

Continuous multilinear maps from G^1 to G' are isomorphic with continuous linear maps from G to G'.

Equations

• continuousMultilinearCurryFin1 𝕜 G G' = (continuousMultilinearCurryRightEquiv 𝕜 (fun (x : Fin 1) => G) G').trans (continuousMultilinearCurryFin0 𝕜 G (G →L[𝕜] G'))

@[simp]

theorem continuousMultilinearCurryFin1_apply {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) => G) G') (x : G) : ((continuousMultilinearCurryFin1 𝕜 G G') f) x = f (Fin.snoc 0 x)

@[simp]

theorem continuousMultilinearCurryFin1_symm_apply {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : G →L[𝕜] G') (v : Fin 1 → G) : ((continuousMultilinearCurryFin1 𝕜 G G').symm f) v = f (v 0)

@[simp]

theorem ContinuousMultilinearMap.norm_domDomCongr (𝕜 : Type u) {ι : Type v} {ι' : Type v'} (G : Type wG) (G' : Type wG') [Fintype ι] [Fintype ι'] [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (σ : ι ≃ ι') (f : ContinuousMultilinearMap 𝕜 (fun (x : ι) => G) G') : ‖ContinuousMultilinearMap.domDomCongr σ f‖ = ‖f‖

noncomputable def ContinuousMultilinearMap.domDomCongrₗᵢ (𝕜 : Type u) {ι : Type v} {ι' : Type v'} (G : Type wG) (G' : Type wG') [Fintype ι] [Fintype ι'] [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (σ : ι ≃ ι') : ContinuousMultilinearMap 𝕜 (fun (x : ι) => G) G' ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι') => G) G'

An equivalence of the index set defines a linear isometric equivalence between the spaces of multilinear maps.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ContinuousMultilinearMap.currySum {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {G : Type wG} {G' : Type wG'} [Fintype ι] [Fintype ι'] [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : ContinuousMultilinearMap 𝕜 (fun (x : ι ⊕ ι') => G) G') : ContinuousMultilinearMap 𝕜 (fun (x : ι) => G) (ContinuousMultilinearMap 𝕜 (fun (x : ι') => G) G')

A continuous multilinear map with variables indexed by ι ⊕ ι' defines a continuous multilinear map with variables indexed by ι taking values in the space of continuous multilinear maps with variables indexed by ι'.

Equations

• f.currySum = f.currySum.mkContinuousMultilinear ‖f‖ ⋯

@[simp]

theorem ContinuousMultilinearMap.currySum_apply {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {G : Type wG} {G' : Type wG'} [Fintype ι] [Fintype ι'] [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : ContinuousMultilinearMap 𝕜 (fun (x : ι ⊕ ι') => G) G') (m : ι → G) (m' : ι' → G) : (f.currySum m) m' = f (Sum.elim m m')

noncomputable def ContinuousMultilinearMap.uncurrySum {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {G : Type wG} {G' : Type wG'} [Fintype ι] [Fintype ι'] [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : ContinuousMultilinearMap 𝕜 (fun (x : ι) => G) (ContinuousMultilinearMap 𝕜 (fun (x : ι') => G) G')) : ContinuousMultilinearMap 𝕜 (fun (x : ι ⊕ ι') => G) G'

A continuous multilinear map with variables indexed by ι taking values in the space of continuous multilinear maps with variables indexed by ι' defines a continuous multilinear map with variables indexed by ι ⊕ ι'.

Equations

• f.uncurrySum = (ContinuousMultilinearMap.toMultilinearMapLinear.compMultilinearMap f.toMultilinearMap).uncurrySum.mkContinuous ‖f‖ ⋯

@[simp]

theorem ContinuousMultilinearMap.uncurrySum_apply {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {G : Type wG} {G' : Type wG'} [Fintype ι] [Fintype ι'] [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : ContinuousMultilinearMap 𝕜 (fun (x : ι) => G) (ContinuousMultilinearMap 𝕜 (fun (x : ι') => G) G')) (m : ι ⊕ ι' → G) : f.uncurrySum m = (f (m ∘ Sum.inl)) (m ∘ Sum.inr)

noncomputable def ContinuousMultilinearMap.currySumEquiv (𝕜 : Type u) (ι : Type v) (ι' : Type v') (G : Type wG) (G' : Type wG') [Fintype ι] [Fintype ι'] [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] : ContinuousMultilinearMap 𝕜 (fun (x : ι ⊕ ι') => G) G' ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) => G) (ContinuousMultilinearMap 𝕜 (fun (x : ι') => G) G')

Linear isometric equivalence between the space of continuous multilinear maps with variables indexed by ι ⊕ ι' and the space of continuous multilinear maps with variables indexed by ι taking values in the space of continuous multilinear maps with variables indexed by ι'.

The forward and inverse functions are ContinuousMultilinearMap.currySum and ContinuousMultilinearMap.uncurrySum. Use this definition only if you need some properties of LinearIsometryEquiv.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ContinuousMultilinearMap.curryFinFinset (𝕜 : Type u) (G : Type wG) (G' : Type wG') [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] {k : ℕ} {l : ℕ} {n : ℕ} {s : Finset (Fin n)} (hk : s.card = k) (hl : sᶜ.card = l) : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => G) G' ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin k) => G) (ContinuousMultilinearMap 𝕜 (fun (i : Fin l) => G) G')

If s : Finset (Fin n) is a finite set of cardinality k and its complement has cardinality l, then the space of continuous multilinear maps G [×n]→L[𝕜] G' of n variables is isomorphic to the space of continuous multilinear maps G [×k]→L[𝕜] G [×l]→L[𝕜] G' of k variables taking values in the space of continuous multilinear maps of l variables.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousMultilinearMap.curryFinFinset_apply {𝕜 : Type u} {n : ℕ} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] {k : ℕ} {l : ℕ} {s : Finset (Fin n)} (hk : s.card = k) (hl : sᶜ.card = l) (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => G) G') (mk : Fin k → G) (ml : Fin l → G) : (((ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl) f) mk) ml = f fun (i : Fin n) => Sum.elim mk ml ((finSumEquivOfFinset hk hl).symm i)

@[simp]

theorem ContinuousMultilinearMap.curryFinFinset_symm_apply {𝕜 : Type u} {n : ℕ} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] {k : ℕ} {l : ℕ} {s : Finset (Fin n)} (hk : s.card = k) (hl : sᶜ.card = l) (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin k) => G) (ContinuousMultilinearMap 𝕜 (fun (i : Fin l) => G) G')) (m : Fin n → G) : ((ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl).symm f) m = (f fun (i : Fin k) => m ((finSumEquivOfFinset hk hl) (Sum.inl i))) fun (i : Fin l) => m ((finSumEquivOfFinset hk hl) (Sum.inr i))

theorem ContinuousMultilinearMap.curryFinFinset_symm_apply_piecewise_const {𝕜 : Type u} {n : ℕ} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] {k : ℕ} {l : ℕ} {s : Finset (Fin n)} (hk : s.card = k) (hl : sᶜ.card = l) (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin k) => G) (ContinuousMultilinearMap 𝕜 (fun (i : Fin l) => G) G')) (x : G) (y : G) : ((ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl).symm f) (s.piecewise (fun (x_1 : Fin n) => x) fun (x : Fin n) => y) = (f fun (x_1 : Fin k) => x) fun (x : Fin l) => y

@[simp]

theorem ContinuousMultilinearMap.curryFinFinset_symm_apply_const {𝕜 : Type u} {n : ℕ} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] {k : ℕ} {l : ℕ} {s : Finset (Fin n)} (hk : s.card = k) (hl : sᶜ.card = l) (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin k) => G) (ContinuousMultilinearMap 𝕜 (fun (i : Fin l) => G) G')) (x : G) : (((ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl).symm f) fun (x_1 : Fin n) => x) = (f fun (x_1 : Fin k) => x) fun (x_1 : Fin l) => x

theorem ContinuousMultilinearMap.curryFinFinset_apply_const {𝕜 : Type u} {n : ℕ} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] {k : ℕ} {l : ℕ} {s : Finset (Fin n)} (hk : s.card = k) (hl : sᶜ.card = l) (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => G) G') (x : G) (y : G) : ((((ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl) f) fun (x_1 : Fin k) => x) fun (x : Fin l) => y) = f (s.piecewise (fun (x_1 : Fin n) => x) fun (x : Fin n) => y)

noncomputable def ContinuousLinearMap.continuousMultilinearMapOption {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) : ContinuousMultilinearMap 𝕜 (fun (x : Option ι) => G × ((i : ι) → E i)) F

Given a linear map into continuous multilinear maps B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F, one can not always uncurry it as G and E might live in a different universe. However, one can always lift it to a continuous multilinear map on (G × (Π i, E i)) ^ (1 + n), which maps (v_0, ..., v_n) to B (g_0) (u_1, ..., u_n) where g_0 is the G-coordinate of v_0 and u_i is the E_i coordinate of v_i.

Equations

• One or more equations did not get rendered due to their size.

theorem ContinuousLinearMap.continuousMultilinearMapOption_apply_eq_self {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) (a : G) (v : (i : ι) → E i) : (B.continuousMultilinearMapOption fun (x : Option ι) => (a, v)) = (B a) v