Mathlib.Topology.Algebra.Module.Multilinear.Basic

ContinuousMultilinearMap structure

(R : Type u) {ι : Type v} (M₁ : ι → Type w₁) (M₂ : Type w₂)
  [Semiring R] [∀ i, AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [∀ i, Module R (M₁ i)] [Module R M₂]
  [∀ i, TopologicalSpace (M₁ i)] [TopologicalSpace M₂] extends MultilinearMap R M₁ M₂

Full source

/-- Continuous multilinear maps over the ring `R`, from `∀ i, M₁ i` to `M₂` where `M₁ i` and `M₂`
are modules over `R` with a topological structure. In applications, there will be compatibility
conditions between the algebraic and the topological structures, but this is not needed for the
definition. -/
structure ContinuousMultilinearMap (R : Type u) {ι : Type v} (M₁ : ι → Type w₁) (M₂ : Type w₂)
  [Semiring R] [∀ i, AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [∀ i, Module R (M₁ i)] [Module R M₂]
  [∀ i, TopologicalSpace (M₁ i)] [TopologicalSpace M₂] extends MultilinearMap R M₁ M₂ where
  cont : Continuous toFun

Continuous multilinear map

Informal description

The structure representing continuous multilinear maps over a ring $R$, from $\prod_{i} M₁ i$ to $M₂$, where each $M₁ i$ and $M₂$ are $R$-modules equipped with a topological structure. These maps are both multilinear and continuous.

term_[×_]→L[_]_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation:25 M " [×" n "]→L[" R "] " M' => ContinuousMultilinearMap R (fun i : Fin n => M) M'

Space of continuous n-multilinear maps

Informal description

The notation `M [×n]→L[R] M'` represents the space of continuous `n`-multilinear maps from `M^n` to `M'`, where `M` and `M'` are modules over the ring `R`. This is a special case of continuous multilinear maps where all arguments have the same type `M`.

ContinuousMultilinearMap.toMultilinearMap_injective theorem

 :
  Function.Injective
    (ContinuousMultilinearMap.toMultilinearMap : ContinuousMultilinearMap R M₁ M₂ → MultilinearMap R M₁ M₂)

Full source

theorem toMultilinearMap_injective :
    Function.Injective
      (ContinuousMultilinearMap.toMultilinearMap :
        ContinuousMultilinearMap R M₁ M₂ → MultilinearMap R M₁ M₂)
  | ⟨f, hf⟩, ⟨g, hg⟩, h => by subst h; rfl

Injectivity of the Continuous-to-Multilinear Map Construction

Informal description

The canonical map from the space of continuous multilinear maps to the space of multilinear maps is injective. That is, if two continuous multilinear maps $f, g \colon \prod_{i} M₁ i \to M₂$ have the same underlying multilinear map, then $f = g$.

ContinuousMultilinearMap.funLike instance

: FunLike (ContinuousMultilinearMap R M₁ M₂) (∀ i, M₁ i) M₂

Full source

instance funLike : FunLike (ContinuousMultilinearMap R M₁ M₂) (∀ i, M₁ i) M₂ where
  coe f := f.toFun
  coe_injective' _ _ h := toMultilinearMap_injective <| MultilinearMap.coe_injective h

Function-Like Structure of Continuous Multilinear Maps

Informal description

The space of continuous multilinear maps from $\prod_{i} M₁ i$ to $M₂$ is a function-like class, where each map can be treated as a function from $\prod_{i} M₁ i$ to $M₂$.

ContinuousMultilinearMap.continuousMapClass instance

: ContinuousMapClass (ContinuousMultilinearMap R M₁ M₂) (∀ i, M₁ i) M₂

Full source

instance continuousMapClass :
    ContinuousMapClass (ContinuousMultilinearMap R M₁ M₂) (∀ i, M₁ i) M₂ where
  map_continuous := ContinuousMultilinearMap.cont

Continuous Multilinear Maps as Continuous Maps

Informal description

The space of continuous multilinear maps from $\prod_{i} M₁ i$ to $M₂$ forms a continuous map class, where each map is continuous with respect to the product topology on $\prod_{i} M₁ i$ and the topology on $M₂$.

ContinuousMultilinearMap.Simps.apply definition

(L₁ : ContinuousMultilinearMap R M₁ M₂) (v : ∀ i, M₁ i) : M₂

Full source

/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
  because it is a composition of multiple projections. -/
def Simps.apply (L₁ : ContinuousMultilinearMap R M₁ M₂) (v : ∀ i, M₁ i) : M₂ :=
  L₁ v

Evaluation of a continuous multilinear map

Informal description

The function application of a continuous multilinear map $L₁$ at a vector $v$ in $\prod_{i} M₁ i$ is an element of $M₂$. This is the evaluation of the continuous multilinear map at the given input vector.

ContinuousMultilinearMap.coe_continuous theorem

: Continuous (f : (∀ i, M₁ i) → M₂)

Full source

@[continuity]
theorem coe_continuous : Continuous (f : (∀ i, M₁ i) → M₂) :=
  f.cont

Continuity of Continuous Multilinear Maps

Informal description

For any continuous multilinear map $f \colon \prod_{i} M₁ i \to M₂$, the function $f$ is continuous with respect to the product topology on $\prod_{i} M₁ i$ and the topology on $M₂$.

ContinuousMultilinearMap.coe_coe theorem

: (f.toMultilinearMap : (∀ i, M₁ i) → M₂) = f

Full source

@[simp]
theorem coe_coe : (f.toMultilinearMap : (∀ i, M₁ i) → M₂) = f :=
  rfl

Equality of Underlying Function and Continuous Multilinear Map

Informal description

For any continuous multilinear map $f$ from $\prod_{i} M₁ i$ to $M₂$, the underlying function of its associated multilinear map $f.\text{toMultilinearMap}$ is equal to $f$ itself. That is, the coercion from the continuous multilinear map to its underlying function coincides with the map $f$.

ContinuousMultilinearMap.ext theorem

{f f' : ContinuousMultilinearMap R M₁ M₂} (H : ∀ x, f x = f' x) : f = f'

Full source

@[ext]
theorem ext {f f' : ContinuousMultilinearMap R M₁ M₂} (H : ∀ x, f x = f' x) : f = f' :=
  DFunLike.ext _ _ H

Extensionality of Continuous Multilinear Maps

Informal description

Let $f$ and $f'$ be continuous multilinear maps from $\prod_{i} M₁ i$ to $M₂$. If $f(x) = f'(x)$ for all $x \in \prod_{i} M₁ i$, then $f = f'$.

ContinuousMultilinearMap.map_update_add theorem

 [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) (x y : M₁ i) : f (update m i (x + y)) = f (update m i x) + f (update m i y)

Full source

@[simp]
theorem map_update_add [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) (x y : M₁ i) :
    f (update m i (x + y)) = f (update m i x) + f (update m i y) :=
  f.map_update_add' m i x y

Additivity of Continuous Multilinear Maps in Each Argument

Informal description

Let $f$ be a continuous multilinear map from $\prod_{i} M₁ i$ to $M₂$, where each $M₁ i$ and $M₂$ are $R$-modules with topological structures. For any element $m \in \prod_{i} M₁ i$, any index $i$, and any elements $x, y \in M₁ i$, we have: \[ f(m[i \mapsto x + y]) = f(m[i \mapsto x]) + f(m[i \mapsto y]) \] where $m[i \mapsto v]$ denotes the function that updates the $i$-th component of $m$ to $v$ while keeping all other components unchanged.

ContinuousMultilinearMap.map_update_smul theorem

[DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) (c : R) (x : M₁ i) : f (update m i (c • x)) = c • f (update m i x)

Full source

@[simp]
theorem map_update_smul [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) (c : R) (x : M₁ i) :
    f (update m i (c • x)) = c • f (update m i x) :=
  f.map_update_smul' m i c x

Linearity of Continuous Multilinear Maps in Each Argument

Informal description

Let $f$ be a continuous multilinear map from $\prod_{i} M₁ i$ to $M₂$, where each $M₁ i$ and $M₂$ are $R$-modules with topological structures. For any element $m \in \prod_{i} M₁ i$, any index $i$, any scalar $c \in R$, and any element $x \in M₁ i$, we have: \[ f(m[i \mapsto c \cdot x]) = c \cdot f(m[i \mapsto x]) \] where $m[i \mapsto v]$ denotes the function that updates the $i$-th component of $m$ to $v$ while keeping all other components unchanged.

ContinuousMultilinearMap.map_coord_zero theorem

{m : ∀ i, M₁ i} (i : ι) (h : m i = 0) : f m = 0

Full source

theorem map_coord_zero {m : ∀ i, M₁ i} (i : ι) (h : m i = 0) : f m = 0 :=
  f.toMultilinearMap.map_coord_zero i h

Continuous multilinear maps vanish when a coordinate is zero

Informal description

Let $f$ be a continuous multilinear map from $\prod_{i} M₁ i$ to $M₂$. For any element $m \in \prod_{i} M₁ i$ and any index $i$, if the $i$-th component $m_i$ is zero, then $f(m) = 0$.

ContinuousMultilinearMap.map_zero theorem

[Nonempty ι] : f 0 = 0

Full source

@[simp]
theorem map_zero [Nonempty ι] : f 0 = 0 :=
  f.toMultilinearMap.map_zero

Continuous Multilinear Maps Vanish at Zero

Informal description

Let $f$ be a continuous multilinear map from $\prod_{i \in \iota} M₁ i$ to $M₂$, where $\iota$ is a nonempty index set. Then $f$ evaluated at the zero function (i.e., the function that maps every $i \in \iota$ to $0_{M₁ i}$) is equal to $0_{M₂}$.

ContinuousMultilinearMap.instZero instance

: Zero (ContinuousMultilinearMap R M₁ M₂)

Full source

instance : Zero (ContinuousMultilinearMap R M₁ M₂) :=
  ⟨{ (0 : MultilinearMap R M₁ M₂) with cont := continuous_const }⟩

Zero Element in Continuous Multilinear Maps

Informal description

The space of continuous multilinear maps from $\prod_{i} M₁ i$ to $M₂$ has a zero element, which is the constant zero map.

ContinuousMultilinearMap.instInhabited instance

: Inhabited (ContinuousMultilinearMap R M₁ M₂)

Full source

instance : Inhabited (ContinuousMultilinearMap R M₁ M₂) :=
  ⟨0⟩

Inhabited Space of Continuous Multilinear Maps

Informal description

The space of continuous multilinear maps from $\prod_{i} M₁ i$ to $M₂$ is inhabited, meaning it contains at least one element.

ContinuousMultilinearMap.zero_apply theorem

(m : ∀ i, M₁ i) : (0 : ContinuousMultilinearMap R M₁ M₂) m = 0

Full source

@[simp]
theorem zero_apply (m : ∀ i, M₁ i) : (0 : ContinuousMultilinearMap R M₁ M₂) m = 0 :=
  rfl

Evaluation of the Zero Continuous Multilinear Map

Informal description

For any continuous multilinear map $f$ from $\prod_{i} M₁ i$ to $M₂$ and any element $m \in \prod_{i} M₁ i$, the zero map evaluated at $m$ is equal to the zero element in $M₂$, i.e., $0(m) = 0$.

ContinuousMultilinearMap.toMultilinearMap_zero theorem

: (0 : ContinuousMultilinearMap R M₁ M₂).toMultilinearMap = 0

Full source

@[simp]
theorem toMultilinearMap_zero : (0 : ContinuousMultilinearMap R M₁ M₂).toMultilinearMap = 0 :=
  rfl

Zero Continuous Multilinear Map Yields Zero Multilinear Map

Informal description

The underlying multilinear map of the zero continuous multilinear map is equal to the zero multilinear map. That is, if $0$ denotes the zero continuous multilinear map from $\prod_{i} M₁ i$ to $M₂$, then its associated multilinear map $0.\text{toMultilinearMap}$ is also the zero map.

ContinuousMultilinearMap.instSMul instance

: SMul R' (ContinuousMultilinearMap A M₁ M₂)

Full source

instance : SMul R' (ContinuousMultilinearMap A M₁ M₂) :=
  ⟨fun c f => { c • f.toMultilinearMap with cont := f.cont.const_smul c }⟩

Scalar Multiplication on Continuous Multilinear Maps

Informal description

For any ring $A$ and topological $A$-modules $M₁$ and $M₂$, the space of continuous multilinear maps from $\prod_i M₁ i$ to $M₂$ is equipped with a scalar multiplication operation by elements of $R'$. Specifically, for any scalar $c \in R'$ and continuous multilinear map $f$, the scalar multiple $c \cdot f$ is defined pointwise as $(c \cdot f)(m) = c \cdot (f(m))$ for all $m \in \prod_i M₁ i$.

ContinuousMultilinearMap.smul_apply theorem

(f : ContinuousMultilinearMap A M₁ M₂) (c : R') (m : ∀ i, M₁ i) : (c • f) m = c • f m

Full source

@[simp]
theorem smul_apply (f : ContinuousMultilinearMap A M₁ M₂) (c : R') (m : ∀ i, M₁ i) :
    (c • f) m = c • f m :=
  rfl

Pointwise scalar multiplication of continuous multilinear maps: $(c \cdot f)(m) = c \cdot f(m)$

Informal description

For any continuous multilinear map $f$ from $\prod_{i} M₁ i$ to $M₂$, any scalar $c \in R'$, and any tuple $m \in \prod_{i} M₁ i$, the evaluation of the scalar multiple $c \cdot f$ at $m$ equals the scalar multiple $c$ of the evaluation of $f$ at $m$, i.e., $(c \cdot f)(m) = c \cdot f(m)$.

ContinuousMultilinearMap.toMultilinearMap_smul theorem

(c : R') (f : ContinuousMultilinearMap A M₁ M₂) : (c • f).toMultilinearMap = c • f.toMultilinearMap

Full source

@[simp]
theorem toMultilinearMap_smul (c : R') (f : ContinuousMultilinearMap A M₁ M₂) :
    (c • f).toMultilinearMap = c • f.toMultilinearMap :=
  rfl

Compatibility of Scalar Multiplication with Underlying Multilinear Map

Informal description

For any scalar $c \in R'$ and any continuous multilinear map $f$ from $\prod_i M₁ i$ to $M₂$, the underlying multilinear map of the scalar multiple $c \cdot f$ is equal to the scalar multiple $c \cdot (f.\text{toMultilinearMap})$.

ContinuousMultilinearMap.instSMulCommClass instance

[SMulCommClass R' R'' M₂] : SMulCommClass R' R'' (ContinuousMultilinearMap A M₁ M₂)

Full source

instance [SMulCommClass R' R'' M₂] : SMulCommClass R' R'' (ContinuousMultilinearMap A M₁ M₂) :=
  ⟨fun _ _ _ => ext fun _ => smul_comm _ _ _⟩

Commutativity of Scalar Multiplication on Continuous Multilinear Maps

Informal description

For any ring $A$ and topological $A$-modules $M₁$ and $M₂$, if the scalar multiplications by $R'$ and $R''$ on $M₂$ commute (i.e., $r' \cdot (r'' \cdot m) = r'' \cdot (r' \cdot m)$ for all $r' \in R'$, $r'' \in R''$, and $m \in M₂$), then the scalar multiplications by $R'$ and $R''$ on the space of continuous multilinear maps from $\prod_i M₁ i$ to $M₂$ also commute.

ContinuousMultilinearMap.instIsScalarTower instance

[SMul R' R''] [IsScalarTower R' R'' M₂] : IsScalarTower R' R'' (ContinuousMultilinearMap A M₁ M₂)

Full source

instance [SMul R' R''] [IsScalarTower R' R'' M₂] :
    IsScalarTower R' R'' (ContinuousMultilinearMap A M₁ M₂) :=
  ⟨fun _ _ _ => ext fun _ => smul_assoc _ _ _⟩

Scalar Tower Property for Continuous Multilinear Maps

Informal description

For any rings $A$ and $R'$, and topological $A$-modules $M₁$ and $M₂$, if $M₂$ has a scalar multiplication action by $R'$ and $R''$ such that $R'$ and $R''$ form a scalar tower (i.e., $(r' \cdot r'') \cdot m = r' \cdot (r'' \cdot m)$ for all $r' \in R'$, $r'' \in R''$, and $m \in M₂$), then the space of continuous multilinear maps from $\prod_i M₁ i$ to $M₂$ also forms a scalar tower with respect to $R'$ and $R''$.

ContinuousMultilinearMap.instIsCentralScalar instance

 [DistribMulAction R'ᵐᵒᵖ M₂] [IsCentralScalar R' M₂] : IsCentralScalar R' (ContinuousMultilinearMap A M₁ M₂)

Full source

instance [DistribMulAction R'ᵐᵒᵖ M₂] [IsCentralScalar R' M₂] :
    IsCentralScalar R' (ContinuousMultilinearMap A M₁ M₂) :=
  ⟨fun _ _ => ext fun _ => op_smul_eq_smul _ _⟩

Central Scalar Property for Continuous Multilinear Maps

Informal description

For any ring $A$, topological $A$-modules $M₁$ and $M₂$, and scalar action type $R'$ with a distributive multiplicative action on $M₂$ that is central (i.e., left and right actions coincide), the space of continuous multilinear maps from $\prod_i M₁ i$ to $M₂$ inherits the central scalar property from $M₂$. This means that for any $r \in R'$ and continuous multilinear map $f$, the left and right scalar multiplications $r \cdot f$ and $f \cdot r$ coincide.

ContinuousMultilinearMap.instMulAction instance

: MulAction R' (ContinuousMultilinearMap A M₁ M₂)

Full source

instance : MulAction R' (ContinuousMultilinearMap A M₁ M₂) :=
  Function.Injective.mulAction toMultilinearMap toMultilinearMap_injective fun _ _ => rfl

Multiplicative Action on Continuous Multilinear Maps

Informal description

For any ring $A$ and topological $A$-modules $M₁$ and $M₂$, the space of continuous multilinear maps from $\prod_i M₁ i$ to $M₂$ forms a multiplicative action structure with respect to any scalar ring $R'$. This means that for any scalar $c \in R'$ and continuous multilinear map $f$, the scalar multiple $c \cdot f$ is defined pointwise as $(c \cdot f)(m) = c \cdot (f(m))$ for all $m \in \prod_i M₁ i$, and satisfies the multiplicative action axioms.

ContinuousMultilinearMap.instAdd instance

: Add (ContinuousMultilinearMap R M₁ M₂)

Full source

instance : Add (ContinuousMultilinearMap R M₁ M₂) :=
  ⟨fun f f' => ⟨f.toMultilinearMap + f'.toMultilinearMap, f.cont.add f'.cont⟩⟩

Additive Structure on Continuous Multilinear Maps

Informal description

The space of continuous multilinear maps from $\prod_{i} M₁ i$ to $M₂$ forms an additive structure, where addition is defined pointwise.

ContinuousMultilinearMap.add_apply theorem

(m : ∀ i, M₁ i) : (f + f') m = f m + f' m

Full source

@[simp]
theorem add_apply (m : ∀ i, M₁ i) : (f + f') m = f m + f' m :=
  rfl

Pointwise Addition of Continuous Multilinear Maps

Informal description

For any continuous multilinear maps $ f $ and $ f' $ from $\prod_{i} M₁ i$ to $ M₂ $, and for any element $ m \in \prod_{i} M₁ i $, the evaluation of the sum $ f + f' $ at $ m $ is equal to the sum of the evaluations $ f(m) + f'(m) $.

ContinuousMultilinearMap.toMultilinearMap_add theorem

(f g : ContinuousMultilinearMap R M₁ M₂) : (f + g).toMultilinearMap = f.toMultilinearMap + g.toMultilinearMap

Full source

@[simp]
theorem toMultilinearMap_add (f g : ContinuousMultilinearMap R M₁ M₂) :
    (f + g).toMultilinearMap = f.toMultilinearMap + g.toMultilinearMap :=
  rfl

Sum of Continuous Multilinear Maps Preserves Underlying Multilinear Map Structure

Informal description

For any two continuous multilinear maps $f$ and $g$ from $\prod_{i} M₁ i$ to $M₂$, the underlying multilinear map of their sum $f + g$ is equal to the sum of their underlying multilinear maps, i.e., $(f + g).\text{toMultilinearMap} = f.\text{toMultilinearMap} + g.\text{toMultilinearMap}$.

ContinuousMultilinearMap.addCommMonoid instance

: AddCommMonoid (ContinuousMultilinearMap R M₁ M₂)

Full source

instance addCommMonoid : AddCommMonoid (ContinuousMultilinearMap R M₁ M₂) :=
  toMultilinearMap_injective.addCommMonoid _ rfl (fun _ _ => rfl) fun _ _ => rfl

Additive Commutative Monoid Structure on Continuous Multilinear Maps

Informal description

The space of continuous multilinear maps from $\prod_{i} M₁ i$ to $M₂$ forms an additive commutative monoid, where addition is defined pointwise and the zero element is the constant zero map.

ContinuousMultilinearMap.applyAddHom definition

(m : ∀ i, M₁ i) : ContinuousMultilinearMap R M₁ M₂ →+ M₂

Full source

/-- Evaluation of a `ContinuousMultilinearMap` at a vector as an `AddMonoidHom`. -/
def applyAddHom (m : ∀ i, M₁ i) : ContinuousMultilinearMapContinuousMultilinearMap R M₁ M₂ →+ M₂ where
  toFun f := f m
  map_zero' := rfl
  map_add' _ _ := rfl

Evaluation of continuous multilinear maps as an additive monoid homomorphism

Informal description

For any fixed vector $ m = (m_i)_{i \in \iota} $ in the product space $ \prod_{i} M₁ i $, the evaluation map that sends a continuous multilinear map $ f $ to its value $ f(m) $ is an additive monoid homomorphism from the space of continuous multilinear maps to $ M₂ $.

ContinuousMultilinearMap.sum_apply theorem

 {α : Type*} (f : α → ContinuousMultilinearMap R M₁ M₂) (m : ∀ i, M₁ i) {s : Finset α} :
  (∑ a ∈ s, f a) m = ∑ a ∈ s, f a m

Full source

@[simp]
theorem sum_apply {α : Type*} (f : α → ContinuousMultilinearMap R M₁ M₂) (m : ∀ i, M₁ i)
    {s : Finset α} : (∑ a ∈ s, f a) m = ∑ a ∈ s, f a m :=
  map_sum (applyAddHom m) f s

Sum of Continuous Multilinear Maps Evaluates to Sum of Evaluations

Informal description

Let $R$ be a semiring, $\iota$ be a type, and for each $i \in \iota$, let $M₁ i$ and $M₂$ be $R$-modules equipped with topological structures. Given a family of continuous multilinear maps $f_\alpha : \prod_{i} M₁ i \to M₂$ indexed by $\alpha$ in some type, and a vector $m \in \prod_{i} M₁ i$, the evaluation of the sum of the maps $f_\alpha$ at $m$ is equal to the sum of the evaluations of each $f_\alpha$ at $m$. More precisely, for any finite set $s$ indexing the family, we have: \[ \left(\sum_{\alpha \in s} f_\alpha\right)(m) = \sum_{\alpha \in s} f_\alpha(m). \]

ContinuousMultilinearMap.toContinuousLinearMap definition

[DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) : M₁ i →L[R] M₂

Full source

/-- If `f` is a continuous multilinear map, then `f.toContinuousLinearMap m i` is the continuous
linear map obtained by fixing all coordinates but `i` equal to those of `m`, and varying the
`i`-th coordinate. -/
@[simps!] def toContinuousLinearMap [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) : M₁ i →L[R] M₂ :=
  { f.toMultilinearMap.toLinearMap m i with
    cont := f.cont.comp (continuous_const.update i continuous_id) }

Continuous linear map obtained by fixing all but one variable in a continuous multilinear map

Informal description

Given a continuous multilinear map $f$ from $\prod_{i} M₁ i$ to $M₂$, and a fixed tuple $m = (m_i)_{i \in \iota}$ in $\prod_{i} M₁ i$, the function `toContinuousLinearMap m i` is the continuous linear map obtained by fixing all coordinates except the $i$-th one to be those of $m$, and varying only the $i$-th coordinate. More formally, for each $i \in \iota$, the map $x \mapsto f(m_1, \dots, m_{i-1}, x, m_{i+1}, \dots)$ is a continuous linear map from $M₁ i$ to $M₂$.

ContinuousMultilinearMap.prod definition

 (f : ContinuousMultilinearMap R M₁ M₂) (g : ContinuousMultilinearMap R M₁ M₃) : ContinuousMultilinearMap R M₁ (M₂ × M₃)

Full source

/-- The cartesian product of two continuous multilinear maps, as a continuous multilinear map. -/
def prod (f : ContinuousMultilinearMap R M₁ M₂) (g : ContinuousMultilinearMap R M₁ M₃) :
    ContinuousMultilinearMap R M₁ (M₂ × M₃) :=
  { f.toMultilinearMap.prod g.toMultilinearMap with cont := f.cont.prodMk g.cont }

Product of continuous multilinear maps

Informal description

Given two continuous multilinear maps $ f : \prod_{i} M₁ i \to M₂ $ and $ g : \prod_{i} M₁ i \to M₃ $ over a ring $ R $, the map $ f \times g $ is the continuous multilinear map from $ \prod_{i} M₁ i $ to $ M₂ \times M₃ $ defined by $ (f \times g)(m) = (f(m), g(m)) $.

ContinuousMultilinearMap.prod_apply theorem

 (f : ContinuousMultilinearMap R M₁ M₂) (g : ContinuousMultilinearMap R M₁ M₃) (m : ∀ i, M₁ i) :
  (f.prod g) m = (f m, g m)

Full source

@[simp]
theorem prod_apply (f : ContinuousMultilinearMap R M₁ M₂) (g : ContinuousMultilinearMap R M₁ M₃)
    (m : ∀ i, M₁ i) : (f.prod g) m = (f m, g m) :=
  rfl

Evaluation of Product of Continuous Multilinear Maps: $(f \times g)(m) = (f(m), g(m))$

Informal description

Let $R$ be a semiring, $\iota$ be an index type, and for each $i \in \iota$, let $M₁ i$ and $M₂$, $M₃$ be topological $R$-modules. Given two continuous multilinear maps $f \colon \prod_{i} M₁ i \to M₂$ and $g \colon \prod_{i} M₁ i \to M₃$, and an element $m \in \prod_{i} M₁ i$, the evaluation of the product map $f \times g$ at $m$ is given by $(f \times g)(m) = (f(m), g(m))$.

ContinuousMultilinearMap.pi definition

 {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)] [∀ i, TopologicalSpace (M' i)] [∀ i, Module R (M' i)]
  (f : ∀ i, ContinuousMultilinearMap R M₁ (M' i)) : ContinuousMultilinearMap R M₁ (∀ i, M' i)

Full source

/-- Combine a family of continuous multilinear maps with the same domain and codomains `M' i` into a
continuous multilinear map taking values in the space of functions `∀ i, M' i`. -/
def pi {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)] [∀ i, TopologicalSpace (M' i)]
    [∀ i, Module R (M' i)] (f : ∀ i, ContinuousMultilinearMap R M₁ (M' i)) :
    ContinuousMultilinearMap R M₁ (∀ i, M' i) where
  cont := continuous_pi fun i => (f i).coe_continuous
  toMultilinearMap := MultilinearMap.pi fun i => (f i).toMultilinearMap

Combining continuous multilinear maps into a product map

Informal description

Given a family of continuous multilinear maps $\{f_i : \prod_{j} M₁ j \to M'_i\}_{i \in \iota'}$ where each $M'_i$ is a topological module over a ring $R$, the function $\text{pi}(f)$ combines them into a single continuous multilinear map from $\prod_{j} M₁ j$ to the product space $\prod_{i \in \iota'} M'_i$, defined by $\text{pi}(f)(m) = \lambda i, f_i(m)$.

ContinuousMultilinearMap.coe_pi theorem

 {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)] [∀ i, TopologicalSpace (M' i)] [∀ i, Module R (M' i)]
  (f : ∀ i, ContinuousMultilinearMap R M₁ (M' i)) : ⇑(pi f) = fun m j => f j m

Full source

@[simp]
theorem coe_pi {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)]
    [∀ i, TopologicalSpace (M' i)] [∀ i, Module R (M' i)]
    (f : ∀ i, ContinuousMultilinearMap R M₁ (M' i)) : ⇑(pi f) = fun m j => f j m :=
  rfl

Componentwise Evaluation of Combined Continuous Multilinear Maps

Informal description

Given a family of continuous multilinear maps $\{f_i : \prod_{j} M₁ j \to M'_i\}_{i \in \iota'}$ where each $M'_i$ is a topological $R$-module, the underlying function of the combined map $\text{pi}(f)$ satisfies $\text{pi}(f)(m)(j) = f_j(m)$ for all $m \in \prod_{j} M₁ j$ and $j \in \iota'$.

ContinuousMultilinearMap.pi_apply theorem

 {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)] [∀ i, TopologicalSpace (M' i)] [∀ i, Module R (M' i)]
  (f : ∀ i, ContinuousMultilinearMap R M₁ (M' i)) (m : ∀ i, M₁ i) (j : ι') : pi f m j = f j m

Full source

theorem pi_apply {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)]
    [∀ i, TopologicalSpace (M' i)] [∀ i, Module R (M' i)]
    (f : ∀ i, ContinuousMultilinearMap R M₁ (M' i)) (m : ∀ i, M₁ i) (j : ι') : pi f m j = f j m :=
  rfl

Componentwise Evaluation of Combined Continuous Multilinear Maps

Informal description

Let $R$ be a semiring, $\iota$ and $\iota'$ be types, and for each $i \in \iota$, let $M₁ i$ be an $R$-module with an additive commutative monoid structure and a topological space structure. For each $j \in \iota'$, let $M' j$ be an $R$-module with an additive commutative monoid structure and a topological space structure. Given a family of continuous multilinear maps $\{f_j : \prod_{i \in \iota} M₁ i \to M' j\}_{j \in \iota'}$, the combined map $\text{pi}(f) : \prod_{i \in \iota} M₁ i \to \prod_{j \in \iota'} M' j$ satisfies $\text{pi}(f)(m)(j) = f_j(m)$ for all $m \in \prod_{i \in \iota} M₁ i$ and $j \in \iota'$.

ContinuousMultilinearMap.codRestrict definition

 (f : ContinuousMultilinearMap R M₁ M₂) (p : Submodule R M₂) (h : ∀ v, f v ∈ p) : ContinuousMultilinearMap R M₁ p

Full source

/-- Restrict the codomain of a continuous multilinear map to a submodule. -/
@[simps! toMultilinearMap apply_coe]
def codRestrict (f : ContinuousMultilinearMap R M₁ M₂) (p : Submodule R M₂) (h : ∀ v, f v ∈ p) :
    ContinuousMultilinearMap R M₁ p :=
  ⟨f.1.codRestrict p h, f.cont.subtype_mk _⟩

Codomain restriction of a continuous multilinear map to a submodule

Informal description

Given a continuous multilinear map $ f $ from $ \prod_{i} M₁ i $ to $ M₂ $ and a submodule $ p $ of $ M₂ $ such that $ f(v) \in p $ for all $ v $, the codomain restriction of $ f $ to $ p $ is a continuous multilinear map from $ \prod_{i} M₁ i $ to $ p $.

ContinuousMultilinearMap.ofSubsingleton definition

[Subsingleton ι] (i : ι) : (M₂ →L[R] M₃) ≃ ContinuousMultilinearMap R (fun _ : ι => M₂) M₃

Full source

/-- The natural equivalence between continuous linear maps from `M₂` to `M₃`
and continuous 1-multilinear maps from `M₂` to `M₃`. -/
@[simps! apply_toMultilinearMap apply_apply symm_apply_apply]
def ofSubsingleton [Subsingleton ι] (i : ι) :
    (M₂ →L[R] M₃) ≃ ContinuousMultilinearMap R (fun _ : ι => M₂) M₃ where
  toFun f := ⟨MultilinearMap.ofSubsingleton R M₂ M₃ i f,
    (map_continuous f).comp (continuous_apply i)⟩
  invFun f := ⟨(MultilinearMap.ofSubsingleton R M₂ M₃ i).symm f.toMultilinearMap,
    (map_continuous f).comp <| continuous_pi fun _ ↦ continuous_id⟩
  left_inv _ := rfl
  right_inv f := toMultilinearMap_injective <|
    (MultilinearMap.ofSubsingleton R M₂ M₃ i).apply_symm_apply f.toMultilinearMap

Equivalence between continuous linear maps and continuous 1-multilinear maps for subsingleton domains

Informal description

Given a type `ι` with at most one element (i.e., `Subsingleton ι`), there is a natural equivalence between continuous linear maps from `M₂` to `M₃` and continuous 1-multilinear maps from the constant family `(fun _ : ι => M₂)` to `M₃`. More precisely, for any fixed `i : ι`, the equivalence maps a continuous linear map `f : M₂ →L[R] M₃` to the continuous multilinear map obtained by viewing `f` as a multilinear map in one variable, and vice versa.

ContinuousMultilinearMap.constOfIsEmpty definition

[IsEmpty ι] (m : M₂) : ContinuousMultilinearMap R M₁ M₂

Full source

/-- The constant map is multilinear when `ι` is empty. -/
@[simps! toMultilinearMap apply]
def constOfIsEmpty [IsEmpty ι] (m : M₂) : ContinuousMultilinearMap R M₁ M₂ where
  toMultilinearMap := MultilinearMap.constOfIsEmpty R _ m
  cont := continuous_const

Constant continuous multilinear map for empty index type

Informal description

Given an empty index type $\iota$ (i.e., `IsEmpty ι`), the constant map that sends every element of $\prod_{i} M₁ i$ to a fixed element $m \in M₂$ is a continuous multilinear map. More precisely, for any fixed $m \in M₂$, the map $\text{constOfIsEmpty}\ m$ is the continuous multilinear map from $\prod_{i} M₁ i$ to $M₂$ that ignores its input (since $\iota$ is empty) and always returns $m$.

ContinuousMultilinearMap.compContinuousLinearMap definition

 (g : ContinuousMultilinearMap R M₁' M₄) (f : ∀ i : ι, M₁ i →L[R] M₁' i) : ContinuousMultilinearMap R M₁ M₄

Full source

/-- If `g` is continuous multilinear and `f` is a collection of continuous linear maps,
then `g (f₁ m₁, ..., fₙ mₙ)` is again a continuous multilinear map, that we call
`g.compContinuousLinearMap f`. -/
def compContinuousLinearMap (g : ContinuousMultilinearMap R M₁' M₄)
    (f : ∀ i : ι, M₁ i →L[R] M₁' i) : ContinuousMultilinearMap R M₁ M₄ :=
  { g.toMultilinearMap.compLinearMap fun i => (f i).toLinearMap with
    cont := g.cont.comp <| continuous_pi fun j => (f j).cont.comp <| continuous_apply _ }

Composition of a continuous multilinear map with continuous linear maps

Informal description

Given a continuous multilinear map $ g $ from $ \prod_{i} M'_i $ to $ M_4 $ and a family of continuous linear maps $ f_i : M_i \to M'_i $ for each $ i \in \iota $, the composition $ g \circ (f_1, \dots, f_n) $ is a continuous multilinear map from $ \prod_{i} M_i $ to $ M_4 $. Here, $ (f_1, \dots, f_n) $ denotes the map that applies each $ f_i $ to the corresponding component of the input tuple.

ContinuousMultilinearMap.compContinuousLinearMap_apply theorem

 (g : ContinuousMultilinearMap R M₁' M₄) (f : ∀ i : ι, M₁ i →L[R] M₁' i) (m : ∀ i, M₁ i) :
  g.compContinuousLinearMap f m = g fun i => f i <| m i

Full source

@[simp]
theorem compContinuousLinearMap_apply (g : ContinuousMultilinearMap R M₁' M₄)
    (f : ∀ i : ι, M₁ i →L[R] M₁' i) (m : ∀ i, M₁ i) :
    g.compContinuousLinearMap f m = g fun i => f i <| m i :=
  rfl

Evaluation of Composition of Continuous Multilinear Map with Linear Maps

Informal description

Let $R$ be a semiring, $\iota$ an index type, and for each $i \in \iota$, let $M_i$ and $M'_i$ be topological $R$-modules. Given a continuous multilinear map $g \colon \prod_{i} M'_i \to M_4$ and a family of continuous linear maps $f_i \colon M_i \to M'_i$ for each $i \in \iota$, the evaluation of the composition $g \circ (f_i)_{i \in \iota}$ at a point $m = (m_i)_{i \in \iota} \in \prod_{i} M_i$ is equal to $g$ evaluated at $(f_i(m_i))_{i \in \iota}$. In symbols: $$(g \circ (f_i)_{i \in \iota})(m) = g\big((f_i(m_i))_{i \in \iota}\big).$$

ContinuousLinearMap.compContinuousMultilinearMap definition

(g : M₂ →L[R] M₃) (f : ContinuousMultilinearMap R M₁ M₂) : ContinuousMultilinearMap R M₁ M₃

Full source

/-- Composing a continuous multilinear map with a continuous linear map gives again a
continuous multilinear map. -/
def _root_.ContinuousLinearMap.compContinuousMultilinearMap (g : M₂ →L[R] M₃)
    (f : ContinuousMultilinearMap R M₁ M₂) : ContinuousMultilinearMap R M₁ M₃ :=
  { g.toLinearMap.compMultilinearMap f.toMultilinearMap with cont := g.cont.comp f.cont }

Composition of a continuous linear map with a continuous multilinear map

Informal description

Given a continuous linear map $ g : M₂ \to M₃ $ and a continuous multilinear map $ f : \prod_i M₁ i \to M₂ $, the composition $ g \circ f $ is a continuous multilinear map from $ \prod_i M₁ i $ to $ M₃ $.

ContinuousLinearMap.compContinuousMultilinearMap_coe theorem

 (g : M₂ →L[R] M₃) (f : ContinuousMultilinearMap R M₁ M₂) :
  (g.compContinuousMultilinearMap f : (∀ i, M₁ i) → M₃) = (g : M₂ → M₃) ∘ (f : (∀ i, M₁ i) → M₂)

Full source

@[simp]
theorem _root_.ContinuousLinearMap.compContinuousMultilinearMap_coe (g : M₂ →L[R] M₃)
    (f : ContinuousMultilinearMap R M₁ M₂) :
    (g.compContinuousMultilinearMap f : (∀ i, M₁ i) → M₃) =
      (g : M₂ → M₃) ∘ (f : (∀ i, M₁ i) → M₂) := by
  ext m
  rfl

Composition of Continuous Linear and Multilinear Maps as Function Composition

Informal description

Let $R$ be a semiring, $\iota$ an arbitrary type, and for each $i \in \iota$, let $M₁_i$ and $M₂$, $M₃$ be topological $R$-modules. Given a continuous linear map $g : M₂ \to M₃$ and a continuous multilinear map $f : \prod_{i \in \iota} M₁_i \to M₂$, the composition $g \circ f$ as a continuous multilinear map from $\prod_{i \in \iota} M₁_i$ to $M₃$ is equal to the pointwise composition of $g$ and $f$ as functions.

ContinuousMultilinearMap.prodEquiv definition

 : (ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃) ≃ ContinuousMultilinearMap R M₁ (M₂ × M₃)

Full source

/-- `ContinuousMultilinearMap.prod` as an `Equiv`. -/
@[simps apply symm_apply_fst symm_apply_snd, simps -isSimp symm_apply]
def prodEquiv :
    (ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃) ≃
      ContinuousMultilinearMap R M₁ (M₂ × M₃) where
  toFun f := f.1.prod f.2
  invFun f := ((ContinuousLinearMap.fst _ _ _).compContinuousMultilinearMap f,
    (ContinuousLinearMap.snd _ _ _).compContinuousMultilinearMap f)
  left_inv _ := rfl
  right_inv _ := rfl

Equivalence between product of continuous multilinear maps and continuous multilinear maps into product space

Informal description

The equivalence between the product of two spaces of continuous multilinear maps and the space of continuous multilinear maps into the product space. Specifically, given continuous multilinear maps $ f : \prod_{i} M₁ i \to M₂ $ and $ g : \prod_{i} M₁ i \to M₃ $, the equivalence maps the pair $(f, g)$ to the continuous multilinear map $ f \times g : \prod_{i} M₁ i \to M₂ \times M₃ $ defined by $(f \times g)(m) = (f(m), g(m))$. The inverse operation decomposes a continuous multilinear map $ h : \prod_{i} M₁ i \to M₂ \times M₃ $ into its component maps $ \pi_1 \circ h $ and $ \pi_2 \circ h $, where $ \pi_1 $ and $ \pi_2 $ are the projections from $ M₂ \times M₃ $ to $ M₂ $ and $ M₃ $ respectively.

ContinuousMultilinearMap.prod_ext_iff theorem

 {f g : ContinuousMultilinearMap R M₁ (M₂ × M₃)} :
  f = g ↔
    (ContinuousLinearMap.fst _ _ _).compContinuousMultilinearMap f =
        (ContinuousLinearMap.fst _ _ _).compContinuousMultilinearMap g ∧
      (ContinuousLinearMap.snd _ _ _).compContinuousMultilinearMap f =
        (ContinuousLinearMap.snd _ _ _).compContinuousMultilinearMap g

Full source

theorem prod_ext_iff {f g : ContinuousMultilinearMap R M₁ (M₂ × M₃)} :
    f = g ↔ (ContinuousLinearMap.fst _ _ _).compContinuousMultilinearMap f =
      (ContinuousLinearMap.fst _ _ _).compContinuousMultilinearMap g ∧
      (ContinuousLinearMap.snd _ _ _).compContinuousMultilinearMap f =
      (ContinuousLinearMap.snd _ _ _).compContinuousMultilinearMap g := by
  rw [← Prod.mk_inj, ← prodEquiv_symm_apply, ← prodEquiv_symm_apply, Equiv.apply_eq_iff_eq]

Equality Criterion for Continuous Multilinear Maps via Projections

Informal description

Let $R$ be a semiring, $\iota$ an arbitrary type, and for each $i \in \iota$, let $M₁_i$, $M₂$, and $M₃$ be topological $R$-modules. For any two continuous multilinear maps $f, g : \prod_{i \in \iota} M₁_i \to M₂ \times M₃$, the equality $f = g$ holds if and only if both of the following conditions are satisfied: 1. The composition of $f$ with the first projection $\pi_1 : M₂ \times M₃ \to M₂$ equals the composition of $g$ with $\pi_1$. 2. The composition of $f$ with the second projection $\pi_2 : M₂ \times M₃ \to M₃$ equals the composition of $g$ with $\pi_2$. In other words, $f = g$ if and only if their component-wise projections are equal.

ContinuousMultilinearMap.prod_ext theorem

 {f g : ContinuousMultilinearMap R M₁ (M₂ × M₃)}
  (h₁ :
    (ContinuousLinearMap.fst _ _ _).compContinuousMultilinearMap f =
      (ContinuousLinearMap.fst _ _ _).compContinuousMultilinearMap g)
  (h₂ :
    (ContinuousLinearMap.snd _ _ _).compContinuousMultilinearMap f =
      (ContinuousLinearMap.snd _ _ _).compContinuousMultilinearMap g) :
  f = g

Full source

@[ext]
theorem prod_ext {f g : ContinuousMultilinearMap R M₁ (M₂ × M₃)}
    (h₁ : (ContinuousLinearMap.fst _ _ _).compContinuousMultilinearMap f =
      (ContinuousLinearMap.fst _ _ _).compContinuousMultilinearMap g)
    (h₂ : (ContinuousLinearMap.snd _ _ _).compContinuousMultilinearMap f =
      (ContinuousLinearMap.snd _ _ _).compContinuousMultilinearMap g) : f = g :=
  prod_ext_iff.mpr ⟨h₁, h₂⟩

Equality of Continuous Multilinear Maps via Component-wise Projections

Informal description

Let $R$ be a semiring, $\iota$ an arbitrary type, and for each $i \in \iota$, let $M₁_i$, $M₂$, and $M₃$ be topological $R$-modules. Given two continuous multilinear maps $f, g : \prod_{i \in \iota} M₁_i \to M₂ \times M₃$, if both of the following conditions hold: 1. The composition of $f$ with the first projection $\pi_1 : M₂ \times M₃ \to M₂$ equals the composition of $g$ with $\pi_1$, and 2. The composition of $f$ with the second projection $\pi_2 : M₂ \times M₃ \to M₃$ equals the composition of $g$ with $\pi_2$, then $f = g$.

ContinuousMultilinearMap.add_prod_add theorem

 [ContinuousAdd M₂] [ContinuousAdd M₃] (f₁ f₂ : ContinuousMultilinearMap R M₁ M₂)
  (g₁ g₂ : ContinuousMultilinearMap R M₁ M₃) : (f₁ + f₂).prod (g₁ + g₂) = f₁.prod g₁ + f₂.prod g₂

Full source

theorem add_prod_add [ContinuousAdd M₂] [ContinuousAdd M₃]
    (f₁ f₂ : ContinuousMultilinearMap R M₁ M₂) (g₁ g₂ : ContinuousMultilinearMap R M₁ M₃) :
    (f₁ + f₂).prod (g₁ + g₂) = f₁.prod g₁ + f₂.prod g₂ :=
  rfl

Additivity of Product of Continuous Multilinear Maps

Informal description

Let $R$ be a semiring, and let $M₁$ be a family of topological $R$-modules indexed by a type $\iota$, and $M₂$ and $M₃$ be topological $R$-modules with continuous addition. For any continuous multilinear maps $f₁, f₂ : \prod_{i} M₁ i \to M₂$ and $g₁, g₂ : \prod_{i} M₁ i \to M₃$, the following equality holds: $$(f₁ + f₂) \times (g₁ + g₂) = (f₁ \times g₁) + (f₂ \times g₂)$$ where $\times$ denotes the product of continuous multilinear maps and $+$ denotes pointwise addition.

ContinuousMultilinearMap.smul_prod_smul theorem

 {S : Type*} [Monoid S] [DistribMulAction S M₂] [DistribMulAction S M₃] [ContinuousConstSMul S M₂]
  [SMulCommClass R S M₂] [ContinuousConstSMul S M₃] [SMulCommClass R S M₃] (c : S)
  (f : ContinuousMultilinearMap R M₁ M₂) (g : ContinuousMultilinearMap R M₁ M₃) : (c • f).prod (c • g) = c • f.prod g

Full source

theorem smul_prod_smul {S : Type*} [Monoid S] [DistribMulAction S M₂] [DistribMulAction S M₃]
    [ContinuousConstSMul S M₂] [SMulCommClass R S M₂]
    [ContinuousConstSMul S M₃] [SMulCommClass R S M₃]
    (c : S) (f : ContinuousMultilinearMap R M₁ M₂) (g : ContinuousMultilinearMap R M₁ M₃) :
    (c • f).prod (c • g) = c • f.prod g :=
  rfl

Compatibility of scalar multiplication with product of continuous multilinear maps

Informal description

Let $S$ be a monoid acting distributively on topological modules $M₂$ and $M₃$ over a semiring $R$, with continuous scalar multiplication in both modules. Suppose the actions of $R$ and $S$ commute on $M₂$ and $M₃$. Then for any $c \in S$ and continuous multilinear maps $f : \prod_i M₁ i \to M₂$, $g : \prod_i M₁ i \to M₃$, the product of the scalar multiples $(c \cdot f) \times (c \cdot g)$ equals the scalar multiple of the product map $c \cdot (f \times g)$.

ContinuousMultilinearMap.zero_prod_zero theorem

: (0 : ContinuousMultilinearMap R M₁ M₂).prod (0 : ContinuousMultilinearMap R M₁ M₃) = 0

Full source

@[simp]
theorem zero_prod_zero :
    (0 : ContinuousMultilinearMap R M₁ M₂).prod (0 : ContinuousMultilinearMap R M₁ M₃) = 0 :=
  rfl

Product of Zero Continuous Multilinear Maps is Zero

Informal description

The product of the zero continuous multilinear map from $\prod_{i} M₁ i$ to $M₂$ with the zero continuous multilinear map from $\prod_{i} M₁ i$ to $M₃$ equals the zero map from $\prod_{i} M₁ i$ to $M₂ \times M₃$.

ContinuousMultilinearMap.piEquiv definition

 {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)] [∀ i, TopologicalSpace (M' i)] [∀ i, Module R (M' i)] :
  (∀ i, ContinuousMultilinearMap R M₁ (M' i)) ≃ ContinuousMultilinearMap R M₁ (∀ i, M' i)

Full source

/-- `ContinuousMultilinearMap.pi` as an `Equiv`. -/
@[simps]
def piEquiv {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)]
    [∀ i, TopologicalSpace (M' i)] [∀ i, Module R (M' i)] :
    (∀ i, ContinuousMultilinearMap R M₁ (M' i)) ≃ ContinuousMultilinearMap R M₁ (∀ i, M' i) where
  toFun := ContinuousMultilinearMap.pi
  invFun f i := (ContinuousLinearMap.proj i : _ →L[R] M' i).compContinuousMultilinearMap f
  left_inv _ := rfl
  right_inv _ := rfl

Equivalence between families of continuous multilinear maps and product-valued continuous multilinear maps

Informal description

The equivalence between the space of families of continuous multilinear maps $\{f_i : \prod_{j} M₁ j \to M'_i\}_{i \in \iota'}$ and the space of continuous multilinear maps from $\prod_{j} M₁ j$ to the product space $\prod_{i \in \iota'} M'_i$. Specifically: 1. The forward direction combines a family of maps into a single map to the product space via $\text{pi}(f)(m) = \lambda i, f_i(m)$. 2. The inverse direction decomposes a product-valued map into its component maps by post-composing with projections.

ContinuousMultilinearMap.domDomCongr definition

 {ι' : Type*} (e : ι ≃ ι') (f : ContinuousMultilinearMap R (fun _ : ι => M₂) M₃) :
  ContinuousMultilinearMap R (fun _ : ι' => M₂) M₃

Full source

/-- An equivalence of the index set defines an equivalence between the spaces of continuous
multilinear maps. This is the forward map of this equivalence. -/
@[simps! toMultilinearMap apply]
nonrec def domDomCongr {ι' : Type*} (e : ι ≃ ι')
    (f : ContinuousMultilinearMap R (fun _ : ι => M₂) M₃) :
    ContinuousMultilinearMap R (fun _ : ι' => M₂) M₃ where
  toMultilinearMap := f.domDomCongr e
  cont := f.cont.comp <| continuous_pi fun _ => continuous_apply _

Continuous multilinear map reindexing via equivalence

Informal description

Given an equivalence (bijection) $e$ between index sets $\iota$ and $\iota'$, and a continuous multilinear map $f$ from $\prod_{i \in \iota} M₂$ to $M₃$, the function constructs a new continuous multilinear map from $\prod_{i \in \iota'} M₂$ to $M₃$ by reindexing the domain of $f$ according to $e$. The continuity of the resulting map follows from the continuity of $f$ composed with the projection maps.

ContinuousMultilinearMap.domDomCongrEquiv definition

 {ι' : Type*} (e : ι ≃ ι') :
  ContinuousMultilinearMap R (fun _ : ι => M₂) M₃ ≃ ContinuousMultilinearMap R (fun _ : ι' => M₂) M₃

Full source

/-- An equivalence of the index set defines an equivalence between the spaces of continuous
multilinear maps. In case of normed spaces, this is a linear isometric equivalence, see
`ContinuousMultilinearMap.domDomCongrₗᵢ`. -/
@[simps]
def domDomCongrEquiv {ι' : Type*} (e : ι ≃ ι') :
    ContinuousMultilinearMapContinuousMultilinearMap R (fun _ : ι => M₂) M₃ ≃
      ContinuousMultilinearMap R (fun _ : ι' => M₂) M₃ where
  toFun := domDomCongr e
  invFun := domDomCongr e.symm
  left_inv _ := ext fun _ => by simp
  right_inv _ := ext fun _ => by simp

Equivalence of continuous multilinear maps under index reordering

Informal description

Given an equivalence (bijection) $e$ between index sets $\iota$ and $\iota'$, there is an equivalence between the spaces of continuous multilinear maps from $\prod_{i \in \iota} M₂$ to $M₃$ and from $\prod_{i \in \iota'} M₂$ to $M₃$. This equivalence is constructed by reindexing the domain of the maps according to $e$ and its inverse $e^{-1}$.

ContinuousMultilinearMap.linearDeriv definition

: (∀ i, M₁ i) →L[R] M₂

Full source

/-- The derivative of a continuous multilinear map, as a continuous linear map
from `∀ i, M₁ i` to `M₂`; see `ContinuousMultilinearMap.hasFDerivAt`. -/
def linearDeriv : (∀ i, M₁ i) →L[R] M₂ := ∑ i : ι, (f.toContinuousLinearMap x i).comp (.proj i)

Linear derivative of a continuous multilinear map

Informal description

The linear derivative of a continuous multilinear map $ f $ from $ \prod_{i} M₁ i $ to $ M₂ $ is the continuous linear map from $ \prod_{i} M₁ i $ to $ M₂ $ defined by summing the directional derivatives in each coordinate direction. Specifically, for any $ x \in \prod_{i} M₁ i $, the linear derivative evaluated at $ x $ is given by \[ \sum_{i \in \iota} (f \circ \text{update}_x i) \] where $ \text{update}_x i $ denotes the function that replaces the $ i $-th component of $ x $ with its input, keeping all other components fixed.

ContinuousMultilinearMap.linearDeriv_apply theorem

: f.linearDeriv x y = ∑ i, f (Function.update x i (y i))

Full source

@[simp]
lemma linearDeriv_apply : f.linearDeriv x y = ∑ i, f (Function.update x i (y i)) := by
  unfold linearDeriv toContinuousLinearMap
  simp only [ContinuousLinearMap.coe_sum', ContinuousLinearMap.coe_comp',
    ContinuousLinearMap.coe_mk', LinearMap.coe_mk, LinearMap.coe_toAddHom, Finset.sum_apply]
  rfl

Formula for the Linear Derivative of a Continuous Multilinear Map

Informal description

Let $R$ be a semiring, $\iota$ a type, and $M₁ \colon \iota \to \text{Type}$ and $M₂$ be topological $R$-modules. For any continuous multilinear map $f \colon \prod_{i \in \iota} M₁ i \to M₂$, and any $x, y \in \prod_{i \in \iota} M₁ i$, the linear derivative of $f$ at $x$ applied to $y$ is given by \[ f.\text{linearDeriv}(x)(y) = \sum_{i \in \iota} f(\text{update}(x, i, y_i)), \] where $\text{update}(x, i, y_i)$ denotes the function that replaces the $i$-th component of $x$ with $y_i$, keeping all other components fixed.

ContinuousMultilinearMap.cons_add theorem

 (f : ContinuousMultilinearMap R M M₂) (m : ∀ i : Fin n, M i.succ) (x y : M 0) :
  f (cons (x + y) m) = f (cons x m) + f (cons y m)

Full source

/-- In the specific case of continuous multilinear maps on spaces indexed by `Fin (n+1)`, where one
can build an element of `(i : Fin (n+1)) → M i` using `cons`, one can express directly the
additivity of a multilinear map along the first variable. -/
theorem cons_add (f : ContinuousMultilinearMap R M M₂) (m : ∀ i : Fin n, M i.succ) (x y : M 0) :
    f (cons (x + y) m) = f (cons x m) + f (cons y m) :=
  f.toMultilinearMap.cons_add m x y

Additivity of Continuous Multilinear Maps in the First Argument

Informal description

Let $R$ be a semiring, $M$ a family of topological $R$-modules indexed by $\text{Fin} (n+1)$, and $M₂$ another topological $R$-module. For any continuous multilinear map $f \colon \prod_{i} M i \to M₂$, any tuple $m \colon \forall i \colon \text{Fin} n, M i.\text{succ}$, and any elements $x, y \in M 0$, we have $$ f(\text{cons}(x + y, m)) = f(\text{cons}(x, m)) + f(\text{cons}(y, m)). $$ Here, $\text{cons}(x, m)$ denotes the tuple obtained by prepending $x$ to $m$.

ContinuousMultilinearMap.cons_smul theorem

 (f : ContinuousMultilinearMap R M M₂) (m : ∀ i : Fin n, M i.succ) (c : R) (x : M 0) :
  f (cons (c • x) m) = c • f (cons x m)

Full source

/-- In the specific case of continuous multilinear maps on spaces indexed by `Fin (n+1)`, where one
can build an element of `(i : Fin (n+1)) → M i` using `cons`, one can express directly the
multiplicativity of a multilinear map along the first variable. -/
theorem cons_smul (f : ContinuousMultilinearMap R M M₂) (m : ∀ i : Fin n, M i.succ) (c : R)
    (x : M 0) : f (cons (c • x) m) = c • f (cons x m) :=
  f.toMultilinearMap.cons_smul m c x

Linearity of Continuous Multilinear Maps in the First Argument

Informal description

Let $R$ be a semiring, $M$ a family of topological $R$-modules indexed by $\text{Fin} (n+1)$, and $M₂$ another topological $R$-module. For any continuous multilinear map $f \colon \prod_{i} M i \to M₂$, any tuple $m \colon \forall i \colon \text{Fin} n, M i.\text{succ}$, any scalar $c \in R$, and any element $x \in M 0$, we have $$ f(\text{cons}(c \cdot x, m)) = c \cdot f(\text{cons}(x, m)). $$ Here, $\text{cons}(x, m)$ denotes the tuple obtained by prepending $x$ to $m$.

ContinuousMultilinearMap.map_piecewise_add theorem

 [DecidableEq ι] (m m' : ∀ i, M₁ i) (t : Finset ι) :
  f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')

Full source

theorem map_piecewise_add [DecidableEq ι] (m m' : ∀ i, M₁ i) (t : Finset ι) :
    f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m') :=
  f.toMultilinearMap.map_piecewise_add _ _ _

Additivity of Continuous Multilinear Maps over Subsets of a Finite Set

Informal description

Let $R$ be a semiring, $\iota$ a type with decidable equality, and for each $i \in \iota$, let $M₁ i$ and $M₂$ be topological $R$-modules. Given a continuous multilinear map $f \colon \prod_{i \in \iota} M₁ i \to M₂$, two tuples $m, m' \colon \prod_{i \in \iota} M₁ i$, and a finite subset $t \subseteq \iota$, we have: $$ f(t.\text{piecewise}\, (m + m')\, m') = \sum_{s \subseteq t} f(s.\text{piecewise}\, m\, m') $$ where $t.\text{piecewise}\, (m + m')\, m'$ denotes the tuple that equals $m_i + m'_i$ for $i \in t$ and $m'_i$ otherwise, and the sum is taken over all subsets $s$ of $t$.

ContinuousMultilinearMap.map_add_univ theorem

[DecidableEq ι] [Fintype ι] (m m' : ∀ i, M₁ i) : f (m + m') = ∑ s : Finset ι, f (s.piecewise m m')

Full source

/-- Additivity of a continuous multilinear map along all coordinates at the same time,
writing `f (m + m')` as the sum of `f (s.piecewise m m')` over all sets `s`. -/
theorem map_add_univ [DecidableEq ι] [Fintype ι] (m m' : ∀ i, M₁ i) :
    f (m + m') = ∑ s : Finset ι, f (s.piecewise m m') :=
  f.toMultilinearMap.map_add_univ _ _

Additivity of Continuous Multilinear Maps over All Subsets

Informal description

Let $R$ be a semiring, $\iota$ a finite type with decidable equality, and for each $i \in \iota$, let $M₁ i$ and $M₂$ be topological $R$-modules. Given a continuous multilinear map $f \colon \prod_{i \in \iota} M₁ i \to M₂$ and two tuples $m, m' \colon \prod_{i \in \iota} M₁ i$, we have: $$ f(m + m') = \sum_{s \subseteq \iota} f(s.\text{piecewise}\, m\, m') $$ where the sum is taken over all subsets $s$ of $\iota$, and $s.\text{piecewise}\, m\, m'$ denotes the tuple that equals $m_i$ for $i \in s$ and $m'_i$ otherwise.

ContinuousMultilinearMap.map_sum_finset theorem

[DecidableEq ι] : (f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i)

Full source

/-- If `f` is continuous multilinear, then `f (Σ_{j₁ ∈ A₁} g₁ j₁, ..., Σ_{jₙ ∈ Aₙ} gₙ jₙ)` is the
sum of `f (g₁ (r 1), ..., gₙ (r n))` where `r` ranges over all functions with `r 1 ∈ A₁`, ...,
`r n ∈ Aₙ`. This follows from multilinearity by expanding successively with respect to each
coordinate. -/
theorem map_sum_finset [DecidableEq ι] :
    (f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i) :=
  f.toMultilinearMap.map_sum_finset _ _

Summation Formula for Continuous Multilinear Maps over Finite Indexed Families

Informal description

Let $R$ be a semiring, $\iota$ a type with decidable equality, and for each $i \in \iota$, let $M₁ i$ and $M₂$ be topological $R$-modules. Given a continuous multilinear map $f \colon \prod_{i \in \iota} M₁ i \to M₂$, a family of finite sets $(A_i)_{i \in \iota}$, and a family of functions $(g_i \colon A_i \to M₁ i)_{i \in \iota}$, we have: $$ f\left(\lambda i, \sum_{j \in A_i} g_i(j)\right) = \sum_{r \in \prod_{i \in \iota} A_i} f\left(\lambda i, g_i(r(i))\right) $$ where $\prod_{i \in \iota} A_i$ denotes the Cartesian product of the sets $(A_i)_{i \in \iota}$.

ContinuousMultilinearMap.map_sum theorem

[DecidableEq ι] [∀ i, Fintype (α i)] : (f fun i => ∑ j, g i j) = ∑ r : ∀ i, α i, f fun i => g i (r i)

Full source

/-- If `f` is continuous multilinear, then `f (Σ_{j₁} g₁ j₁, ..., Σ_{jₙ} gₙ jₙ)` is the sum of
`f (g₁ (r 1), ..., gₙ (r n))` where `r` ranges over all functions `r`. This follows from
multilinearity by expanding successively with respect to each coordinate. -/
theorem map_sum [DecidableEq ι] [∀ i, Fintype (α i)] :
    (f fun i => ∑ j, g i j) = ∑ r : ∀ i, α i, f fun i => g i (r i) :=
  f.toMultilinearMap.map_sum _

Summation Formula for Continuous Multilinear Maps over Finite Types

Informal description

Let $R$ be a semiring, $\iota$ a type with decidable equality, and for each $i \in \iota$, let $M₁ i$ and $M₂$ be topological $R$-modules. Given a continuous multilinear map $f \colon \prod_{i \in \iota} M₁ i \to M₂$, and for each $i \in \iota$, a finite type $\alpha_i$ and a function $g_i \colon \alpha_i \to M₁ i$, we have: $$ f\left(\lambda i, \sum_{j \in \alpha_i} g_i(j)\right) = \sum_{r \in \prod_{i \in \iota} \alpha_i} f\left(\lambda i, g_i(r(i))\right) $$ where $\prod_{i \in \iota} \alpha_i$ denotes the Cartesian product of the types $(\alpha_i)_{i \in \iota}$.

ContinuousMultilinearMap.restrictScalars definition

(f : ContinuousMultilinearMap A M₁ M₂) : ContinuousMultilinearMap R M₁ M₂

Full source

/-- Reinterpret an `A`-multilinear map as an `R`-multilinear map, if `A` is an algebra over `R`
and their actions on all involved modules agree with the action of `R` on `A`. -/
def restrictScalars (f : ContinuousMultilinearMap A M₁ M₂) : ContinuousMultilinearMap R M₁ M₂ where
  toMultilinearMap := f.toMultilinearMap.restrictScalars R
  cont := f.cont

Restriction of scalars for continuous multilinear maps

Informal description

Given an algebra $A$ over a ring $R$, and continuous multilinear maps $f$ from $\prod_{i} M₁ i$ to $M₂$ that are $A$-multilinear, the function `restrictScalars` reinterprets $f$ as an $R$-multilinear map, provided the actions of $A$ and $R$ on the modules $M₁ i$ and $M₂$ agree.

ContinuousMultilinearMap.coe_restrictScalars theorem

(f : ContinuousMultilinearMap A M₁ M₂) : ⇑(f.restrictScalars R) = f

Full source

@[simp]
theorem coe_restrictScalars (f : ContinuousMultilinearMap A M₁ M₂) : ⇑(f.restrictScalars R) = f :=
  rfl

Underlying Function of Scalar-Restricted Continuous Multilinear Map Equals Original

Informal description

Let $A$ be an algebra over a ring $R$, and let $f \colon \prod_{i} M₁ i \to M₂$ be a continuous $A$-multilinear map. Then the underlying function of the scalar-restricted map $f.\text{restrictScalars}(R)$ is equal to $f$ itself. That is, for all $m \in \prod_{i} M₁ i$, we have $f.\text{restrictScalars}(R)(m) = f(m)$.

ContinuousMultilinearMap.map_update_sub theorem

 [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) (x y : M₁ i) : f (update m i (x - y)) = f (update m i x) - f (update m i y)

Full source

@[simp]
theorem map_update_sub [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) (x y : M₁ i) :
    f (update m i (x - y)) = f (update m i x) - f (update m i y) :=
  f.toMultilinearMap.map_update_sub _ _ _ _

Subtraction Rule for Continuous Multilinear Maps under Pointwise Update

Informal description

Let $R$ be a semiring, $\iota$ a type with decidable equality, and for each $i \in \iota$, let $M₁ i$ and $M₂$ be topological $R$-modules. Given a continuous multilinear map $f : \prod_{i \in \iota} M₁ i \to M₂$, a family of elements $m \in \prod_{i \in \iota} M₁ i$, an index $i \in \iota$, and elements $x, y \in M₁ i$, we have: \[ f(m[i \mapsto x - y]) = f(m[i \mapsto x]) - f(m[i \mapsto y]) \] where $m[i \mapsto z]$ denotes the function that updates the $i$-th component of $m$ to $z$ while keeping all other components unchanged.

ContinuousMultilinearMap.instNeg instance

: Neg (ContinuousMultilinearMap R M₁ M₂)

Full source

instance : Neg (ContinuousMultilinearMap R M₁ M₂) :=
  ⟨fun f => { -f.toMultilinearMap with cont := f.cont.neg }⟩

Negation of Continuous Multilinear Maps

Informal description

The space of continuous multilinear maps from $\prod_{i \in \iota} M₁ i$ to $M₂$ has a negation operation, where for any continuous multilinear map $f$ and any family of elements $m \in \prod_{i \in \iota} M₁ i$, the negation $(-f)(m)$ is defined as $-f(m)$.

ContinuousMultilinearMap.neg_apply theorem

(m : ∀ i, M₁ i) : (-f) m = -f m

Full source

@[simp]
theorem neg_apply (m : ∀ i, M₁ i) : (-f) m = -f m :=
  rfl

Negation of Continuous Multilinear Maps Evaluates to Negation of Evaluation

Informal description

For any continuous multilinear map $f$ from $\prod_{i \in \iota} M₁ i$ to $M₂$ and any family of elements $m \in \prod_{i \in \iota} M₁ i$, the evaluation of the negation of $f$ at $m$ equals the negation of the evaluation of $f$ at $m$, i.e., $(-f)(m) = -f(m)$.

ContinuousMultilinearMap.instSub instance

: Sub (ContinuousMultilinearMap R M₁ M₂)

Full source

instance : Sub (ContinuousMultilinearMap R M₁ M₂) :=
  ⟨fun f g => { f.toMultilinearMap - g.toMultilinearMap with cont := f.cont.sub g.cont }⟩

Subtraction of Continuous Multilinear Maps

Informal description

The space of continuous multilinear maps from $\prod_{i} M₁ i$ to $M₂$ is equipped with a subtraction operation, where for any two such maps $f$ and $f'$, the difference $(f - f')(m)$ at a point $m \in \prod_{i} M₁ i$ is defined as $f(m) - f'(m)$.

ContinuousMultilinearMap.sub_apply theorem

(m : ∀ i, M₁ i) : (f - f') m = f m - f' m

Full source

@[simp]
theorem sub_apply (m : ∀ i, M₁ i) : (f - f') m = f m - f' m :=
  rfl

Evaluation of the Difference of Continuous Multilinear Maps

Informal description

For any continuous multilinear maps $ f $ and $ f' $ from $\prod_{i} M_i$ to $ M' $ and any element $ m \in \prod_{i} M_i $, the evaluation of the difference $ f - f' $ at $ m $ is equal to the difference of the evaluations $ f(m) - f'(m) $.

ContinuousMultilinearMap.instAddCommGroup instance

: AddCommGroup (ContinuousMultilinearMap R M₁ M₂)

Full source

instance : AddCommGroup (ContinuousMultilinearMap R M₁ M₂) :=
  toMultilinearMap_injective.addCommGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) fun _ _ => rfl

Additive Commutative Group Structure on Continuous Multilinear Maps

Informal description

The space of continuous multilinear maps from $\prod_{i} M₁ i$ to $M₂$ forms an additive commutative group, where addition and negation are defined pointwise.

ContinuousMultilinearMap.neg_prod_neg theorem

 [AddCommGroup M₃] [Module R M₃] [TopologicalSpace M₃] [IsTopologicalAddGroup M₃] (f : ContinuousMultilinearMap R M₁ M₂)
  (g : ContinuousMultilinearMap R M₁ M₃) : (-f).prod (-g) = -f.prod g

Full source

theorem neg_prod_neg [AddCommGroup M₃] [Module R M₃] [TopologicalSpace M₃]
    [IsTopologicalAddGroup M₃] (f : ContinuousMultilinearMap R M₁ M₂)
    (g : ContinuousMultilinearMap R M₁ M₃) : (-f).prod (-g) = - f.prod g :=
  rfl

Negation of Product of Continuous Multilinear Maps: $(-f) \times (-g) = -(f \times g)$

Informal description

Let $R$ be a semiring, $\iota$ a type, and for each $i \in \iota$, let $M₁ i$ and $M₂$, $M₃$ be $R$-modules equipped with topological structures, where $M₃$ is an additive commutative group and its addition is continuous. For any continuous multilinear maps $f \colon \prod_{i} M₁ i \to M₂$ and $g \colon \prod_{i} M₁ i \to M₃$, the product of their negations equals the negation of their product, i.e., \[ (-f) \times (-g) = -(f \times g). \] Here, $\times$ denotes the product of continuous multilinear maps, defined by $(f \times g)(m) = (f(m), g(m))$ for all $m \in \prod_{i} M₁ i$.

ContinuousMultilinearMap.sub_prod_sub theorem

 [AddCommGroup M₃] [Module R M₃] [TopologicalSpace M₃] [IsTopologicalAddGroup M₃]
  (f₁ f₂ : ContinuousMultilinearMap R M₁ M₂) (g₁ g₂ : ContinuousMultilinearMap R M₁ M₃) :
  (f₁ - f₂).prod (g₁ - g₂) = f₁.prod g₁ - f₂.prod g₂

Full source

theorem sub_prod_sub [AddCommGroup M₃] [Module R M₃] [TopologicalSpace M₃]
    [IsTopologicalAddGroup M₃] (f₁ f₂ : ContinuousMultilinearMap R M₁ M₂)
    (g₁ g₂ : ContinuousMultilinearMap R M₁ M₃) :
    (f₁ - f₂).prod (g₁ - g₂) = f₁.prod g₁ - f₂.prod g₂ :=
  rfl

Difference of Products Equals Product of Differences for Continuous Multilinear Maps

Informal description

Let $R$ be a semiring, $\iota$ a type, and for each $i \in \iota$, let $M₁ i$ and $M₂$, $M₃$ be $R$-modules equipped with topological structures, where $M₃$ is an additive commutative group with a topological additive group structure. Given continuous multilinear maps $f₁, f₂ \colon \prod_{i} M₁ i \to M₂$ and $g₁, g₂ \colon \prod_{i} M₁ i \to M₃$, the following equality holds: \[ (f₁ - f₂) \times (g₁ - g₂) = (f₁ \times g₁) - (f₂ \times g₂), \] where $\times$ denotes the product of continuous multilinear maps and $-$ denotes their pointwise difference.

ContinuousMultilinearMap.map_piecewise_smul theorem

 [DecidableEq ι] (c : ι → R) (m : ∀ i, M₁ i) (s : Finset ι) :
  f (s.piecewise (fun i => c i • m i) m) = (∏ i ∈ s, c i) • f m

Full source

theorem map_piecewise_smul [DecidableEq ι] (c : ι → R) (m : ∀ i, M₁ i) (s : Finset ι) :
    f (s.piecewise (fun i => c i • m i) m) = (∏ i ∈ s, c i) • f m :=
  f.toMultilinearMap.map_piecewise_smul _ _ _

Multilinearity of continuous multilinear maps over piecewise scalar multiplication

Informal description

Let $R$ be a semiring, $\iota$ a type with decidable equality, and for each $i \in \iota$, let $M₁ i$ and $M₂$ be $R$-modules with topological structures. Given a continuous multilinear map $f \colon \prod_{i \in \iota} M₁ i \to M₂$, a family of scalars $c \colon \iota \to R$, a family of vectors $m \colon \prod_{i \in \iota} M₁ i$, and a finite subset $s \subseteq \iota$, we have: \[ f \left( s.\text{piecewise} (\lambda i, c i \cdot m i) \, m \right) = \left( \prod_{i \in s} c i \right) \cdot f m, \] where $s.\text{piecewise}$ denotes the function that equals $c i \cdot m i$ on $s$ and $m i$ elsewhere.

ContinuousMultilinearMap.map_smul_univ theorem

[Fintype ι] (c : ι → R) (m : ∀ i, M₁ i) : (f fun i => c i • m i) = (∏ i, c i) • f m

Full source

/-- Multiplicativity of a continuous multilinear map along all coordinates at the same time,
writing `f (fun i ↦ c i • m i)` as `(∏ i, c i) • f m`. -/
theorem map_smul_univ [Fintype ι] (c : ι → R) (m : ∀ i, M₁ i) :
    (f fun i => c i • m i) = (∏ i, c i) • f m :=
  f.toMultilinearMap.map_smul_univ _ _

Multilinearity of continuous multilinear maps over finite types

Informal description

Let $R$ be a semiring, $\iota$ a finite type, and for each $i \in \iota$, let $M₁ i$ and $M₂$ be $R$-modules with topological structures. Given a continuous multilinear map $f \colon \prod_{i \in \iota} M₁ i \to M₂$, a family of scalars $c \colon \iota \to R$, and a family of vectors $m \colon \prod_{i \in \iota} M₁ i$, we have: \[ f \left( \lambda i, c i \cdot m i \right) = \left( \prod_{i \in \iota} c i \right) \cdot f m. \]

ContinuousMultilinearMap.instDistribMulAction instance

[ContinuousAdd M₂] : DistribMulAction R' (ContinuousMultilinearMap A M₁ M₂)

Full source

instance [ContinuousAdd M₂] : DistribMulAction R' (ContinuousMultilinearMap A M₁ M₂) :=
  Function.Injective.distribMulAction
    { toFun := toMultilinearMap,
      map_zero' := toMultilinearMap_zero,
      map_add' := toMultilinearMap_add }
    toMultilinearMap_injective
    fun _ _ => rfl

Distributive Module Action on Continuous Multilinear Maps

Informal description

For any topological $A$-modules $M₁$ and $M₂$ with continuous addition in $M₂$, the space of continuous multilinear maps from $\prod_i M₁ i$ to $M₂$ forms a distributive module action by $R'$. This means that scalar multiplication by elements of $R'$ distributes over addition of continuous multilinear maps and is compatible with the module structure.

ContinuousMultilinearMap.instModule instance

: Module R' (ContinuousMultilinearMap A M₁ M₂)

Full source

/-- The space of continuous multilinear maps over an algebra over `R` is a module over `R`, for the
pointwise addition and scalar multiplication. -/
instance : Module R' (ContinuousMultilinearMap A M₁ M₂) :=
  Function.Injective.module _
    { toFun := toMultilinearMap,
      map_zero' := toMultilinearMap_zero,
      map_add' := toMultilinearMap_add }
    toMultilinearMap_injective fun _ _ => rfl

Module Structure on Continuous Multilinear Maps

Informal description

For any ring $A$ and topological $A$-modules $M₁$ and $M₂$, the space of continuous multilinear maps from $\prod_i M₁ i$ to $M₂$ forms an $R'$-module, where the addition and scalar multiplication are defined pointwise.

ContinuousMultilinearMap.toMultilinearMapLinear definition

: ContinuousMultilinearMap A M₁ M₂ →ₗ[R'] MultilinearMap A M₁ M₂

Full source

/-- Linear map version of the map `toMultilinearMap` associating to a continuous multilinear map
the corresponding multilinear map. -/
@[simps]
def toMultilinearMapLinear : ContinuousMultilinearMapContinuousMultilinearMap A M₁ M₂ →ₗ[R'] MultilinearMap A M₁ M₂ where
  toFun := toMultilinearMap
  map_add' := toMultilinearMap_add
  map_smul' := toMultilinearMap_smul

Linear map from continuous multilinear maps to multilinear maps

Informal description

The linear map that associates to each continuous multilinear map $f \colon \prod_i M₁ i \to M₂$ its underlying multilinear map. This map is linear with respect to the ring $R'$, meaning it preserves addition and scalar multiplication.

ContinuousMultilinearMap.piLinearEquiv definition

 {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)] [∀ i, TopologicalSpace (M' i)] [∀ i, ContinuousAdd (M' i)]
  [∀ i, Module R' (M' i)] [∀ i, Module A (M' i)] [∀ i, SMulCommClass A R' (M' i)] [∀ i, ContinuousConstSMul R' (M' i)] :
  (∀ i, ContinuousMultilinearMap A M₁ (M' i)) ≃ₗ[R'] ContinuousMultilinearMap A M₁ (∀ i, M' i)

Full source

/-- `ContinuousMultilinearMap.pi` as a `LinearEquiv`. -/
@[simps +simpRhs]
def piLinearEquiv {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)]
    [∀ i, TopologicalSpace (M' i)] [∀ i, ContinuousAdd (M' i)] [∀ i, Module R' (M' i)]
    [∀ i, Module A (M' i)] [∀ i, SMulCommClass A R' (M' i)] [∀ i, ContinuousConstSMul R' (M' i)] :
    (∀ i, ContinuousMultilinearMap A M₁ (M' i)) ≃ₗ[R'] ContinuousMultilinearMap A M₁ (∀ i, M' i) :=
  { piEquiv with
    map_add' := fun _ _ => rfl
    map_smul' := fun _ _ => rfl }

Linear equivalence between families of continuous multilinear maps and product-valued continuous multilinear maps

Informal description

The linear equivalence between the space of families of continuous multilinear maps $\{f_i \colon \prod_j M₁ j \to M'_i\}_{i \in \iota'}$ and the space of continuous multilinear maps from $\prod_j M₁ j$ to the product space $\prod_{i \in \iota'} M'_i$. Specifically: 1. The forward direction combines a family of maps into a single map to the product space via $f \mapsto \big(\mathbf{m} \mapsto (f_i(\mathbf{m}))_{i \in \iota'}\big)$. 2. The inverse direction decomposes a product-valued map into its component maps by post-composing with projections. This equivalence is linear with respect to the ring $R'$, meaning it preserves addition and scalar multiplication.

ContinuousMultilinearMap.mkPiAlgebra definition

: ContinuousMultilinearMap R (fun _ : ι => A) A

Full source

/-- The continuous multilinear map on `A^ι`, where `A` is a normed commutative algebra
over `𝕜`, associating to `m` the product of all the `m i`.

See also `ContinuousMultilinearMap.mkPiAlgebraFin`. -/
protected def mkPiAlgebra : ContinuousMultilinearMap R (fun _ : ι => A) A where
  cont := continuous_finset_prod _ fun _ _ => continuous_apply _
  toMultilinearMap := MultilinearMap.mkPiAlgebra R ι A

Product of elements in a normed commutative algebra as a continuous multilinear map

Informal description

The continuous multilinear map on the product space $A^\iota$, where $A$ is a normed commutative algebra over $\mathbb{K}$, which maps each tuple $(m_i)_{i \in \iota}$ to the product $\prod_{i \in \iota} m_i$.

ContinuousMultilinearMap.mkPiAlgebra_apply theorem

(m : ι → A) : ContinuousMultilinearMap.mkPiAlgebra R ι A m = ∏ i, m i

Full source

@[simp]
theorem mkPiAlgebra_apply (m : ι → A) : ContinuousMultilinearMap.mkPiAlgebra R ι A m = ∏ i, m i :=
  rfl

Evaluation of the Continuous Multilinear Product Map: $\mathrm{mkPiAlgebra}(m) = \prod_i m_i$

Informal description

For any tuple $(m_i)_{i \in \iota}$ of elements in a normed commutative algebra $A$ over a ring $R$, the continuous multilinear map `mkPiAlgebra` evaluates to the product $\prod_{i \in \iota} m_i$.

ContinuousMultilinearMap.mkPiAlgebraFin definition

: A [×n]→L[R] A

Full source

/-- The continuous multilinear map on `A^n`, where `A` is a normed algebra over `𝕜`, associating to
`m` the product of all the `m i`.

See also: `ContinuousMultilinearMap.mkPiAlgebra`. -/
protected def mkPiAlgebraFin : A[×n]→L[R] A where
  cont := by
    change Continuous fun m => (List.ofFn m).prod
    simp_rw [List.ofFn_eq_map]
    exact continuous_list_prod _ fun i _ => continuous_apply _
  toMultilinearMap := MultilinearMap.mkPiAlgebraFin R n A

Continuous multilinear map of product in a normed algebra

Informal description

The continuous multilinear map on $A^n$, where $A$ is a normed algebra over $\mathbb{K}$, which maps a tuple $(m_1, \dots, m_n)$ to the product $m_1 \cdots m_n$.

ContinuousMultilinearMap.mkPiAlgebraFin_apply theorem

(m : Fin n → A) : ContinuousMultilinearMap.mkPiAlgebraFin R n A m = (List.ofFn m).prod

Full source

@[simp]
theorem mkPiAlgebraFin_apply (m : Fin n → A) :
    ContinuousMultilinearMap.mkPiAlgebraFin R n A m = (List.ofFn m).prod :=
  rfl

Evaluation of Continuous Multilinear Map on Product Algebra: $\text{mkPiAlgebraFin}(m) = \prod_{i=1}^n m_i$

Informal description

For any tuple $m = (m_1, \dots, m_n)$ in $A^n$, where $A$ is a normed algebra over $\mathbb{K}$, the continuous multilinear map `mkPiAlgebraFin` evaluated at $m$ equals the product of the elements of $m$, i.e., \[ \text{mkPiAlgebraFin}(m) = \prod_{i=1}^n m_i. \]

ContinuousMultilinearMap.smulRight definition

: ContinuousMultilinearMap R M₁ M₂

Full source

/-- Given a continuous `R`-multilinear map `f` taking values in `R`, `f.smulRight z` is the
continuous multilinear map sending `m` to `f m • z`. -/
@[simps! toMultilinearMap apply]
def smulRight : ContinuousMultilinearMap R M₁ M₂ where
  toMultilinearMap := f.toMultilinearMap.smulRight z
  cont := f.cont.smul continuous_const

Scalar multiplication of a continuous multilinear map's output

Informal description

Given a continuous $R$-multilinear map $f$ from $\prod_{i} M₁ i$ to $R$ and an element $z$ in $M₂$, the function `smulRight` constructs a new continuous multilinear map that sends any tuple $m$ to $f(m) \cdot z$. Here, $M₂$ is an $R$-module with a topological structure, and the scalar multiplication operation is continuous.

ContinuousMultilinearMap.mkPiRing definition

(z : M) : ContinuousMultilinearMap R (fun _ : ι => R) M

Full source

/-- The canonical continuous multilinear map on `R^ι`, associating to `m` the product of all the
`m i` (multiplied by a fixed reference element `z` in the target module) -/
protected def mkPiRing (z : M) : ContinuousMultilinearMap R (fun _ : ι => R) M :=
  (ContinuousMultilinearMap.mkPiAlgebra R ι R).smulRight z

Continuous multilinear map of product scaled by fixed element

Informal description

Given a ring $R$, a type $\iota$, and an $R$-module $M$ with a topological structure, the function constructs a continuous multilinear map from the product space $R^\iota$ to $M$. For any tuple $(m_i)_{i \in \iota}$ in $R^\iota$, the map evaluates to the product $\prod_{i \in \iota} m_i$ scaled by a fixed element $z \in M$.

ContinuousMultilinearMap.mkPiRing_apply theorem

(z : M) (m : ι → R) : (ContinuousMultilinearMap.mkPiRing R ι z : (ι → R) → M) m = (∏ i, m i) • z

Full source

@[simp]
theorem mkPiRing_apply (z : M) (m : ι → R) :
    (ContinuousMultilinearMap.mkPiRing R ι z : (ι → R) → M) m = (∏ i, m i) • z :=
  rfl

Evaluation of Continuous Multilinear Map $\text{mkPiRing}_R^\iota z$ at $m$ is $\left(\prod_i m_i\right) \cdot z$

Informal description

Let $R$ be a semiring, $\iota$ a type, and $M$ an $R$-module with a topological space structure. Given an element $z \in M$ and a tuple $m = (m_i)_{i \in \iota} \in R^\iota$, the continuous multilinear map $\text{mkPiRing}_R^\iota z$ evaluated at $m$ equals the product $\prod_{i \in \iota} m_i$ scaled by $z$, i.e., \[ (\text{mkPiRing}_R^\iota z)(m) = \left(\prod_{i \in \iota} m_i\right) \cdot z. \]

ContinuousMultilinearMap.mkPiRing_apply_one_eq_self theorem

(f : ContinuousMultilinearMap R (fun _ : ι => R) M) : ContinuousMultilinearMap.mkPiRing R ι (f fun _ => 1) = f

Full source

theorem mkPiRing_apply_one_eq_self (f : ContinuousMultilinearMap R (fun _ : ι => R) M) :
    ContinuousMultilinearMap.mkPiRing R ι (f fun _ => 1) = f :=
  toMultilinearMap_injective f.toMultilinearMap.mkPiRing_apply_one_eq_self

Reconstruction of Continuous Multilinear Map via $\text{mkPiRing}_R^\iota$ at Constant One Input

Informal description

Let $R$ be a semiring, $\iota$ a type, and $M$ an $R$-module with a topological space structure. For any continuous multilinear map $f \colon R^\iota \to M$, the continuous multilinear map constructed by $\text{mkPiRing}_R^\iota$ applied to $f(\lambda i. 1)$ is equal to $f$ itself. That is, \[ \text{mkPiRing}_R^\iota (f(\lambda i. 1)) = f. \]

ContinuousMultilinearMap.mkPiRing_eq_iff theorem

 {z₁ z₂ : M} : ContinuousMultilinearMap.mkPiRing R ι z₁ = ContinuousMultilinearMap.mkPiRing R ι z₂ ↔ z₁ = z₂

Full source

theorem mkPiRing_eq_iff {z₁ z₂ : M} :
    ContinuousMultilinearMap.mkPiRingContinuousMultilinearMap.mkPiRing R ι z₁ = ContinuousMultilinearMap.mkPiRing R ι z₂ ↔
      z₁ = z₂ := by
  rw [← toMultilinearMap_injective.eq_iff]
  exact MultilinearMap.mkPiRing_eq_iff

Equality of Continuous Multilinear Maps $\text{mkPiRing}_R^\iota z$ is Equivalent to Equality of $z$

Informal description

For any two elements $z_1, z_2$ in an $R$-module $M$, the continuous multilinear maps $\text{mkPiRing}_R^\iota z_1$ and $\text{mkPiRing}_R^\iota z_2$ are equal if and only if $z_1 = z_2$.

ContinuousMultilinearMap.mkPiRing_zero theorem

: ContinuousMultilinearMap.mkPiRing R ι (0 : M) = 0

Full source

theorem mkPiRing_zero : ContinuousMultilinearMap.mkPiRing R ι (0 : M) = 0 := by
  ext; rw [mkPiRing_apply, smul_zero, ContinuousMultilinearMap.zero_apply]

$\text{mkPiRing}_R^\iota 0$ is the zero map

Informal description

The continuous multilinear map $\text{mkPiRing}_R^\iota$ constructed with the zero element $0 \in M$ is equal to the zero continuous multilinear map, i.e., \[ \text{mkPiRing}_R^\iota 0 = 0. \]

ContinuousMultilinearMap.mkPiRing_eq_zero_iff theorem

(z : M) : ContinuousMultilinearMap.mkPiRing R ι z = 0 ↔ z = 0

Full source

theorem mkPiRing_eq_zero_iff (z : M) : ContinuousMultilinearMap.mkPiRingContinuousMultilinearMap.mkPiRing R ι z = 0 ↔ z = 0 := by
  rw [← mkPiRing_zero, mkPiRing_eq_iff]

$\text{mkPiRing}_R^\iota z$ is zero if and only if $z$ is zero

Informal description

For any element $z$ in an $R$-module $M$, the continuous multilinear map $\text{mkPiRing}_R^\iota z$ is equal to the zero map if and only if $z$ is equal to zero, i.e., \[ \text{mkPiRing}_R^\iota z = 0 \leftrightarrow z = 0. \]

Mathlib.Topology.Algebra.Module.Multilinear.Basic

Main definitions

Implementation notes

Notation