doc-next-gen

Mathlib.Analysis.NormedSpace.Multilinear.Curry

Module docstring

{"# 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 π•œ. ","#### Left currying ","#### Right currying ","#### 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. ","#### With 1 variable "}

ContinuousLinearMap.norm_map_tail_le theorem
(f : Ei 0 β†’L[π•œ] ContinuousMultilinearMap π•œ (fun i : Fin n => Ei i.succ) G) (m : βˆ€ i, Ei i) : β€–f (m 0) (tail m)β€– ≀ β€–fβ€– * ∏ i, β€–m iβ€–
Full source 
theorem ContinuousLinearMap.norm_map_tail_le
    (f : Ei 0 β†’L[π•œ] ContinuousMultilinearMap π•œ (fun i : Fin n => Ei i.succ) G) (m : βˆ€ i, Ei i) :
    β€–f (m 0) (tail m)β€– ≀ β€–fβ€– * ∏ i, β€–m iβ€– :=
  calc
    β€–f (m 0) (tail m)β€– ≀ β€–f (m 0)β€– * ∏ i, β€–(tail m) iβ€– := (f (m 0)).le_opNorm _
    _ ≀ β€–fβ€– * β€–m 0β€– * ∏ i, β€–tail m iβ€– := mul_le_mul_of_nonneg_right (f.le_opNorm _) <| by positivity
    _ = β€–fβ€– * (β€–m 0β€– * ∏ i, β€–(tail m) iβ€–) := by ring
    _ = β€–fβ€– * ∏ i, β€–m iβ€– := by
      rw [prod_univ_succ]
      rfl
Norm Inequality for Tail of Continuous Multilinear Map under Linear Map Application
Informal description
Let $\mathbb{K}$ be a nontrivially normed field, $n$ a natural number, and $(E_i)_{i \in \text{Fin}(n+1)}$ a family of normed vector spaces over $\mathbb{K}$. For any continuous linear map $f \colon E_0 \to \text{ContinuousMultilinearMap}_{\mathbb{K}}((E_i)_{i \in \text{Fin}(n)}, G)$ and any $m \in \prod_{i \in \text{Fin}(n+1)} E_i$, we have the inequality: \[ \|f(m_0)(\text{tail } m)\| \leq \|f\| \cdot \prod_{i \in \text{Fin}(n+1)} \|m_i\|, \] where $\text{tail } m$ denotes the restriction of $m$ to $\text{Fin}(n)$ (omitting the first component).
ContinuousMultilinearMap.norm_map_init_le theorem
(f : ContinuousMultilinearMap π•œ (fun i : Fin n => Ei <| castSucc i) (Ei (last n) β†’L[π•œ] G)) (m : βˆ€ i, Ei i) : β€–f (init m) (m (last n))β€– ≀ β€–fβ€– * ∏ i, β€–m iβ€–
Full source 
theorem ContinuousMultilinearMap.norm_map_init_le
    (f : ContinuousMultilinearMap π•œ (fun i : Fin n => Ei <| castSucc i) (Ei (last n) β†’L[π•œ] G))
    (m : βˆ€ i, Ei i) : β€–f (init m) (m (last n))β€– ≀ β€–fβ€– * ∏ i, β€–m iβ€– :=
  calc
    β€–f (init m) (m (last n))β€– ≀ β€–f (init m)β€– * β€–m (last n)β€– := (f (init m)).le_opNorm _
    _ ≀ (β€–fβ€– * ∏ i, β€–(init m) iβ€–) * β€–m (last n)β€– :=
      (mul_le_mul_of_nonneg_right (f.le_opNorm _) (norm_nonneg _))
    _ = β€–fβ€– * ((∏ i, β€–(init m) iβ€–) * β€–m (last n)β€–) := mul_assoc _ _ _
    _ = β€–fβ€– * ∏ i, β€–m iβ€– := by
      rw [prod_univ_castSucc]
      rfl
Norm Inequality for Initial Segment of Continuous Multilinear Map with Linear Map Application
Informal description
Let $f$ be a continuous multilinear map from the family of normed vector spaces $(E_i)_{i \in \text{Fin } n}$ to the space of continuous linear maps from $E_{\text{last } n}$ to $G$, where $\mathbb{K}$ is a nontrivially normed field. For any $m \in \prod_{i \in \text{Fin } (n+1)} E_i$, the following inequality holds: \[ \|f(\text{init } m)(m_{\text{last } n})\| \leq \|f\| \cdot \prod_{i \in \text{Fin } (n+1)} \|m_i\|, \] where $\text{init } m$ denotes the restriction of $m$ to $\text{Fin } n$.
ContinuousMultilinearMap.norm_map_cons_le theorem
(f : ContinuousMultilinearMap π•œ Ei G) (x : Ei 0) (m : βˆ€ i : Fin n, Ei i.succ) : β€–f (cons x m)β€– ≀ β€–fβ€– * β€–xβ€– * ∏ i, β€–m iβ€–
Full source 
theorem ContinuousMultilinearMap.norm_map_cons_le (f : ContinuousMultilinearMap π•œ Ei G) (x : Ei 0)
    (m : βˆ€ i : Fin n, Ei i.succ) : β€–f (cons x m)β€– ≀ β€–fβ€– * β€–xβ€– * ∏ i, β€–m iβ€– :=
  calc
    β€–f (cons x m)β€– ≀ β€–fβ€– * ∏ i, β€–cons x m iβ€– := f.le_opNorm _
    _ = β€–fβ€– * β€–xβ€– * ∏ i, β€–m iβ€– := by
      rw [prod_univ_succ]
      simp [mul_assoc]
Norm Inequality for Continuous Multilinear Maps with Prepended Argument
Informal description
For any continuous multilinear map $f$ from a family of normed vector spaces $(E_i)_{i \in \text{Fin}(n+1)}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, any element $x \in E_0$, and any family of vectors $m \in \prod_{i=1}^n E_i$, the following inequality holds: \[ \|f(x, m)\| \leq \|f\| \cdot \|x\| \cdot \prod_{i=1}^n \|m_i\|. \] Here $(x, m)$ denotes the vector in $\prod_{i=0}^n E_i$ obtained by prepending $x$ to $m$.
ContinuousMultilinearMap.norm_map_snoc_le theorem
(f : ContinuousMultilinearMap π•œ Ei G) (m : βˆ€ i : Fin n, Ei <| castSucc i) (x : Ei (last n)) : β€–f (snoc m x)β€– ≀ (β€–fβ€– * ∏ i, β€–m iβ€–) * β€–xβ€–
Full source 
theorem ContinuousMultilinearMap.norm_map_snoc_le (f : ContinuousMultilinearMap π•œ Ei G)
    (m : βˆ€ i : Fin n, Ei <| castSucc i) (x : Ei (last n)) :
    β€–f (snoc m x)β€– ≀ (β€–fβ€– * ∏ i, β€–m iβ€–) * β€–xβ€– :=
  calc
    β€–f (snoc m x)β€– ≀ β€–fβ€– * ∏ i, β€–snoc m x iβ€– := f.le_opNorm _
    _ = (β€–fβ€– * ∏ i, β€–m iβ€–) * β€–xβ€– := by
      rw [prod_univ_castSucc]
      simp [mul_assoc]
