Documentation

Mathlib.Analysis.NormedSpace.Multilinear.Curry

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 #

Type variables #

We use the following type variables in this file:

source
theorem ContinuousLinearMap.norm_map_tail_le {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : Ei 0 β†’L[π•œ] ContinuousMultilinearMap π•œ (fun (i : Fin n) => Ei (Fin.succ i)) G) (m : (i : Fin (Nat.succ n)) β†’ Ei i) :
β€–(f (m 0)) (Fin.tail m)β€– ≀ β€–fβ€– * Finset.prod Finset.univ fun (i : Fin (Nat.succ n)) => β€–m iβ€–
source
theorem ContinuousMultilinearMap.norm_map_init_le {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : ContinuousMultilinearMap π•œ (fun (i : Fin n) => Ei (Fin.castSucc i)) (Ei (Fin.last n) β†’L[π•œ] G)) (m : (i : Fin (Nat.succ n)) β†’ Ei i) :
β€–(f (Fin.init m)) (m (Fin.last n))β€– ≀ β€–fβ€– * Finset.prod Finset.univ fun (i : Fin (Nat.succ n)) => β€–m iβ€–
source
theorem ContinuousMultilinearMap.norm_map_cons_le {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : ContinuousMultilinearMap π•œ Ei G) (x : Ei 0) (m : (i : Fin n) β†’ Ei (Fin.succ i)) :
β€–f (Fin.cons x m)β€– ≀ β€–fβ€– * β€–xβ€– * Finset.prod Finset.univ fun (i : Fin n) => β€–m iβ€–
source
theorem ContinuousMultilinearMap.norm_map_snoc_le {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : ContinuousMultilinearMap π•œ Ei G) (m : (i : Fin n) β†’ Ei (Fin.castSucc i)) (x : Ei (Fin.last n)) :
β€–f (Fin.snoc m x)β€– ≀ (β€–fβ€– * Finset.prod Finset.univ fun (i : Fin n) => β€–m iβ€–) * β€–xβ€–

Left currying #

