Continuous multilinear maps #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define continuous multilinear maps as maps from Π(i : ι), M₁ i to M₂ which are multilinear
and continuous, by extending the space of multilinear maps with a continuity assumption.
Here, M₁ i and M₂ are modules over a ring R, and ι is an arbitrary type, and all these
spaces are also topological spaces.
Main definitions #
continuous_multilinear_map R M₁ M₂is the space of continuous multilinear maps fromΠ(i : ι), M₁ itoM₂. We show that it is anR-module.
Implementation notes #
We mostly follow the API of multilinear maps.
Notation #
We introduce the notation M [×n]→L[R] M' for the space of continuous n-multilinear maps from
M^n to M'. This is a particular case of the general notion (where we allow varying dependent
types as the arguments of our continuous multilinear maps), but arguably the most important one,
especially when defining iterated derivatives.
structure
continuous_multilinear_map
(R : Type u)
{ι : Type v}
(M₁ : ι → Type w₁)
(M₂ : Type w₂)
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂] :
Type (max v w₁ w₂)
- to_multilinear_map : multilinear_map R M₁ M₂
- cont : continuous self.to_multilinear_map.to_fun
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.
Instances for continuous_multilinear_map
- continuous_multilinear_map.has_sizeof_inst
- continuous_multilinear_map.continuous_map_class
- continuous_multilinear_map.has_coe_to_fun
- continuous_multilinear_map.has_zero
- continuous_multilinear_map.inhabited
- continuous_multilinear_map.has_smul
- continuous_multilinear_map.smul_comm_class
- continuous_multilinear_map.is_scalar_tower
- continuous_multilinear_map.is_central_scalar
- continuous_multilinear_map.mul_action
- continuous_multilinear_map.has_add
- continuous_multilinear_map.add_comm_monoid
- continuous_multilinear_map.has_neg
- continuous_multilinear_map.has_sub
- continuous_multilinear_map.add_comm_group
- continuous_multilinear_map.distrib_mul_action
- continuous_multilinear_map.module
- continuous_multilinear_map.has_op_norm
- continuous_multilinear_map.has_op_norm'
- continuous_multilinear_map.normed_add_comm_group
- continuous_multilinear_map.normed_add_comm_group'
- continuous_multilinear_map.normed_space
- continuous_multilinear_map.normed_space'
- continuous_multilinear_map.complete_space
- continuous_multilinear_map.has_continuous_const_smul
theorem
continuous_multilinear_map.to_multilinear_map_injective
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂] :
@[protected, instance]
def
continuous_multilinear_map.continuous_map_class
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂] :
continuous_map_class (continuous_multilinear_map R M₁ M₂) (Π (i : ι), M₁ i) M₂
Equations
- continuous_multilinear_map.continuous_map_class = {coe := λ (f : continuous_multilinear_map R M₁ M₂), f.to_multilinear_map.to_fun, coe_injective' := _, map_continuous := _}
@[protected, instance]
def
continuous_multilinear_map.has_coe_to_fun
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂] :
has_coe_to_fun (continuous_multilinear_map R M₁ M₂) (λ (_x : continuous_multilinear_map R M₁ M₂), (Π (i : ι), M₁ i) → M₂)
Equations
- continuous_multilinear_map.has_coe_to_fun = {coe := λ (f : continuous_multilinear_map R M₁ M₂), ⇑f}
def
continuous_multilinear_map.simps.apply
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
(L₁ : continuous_multilinear_map R M₁ M₂)
(v : Π (i : ι), M₁ i) :
M₂
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
- continuous_multilinear_map.simps.apply L₁ v = ⇑L₁ v
@[continuity]
theorem
continuous_multilinear_map.coe_continuous
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
(f : continuous_multilinear_map R M₁ M₂) :
@[simp]
theorem
continuous_multilinear_map.coe_coe
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
(f : continuous_multilinear_map R M₁ M₂) :
⇑(f.to_multilinear_map) = ⇑f
@[ext]
theorem
continuous_multilinear_map.ext
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
{f f' : continuous_multilinear_map R M₁ M₂}
(H : ∀ (x : Π (i : ι), M₁ i), ⇑f x = ⇑f' x) :
f = f'
theorem
continuous_multilinear_map.ext_iff
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
{f f' : continuous_multilinear_map R M₁ M₂} :
@[simp]
theorem
continuous_multilinear_map.map_add
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
(f : continuous_multilinear_map R M₁ M₂)
[decidable_eq ι]
(m : Π (i : ι), M₁ i)
(i : ι)
(x y : M₁ i) :
⇑f (function.update m i (x + y)) = ⇑f (function.update m i x) + ⇑f (function.update m i y)
@[simp]
theorem
continuous_multilinear_map.map_smul
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
(f : continuous_multilinear_map R M₁ M₂)
[decidable_eq ι]
(m : Π (i : ι), M₁ i)
(i : ι)
(c : R)
(x : M₁ i) :
⇑f (function.update m i (c • x)) = c • ⇑f (function.update m i x)
theorem
continuous_multilinear_map.map_coord_zero
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
(f : continuous_multilinear_map R M₁ M₂)
{m : Π (i : ι), M₁ i}
(i : ι)
(h : m i = 0) :
@[simp]
theorem
continuous_multilinear_map.map_zero
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
(f : continuous_multilinear_map R M₁ M₂)
[nonempty ι] :
@[protected, instance]
def
continuous_multilinear_map.has_zero
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂] :
has_zero (continuous_multilinear_map R M₁ M₂)
@[protected, instance]
def
continuous_multilinear_map.inhabited
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂] :
inhabited (continuous_multilinear_map R M₁ M₂)
Equations
@[simp]
theorem
continuous_multilinear_map.zero_apply
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
(m : Π (i : ι), M₁ i) :
@[simp]
theorem
continuous_multilinear_map.to_multilinear_map_zero
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂] :
0.to_multilinear_map = 0
@[protected, instance]
def
continuous_multilinear_map.has_smul
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
{R' : Type u_1}
{A : Type u_3}
[monoid R']
[semiring A]
[Π (i : ι), module A (M₁ i)]
[module A M₂]
[distrib_mul_action R' M₂]
[has_continuous_const_smul R' M₂]
[smul_comm_class A R' M₂] :
has_smul R' (continuous_multilinear_map A M₁ M₂)
Equations
- continuous_multilinear_map.has_smul = {smul := λ (c : R') (f : continuous_multilinear_map A M₁ M₂), {to_multilinear_map := {to_fun := (c • f.to_multilinear_map).to_fun, map_add' := _, map_smul' := _}, cont := _}}
@[simp]
theorem
continuous_multilinear_map.smul_apply
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
{R' : Type u_1}
{A : Type u_3}
[monoid R']
[semiring A]
[Π (i : ι), module A (M₁ i)]
[module A M₂]
[distrib_mul_action R' M₂]
[has_continuous_const_smul R' M₂]
[smul_comm_class A R' M₂]
(f : continuous_multilinear_map A M₁ M₂)
(c : R')
(m : Π (i : ι), M₁ i) :
@[simp]
theorem
continuous_multilinear_map.to_multilinear_map_smul
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
{R' : Type u_1}
{A : Type u_3}
[monoid R']
[semiring A]
[Π (i : ι), module A (M₁ i)]
[module A M₂]
[distrib_mul_action R' M₂]
[has_continuous_const_smul R' M₂]
[smul_comm_class A R' M₂]
(c : R')
(f : continuous_multilinear_map A M₁ M₂) :
(c • f).to_multilinear_map = c • f.to_multilinear_map
@[protected, instance]
def
continuous_multilinear_map.smul_comm_class
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
{R' : Type u_1}
{R'' : Type u_2}
{A : Type u_3}
[monoid R']
[monoid R'']
[semiring A]
[Π (i : ι), module A (M₁ i)]
[module A M₂]
[distrib_mul_action R' M₂]
[has_continuous_const_smul R' M₂]
[smul_comm_class A R' M₂]
[distrib_mul_action R'' M₂]
[has_continuous_const_smul R'' M₂]
[smul_comm_class A R'' M₂]
[smul_comm_class R' R'' M₂] :
smul_comm_class R' R'' (continuous_multilinear_map A M₁ M₂)
@[protected, instance]
def
continuous_multilinear_map.is_scalar_tower
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
{R' : Type u_1}
{R'' : Type u_2}
{A : Type u_3}
[monoid R']
[monoid R'']
[semiring A]
[Π (i : ι), module A (M₁ i)]
[module A M₂]
[distrib_mul_action R' M₂]
[has_continuous_const_smul R' M₂]
[smul_comm_class A R' M₂]
[distrib_mul_action R'' M₂]
[has_continuous_const_smul R'' M₂]
[smul_comm_class A R'' M₂]
[has_smul R' R'']
[is_scalar_tower R' R'' M₂] :
is_scalar_tower R' R'' (continuous_multilinear_map A M₁ M₂)
@[protected, instance]
def
continuous_multilinear_map.is_central_scalar
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
{R' : Type u_1}
{A : Type u_3}
[monoid R']
[semiring A]
[Π (i : ι), module A (M₁ i)]
[module A M₂]
[distrib_mul_action R' M₂]
[has_continuous_const_smul R' M₂]
[smul_comm_class A R' M₂]
[distrib_mul_action R'ᵐᵒᵖ M₂]
[is_central_scalar R' M₂] :
is_central_scalar R' (continuous_multilinear_map A M₁ M₂)
@[protected, instance]
def
continuous_multilinear_map.mul_action
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
{R' : Type u_1}
{A : Type u_3}
[monoid R']
[semiring A]
[Π (i : ι), module A (M₁ i)]
[module A M₂]
[distrib_mul_action R' M₂]
[has_continuous_const_smul R' M₂]
[smul_comm_class A R' M₂] :
mul_action R' (continuous_multilinear_map A M₁ M₂)
Equations
- continuous_multilinear_map.mul_action = function.injective.mul_action continuous_multilinear_map.to_multilinear_map continuous_multilinear_map.mul_action._proof_1 continuous_multilinear_map.mul_action._proof_2
@[protected, instance]
def
continuous_multilinear_map.has_add
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
[has_continuous_add M₂] :
has_add (continuous_multilinear_map R M₁ M₂)
Equations
- continuous_multilinear_map.has_add = {add := λ (f f' : continuous_multilinear_map R M₁ M₂), {to_multilinear_map := f.to_multilinear_map + f'.to_multilinear_map, cont := _}}
@[simp]
theorem
continuous_multilinear_map.add_apply
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
(f f' : continuous_multilinear_map R M₁ M₂)
[has_continuous_add M₂]
(m : Π (i : ι), M₁ i) :
@[simp]
theorem
continuous_multilinear_map.to_multilinear_map_add
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
[has_continuous_add M₂]
(f g : continuous_multilinear_map R M₁ M₂) :
(f + g).to_multilinear_map = f.to_multilinear_map + g.to_multilinear_map
@[protected, instance]
def
continuous_multilinear_map.add_comm_monoid
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
[has_continuous_add M₂] :
add_comm_monoid (continuous_multilinear_map R M₁ M₂)
Equations
- continuous_multilinear_map.add_comm_monoid = function.injective.add_comm_monoid continuous_multilinear_map.to_multilinear_map continuous_multilinear_map.add_comm_monoid._proof_3 continuous_multilinear_map.add_comm_monoid._proof_4 continuous_multilinear_map.add_comm_monoid._proof_5 continuous_multilinear_map.add_comm_monoid._proof_6
def
continuous_multilinear_map.apply_add_hom
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
[has_continuous_add M₂]
(m : Π (i : ι), M₁ i) :
continuous_multilinear_map R M₁ M₂ →+ M₂
Evaluation of a continuous_multilinear_map at a vector as an add_monoid_hom.
Equations
- continuous_multilinear_map.apply_add_hom m = {to_fun := λ (f : continuous_multilinear_map R M₁ M₂), ⇑f m, map_zero' := _, map_add' := _}
@[simp]
theorem
continuous_multilinear_map.sum_apply
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
[has_continuous_add M₂]
{α : Type u_1}
(f : α → continuous_multilinear_map R M₁ M₂)
(m : Π (i : ι), M₁ i)
{s : finset α} :
def
continuous_multilinear_map.to_continuous_linear_map
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
(f : continuous_multilinear_map R M₁ M₂)
[decidable_eq ι]
(m : Π (i : ι), M₁ i)
(i : ι) :
If f is a continuous multilinear map, then f.to_continuous_linear_map 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.
Equations
- f.to_continuous_linear_map m i = {to_linear_map := {to_fun := (f.to_multilinear_map.to_linear_map m i).to_fun, map_add' := _, map_smul' := _}, cont := _}
def
continuous_multilinear_map.prod
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
{M₃ : Type w₃}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[module R M₃]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
[topological_space M₃]
(f : continuous_multilinear_map R M₁ M₂)
(g : continuous_multilinear_map R M₁ M₃) :
continuous_multilinear_map R M₁ (M₂ × M₃)
The cartesian product of two continuous multilinear maps, as a continuous multilinear map.
Equations
- f.prod g = {to_multilinear_map := {to_fun := (f.to_multilinear_map.prod g.to_multilinear_map).to_fun, map_add' := _, map_smul' := _}, cont := _}
@[simp]
theorem
continuous_multilinear_map.prod_apply
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
{M₃ : Type w₃}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[module R M₃]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
[topological_space M₃]
(f : continuous_multilinear_map R M₁ M₂)
(g : continuous_multilinear_map R M₁ M₃)
(m : Π (i : ι), M₁ i) :
def
continuous_multilinear_map.pi
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[Π (i : ι), module R (M₁ i)]
[Π (i : ι), topological_space (M₁ i)]
{ι' : Type u_1}
{M' : ι' → Type u_2}
[Π (i : ι'), add_comm_monoid (M' i)]
[Π (i : ι'), topological_space (M' i)]
[Π (i : ι'), module R (M' i)]
(f : Π (i : ι'), continuous_multilinear_map R M₁ (M' i)) :
continuous_multilinear_map R M₁ (Π (i : ι'), M' i)
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.
Equations
- continuous_multilinear_map.pi f = {to_multilinear_map := multilinear_map.pi (λ (i : ι'), (f i).to_multilinear_map), cont := _}
@[simp]
theorem
continuous_multilinear_map.coe_pi
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[Π (i : ι), module R (M₁ i)]
[Π (i : ι), topological_space (M₁ i)]
{ι' : Type u_1}
{M' : ι' → Type u_2}
[Π (i : ι'), add_comm_monoid (M' i)]
[Π (i : ι'), topological_space (M' i)]
[Π (i : ι'), module R (M' i)]
(f : Π (i : ι'), continuous_multilinear_map R M₁ (M' i)) :
⇑(continuous_multilinear_map.pi f) = λ (m : Π (i : ι), M₁ i) (j : ι'), ⇑(f j) m
theorem
continuous_multilinear_map.pi_apply
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[Π (i : ι), module R (M₁ i)]
[Π (i : ι), topological_space (M₁ i)]
{ι' : Type u_1}
{M' : ι' → Type u_2}
[Π (i : ι'), add_comm_monoid (M' i)]
[Π (i : ι'), topological_space (M' i)]
[Π (i : ι'), module R (M' i)]
(f : Π (i : ι'), continuous_multilinear_map R M₁ (M' i))
(m : Π (i : ι), M₁ i)
(j : ι') :
⇑(continuous_multilinear_map.pi f) m j = ⇑(f j) m
@[simp]
theorem
continuous_multilinear_map.cod_restrict_to_multilinear_map
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
(f : continuous_multilinear_map R M₁ M₂)
(p : submodule R M₂)
(h : ∀ (v : Π (i : ι), M₁ i), ⇑f v ∈ p) :
(f.cod_restrict p h).to_multilinear_map = f.to_multilinear_map.cod_restrict p h
def
continuous_multilinear_map.cod_restrict
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
(f : continuous_multilinear_map R M₁ M₂)
(p : submodule R M₂)
(h : ∀ (v : Π (i : ι), M₁ i), ⇑f v ∈ p) :
continuous_multilinear_map R M₁ ↥p
Restrict the codomain of a continuous multilinear map to a submodule.
Equations
- f.cod_restrict p h = {to_multilinear_map := f.to_multilinear_map.cod_restrict p h, cont := _}
@[simp]
theorem
continuous_multilinear_map.cod_restrict_apply_coe
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
(f : continuous_multilinear_map R M₁ M₂)
(p : submodule R M₂)
(h : ∀ (v : Π (i : ι), M₁ i), ⇑f v ∈ p)
(v : Π (i : ι), M₁ i) :
↑(⇑(f.cod_restrict p h) v) = ⇑f v
@[simp]
theorem
continuous_multilinear_map.of_subsingleton_apply
(R : Type u)
{ι : Type v}
(M₂ : Type w₂)
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
[topological_space M₂]
[subsingleton ι]
(i' : ι)
(f : Π (x : ι), (λ (i : ι), M₂) x) :
⇑(continuous_multilinear_map.of_subsingleton R M₂ i') f = f i'
@[simp]
theorem
continuous_multilinear_map.of_subsingleton_to_multilinear_map
(R : Type u)
{ι : Type v}
(M₂ : Type w₂)
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
[topological_space M₂]
[subsingleton ι]
(i' : ι) :
def
continuous_multilinear_map.of_subsingleton
(R : Type u)
{ι : Type v}
(M₂ : Type w₂)
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
[topological_space M₂]
[subsingleton ι]
(i' : ι) :
continuous_multilinear_map R (λ (_x : ι), M₂) M₂
The evaluation map from ι → M₂ to M₂ is multilinear at a given i when ι is subsingleton.
Equations
- continuous_multilinear_map.of_subsingleton R M₂ i' = {to_multilinear_map := multilinear_map.of_subsingleton R M₂ i', cont := _}
@[simp]
theorem
continuous_multilinear_map.const_of_is_empty_to_multilinear_map
(R : Type u)
{ι : Type v}
(M₁ : ι → Type w₁)
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
[is_empty ι]
(m : M₂) :
def
continuous_multilinear_map.const_of_is_empty
(R : Type u)
{ι : Type v}
(M₁ : ι → Type w₁)
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
[is_empty ι]
(m : M₂) :
continuous_multilinear_map R M₁ M₂
The constant map is multilinear when ι is empty.
Equations
- continuous_multilinear_map.const_of_is_empty R M₁ m = {to_multilinear_map := multilinear_map.const_of_is_empty R M₁ m, cont := _}
@[simp]
theorem
continuous_multilinear_map.const_of_is_empty_apply
(R : Type u)
{ι : Type v}
(M₁ : ι → Type w₁)
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
[is_empty ι]
(m : M₂)
(ᾰ : Π (i : ι), M₁ i) :
⇑(continuous_multilinear_map.const_of_is_empty R M₁ m) ᾰ = m
def
continuous_multilinear_map.comp_continuous_linear_map
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₁' : ι → Type w₁'}
{M₄ : Type w₄}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[Π (i : ι), add_comm_monoid (M₁' i)]
[add_comm_monoid M₄]
[Π (i : ι), module R (M₁ i)]
[Π (i : ι), module R (M₁' i)]
[module R M₄]
[Π (i : ι), topological_space (M₁ i)]
[Π (i : ι), topological_space (M₁' i)]
[topological_space M₄]
(g : continuous_multilinear_map R M₁' M₄)
(f : Π (i : ι), M₁ i →L[R] M₁' i) :
continuous_multilinear_map R M₁ M₄
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.comp_continuous_linear_map f.
Equations
- g.comp_continuous_linear_map f = {to_multilinear_map := {to_fun := (g.to_multilinear_map.comp_linear_map (λ (i : ι), (f i).to_linear_map)).to_fun, map_add' := _, map_smul' := _}, cont := _}
@[simp]
theorem
continuous_multilinear_map.comp_continuous_linear_map_apply
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₁' : ι → Type w₁'}
{M₄ : Type w₄}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[Π (i : ι), add_comm_monoid (M₁' i)]
[add_comm_monoid M₄]
[Π (i : ι), module R (M₁ i)]
[Π (i : ι), module R (M₁' i)]
[module R M₄]
[Π (i : ι), topological_space (M₁ i)]
[Π (i : ι), topological_space (M₁' i)]
[topological_space M₄]
(g : continuous_multilinear_map R M₁' M₄)
(f : Π (i : ι), M₁ i →L[R] M₁' i)
(m : Π (i : ι), M₁ i) :
⇑(g.comp_continuous_linear_map f) m = ⇑g (λ (i : ι), ⇑(f i) (m i))
def
continuous_linear_map.comp_continuous_multilinear_map
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
{M₃ : Type w₃}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[module R M₃]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
[topological_space M₃]
(g : M₂ →L[R] M₃)
(f : continuous_multilinear_map R M₁ M₂) :
continuous_multilinear_map R M₁ M₃
Composing a continuous multilinear map with a continuous linear map gives again a continuous multilinear map.
Equations
- g.comp_continuous_multilinear_map f = {to_multilinear_map := {to_fun := (g.to_linear_map.comp_multilinear_map f.to_multilinear_map).to_fun, map_add' := _, map_smul' := _}, cont := _}
@[simp]
theorem
continuous_linear_map.comp_continuous_multilinear_map_coe
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
{M₃ : Type w₃}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[module R M₃]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
[topological_space M₃]
(g : M₂ →L[R] M₃)
(f : continuous_multilinear_map R M₁ M₂) :
@[simp]
theorem
continuous_multilinear_map.pi_equiv_symm_apply
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[Π (i : ι), module R (M₁ i)]
[Π (i : ι), topological_space (M₁ i)]
{ι' : Type u_1}
{M' : ι' → Type u_2}
[Π (i : ι'), add_comm_monoid (M' i)]
[Π (i : ι'), topological_space (M' i)]
[Π (i : ι'), module R (M' i)]
(f : continuous_multilinear_map R M₁ (Π (i : ι'), M' i))
(i : ι') :
def
continuous_multilinear_map.pi_equiv
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[Π (i : ι), module R (M₁ i)]
[Π (i : ι), topological_space (M₁ i)]
{ι' : Type u_1}
{M' : ι' → Type u_2}
[Π (i : ι'), add_comm_monoid (M' i)]
[Π (i : ι'), topological_space (M' i)]
[Π (i : ι'), module R (M' i)] :
(Π (i : ι'), continuous_multilinear_map R M₁ (M' i)) ≃ continuous_multilinear_map R M₁ (Π (i : ι'), M' i)
continuous_multilinear_map.pi as an equiv.
Equations
- continuous_multilinear_map.pi_equiv = {to_fun := continuous_multilinear_map.pi (λ (i : ι'), _inst_22 i), inv_fun := λ (f : continuous_multilinear_map R M₁ (Π (i : ι'), M' i)) (i : ι'), (continuous_linear_map.proj i).comp_continuous_multilinear_map f, left_inv := _, right_inv := _}
@[simp]
theorem
continuous_multilinear_map.pi_equiv_apply
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[Π (i : ι), module R (M₁ i)]
[Π (i : ι), topological_space (M₁ i)]
{ι' : Type u_1}
{M' : ι' → Type u_2}
[Π (i : ι'), add_comm_monoid (M' i)]
[Π (i : ι'), topological_space (M' i)]
[Π (i : ι'), module R (M' i)]
(f : Π (i : ι'), continuous_multilinear_map R M₁ ((λ (i : ι'), M' i) i)) :
def
continuous_multilinear_map.dom_dom_congr
{R : Type u}
{ι : Type v}
{M₂ : Type w₂}
{M₃ : Type w₃}
[semiring R]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M₂]
[module R M₃]
[topological_space M₂]
[topological_space M₃]
{ι' : Type u_1}
(e : ι ≃ ι')
(f : continuous_multilinear_map R (λ (_x : ι), M₂) M₃) :
continuous_multilinear_map R (λ (_x : ι'), M₂) M₃
An equivalence of the index set defines an equivalence between the spaces of continuous multilinear maps. This is the forward map of this equivalence.
Equations
@[simp]
theorem
continuous_multilinear_map.dom_dom_congr_apply
{R : Type u}
{ι : Type v}
{M₂ : Type w₂}
{M₃ : Type w₃}
[semiring R]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M₂]
[module R M₃]
[topological_space M₂]
[topological_space M₃]
{ι' : Type u_1}
(e : ι ≃ ι')
(f : continuous_multilinear_map R (λ (_x : ι), M₂) M₃)
(v : ι' → M₂) :
⇑(continuous_multilinear_map.dom_dom_congr e f) v = ⇑f (λ (i : ι), v (⇑e i))
@[simp]
theorem
continuous_multilinear_map.dom_dom_congr_to_multilinear_map
{R : Type u}
{ι : Type v}
{M₂ : Type w₂}
{M₃ : Type w₃}
[semiring R]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M₂]
[module R M₃]
[topological_space M₂]
[topological_space M₃]
{ι' : Type u_1}
(e : ι ≃ ι')
(f : continuous_multilinear_map R (λ (_x : ι), M₂) M₃) :
def
continuous_multilinear_map.dom_dom_congr_equiv
{R : Type u}
{ι : Type v}
{M₂ : Type w₂}
{M₃ : Type w₃}
[semiring R]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M₂]
[module R M₃]
[topological_space M₂]
[topological_space M₃]
{ι' : Type u_1}
(e : ι ≃ ι') :
continuous_multilinear_map R (λ (_x : ι), M₂) M₃ ≃ continuous_multilinear_map R (λ (_x : ι'), M₂) M₃
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
continuous.multilinear_map.dom_dom_congrₗᵢ.
Equations
@[simp]
theorem
continuous_multilinear_map.dom_dom_congr_equiv_apply
{R : Type u}
{ι : Type v}
{M₂ : Type w₂}
{M₃ : Type w₃}
[semiring R]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M₂]
[module R M₃]
[topological_space M₂]
[topological_space M₃]
{ι' : Type u_1}
(e : ι ≃ ι')
(f : continuous_multilinear_map R (λ (_x : ι), M₂) M₃) :
@[simp]
theorem
continuous_multilinear_map.dom_dom_congr_equiv_symm_apply
{R : Type u}
{ι : Type v}
{M₂ : Type w₂}
{M₃ : Type w₃}
[semiring R]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M₂]
[module R M₃]
[topological_space M₂]
[topological_space M₃]
{ι' : Type u_1}
(e : ι ≃ ι')
(f : continuous_multilinear_map R (λ (_x : ι'), M₂) M₃) :
theorem
continuous_multilinear_map.cons_add
{R : Type u}
{n : ℕ}
{M : fin n.succ → Type w}
{M₂ : Type w₂}
[semiring R]
[Π (i : fin n.succ), add_comm_monoid (M i)]
[add_comm_monoid M₂]
[Π (i : fin n.succ), module R (M i)]
[module R M₂]
[Π (i : fin n.succ), topological_space (M i)]
[topological_space M₂]
(f : continuous_multilinear_map R M M₂)
(m : Π (i : fin n), M i.succ)
(x y : M 0) :
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
continuous_multilinear_map.cons_smul
{R : Type u}
{n : ℕ}
{M : fin n.succ → Type w}
{M₂ : Type w₂}
[semiring R]
[Π (i : fin n.succ), add_comm_monoid (M i)]
[add_comm_monoid M₂]
[Π (i : fin n.succ), module R (M i)]
[module R M₂]
[Π (i : fin n.succ), topological_space (M i)]
[topological_space M₂]
(f : continuous_multilinear_map R M M₂)
(m : Π (i : fin n), M i.succ)
(c : R)
(x : M 0) :
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
continuous_multilinear_map.map_piecewise_add
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
(f : continuous_multilinear_map R M₁ M₂)
[decidable_eq ι]
(m m' : Π (i : ι), M₁ i)
(t : finset ι) :
theorem
continuous_multilinear_map.map_add_univ
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
(f : continuous_multilinear_map R M₁ M₂)
[decidable_eq ι]
[fintype ι]
(m m' : Π (i : ι), M₁ i) :
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
continuous_multilinear_map.map_sum_finset
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
(f : continuous_multilinear_map R M₁ M₂)
{α : ι → Type u_1}
[fintype ι]
(g : Π (i : ι), α i → M₁ i)
(A : Π (i : ι), finset (α i))
[decidable_eq ι] :
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
continuous_multilinear_map.map_sum
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
(f : continuous_multilinear_map R M₁ M₂)
{α : ι → Type u_1}
[fintype ι]
(g : Π (i : ι), α i → M₁ i)
[decidable_eq ι]
[Π (i : ι), fintype (α i)] :
⇑f (λ (i : ι), finset.univ.sum (λ (j : α i), g i j)) = finset.univ.sum (λ (r : Π (i : ι), α i), ⇑f (λ (i : ι), g i (r i)))
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.
def
continuous_multilinear_map.restrict_scalars
(R : Type u)
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
{A : Type u_1}
[semiring A]
[has_smul R A]
[Π (i : ι), module A (M₁ i)]
[module A M₂]
[∀ (i : ι), is_scalar_tower R A (M₁ i)]
[is_scalar_tower R A M₂]
(f : continuous_multilinear_map A M₁ M₂) :
continuous_multilinear_map R M₁ M₂
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.
Equations
@[simp]
theorem
continuous_multilinear_map.coe_restrict_scalars
(R : Type u)
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
{A : Type u_1}
[semiring A]
[has_smul R A]
[Π (i : ι), module A (M₁ i)]
[module A M₂]
[∀ (i : ι), is_scalar_tower R A (M₁ i)]
[is_scalar_tower R A M₂]
(f : continuous_multilinear_map A M₁ M₂) :
@[simp]
theorem
continuous_multilinear_map.map_sub
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[ring R]
[Π (i : ι), add_comm_group (M₁ i)]
[add_comm_group M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
(f : continuous_multilinear_map R M₁ M₂)
[decidable_eq ι]
(m : Π (i : ι), M₁ i)
(i : ι)
(x y : M₁ i) :
⇑f (function.update m i (x - y)) = ⇑f (function.update m i x) - ⇑f (function.update m i y)
@[protected, instance]
def
continuous_multilinear_map.has_neg
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[ring R]
[Π (i : ι), add_comm_group (M₁ i)]
[add_comm_group M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
[topological_add_group M₂] :
has_neg (continuous_multilinear_map R M₁ M₂)
Equations
- continuous_multilinear_map.has_neg = {neg := λ (f : continuous_multilinear_map R M₁ M₂), {to_multilinear_map := {to_fun := (-f.to_multilinear_map).to_fun, map_add' := _, map_smul' := _}, cont := _}}
@[simp]
theorem
continuous_multilinear_map.neg_apply
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[ring R]
[Π (i : ι), add_comm_group (M₁ i)]
[add_comm_group M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
(f : continuous_multilinear_map R M₁ M₂)
[topological_add_group M₂]
(m : Π (i : ι), M₁ i) :
@[protected, instance]
def
continuous_multilinear_map.has_sub
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[ring R]
[Π (i : ι), add_comm_group (M₁ i)]
[add_comm_group M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
[topological_add_group M₂] :
has_sub (continuous_multilinear_map R M₁ M₂)
Equations
- continuous_multilinear_map.has_sub = {sub := λ (f g : continuous_multilinear_map R M₁ M₂), {to_multilinear_map := {to_fun := (f.to_multilinear_map - g.to_multilinear_map).to_fun, map_add' := _, map_smul' := _}, cont := _}}
@[simp]
theorem
continuous_multilinear_map.sub_apply
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[ring R]
[Π (i : ι), add_comm_group (M₁ i)]
[add_comm_group M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
(f f' : continuous_multilinear_map R M₁ M₂)
[topological_add_group M₂]
(m : Π (i : ι), M₁ i) :
@[protected, instance]
def
continuous_multilinear_map.add_comm_group
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[ring R]
[Π (i : ι), add_comm_group (M₁ i)]
[add_comm_group M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
[topological_add_group M₂] :
add_comm_group (continuous_multilinear_map R M₁ M₂)
Equations
- continuous_multilinear_map.add_comm_group = function.injective.add_comm_group continuous_multilinear_map.to_multilinear_map continuous_multilinear_map.add_comm_group._proof_6 continuous_multilinear_map.add_comm_group._proof_7 continuous_multilinear_map.add_comm_group._proof_8 continuous_multilinear_map.add_comm_group._proof_9 continuous_multilinear_map.add_comm_group._proof_10 continuous_multilinear_map.add_comm_group._proof_11 continuous_multilinear_map.add_comm_group._proof_12
theorem
continuous_multilinear_map.map_piecewise_smul
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[comm_semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
(f : continuous_multilinear_map R M₁ M₂)
[decidable_eq ι]
(c : ι → R)
(m : Π (i : ι), M₁ i)
(s : finset ι) :
theorem
continuous_multilinear_map.map_smul_univ
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[comm_semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
(f : continuous_multilinear_map R M₁ M₂)
[fintype ι]
(c : ι → R)
(m : Π (i : ι), M₁ i) :
Multiplicativity of a continuous multilinear map along all coordinates at the same time,
writing f (λ i, c i • m i) as (∏ i, c i) • f m.
@[protected, instance]
def
continuous_multilinear_map.distrib_mul_action
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
{R' : Type u_1}
{A : Type u_3}
[monoid R']
[semiring A]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
[Π (i : ι), module A (M₁ i)]
[module A M₂]
[distrib_mul_action R' M₂]
[has_continuous_const_smul R' M₂]
[smul_comm_class A R' M₂]
[has_continuous_add M₂] :
distrib_mul_action R' (continuous_multilinear_map A M₁ M₂)
Equations
- continuous_multilinear_map.distrib_mul_action = function.injective.distrib_mul_action {to_fun := continuous_multilinear_map.to_multilinear_map _inst_7, map_zero' := _, map_add' := _} continuous_multilinear_map.distrib_mul_action._proof_3 continuous_multilinear_map.distrib_mul_action._proof_4
@[protected, instance]
def
continuous_multilinear_map.module
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
{R' : Type u_1}
{A : Type u_2}
[semiring R']
[semiring A]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
[has_continuous_add M₂]
[Π (i : ι), module A (M₁ i)]
[module A M₂]
[module R' M₂]
[has_continuous_const_smul R' M₂]
[smul_comm_class A R' M₂] :
module R' (continuous_multilinear_map A M₁ M₂)
The space of continuous multilinear maps over an algebra over R is a module over R, for the
pointwise addition and scalar multiplication.
Equations
- continuous_multilinear_map.module = function.injective.module R' {to_fun := continuous_multilinear_map.to_multilinear_map _inst_6, map_zero' := _, map_add' := _} continuous_multilinear_map.module._proof_3 continuous_multilinear_map.module._proof_4
def
continuous_multilinear_map.to_multilinear_map_linear
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
{R' : Type u_1}
{A : Type u_2}
[semiring R']
[semiring A]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
[has_continuous_add M₂]
[Π (i : ι), module A (M₁ i)]
[module A M₂]
[module R' M₂]
[has_continuous_const_smul R' M₂]
[smul_comm_class A R' M₂] :
continuous_multilinear_map A M₁ M₂ →ₗ[R'] multilinear_map A M₁ M₂
Linear map version of the map to_multilinear_map associating to a continuous multilinear map
the corresponding multilinear map.
Equations
@[simp]
theorem
continuous_multilinear_map.to_multilinear_map_linear_apply
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
{R' : Type u_1}
{A : Type u_2}
[semiring R']
[semiring A]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
[has_continuous_add M₂]
[Π (i : ι), module A (M₁ i)]
[module A M₂]
[module R' M₂]
[has_continuous_const_smul R' M₂]
[smul_comm_class A R' M₂]
(self : continuous_multilinear_map A M₁ M₂) :
@[simp]
theorem
continuous_multilinear_map.pi_linear_equiv_apply
{ι : Type v}
{M₁ : ι → Type w₁}
{R' : Type u_1}
{A : Type u_2}
[semiring R']
[semiring A]
[Π (i : ι), add_comm_monoid (M₁ i)]
[Π (i : ι), topological_space (M₁ i)]
[Π (i : ι), module A (M₁ i)]
{ι' : Type u_3}
{M' : ι' → Type u_4}
[Π (i : ι'), add_comm_monoid (M' i)]
[Π (i : ι'), topological_space (M' i)]
[∀ (i : ι'), has_continuous_add (M' i)]
[Π (i : ι'), module R' (M' i)]
[Π (i : ι'), module A (M' i)]
[∀ (i : ι'), smul_comm_class A R' (M' i)]
[∀ (i : ι'), has_continuous_const_smul R' (M' i)]
(ᾰ : Π (i : ι'), continuous_multilinear_map A M₁ (M' i)) :
@[simp]
theorem
continuous_multilinear_map.pi_linear_equiv_symm_apply
{ι : Type v}
{M₁ : ι → Type w₁}
{R' : Type u_1}
{A : Type u_2}
[semiring R']
[semiring A]
[Π (i : ι), add_comm_monoid (M₁ i)]
[Π (i : ι), topological_space (M₁ i)]
[Π (i : ι), module A (M₁ i)]
{ι' : Type u_3}
{M' : ι' → Type u_4}
[Π (i : ι'), add_comm_monoid (M' i)]
[Π (i : ι'), topological_space (M' i)]
[∀ (i : ι'), has_continuous_add (M' i)]
[Π (i : ι'), module R' (M' i)]
[Π (i : ι'), module A (M' i)]
[∀ (i : ι'), smul_comm_class A R' (M' i)]
[∀ (i : ι'), has_continuous_const_smul R' (M' i)]
(ᾰ : continuous_multilinear_map A M₁ (Π (i : ι'), M' i))
(i : ι') :
def
continuous_multilinear_map.pi_linear_equiv
{ι : Type v}
{M₁ : ι → Type w₁}
{R' : Type u_1}
{A : Type u_2}
[semiring R']
[semiring A]
[Π (i : ι), add_comm_monoid (M₁ i)]
[Π (i : ι), topological_space (M₁ i)]
[Π (i : ι), module A (M₁ i)]
{ι' : Type u_3}
{M' : ι' → Type u_4}
[Π (i : ι'), add_comm_monoid (M' i)]
[Π (i : ι'), topological_space (M' i)]
[∀ (i : ι'), has_continuous_add (M' i)]
[Π (i : ι'), module R' (M' i)]
[Π (i : ι'), module A (M' i)]
[∀ (i : ι'), smul_comm_class A R' (M' i)]
[∀ (i : ι'), has_continuous_const_smul R' (M' i)] :
(Π (i : ι'), continuous_multilinear_map A M₁ (M' i)) ≃ₗ[R'] continuous_multilinear_map A M₁ (Π (i : ι'), M' i)
continuous_multilinear_map.pi as a linear_equiv.
Equations
@[protected]
def
continuous_multilinear_map.mk_pi_algebra
(R : Type u)
(ι : Type v)
(A : Type u_1)
[fintype ι]
[comm_semiring R]
[comm_semiring A]
[algebra R A]
[topological_space A]
[has_continuous_mul A] :
continuous_multilinear_map R (λ (i : ι), A) A
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 continuous_multilinear_map.mk_pi_algebra_fin.
Equations
- continuous_multilinear_map.mk_pi_algebra R ι A = {to_multilinear_map := multilinear_map.mk_pi_algebra R ι A _inst_1, cont := _}
@[simp]
theorem
continuous_multilinear_map.mk_pi_algebra_apply
(R : Type u)
(ι : Type v)
(A : Type u_1)
[fintype ι]
[comm_semiring R]
[comm_semiring A]
[algebra R A]
[topological_space A]
[has_continuous_mul A]
(m : ι → A) :
⇑(continuous_multilinear_map.mk_pi_algebra R ι A) m = finset.univ.prod (λ (i : ι), m i)
@[protected]
def
continuous_multilinear_map.mk_pi_algebra_fin
(R : Type u)
(n : ℕ)
(A : Type u_1)
[comm_semiring R]
[semiring A]
[algebra R A]
[topological_space A]
[has_continuous_mul A] :
continuous_multilinear_map R (λ (i : fin n), A) A
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: continuous_multilinear_map.mk_pi_algebra.
Equations
- continuous_multilinear_map.mk_pi_algebra_fin R n A = {to_multilinear_map := multilinear_map.mk_pi_algebra_fin R n A _inst_3, cont := _}
@[simp]
theorem
continuous_multilinear_map.mk_pi_algebra_fin_apply
{R : Type u}
{n : ℕ}
{A : Type u_1}
[comm_semiring R]
[semiring A]
[algebra R A]
[topological_space A]
[has_continuous_mul A]
(m : fin n → A) :
⇑(continuous_multilinear_map.mk_pi_algebra_fin R n A) m = (list.of_fn m).prod
@[simp]
theorem
continuous_multilinear_map.smul_right_to_multilinear_map
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[comm_semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[topological_space R]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
[has_continuous_smul R M₂]
(f : continuous_multilinear_map R M₁ R)
(z : M₂) :
@[simp]
theorem
continuous_multilinear_map.smul_right_apply
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[comm_semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[topological_space R]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
[has_continuous_smul R M₂]
(f : continuous_multilinear_map R M₁ R)
(z : M₂)
(ᾰ : Π (i : ι), M₁ i) :
⇑(f.smul_right z) ᾰ = ⇑f ᾰ • z
def
continuous_multilinear_map.smul_right
{R : Type u}
{ι : Type v}
{M₁ : ι → Type w₁}
{M₂ : Type w₂}
[comm_semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[topological_space R]
[Π (i : ι), topological_space (M₁ i)]
[topological_space M₂]
[has_continuous_smul R M₂]
(f : continuous_multilinear_map R M₁ R)
(z : M₂) :
continuous_multilinear_map R M₁ M₂
Given a continuous R-multilinear map f taking values in R, f.smul_right z is the
continuous multilinear map sending m to f m • z.
Equations
- f.smul_right z = {to_multilinear_map := f.to_multilinear_map.smul_right z, cont := _}