Norm Inequality for Snoc-Extended Continuous Multilinear Maps
Informal description
Let $f$ be a continuous multilinear map from a family of normed vector spaces $(E_i)_{i \in \text{Fin } n}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$. For any $m \in \prod_{i \in \text{Fin } n} E_i$ and any $x \in E_{\text{last } n}$, the following inequality holds: \[ \|f(\text{snoc } m \ x)\| \leq \left(\|f\| \cdot \prod_{i \in \text{Fin } n} \|m_i\|\right) \cdot \|x\|, \] where $\text{snoc } m \ x$ denotes the extension of the tuple $m$ by appending $x$ at the end.
ContinuousLinearMap.uncurryLeft_apply theorem
(f : Ei 0 β†’L[π•œ] ContinuousMultilinearMap π•œ (fun i : Fin n => Ei i.succ) G) (m : βˆ€ i, Ei i) : f.uncurryLeft m = f (m 0) (tail m)
Full source 
@[simp]
theorem ContinuousLinearMap.uncurryLeft_apply
    (f : Ei 0 β†’L[π•œ] ContinuousMultilinearMap π•œ (fun i : Fin n => Ei i.succ) G) (m : βˆ€ i, Ei i) :
    f.uncurryLeft m = f (m 0) (tail m) :=
  rfl
Uncurrying Formula for Continuous Linear Maps of Multilinear Maps
Informal description
Let $f$ be a continuous linear map from $E_0$ to the space of continuous multilinear maps from $\prod_{i=1}^n E_i$ to $G$, where $E_i$ are normed vector spaces over a nontrivially normed field $\mathbb{K}$. For any tuple $m \in \prod_{i=0}^n E_i$, the uncurried version of $f$ satisfies: \[ f.\text{uncurryLeft}(m) = f(m_0)(\text{tail}(m)), \] where $\text{tail}(m)$ denotes the tuple obtained by removing the first element $m_0$ from $m$.
ContinuousMultilinearMap.curryLeft_apply theorem
(f : ContinuousMultilinearMap π•œ Ei G) (x : Ei 0) (m : βˆ€ i : Fin n, Ei i.succ) : f.curryLeft x m = f (cons x m)
Full source 
@[simp]
theorem ContinuousMultilinearMap.curryLeft_apply (f : ContinuousMultilinearMap π•œ Ei G) (x : Ei 0)
    (m : βˆ€ i : Fin n, Ei i.succ) : f.curryLeft x m = f (cons x m) :=
  rfl
Left Currying Formula for Continuous Multilinear Maps
Informal description
Let $f$ be a continuous multilinear map from a family of normed vector spaces $(E_i)_{i \in \text{Fin}(n+1)}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$. For any $x \in E_0$ and any tuple $m \in \prod_{i=1}^n E_i$, the left-curried version of $f$ satisfies: \[ f.\text{curryLeft}(x)(m) = f(\text{cons}(x, m)), \] where $\text{cons}(x, m)$ denotes the tuple obtained by prepending $x$ to $m$.
ContinuousLinearMap.curry_uncurryLeft theorem
(f : Ei 0 β†’L[π•œ] ContinuousMultilinearMap π•œ (fun i : Fin n => Ei i.succ) G) : f.uncurryLeft.curryLeft = f
Full source 
@[simp]
theorem ContinuousLinearMap.curry_uncurryLeft
    (f : Ei 0 β†’L[π•œ] ContinuousMultilinearMap π•œ (fun i : Fin n => Ei i.succ) G) :
    f.uncurryLeft.curryLeft = f := by
  ext m x
  rw [ContinuousMultilinearMap.curryLeft_apply, ContinuousLinearMap.uncurryLeft_apply, tail_cons,
    cons_zero]
Left Currying and Uncurrying are Inverse Operations for Continuous Linear Maps of Multilinear Maps
Informal description
Let $f$ be a continuous linear map from $E_0$ to the space of continuous multilinear maps from $\prod_{i=1}^n E_i$ to $G$, where $E_i$ are normed vector spaces over a nontrivially normed field $\mathbb{K}$. Then the left-currying of the left-uncurried version of $f$ recovers $f$ itself, i.e., \[ f.\text{uncurryLeft}.\text{curryLeft} = f. \]
ContinuousMultilinearMap.uncurry_curryLeft theorem
(f : ContinuousMultilinearMap π•œ Ei G) : f.curryLeft.uncurryLeft = f
Full source 
@[simp]
theorem ContinuousMultilinearMap.uncurry_curryLeft (f : ContinuousMultilinearMap π•œ Ei G) :
    f.curryLeft.uncurryLeft = f :=
  ContinuousMultilinearMap.toMultilinearMap_injective <| f.toMultilinearMap.uncurry_curryLeft
Left Uncurrying Recovers Original Continuous Multilinear Map
Informal description
Let $f$ be a continuous multilinear map from a family of normed vector spaces $(E_i)_{i \in \text{Fin}(n+1)}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$. Then the left-uncurrying of the left-curried version of $f$ recovers $f$ itself, i.e., \[ f.\text{curryLeft}.\text{uncurryLeft} = f. \]
continuousMultilinearCurryLeftEquiv_apply theorem
(f : ContinuousMultilinearMap π•œ Ei G) (x : Ei 0) (v : Ξ  i : Fin n, Ei i.succ) : continuousMultilinearCurryLeftEquiv π•œ Ei G f x v = f (cons x v)
Full source 
@[simp]
theorem continuousMultilinearCurryLeftEquiv_apply
    (f : ContinuousMultilinearMap π•œ Ei G) (x : Ei 0) (v : Ξ  i : Fin n, Ei i.succ) :
    continuousMultilinearCurryLeftEquiv π•œ Ei G f x v = f (cons x v) :=
  rfl
Evaluation of Left-Curried Continuous Multilinear Map Equals Original Map on Concatenated Input
Informal description
Let $f$ be a continuous multilinear map from a family of normed vector spaces $(E_i)_{i \in \text{Fin}(n+1)}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$. For any $x \in E_0$ and any tuple $v \in \prod_{i=1}^n E_i$, the evaluation of the left-curried version of $f$ at $x$ and $v$ equals the evaluation of $f$ at the concatenation of $x$ with $v$, i.e., \[ \text{continuousMultilinearCurryLeftEquiv}_{\mathbb{K}, E_i, G}(f)(x)(v) = f(\text{cons}(x, v)). \]
continuousMultilinearCurryLeftEquiv_symm_apply theorem
(f : Ei 0 β†’L[π•œ] ContinuousMultilinearMap π•œ (fun i : Fin n => Ei i.succ) G) (v : Ξ  i, Ei i) : (continuousMultilinearCurryLeftEquiv π•œ Ei G).symm f v = f (v 0) (tail v)
Full source 
@[simp]
theorem continuousMultilinearCurryLeftEquiv_symm_apply
    (f : Ei 0 β†’L[π•œ] ContinuousMultilinearMap π•œ (fun i : Fin n => Ei i.succ) G) (v : Ξ  i, Ei i) :
    (continuousMultilinearCurryLeftEquiv π•œ Ei G).symm f v = f (v 0) (tail v) :=
  rfl