source
noncomputable def ContinuousLinearMap.uncurryLeft {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : Ei 0 β†’L[π•œ] ContinuousMultilinearMap π•œ (fun (i : Fin n) => Ei (Fin.succ i)) 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
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem ContinuousLinearMap.uncurryLeft_apply {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : Ei 0 β†’L[π•œ] ContinuousMultilinearMap π•œ (fun (i : Fin n) => Ei (Fin.succ i)) G) (m : (i : Fin (Nat.succ n)) β†’ Ei i) :
    (ContinuousLinearMap.uncurryLeft f) m = (f (m 0)) (Fin.tail m)
    source
    noncomputable def ContinuousMultilinearMap.curryLeft {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : ContinuousMultilinearMap π•œ Ei G) :
    Ei 0 β†’L[π•œ] ContinuousMultilinearMap π•œ (fun (i : Fin n) => Ei (Fin.succ i)) 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
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem ContinuousMultilinearMap.curryLeft_apply {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : ContinuousMultilinearMap π•œ Ei G) (x : Ei 0) (m : (i : Fin n) β†’ Ei (Fin.succ i)) :
      ((ContinuousMultilinearMap.curryLeft f) x) m = f (Fin.cons x m)
      source
      @[simp]
      theorem ContinuousLinearMap.curry_uncurryLeft {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : Ei 0 β†’L[π•œ] ContinuousMultilinearMap π•œ (fun (i : Fin n) => Ei (Fin.succ i)) G) :
      ContinuousMultilinearMap.curryLeft (ContinuousLinearMap.uncurryLeft f) = f
      source
      @[simp]
      theorem ContinuousMultilinearMap.uncurry_curryLeft {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : ContinuousMultilinearMap π•œ Ei G) :
      ContinuousLinearMap.uncurryLeft (ContinuousMultilinearMap.curryLeft f) = f
      source
      noncomputable def continuousMultilinearCurryLeftEquiv (π•œ : Type u) {n : β„•} (Ei : Fin (Nat.succ n) β†’ Type wEi) (G : Type wG) [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] :
      (Ei 0 β†’L[π•œ] ContinuousMultilinearMap π•œ (fun (i : Fin n) => Ei (Fin.succ i)) G) ≃ₗᡒ[π•œ] ContinuousMultilinearMap π•œ Ei 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.uncurryLeft and f.curryLeft. 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.
      Instances For
        source
        @[simp]
        theorem continuousMultilinearCurryLeftEquiv_apply {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : Ei 0 β†’L[π•œ] ContinuousMultilinearMap π•œ (fun (i : Fin n) => Ei (Fin.succ i)) G) (v : (i : Fin (Nat.succ n)) β†’ Ei i) :
        ((continuousMultilinearCurryLeftEquiv π•œ Ei G) f) v = (f (v 0)) (Fin.tail v)
        source
        @[simp]
        theorem continuousMultilinearCurryLeftEquiv_symm_apply {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : ContinuousMultilinearMap π•œ Ei G) (x : Ei 0) (v : (i : Fin n) β†’ Ei (Fin.succ i)) :
        (((LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv π•œ Ei G)) f) x) v = f (Fin.cons x v)
        source
        @[simp]
        theorem ContinuousMultilinearMap.curryLeft_norm {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : ContinuousMultilinearMap π•œ Ei G) :
        β€–ContinuousMultilinearMap.curryLeft fβ€– = β€–fβ€–
        source
        @[simp]
        theorem ContinuousLinearMap.uncurryLeft_norm {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : Ei 0 β†’L[π•œ] ContinuousMultilinearMap π•œ (fun (i : Fin n) => Ei (Fin.succ i)) G) :
        β€–ContinuousLinearMap.uncurryLeft fβ€– = β€–fβ€–

        Right currying #

        source
        noncomputable def ContinuousMultilinearMap.uncurryRight {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : ContinuousMultilinearMap π•œ (fun (i : Fin n) => Ei (Fin.castSucc i)) (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
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem ContinuousMultilinearMap.uncurryRight_apply {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : ContinuousMultilinearMap π•œ (fun (i : Fin n) => Ei (Fin.castSucc i)) (Ei (Fin.last n) β†’L[π•œ] G)) (m : (i : Fin (Nat.succ n)) β†’ Ei i) :
          (ContinuousMultilinearMap.uncurryRight f) m = (f (Fin.init m)) (m (Fin.last n))
          source
          noncomputable def ContinuousMultilinearMap.curryRight {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : ContinuousMultilinearMap π•œ Ei G) :
          ContinuousMultilinearMap π•œ (fun (i : Fin n) => Ei (Fin.castSucc i)) (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
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem ContinuousMultilinearMap.curryRight_apply {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : ContinuousMultilinearMap π•œ Ei G) (m : (i : Fin n) β†’ Ei (Fin.castSucc i)) (x : Ei (Fin.last n)) :
            ((ContinuousMultilinearMap.curryRight f) m) x = f (Fin.snoc m x)
            source
            @[simp]
            theorem ContinuousMultilinearMap.curry_uncurryRight {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : ContinuousMultilinearMap π•œ (fun (i : Fin n) => Ei (Fin.castSucc i)) (Ei (Fin.last n) β†’L[π•œ] G)) :
            ContinuousMultilinearMap.curryRight (ContinuousMultilinearMap.uncurryRight f) = f
            source
            @[simp]
            theorem ContinuousMultilinearMap.uncurry_curryRight {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : ContinuousMultilinearMap π•œ Ei G) :
            ContinuousMultilinearMap.uncurryRight (ContinuousMultilinearMap.curryRight f) = f
            source
            noncomputable def continuousMultilinearCurryRightEquiv (π•œ : Type u) {n : β„•} (Ei : Fin (Nat.succ n) β†’ Type wEi) (G : Type wG) [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] :
            ContinuousMultilinearMap π•œ (fun (i : Fin n) => Ei (Fin.castSucc i)) (Ei (Fin.last n) β†’L[π•œ] G) ≃ₗᡒ[π•œ] ContinuousMultilinearMap π•œ Ei 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.uncurryRight and f.curryRight. 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.
            Instances For
              source
              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) => G) (G β†’L[π•œ] G') ≃ₗᡒ[π•œ] ContinuousMultilinearMap π•œ (fun (i : Fin (Nat.succ n)) => G) 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.uncurryRight and f.curryRight. Use these unless you need the full framework of linear isometric equivs.

              Equations
              Instances For
                source
                @[simp]
                theorem continuousMultilinearCurryRightEquiv_apply {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : ContinuousMultilinearMap π•œ (fun (i : Fin n) => Ei (Fin.castSucc i)) (Ei (Fin.last n) β†’L[π•œ] G)) (v : (i : Fin (Nat.succ n)) β†’ Ei i) :
                ((continuousMultilinearCurryRightEquiv π•œ Ei G) f) v = (f (Fin.init v)) (v (Fin.last n))
                source
                @[simp]
                theorem continuousMultilinearCurryRightEquiv_symm_apply {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : ContinuousMultilinearMap π•œ Ei G) (v : (i : Fin n) β†’ Ei (Fin.castSucc i)) (x : Ei (Fin.last n)) :
                (((LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv π•œ Ei G)) f) v) x = f (Fin.snoc v x)
                source
                @[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) => G) (G β†’L[π•œ] G')) (v : Fin (n + 1) β†’ G) :
                ((continuousMultilinearCurryRightEquiv' π•œ n G G') f) v = (f (Fin.init v)) (v (Fin.last n))
                source
                @[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 (Nat.succ n)) => G) G') (v : Fin n β†’ G) (x : G) :
                (((LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' π•œ n G G')) f) v) x = f (Fin.snoc v x)
                source
                @[simp]
                theorem ContinuousMultilinearMap.curryRight_norm {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : ContinuousMultilinearMap π•œ Ei G) :
                β€–ContinuousMultilinearMap.curryRight fβ€– = β€–fβ€–
                source
                @[simp]
                theorem ContinuousMultilinearMap.uncurryRight_norm {π•œ : Type u} {n : β„•} {Ei : Fin (Nat.succ n) β†’ Type wEi} {G : Type wG} [NontriviallyNormedField π•œ] [(i : Fin (Nat.succ n)) β†’ NormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) β†’ NormedSpace π•œ (Ei i)] [NormedAddCommGroup G] [NormedSpace π•œ G] (f : ContinuousMultilinearMap π•œ (fun (i : Fin n) => Ei (Fin.castSucc i)) (Ei (Fin.last n) β†’L[π•œ] G)) :
                β€–ContinuousMultilinearMap.uncurryRight fβ€– = β€–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.

                source
                noncomputable def ContinuousMultilinearMap.uncurry0 {π•œ : 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
                Instances For
                  source
                  noncomputable def ContinuousMultilinearMap.curry0 (π•œ : 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
                  Instances For
                    source
                    @[simp]
                    theorem ContinuousMultilinearMap.curry0_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.curry0 π•œ G x) m = x
                    source
                    @[simp]
                    theorem ContinuousMultilinearMap.uncurry0_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') :
                    ContinuousMultilinearMap.uncurry0 f = f 0
                    source
                    @[simp]
                    theorem ContinuousMultilinearMap.apply_zero_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') {x : Fin 0 β†’ G} :
                    ContinuousMultilinearMap.curry0 π•œ G (f x) = f
                    source
                    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.curry0 π•œ G (ContinuousMultilinearMap.uncurry0 f) = f
                    source
                    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 (ContinuousMultilinearMap.curry0 π•œ G x) = x
                    source
                    @[simp]
                    theorem ContinuousMultilinearMap.curry0_norm (π•œ : Type u) (G : Type wG) {G' : Type wG'} [NontriviallyNormedField π•œ] [NormedAddCommGroup G] [NormedSpace π•œ G] [NormedAddCommGroup G'] [NormedSpace π•œ G'] (x : G') :
                    β€–ContinuousMultilinearMap.curry0 π•œ G xβ€– = β€–xβ€–
                    source
                    @[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β€–
                    source
                    theorem ContinuousMultilinearMap.uncurry0_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') :
                    β€–ContinuousMultilinearMap.uncurry0 fβ€– = β€–fβ€–
                    source
                    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.
                    Instances For
                      source
                      @[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
                      source
                      @[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) :
                      ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 π•œ G G')) x) v = x

                      With 1 variable #

                      source
                      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
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        @[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)
                        source
                        @[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) :
                        ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 π•œ G G')) f) v = f (v 0)
                        source
                        @[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β€–
                        source
                        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.
                        Instances For
                          source
                          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
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            @[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) :
                            ((ContinuousMultilinearMap.currySum f) m) m' = f (Sum.elim m m')
                            source
                            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
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              @[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) :
                              (ContinuousMultilinearMap.uncurrySum f) m = (f (m ∘ Sum.inl)) (m ∘ Sum.inr)
                              source
                              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.
                              Instances For
                                source
                                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.
                                Instances For
                                  source
                                  @[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)
                                  source
                                  @[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) :
                                  ((LinearIsometryEquiv.symm (ContinuousMultilinearMap.curryFinFinset π•œ G G' hk hl)) 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))
                                  source
                                  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) :
                                  ((LinearIsometryEquiv.symm (ContinuousMultilinearMap.curryFinFinset π•œ G G' hk hl)) f) (Finset.piecewise s (fun (x_1 : Fin n) => x) fun (x : Fin n) => y) = (f fun (x_1 : Fin k) => x) fun (x : Fin l) => y
                                  source
                                  @[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) :
                                  (((LinearIsometryEquiv.symm (ContinuousMultilinearMap.curryFinFinset π•œ G G' hk hl)) f) fun (x_1 : Fin n) => x) = (f fun (x_1 : Fin k) => x) fun (x_1 : Fin l) => x
                                  source
                                  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 (Finset.piecewise s (fun (x_1 : Fin n) => x) fun (x : Fin n) => y)