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:

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) :
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)) :

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) :

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β€– β‹―
Instances For
    @[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β€– β‹―
    Instances For
      @[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] :
      (Ei 0 β†’L[π•œ] ContinuousMultilinearMap π•œ (fun (i : Fin n) => Ei i.succ) 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
        @[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 : Ei 0 β†’L[π•œ] ContinuousMultilinearMap π•œ (fun (i : Fin n) => Ei i.succ) G) (v : (i : Fin n.succ) β†’ Ei i) :
        ((continuousMultilinearCurryLeftEquiv π•œ Ei G) f) v = (f (v 0)) (Fin.tail 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 : ContinuousMultilinearMap π•œ Ei G) (x : Ei 0) (v : (i : Fin n) β†’ Ei i.succ) :
        (((continuousMultilinearCurryLeftEquiv π•œ Ei G).symm f) x) v = f (Fin.cons x 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) :
        @[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) :

        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)) :

        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 = let f' := { toFun := fun (m : (i : Fin n) β†’ Ei i.castSucc) => ↑(f m), map_add' := β‹―, map_smul' := β‹― }; f'.uncurryRight.mkContinuous β€–fβ€– β‹―
        Instances For
          @[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
          • One or more equations did not get rendered due to their size.
          Instances For
            @[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 π•œ (fun (i : Fin n) => Ei i.castSucc) (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
              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 n.succ) => 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
                @[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 π•œ (fun (i : Fin n) => Ei i.castSucc) (Ei (Fin.last n) β†’L[π•œ] G)) (v : (i : Fin n.succ) β†’ Ei i) :
                ((continuousMultilinearCurryRightEquiv π•œ Ei G) f) v = (f (Fin.init v)) (v (Fin.last n))
                @[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 π•œ Ei G) (v : (i : Fin n) β†’ Ei i.castSucc) (x : Ei (Fin.last n)) :
                (((continuousMultilinearCurryRightEquiv π•œ Ei G).symm f) v) x = f (Fin.snoc v x)
                @[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))
                @[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.succ) => G) G') (v : Fin n β†’ G) (x : G) :
                (((continuousMultilinearCurryRightEquiv' π•œ n G G').symm f) v) x = f (Fin.snoc v x)
                @[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) :
                @[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.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
                • f.uncurry0 = f 0
                Instances For
                  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
                    @[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) :
                    @[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') :
                    f.uncurry0 = f 0
                    @[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} :
                    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 f.uncurry0 = 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.curry0 π•œ G x).uncurry0 = x
                    @[simp]
                    theorem ContinuousMultilinearMap.curry0_norm (π•œ : Type u) (G : Type wG) {G' : Type wG'} [NontriviallyNormedField π•œ] [NormedAddCommGroup G] [NormedSpace π•œ G] [NormedAddCommGroup G'] [NormedSpace π•œ G'] (x : G') :
                    @[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} :
                    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') :
                    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
                      @[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
                      Instances For
                        @[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') :
                        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
                          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β€– β‹―
                          Instances For
                            @[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β€– β‹―
                            Instances For
                              @[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.
                              Instances For
                                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
                                  @[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)