Inverse of Left-Currying Equivalence for Continuous Multilinear Maps
Informal description
Let $\mathbb{K}$ be a nontrivially normed field, and let $(E_i)_{i \in \text{Fin}(n+1)}$ be a family of normed vector spaces over $\mathbb{K}$. For any continuous linear map $f$ from $E_0$ to the space of continuous multilinear maps from $(E_{i+1})_{i \in \text{Fin}(n)}$ to a normed vector space $G$, and for any vector $v$ in the product space $\prod_{i} E_i$, the inverse of the left-currying equivalence evaluated at $f$ and $v$ satisfies \[ (\text{continuousMultilinearCurryLeftEquiv}_{\mathbb{K}, E, G})^{-1}(f)(v) = f(v_0)(\text{tail}(v)), \] where $\text{tail}(v)$ denotes the vector $(v_{i+1})_{i \in \text{Fin}(n)}$.
ContinuousMultilinearMap.curryLeft_norm theorem
(f : ContinuousMultilinearMap π•œ Ei G) : β€–f.curryLeftβ€– = β€–fβ€–
Full source 
@[simp]
theorem ContinuousMultilinearMap.curryLeft_norm (f : ContinuousMultilinearMap π•œ Ei G) :
    β€–f.curryLeftβ€– = β€–fβ€– :=
  (continuousMultilinearCurryLeftEquiv π•œ Ei G).norm_map f
Norm Preservation under Left Currying of Continuous Multilinear Maps
Informal description
For any continuous multilinear map $f$ from a family of normed vector spaces $(E_i)_{i \in \text{Fin}(n+1)}$ over a nontrivially normed field $\mathbb{K}$ to a normed vector space $G$, the operator norm of the left-curried version of $f$ is equal to the operator norm of $f$ itself. That is, $\|f.\text{curryLeft}\| = \|f\|$.
ContinuousLinearMap.uncurryLeft_norm theorem
(f : Ei 0 β†’L[π•œ] ContinuousMultilinearMap π•œ (fun i : Fin n => Ei i.succ) G) : β€–f.uncurryLeftβ€– = β€–fβ€–
Full source 
@[simp]
theorem ContinuousLinearMap.uncurryLeft_norm
    (f : Ei 0 β†’L[π•œ] ContinuousMultilinearMap π•œ (fun i : Fin n => Ei i.succ) G) :
    β€–f.uncurryLeftβ€– = β€–fβ€– :=
  (continuousMultilinearCurryLeftEquiv π•œ Ei G).symm.norm_map f
Norm Preservation in Left Uncurrying of Continuous Linear Maps
Informal description
Let $π•œ$ be a nontrivially normed field, $n$ a natural number, $E_i$ a family of normed vector spaces over $π•œ$ indexed by $i \in \text{Fin}(n+1)$, and $G$ a normed vector space over $π•œ$. For any continuous linear map $f$ from $E_0$ to the space of continuous multilinear maps from $\prod_{i=1}^n E_i$ to $G$, the operator norm of the uncurried version of $f$ equals the operator norm of $f$. In mathematical notation: $$\|f.\text{uncurryLeft}\| = \|f\|$$
ContinuousMultilinearMap.uncurryRight_apply theorem
(f : ContinuousMultilinearMap π•œ (fun i : Fin n => Ei <| castSucc i) (Ei (last n) β†’L[π•œ] G)) (m : βˆ€ i, Ei i) : f.uncurryRight m = f (init m) (m (last n))
Full source 
@[simp]
theorem ContinuousMultilinearMap.uncurryRight_apply
    (f : ContinuousMultilinearMap π•œ (fun i : Fin n => Ei <| castSucc i) (Ei (last n) β†’L[π•œ] G))
    (m : βˆ€ i, Ei i) : f.uncurryRight m = f (init m) (m (last n)) :=
  rfl
Evaluation of Uncurried Right Continuous Multilinear Map
Informal description
Let $π•œ$ be a nontrivially normed field, $n$ a natural number, $E_i$ a family of normed vector spaces over $π•œ$ indexed by $i \in \text{Fin}(n+1)$, and $G$ a normed vector space over $π•œ$. For any continuous multilinear map $f$ from $\prod_{i=0}^{n-1} E_{\text{castSucc}(i)}$ to the space of continuous linear maps from $E_{\text{last}(n)}$ to $G$, and for any family of vectors $m = (m_i)_{i \in \text{Fin}(n+1)}$ where $m_i \in E_i$, the uncurried version of $f$ evaluated at $m$ equals $f$ evaluated at the initial segment of $m$ (i.e., $(m_i)_{i \in \text{Fin}(n)}$) applied to the last component $m_{\text{last}(n)}$. In mathematical notation: $$f.\text{uncurryRight}(m) = f(\text{init}(m))(m_{\text{last}(n)})$$ where $\text{init}(m)$ denotes the vector in $\prod_{i=0}^{n-1} E_{\text{castSucc}(i)}$ obtained by omitting the last component of $m$.
ContinuousMultilinearMap.curryRight_apply theorem
(f : ContinuousMultilinearMap π•œ Ei G) (m : βˆ€ i : Fin n, Ei <| castSucc i) (x : Ei (last n)) : f.curryRight m x = f (snoc m x)
Full source 
@[simp]
theorem ContinuousMultilinearMap.curryRight_apply (f : ContinuousMultilinearMap π•œ Ei G)
    (m : βˆ€ i : Fin n, Ei <| castSucc i) (x : Ei (last n)) : f.curryRight m x = f (snoc m x) :=
  rfl
Evaluation of Right-Curried Continuous Multilinear Map
Informal description
Let $π•œ$ be a nontrivially normed field, $n$ a natural number, $E_i$ a family of normed vector spaces over $π•œ$ indexed by $i \in \text{Fin}(n+1)$, and $G$ a normed vector space over $π•œ$. For any continuous multilinear map $f$ from $\prod_{i=0}^n E_i$ to $G$, and for any family of vectors $m = (m_i)_{i \in \text{Fin}(n)}$ where $m_i \in E_{\text{castSucc}(i)}$, and any vector $x \in E_{\text{last}(n)}$, the right-curried version of $f$ evaluated at $m$ and $x$ equals $f$ evaluated at the vector obtained by appending $x$ to $m$. In mathematical notation: $$f.\text{curryRight}(m)(x) = f(\text{snoc}(m, x))$$ where $\text{snoc}(m, x)$ denotes the vector in $\prod_{i=0}^n E_i$ obtained by extending $m$ with $x$ at the last position.
ContinuousMultilinearMap.curry_uncurryRight theorem
(f : ContinuousMultilinearMap π•œ (fun i : Fin n => Ei <| castSucc i) (Ei (last n) β†’L[π•œ] G)) : f.uncurryRight.curryRight = f
Full source 
@[simp]
theorem ContinuousMultilinearMap.curry_uncurryRight
    (f : ContinuousMultilinearMap π•œ (fun i : Fin n => Ei <| castSucc i) (Ei (last n) β†’L[π•œ] G)) :
    f.uncurryRight.curryRight = f := by
  ext m x
  rw [ContinuousMultilinearMap.curryRight_apply, ContinuousMultilinearMap.uncurryRight_apply,
    snoc_last, init_snoc]
Right Curry-Uncurry Invariance for Continuous Multilinear Maps
Informal description
Let $π•œ$ be a nontrivially normed field, $n$ a natural number, $E_i$ a family of normed vector spaces over $π•œ$ indexed by $i \in \text{Fin}(n+1)$, and $G$ a normed vector space over $π•œ$. For any continuous multilinear map $f$ from $\prod_{i=0}^{n-1} E_{\text{castSucc}(i)}$ to the space of continuous linear maps from $E_{\text{last}(n)}$ to $G$, the right-curried version of the uncurried version of $f$ equals $f$ itself. In mathematical notation: $$(f.\text{uncurryRight}).\text{curryRight} = f$$
ContinuousMultilinearMap.uncurry_curryRight theorem
(f : ContinuousMultilinearMap π•œ Ei G) : f.curryRight.uncurryRight = f
Full source 
@[simp]
theorem ContinuousMultilinearMap.uncurry_curryRight (f : ContinuousMultilinearMap π•œ Ei G) :
    f.curryRight.uncurryRight = f := by
  ext m
  rw [uncurryRight_apply, curryRight_apply, snoc_init_self]
Right Currying and Uncurrying are Inverse Operations for Continuous Multilinear Maps
Informal description
Let $π•œ$ be a nontrivially normed field, $n$ a natural number, $E_i$ a family of normed vector spaces over $π•œ$ indexed by $i \in \text{Fin}(n+1)$, and $G$ a normed vector space over $π•œ$. For any continuous multilinear map $f$ from $\prod_{i=0}^n E_i$ to $G$, the uncurried version of the right-curried $f$ equals $f$ itself. In mathematical notation: $$\text{uncurryRight}(\text{curryRight}(f)) = f$$
continuousMultilinearCurryRightEquiv_apply theorem
(f : ContinuousMultilinearMap π•œ Ei G) (v : Ξ  i : Fin n, Ei <| castSucc i) (x : Ei (last n)) : continuousMultilinearCurryRightEquiv π•œ Ei G f v x = f (snoc v x)
Full source 
@[simp]
theorem continuousMultilinearCurryRightEquiv_apply
    (f : ContinuousMultilinearMap π•œ Ei G) (v : Ξ  i : Fin n, Ei <| castSucc i) (x : Ei (last n)) :
    continuousMultilinearCurryRightEquiv π•œ Ei G f v x = f (snoc v x) :=
  rfl
Evaluation of Right-Curried Continuous Multilinear Map
Informal description
Let $π•œ$ be a nontrivially normed field, $n$ a natural number, $(E_i)_{i \in \text{Fin}(n+1)}$ a family of normed vector spaces over $π•œ$, and $G$ a normed vector space over $π•œ$. For any continuous multilinear map $f : \prod_{i=0}^n E_i \to G$, vector $v \in \prod_{i=0}^{n-1} E_{\text{castSucc}(i)}$, and element $x \in E_{\text{last}(n)}$, the evaluation of the right-curried equivalent of $f$ at $v$ and $x$ equals the evaluation of $f$ at the vector obtained by appending $x$ to $v$. In mathematical notation: $$\text{curryRight}(f)(v)(x) = f(v \snoc x)$$
continuousMultilinearCurryRightEquiv_symm_apply theorem
(f : ContinuousMultilinearMap π•œ (fun i : Fin n => Ei <| castSucc i) (Ei (last n) β†’L[π•œ] G)) (v : Ξ  i, Ei i) : (continuousMultilinearCurryRightEquiv π•œ Ei G).symm f v = f (init v) (v (last n))
Full source 
@[simp]
theorem continuousMultilinearCurryRightEquiv_symm_apply
    (f : ContinuousMultilinearMap π•œ (fun i : Fin n => Ei <| castSucc i) (Ei (last n) β†’L[π•œ] G))
    (v : Ξ  i, Ei i) :
    (continuousMultilinearCurryRightEquiv π•œ Ei G).symm f v = f (init v) (v (last n)) :=
  rfl
Inverse Right-Currying Equivalence for Continuous Multilinear Maps
Informal description
Let $π•œ$ be a nontrivially normed field, $n$ a natural number, $E_i$ a family of normed vector spaces over $π•œ$ indexed by $i \in \text{Fin}(n+1)$, and $G$ a normed vector space over $π•œ$. For any continuous multilinear map $f$ from $\prod_{i=0}^{n-1} E_i$ to the space of continuous linear maps from $E_n$ to $G$, and for any vector $v \in \prod_{i=0}^n E_i$, the inverse of the right-currying equivalence applied to $f$ evaluated at $v$ equals $f$ applied to the initial segment $\text{init}(v)$ evaluated at the last component $v_n$. In mathematical notation: $$(\text{continuousMultilinearCurryRightEquiv}_{π•œ,E_i,G})^{-1}(f)(v) = f(\text{init}(v))(v_n)$$
continuousMultilinearCurryRightEquiv_apply' theorem
(f : G [Γ—n.succ]β†’L[π•œ] G') (v : Fin n β†’ G) (x : G) : continuousMultilinearCurryRightEquiv' π•œ n G G' f v x = f (snoc v x)
Full source 
@[simp]
theorem continuousMultilinearCurryRightEquiv_apply'
    (f : G [Γ—n.succ]β†’L[π•œ] G') (v : Fin n β†’ G) (x : G) :
    continuousMultilinearCurryRightEquiv' π•œ n G G' f v x = f (snoc v x) :=
  rfl
Evaluation of Right-Curried Continuous Multilinear Map on Uniform Spaces
Informal description
Let $\mathbb{K}$ be a nontrivially normed field, $n$ a natural number, and $G$, $G'$ normed vector spaces over $\mathbb{K}$. For any continuous multilinear map $f \colon G^{n+1} \to G'$, vector $v \in G^n$, and element $x \in G$, the evaluation of the right-curried equivalent of $f$ at $v$ and $x$ equals the evaluation of $f$ at the vector obtained by appending $x$ to $v$. In mathematical notation: $$\text{curryRight}(f)(v)(x) = f(v \snoc x)$$
continuousMultilinearCurryRightEquiv_symm_apply' theorem
(f : G [Γ—n]β†’L[π•œ] G β†’L[π•œ] G') (v : Fin (n + 1) β†’ G) : (continuousMultilinearCurryRightEquiv' π•œ n G G').symm f v = f (init v) (v (last n))
Full source 
@[simp]
theorem continuousMultilinearCurryRightEquiv_symm_apply'
    (f : G [Γ—n]β†’L[π•œ] G β†’L[π•œ] G') (v : Fin (n + 1) β†’ G) :
    (continuousMultilinearCurryRightEquiv' π•œ n G G').symm f v = f (init v) (v (last n)) :=
  rfl
Inverse Right-Currying Equivalence for Continuous Multilinear Maps (Special Case)
Informal description
Let $π•œ$ be a nontrivially normed field, $G$ and $G'$ be normed vector spaces over $π•œ$, and $n$ a natural number. For any continuous multilinear map $f$ from $G^n$ to the space of continuous linear maps from $G$ to $G'$, and for any vector $v \in G^{n+1}$, the inverse of the right-currying equivalence applied to $f$ evaluated at $v$ equals $f$ applied to the initial segment $\text{init}(v)$ evaluated at the last component $v_n$. In mathematical notation: $$(\text{continuousMultilinearCurryRightEquiv}'_{π•œ,n,G,G'})^{-1}(f)(v) = f(\text{init}(v))(v_n)$$
ContinuousMultilinearMap.curryRight_norm theorem
(f : ContinuousMultilinearMap π•œ Ei G) : β€–f.curryRightβ€– = β€–fβ€–
Full source 
@[simp]
theorem ContinuousMultilinearMap.curryRight_norm (f : ContinuousMultilinearMap π•œ Ei G) :
    β€–f.curryRightβ€– = β€–fβ€– :=
  (continuousMultilinearCurryRightEquiv π•œ Ei G).norm_map f
Norm Preservation under Right Currying of Continuous Multilinear Maps
Informal description
For any continuous multilinear map $f$ from a family of normed vector spaces $(E_i)_{i \in \text{Fin}\, (n+1)}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, the operator norm of the right-curried version of $f$ equals the operator norm of $f$ itself, i.e., $\|f.\text{curryRight}\| = \|f\|$.
ContinuousMultilinearMap.uncurry0_apply theorem
(x : G') (m : Fin 0 β†’ G) : ContinuousMultilinearMap.uncurry0 π•œ G x m = x
Full source 
@[simp]
theorem ContinuousMultilinearMap.uncurry0_apply (x : G') (m : Fin 0 β†’ G) :
    ContinuousMultilinearMap.uncurry0 π•œ G x m = x :=
  rfl
Evaluation of Zero-Variable Uncurried Continuous Multilinear Map
Informal description
For any element $x$ in a normed vector space $G'$ over a nontrivially normed field $\mathbb{K}$, and for any function $m$ from $\text{Fin}\, 0$ to $G$ (which is necessarily the empty function), the uncurried zero-variable continuous multilinear map $\text{uncurry0}_{\mathbb{K},G}(x)$ evaluated at $m$ equals $x$.
ContinuousMultilinearMap.curry0_apply theorem
(f : G [Γ—0]β†’L[π•œ] G') : f.curry0 = f 0
Full source 
@[simp]
theorem ContinuousMultilinearMap.curry0_apply (f : G [Γ—0]β†’L[π•œ] G') : f.curry0 = f 0 :=
  rfl
Left-Curried Zero-Variable Continuous Multilinear Map Evaluates to Original at Zero
Informal description
For any continuous multilinear map $f$ with zero variables from a normed vector space $G$ to another normed vector space $G'$ over a nontrivially normed field $\mathbb{K}$, the left-curried version $f.\text{curry0}$ is equal to $f$ evaluated at the zero vector.
ContinuousMultilinearMap.apply_zero_uncurry0 theorem
(f : G [Γ—0]β†’L[π•œ] G') {x : Fin 0 β†’ G} : ContinuousMultilinearMap.uncurry0 π•œ G (f x) = f
Full source 
@[simp]
theorem ContinuousMultilinearMap.apply_zero_uncurry0 (f : G [Γ—0]β†’L[π•œ] G') {x : Fin 0 β†’ G} :
    ContinuousMultilinearMap.uncurry0 π•œ G (f x) = f := by
  ext m
  simp [Subsingleton.elim x m]
Uncurrying preserves zero-variable continuous multilinear maps
Informal description
Let $G$ and $G'$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$. For any continuous multilinear map $f : G^{[Γ—0]} β†’_{L[\mathbb{K}]} G'$ (where $G^{[Γ—0]}$ denotes the space of 0-variable maps from $G$) and any $x : \text{Fin}\, 0 β†’ G$ (the empty tuple), the uncurried version of $f(x)$ equals $f$ itself.
ContinuousMultilinearMap.uncurry0_curry0 theorem
(f : G [Γ—0]β†’L[π•œ] G') : ContinuousMultilinearMap.uncurry0 π•œ G f.curry0 = f
Full source 
theorem ContinuousMultilinearMap.uncurry0_curry0 (f : G [Γ—0]β†’L[π•œ] G') :
    ContinuousMultilinearMap.uncurry0 π•œ G f.curry0 = f := by simp
Uncurrying-Currying Identity for Zero-Variable Continuous Multilinear Maps
Informal description
For any continuous multilinear map $f \colon G^{[Γ—0]} \to_{L[\mathbb{K}]} G'$ with zero variables, the uncurried version of its left-curried form equals $f$ itself, i.e., $\text{uncurry0}_{\mathbb{K},G}(f.\text{curry0}) = f$.
ContinuousMultilinearMap.curry0_uncurry0 theorem
(x : G') : (ContinuousMultilinearMap.uncurry0 π•œ G x).curry0 = x
Full source 
theorem ContinuousMultilinearMap.curry0_uncurry0 (x : G') :
    (ContinuousMultilinearMap.uncurry0 π•œ G x).curry0 = x :=
  rfl
Currying-Uncurrying Identity for Zero-Variable Continuous Multilinear Maps
Informal description
For any element $x$ in a normed vector space $G'$ over a nontrivially normed field $\mathbb{K}$, the operation of first uncurrying $x$ to a zero-variable continuous multilinear map and then currying it back yields $x$ itself, i.e., $(\text{uncurry0}_{\mathbb{K},G}(x)).\text{curry0} = x$.
ContinuousMultilinearMap.uncurry0_norm theorem
(x : G') : β€–ContinuousMultilinearMap.uncurry0 π•œ G xβ€– = β€–xβ€–
Full source 
@[simp]
theorem ContinuousMultilinearMap.uncurry0_norm (x : G') :
    β€–ContinuousMultilinearMap.uncurry0 π•œ G xβ€– = β€–xβ€– :=
  norm_constOfIsEmpty _ _ _
Norm Preservation in Uncurrying Zero-Variable Continuous Multilinear Maps
Informal description
For any element $x$ in a normed vector space $G'$ over a nontrivially normed field $\mathbb{K}$, the operator norm of the uncurried zero-variable continuous multilinear map $\text{uncurry0}_{\mathbb{K},G}(x)$ is equal to the norm of $x$, i.e., $\|\text{uncurry0}_{\mathbb{K},G}(x)\| = \|x\|$.
ContinuousMultilinearMap.fin0_apply_norm theorem
(f : G [Γ—0]β†’L[π•œ] G') {x : Fin 0 β†’ G} : β€–f xβ€– = β€–fβ€–
Full source 
@[simp]
theorem ContinuousMultilinearMap.fin0_apply_norm (f : G [Γ—0]β†’L[π•œ] G') {x : Fin 0 β†’ G} :
    β€–f xβ€– = β€–fβ€– := by
  obtain rfl : x = 0 := Subsingleton.elim _ _
  refine le_antisymm (by simpa using f.le_opNorm 0) ?_
  have : β€–ContinuousMultilinearMap.uncurry0 π•œ G f.curry0β€– ≀ β€–f.curry0β€– :=
    ContinuousMultilinearMap.opNorm_le_bound (norm_nonneg _) fun m => by
      simp [-ContinuousMultilinearMap.apply_zero_uncurry0]
  simpa [-Matrix.zero_empty] using this
Norm Equality for Zero-Variable Continuous Multilinear Maps
Informal description
For any continuous multilinear map $f \colon G^{[Γ—0]} \to_{L[\mathbb{K}]} G'$ (where $G^{[Γ—0]}$ denotes the space of 0-variable maps from $G$) and any $x \colon \text{Fin}\, 0 \to G$ (the empty tuple), the norm of $f(x)$ equals the operator norm of $f$, i.e., $\|f(x)\| = \|f\|$.
ContinuousMultilinearMap.curry0_norm theorem
(f : G [Γ—0]β†’L[π•œ] G') : β€–f.curry0β€– = β€–fβ€–
Full source 
theorem ContinuousMultilinearMap.curry0_norm (f : G [Γ—0]β†’L[π•œ] G') : β€–f.curry0β€– = β€–fβ€– := by simp
Norm Preservation under Zero-Variable Currying
Informal description
For any continuous multilinear map $f \colon G^{[Γ—0]} \to_{L[\mathbb{K}]} G'$ (where $G^{[Γ—0]}$ denotes the space of 0-variable maps from $G$), the operator norm of its curried version $f.\text{curry0}$ equals the operator norm of $f$, i.e., $\|f.\text{curry0}\| = \|f\|$.
continuousMultilinearCurryFin0_apply theorem
(f : G [Γ—0]β†’L[π•œ] G') : continuousMultilinearCurryFin0 π•œ G G' f = f 0
Full source 
@[simp]
theorem continuousMultilinearCurryFin0_apply (f : G [Γ—0]β†’L[π•œ] G') :
    continuousMultilinearCurryFin0 π•œ G G' f = f 0 :=
  rfl
Evaluation of Zero-Variable Continuous Multilinear Curry Operation
Informal description
For any continuous multilinear map $f \colon G^{[Γ—0]} \to_{L[\mathbb{K}]} G'$ (where $G^{[Γ—0]}$ denotes the space of 0-variable maps from $G$ to $G'$ over the field $\mathbb{K}$), the continuous multilinear curry operation `continuousMultilinearCurryFin0` evaluated at $f$ equals $f$ evaluated at the zero tuple, i.e., $$\text{continuousMultilinearCurryFin0}_{\mathbb{K},G,G'}(f) = f(0).$$
continuousMultilinearCurryFin0_symm_apply theorem
(x : G') (v : Fin 0 β†’ G) : (continuousMultilinearCurryFin0 π•œ G G').symm x v = x
Full source 
@[simp]
theorem continuousMultilinearCurryFin0_symm_apply (x : G') (v : Fin 0 β†’ G) :
    (continuousMultilinearCurryFin0 π•œ G G').symm x v = x :=
  rfl
Inverse Zero-Variable Curry Operator Evaluation: $(\text{curryFin0}^{-1})(x)(v) = x$
Informal description
For any element $x \in G'$ and any function $v \colon \text{Fin}\,0 \to G$, the inverse of the continuous multilinear curry operator for zero variables, evaluated at $x$ and $v$, returns $x$. That is, $(\text{continuousMultilinearCurryFin0}\,\mathbb{K}\,G\,G')^{-1}(x)(v) = x$.
continuousMultilinearCurryFin1_apply theorem
(f : G [Γ—1]β†’L[π•œ] G') (x : G) : continuousMultilinearCurryFin1 π•œ G G' f x = f (Fin.snoc 0 x)
Full source 
@[simp]
theorem continuousMultilinearCurryFin1_apply (f : G [Γ—1]β†’L[π•œ] G') (x : G) :
    continuousMultilinearCurryFin1 π•œ G G' f x = f (Fin.snoc 0 x) :=
  rfl
Evaluation of One-Variable Continuous Multilinear Curry Operation
Informal description
For any continuous multilinear map $f \colon G^{[Γ—1]} \to_{L[\mathbb{K}]} G'$ (where $G^{[Γ—1]}$ denotes the space of 1-variable maps from $G$ to $G'$ over the field $\mathbb{K}$) and any element $x \in G$, the continuous multilinear curry operation `continuousMultilinearCurryFin1` evaluated at $f$ and $x$ equals $f$ evaluated at the singleton tuple $(x)$. That is, $$\text{continuousMultilinearCurryFin1}_{\mathbb{K},G,G'}(f)(x) = f(x).$$
continuousMultilinearCurryFin1_symm_apply theorem
(f : G β†’L[π•œ] G') (v : Fin 1 β†’ G) : (continuousMultilinearCurryFin1 π•œ G G').symm f v = f (v 0)
Full source 
@[simp]
theorem continuousMultilinearCurryFin1_symm_apply (f : G β†’L[π•œ] G') (v : Fin 1 β†’ G) :
    (continuousMultilinearCurryFin1 π•œ G G').symm f v = f (v 0) :=
  rfl
Inverse One-Variable Curry Operator Evaluation: $(\text{curryFin1}^{-1})(f)(v) = f(v(0))$
Informal description
For any continuous linear map $f \colon G \to G'$ and any vector $v \colon \text{Fin}\,1 \to G$, the inverse of the continuous multilinear curry operator for one variable, evaluated at $f$ and $v$, is equal to $f$ applied to the first (and only) component of $v$, i.e., $(\text{continuousMultilinearCurryFin1}\,\mathbb{K}\,G\,G')^{-1}(f)(v) = f(v(0))$.
ContinuousMultilinearMap.norm_domDomCongr theorem
(Οƒ : ΞΉ ≃ ΞΉ') (f : ContinuousMultilinearMap π•œ (fun _ : ΞΉ => G) G') : β€–domDomCongr Οƒ fβ€– = β€–fβ€–
Full source 
@[simp]
theorem norm_domDomCongr (Οƒ : ΞΉ ≃ ΞΉ') (f : ContinuousMultilinearMap π•œ (fun _ : ΞΉ => G) G') :
    β€–domDomCongr Οƒ fβ€– = β€–fβ€– := by
  simp only [norm_def, LinearEquiv.coe_mk, ← Οƒ.prod_comp,
    (Οƒ.arrowCongr (Equiv.refl G)).surjective.forall, domDomCongr_apply, Equiv.arrowCongr_apply,
    Equiv.coe_refl, id_comp, comp_apply, Equiv.symm_apply_apply, id]
Invariance of Operator Norm under Domain Rearrangement
Informal description
For any linear equivalence $\sigma : \iota \simeq \iota'$ between finite index types and any continuous multilinear map $f$ from $\prod_{i \in \iota} G$ to $G'$, the operator norm of the domain-rearranged map $\text{domDomCongr}_{\sigma} f$ is equal to the operator norm of $f$.
ContinuousMultilinearMap.currySum_apply theorem
(f : ContinuousMultilinearMap π•œ (fun _ : ΞΉ βŠ• ΞΉ' => G) G') (m : ΞΉ β†’ G) (m' : ΞΉ' β†’ G) : f.currySum m m' = f (Sum.elim m m')
Full source 
@[simp]
theorem currySum_apply (f : ContinuousMultilinearMap π•œ (fun _ : ΞΉ βŠ• ΞΉ' => G) G') (m : ΞΉ β†’ G)
    (m' : ΞΉ' β†’ G) : f.currySum m m' = f (Sum.elim m m') :=
  rfl
Curried Sum Evaluation for Continuous Multilinear Maps
Informal description
For any continuous multilinear map $f$ defined on the product space $\prod_{i \in \iota \oplus \iota'} G$ with values in $G'$, and for any vectors $m \in \iota \to G$ and $m' \in \iota' \to G$, the curried sum $f.\text{currySum}$ evaluated at $m$ and $m'$ equals the original map $f$ evaluated at the concatenated vector $\text{Sum.elim}\, m\, m'$.
ContinuousMultilinearMap.uncurrySum_apply theorem
(f : ContinuousMultilinearMap π•œ (fun _ : ΞΉ => G) (ContinuousMultilinearMap π•œ (fun _ : ΞΉ' => G) G')) (m : ΞΉ βŠ• ΞΉ' β†’ G) : f.uncurrySum m = f (m ∘ Sum.inl) (m ∘ Sum.inr)
Full source 
@[simp]
theorem uncurrySum_apply (f : ContinuousMultilinearMap π•œ (fun _ : ΞΉ => G)
    (ContinuousMultilinearMap π•œ (fun _ : ΞΉ' => G) G'))
    (m : ΞΉ βŠ• ΞΉ' β†’ G) : f.uncurrySum m = f (m ∘ Sum.inl) (m ∘ Sum.inr) :=
  rfl
Evaluation of Uncurried Continuous Multilinear Map via Restrictions
Informal description
Let $f$ be a continuous multilinear map from $\prod_{i \in \iota} G$ to the space of continuous multilinear maps from $\prod_{j \in \iota'} G$ to $G'$. For any function $m : \iota \oplus \iota' \to G$, the uncurried version of $f$ evaluated at $m$ equals $f$ applied to the restriction of $m$ to $\iota$ and then to the restriction of $m$ to $\iota'$. In symbols: $$f^{\text{uncurry}}(m) = f(m|_{\iota})(m|_{\iota'})$$ where $m|_{\iota} = m \circ \text{inl}$ and $m|_{\iota'} = m \circ \text{inr}$ are the restrictions of $m$ to $\iota$ and $\iota'$ respectively.
ContinuousMultilinearMap.curryFinFinset_apply theorem
(hk : #s = k) (hl : #sᢜ = l) (f : G [Γ—n]β†’L[π•œ] G') (mk : Fin k β†’ G) (ml : Fin l β†’ G) : curryFinFinset π•œ G G' hk hl f mk ml = f fun i => Sum.elim mk ml ((finSumEquivOfFinset hk hl).symm i)
Full source 
@[simp]
theorem curryFinFinset_apply (hk : #s = k) (hl : #sᢜ = l) (f : G [Γ—n]β†’L[π•œ] G')
    (mk : Fin k β†’ G) (ml : Fin l β†’ G) : curryFinFinset π•œ G G' hk hl f mk ml =
      f fun i => Sum.elim mk ml ((finSumEquivOfFinset hk hl).symm i) :=
  rfl
Evaluation of Curried Continuous Multilinear Map via Finite Set Partition
Informal description
Let $s$ be a finite set with cardinality $k$ and its complement $s^c$ with cardinality $l$. Given a continuous multilinear map $f : G^n \to G'$ over a field $\mathbb{K}$, and vectors $m_k \in G^k$, $m_l \in G^l$, the curried map $\text{curryFinFinset}_{\mathbb{K},G,G'}(h_k, h_l, f)$ evaluated at $m_k$ and $m_l$ equals $f$ applied to the vector obtained by combining $m_k$ and $m_l$ via the inverse of the equivalence $\text{finSumEquivOfFinset}(h_k, h_l)$. In symbols: $$\text{curryFinFinset}_{\mathbb{K},G,G'}(h_k, h_l, f)(m_k, m_l) = f\left(\lambda i.\, \text{Sum.elim}\, m_k\, m_l\, ((\text{finSumEquivOfFinset}\, h_k\, h_l)^{-1}\, i)\right)$$
ContinuousMultilinearMap.curryFinFinset_symm_apply theorem
(hk : #s = k) (hl : #sᢜ = l) (f : G [Γ—k]β†’L[π•œ] G [Γ—l]β†’L[π•œ] G') (m : Fin n β†’ G) : (curryFinFinset π•œ G G' hk hl).symm f m = f (fun i => m <| finSumEquivOfFinset hk hl (Sum.inl i)) fun i => m <| finSumEquivOfFinset hk hl (Sum.inr i)
Full source 
@[simp]
theorem curryFinFinset_symm_apply (hk : #s = k) (hl : #sᢜ = l)
    (f : G [Γ—k]β†’L[π•œ] G [Γ—l]β†’L[π•œ] G') (m : Fin n β†’ G) : (curryFinFinset π•œ G G' hk hl).symm f m =
      f (fun i => m <| finSumEquivOfFinset hk hl (Sum.inl i)) fun i =>
        m <| finSumEquivOfFinset hk hl (Sum.inr i) :=
  rfl
Inverse Currying of Continuous Multilinear Map via Finite Set Partition
Informal description
Let $s$ be a finite set with cardinality $k$ and its complement $s^c$ with cardinality $l$. Given a continuous multilinear map $f : G^k \to (G^l \to G')$ over a field $\mathbb{K}$ and a vector $m \in G^n$, the inverse of the currying map $\text{curryFinFinset}_{\mathbb{K},G,G'}(h_k, h_l)$ evaluated at $f$ and $m$ equals $f$ applied to the restrictions of $m$ to the indices corresponding to $s$ and $s^c$ via the equivalence $\text{finSumEquivOfFinset}(h_k, h_l)$. In symbols: $$(\text{curryFinFinset}_{\mathbb{K},G,G'}(h_k, h_l))^{-1}(f)(m) = f\left(\lambda i.\, m(\text{finSumEquivOfFinset}(h_k, h_l)(\text{inl}(i)))\right)\left(\lambda j.\, m(\text{finSumEquivOfFinset}(h_k, h_l)(\text{inr}(j)))\right)$$
ContinuousMultilinearMap.curryFinFinset_symm_apply_piecewise_const theorem
(hk : #s = k) (hl : #sᢜ = l) (f : G [Γ—k]β†’L[π•œ] G [Γ—l]β†’L[π•œ] G') (x y : G) : (curryFinFinset π•œ G G' hk hl).symm f (s.piecewise (fun _ => x) fun _ => y) = f (fun _ => x) fun _ => y
Full source 
theorem curryFinFinset_symm_apply_piecewise_const (hk : #s = k) (hl : #sᢜ = l)
    (f : G [Γ—k]β†’L[π•œ] G [Γ—l]β†’L[π•œ] G') (x y : G) :
    (curryFinFinset π•œ G G' hk hl).symm f (s.piecewise (fun _ => x) fun _ => y) =
      f (fun _ => x) fun _ => y :=
  MultilinearMap.curryFinFinset_symm_apply_piecewise_const hk hl _ x y
Evaluation of Uncurried Continuous Multilinear Map on Piecewise Constant Function
Informal description
Let $s$ be a finite set with cardinality $k$ and its complement $s^c$ with cardinality $l$. Given a continuous multilinear map $f : G^k \to (G^l \to G')$ over a field $\mathbb{K}$, and vectors $x, y \in G$, the uncurried map $\text{curryFinFinset}_{\mathbb{K},G,G'}(h_k, h_l)^{-1}(f)$ evaluated at the piecewise constant function $\lambda i.\, \text{if } i \in s \text{ then } x \text{ else } y$ equals $f$ applied to the constant functions $\lambda \_.\, x$ and $\lambda \_.\, y$. In symbols: $$\text{curryFinFinset}_{\mathbb{K},G,G'}(h_k, h_l)^{-1}(f)(s.\text{piecewise}\, (\lambda \_.\, x)\, (\lambda \_.\, y)) = f (\lambda \_.\, x) (\lambda \_.\, y)$$
ContinuousMultilinearMap.curryFinFinset_symm_apply_const theorem
(hk : #s = k) (hl : #sᢜ = l) (f : G [Γ—k]β†’L[π•œ] G [Γ—l]β†’L[π•œ] G') (x : G) : ((curryFinFinset π•œ G G' hk hl).symm f fun _ => x) = f (fun _ => x) fun _ => x
Full source 
@[simp]
theorem curryFinFinset_symm_apply_const (hk : #s = k) (hl : #sᢜ = l)
    (f : G [Γ—k]β†’L[π•œ] G [Γ—l]β†’L[π•œ] G') (x : G) :
    ((curryFinFinset π•œ G G' hk hl).symm f fun _ => x) = f (fun _ => x) fun _ => x :=
  rfl
Uncurried Constant Evaluation of Continuous Multilinear Maps
Informal description
Let $s$ be a finite set with cardinality $k$, and let its complement $s^c$ have cardinality $l$. Given a continuous multilinear map $f : G^k \to (G^l \to G')$ over a nontrivially normed field $\mathbb{K}$, and a constant vector $x \in G$, the uncurried version of $f$ evaluated at the constant function $\lambda \_. x$ equals $f$ evaluated at the constant functions $\lambda \_. x$ in both arguments. In other words, $(\text{curryFinFinset}_{\mathbb{K},G,G'}(h_k, h_l))^{-1}(f)(\lambda \_. x) = f(\lambda \_. x)(\lambda \_. x)$.
ContinuousMultilinearMap.curryFinFinset_apply_const theorem
(hk : #s = k) (hl : #sᢜ = l) (f : G [Γ—n]β†’L[π•œ] G') (x y : G) : (curryFinFinset π•œ G G' hk hl f (fun _ => x) fun _ => y) = f (s.piecewise (fun _ => x) fun _ => y)
Full source 
theorem curryFinFinset_apply_const (hk : #s = k) (hl : #sᢜ = l) (f : G [Γ—n]β†’L[π•œ] G')
    (x y : G) : (curryFinFinset π•œ G G' hk hl f (fun _ => x) fun _ => y) =
      f (s.piecewise (fun _ => x) fun _ => y) := by
  refine (curryFinFinset_symm_apply_piecewise_const hk hl _ _ _).symm.trans ?_
  rw [LinearIsometryEquiv.symm_apply_apply]
Evaluation of Curried Continuous Multilinear Map on Constant Functions Equals Piecewise Evaluation
Informal description
Let $s$ be a finite set with cardinality $k$ and its complement $s^c$ with cardinality $l$. Given a continuous multilinear map $f : G^n \to G'$ over a nontrivially normed field $\mathbb{K}$, and vectors $x, y \in G$, the curried map $\text{curryFinFinset}_{\mathbb{K},G,G'}(h_k, h_l)(f)$ evaluated at the constant functions $\lambda \_.\, x$ and $\lambda \_.\, y$ equals $f$ evaluated at the piecewise constant function $\lambda i.\, \text{if } i \in s \text{ then } x \text{ else } y$. In symbols: $$\text{curryFinFinset}_{\mathbb{K},G,G'}(h_k, h_l)(f)(\lambda \_.\, x)(\lambda \_.\, y) = f(s.\text{piecewise}\, (\lambda \_.\, x)\, (\lambda \_.\, y))$$
ContinuousLinearMap.continuousMultilinearMapOption_apply_eq_self theorem
(B : G β†’L[π•œ] ContinuousMultilinearMap π•œ E F) (a : G) (v : Ξ  i, E i) : B.continuousMultilinearMapOption (fun _ ↦ (a, v)) = B a v
Full source 
lemma continuousMultilinearMapOption_apply_eq_self (B : G β†’L[π•œ] ContinuousMultilinearMap π•œ E F)
    (a : G) (v : Ξ  i, E i) : B.continuousMultilinearMapOption (fun _ ↦ (a, v)) = B a v := rfl
Evaluation of Continuous Multilinear Map Option Equals Direct Evaluation
Informal description
Let $B$ be a continuous linear map from a normed vector space $G$ to the space of continuous multilinear maps on a family of normed vector spaces $E$ with values in another normed vector space $F$. Then for any element $a \in G$ and any vector $v$ in the product space $\prod_i E_i$, the evaluation of the continuous multilinear map obtained by applying the `continuousMultilinearMapOption` to $B$ at the constant function $\lambda \_. (a, v)$ is equal to the evaluation of $B(a)$ at $v$.