# mathlibdocumentation

analysis.normed_space.multilinear

# Operator norm on the space of continuous multilinear maps #

When `f` is a continuous multilinear map in finitely many variables, we define its norm `∥f∥` as the smallest number such that `∥f m∥ ≤ ∥f∥ * ∏ i, ∥m i∥` for all `m`.

We show that it is indeed a norm, and prove its basic properties.

## Main results #

Let `f` be a multilinear map in finitely many variables.

• `exists_bound_of_continuous` asserts that, if `f` is continuous, then there exists `C > 0` with `∥f m∥ ≤ C * ∏ i, ∥m i∥` for all `m`.
• `continuous_of_bound`, conversely, asserts that this bound implies continuity.
• `mk_continuous` constructs the associated continuous multilinear map.

Let `f` be a continuous multilinear map in finitely many variables.

• `∥f∥` is its norm, i.e., the smallest number such that `∥f m∥ ≤ ∥f∥ * ∏ i, ∥m i∥` for all `m`.
• `le_op_norm f m` asserts the fundamental inequality `∥f m∥ ≤ ∥f∥ * ∏ i, ∥m i∥`.
• `norm_image_sub_le f m₁ m₂` gives a control of the difference `f m₁ - f m₂` in terms of `∥f∥` and `∥m₁ - m₂∥`.

We also register isomorphisms corresponding to currying or uncurrying variables, transforming a continuous multilinear function `f` in `n+1` variables into a continuous linear function taking values in continuous multilinear functions in `n` variables, and also into a continuous multilinear function in `n` variables taking values in continuous linear functions. These operations are called `f.curry_left` and `f.curry_right` respectively (with inverses `f.uncurry_left` and `f.uncurry_right`). They induce continuous linear equivalences between spaces of continuous multilinear functions in `n+1` variables and spaces of continuous linear functions into continuous multilinear functions in `n` variables (resp. continuous multilinear functions in `n` variables taking values in continuous linear functions), called respectively `continuous_multilinear_curry_left_equiv` and `continuous_multilinear_curry_right_equiv`.

## Implementation notes #

We mostly follow the API (and the proofs) of `operator_norm.lean`, with the additional complexity that we should deal with multilinear maps in several variables. The currying/uncurrying constructions are based on those in `multilinear.lean`.

From the mathematical point of view, all the results follow from the results on operator norm in one variable, by applying them to one variable after the other through currying. However, this is only well defined when there is an order on the variables (for instance on `fin n`) although the final result is independent of the order. While everything could be done following this approach, it turns out that direct proofs are easier and more efficient.

### Type variables #

We use the following type variables in this file:

• `𝕜` : a `nondiscrete_normed_field`;
• `ι`, `ι'` : finite index types with decidable equality;
• `E`, `E₁` : families of normed vector spaces over `𝕜` indexed by `i : ι`;
• `E'` : a family of normed vector spaces over `𝕜` indexed by `i' : ι'`;
• `Ei` : a family of normed vector spaces over `𝕜` indexed by `i : fin (nat.succ n)`;
• `G`, `G'` : normed vector spaces over `𝕜`.

### Continuity properties of multilinear maps #

We relate continuity of multilinear maps to the inequality `∥f m∥ ≤ C * ∏ i, ∥m i∥`, in both directions. Along the way, we prove useful bounds on the difference `∥f m₁ - f m₂∥`.

theorem multilinear_map.bound_of_shell {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) {ε : ι → } {C : } (hε : ∀ (i : ι), 0 < ε i) {c : ι → 𝕜} (hc : ∀ (i : ι), 1 < c i) (hf : ∀ (m : Π (i : ι), E i), (∀ (i : ι), ε i / c i m i)(∀ (i : ι), m i < ε i)f m C * ∏ (i : ι), m i) (m : Π (i : ι), E i) :
f m C * ∏ (i : ι), m i

If a multilinear map in finitely many variables on normed spaces satisfies the inequality `∥f m∥ ≤ C * ∏ i, ∥m i∥` on a shell `ε i / ∥c i∥ < ∥m i∥ < ε i` for some positive numbers `ε i` and elements `c i : 𝕜`, `1 < ∥c i∥`, then it satisfies this inequality for all `m`.

theorem multilinear_map.exists_bound_of_continuous {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) (hf : continuous f) :
∃ (C : ), 0 < C ∀ (m : Π (i : ι), E i), f m C * ∏ (i : ι), m i

If a multilinear map in finitely many variables on normed spaces is continuous, then it satisfies the inequality `∥f m∥ ≤ C * ∏ i, ∥m i∥`, for some `C` which can be chosen to be positive.

theorem multilinear_map.norm_image_sub_le_of_bound' {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) {C : } (hC : 0 C) (H : ∀ (m : Π (i : ι), E i), f m C * ∏ (i : ι), m i) (m₁ m₂ : Π (i : ι), E i) :
f m₁ - f m₂ C * ∑ (i : ι), ∏ (j : ι), ite (j = i) m₁ i - m₂ i (max m₁ j m₂ j)

If `f` satisfies a boundedness property around `0`, one can deduce a bound on `f m₁ - f m₂` using the multilinearity. Here, we give a precise but hard to use version. See `norm_image_sub_le_of_bound` for a less precise but more usable version. The bound reads `∥f m - f m'∥ ≤ C * ∥m 1 - m' 1∥ * max ∥m 2∥ ∥m' 2∥ * max ∥m 3∥ ∥m' 3∥ * ... * max ∥m n∥ ∥m' n∥ + ...`, where the other terms in the sum are the same products where `1` is replaced by any `i`.

theorem multilinear_map.norm_image_sub_le_of_bound {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) {C : } (hC : 0 C) (H : ∀ (m : Π (i : ι), E i), f m C * ∏ (i : ι), m i) (m₁ m₂ : Π (i : ι), E i) :
f m₁ - f m₂ ((C * (fintype.card ι)) * max m₁ m₂ ^ - 1)) * m₁ - m₂

If `f` satisfies a boundedness property around `0`, one can deduce a bound on `f m₁ - f m₂` using the multilinearity. Here, we give a usable but not very precise version. See `norm_image_sub_le_of_bound'` for a more precise but less usable version. The bound is `∥f m - f m'∥ ≤ C * card ι * ∥m - m'∥ * (max ∥m∥ ∥m'∥) ^ (card ι - 1)`.

theorem multilinear_map.continuous_of_bound {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) (C : ) (H : ∀ (m : Π (i : ι), E i), f m C * ∏ (i : ι), m i) :

If a multilinear map satisfies an inequality `∥f m∥ ≤ C * ∏ i, ∥m i∥`, then it is continuous.

def multilinear_map.mk_continuous {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) (C : ) (H : ∀ (m : Π (i : ι), E i), f m C * ∏ (i : ι), m i) :

Constructing a continuous multilinear map from a multilinear map satisfying a boundedness condition.

Equations
@[simp]
theorem multilinear_map.coe_mk_continuous {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) (C : ) (H : ∀ (m : Π (i : ι), E i), f m C * ∏ (i : ι), m i) :
theorem multilinear_map.restr_norm_le {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] {k n : } (f : (λ (i : fin n), G) G') (s : finset (fin n)) (hk : s.card = k) (z : G) {C : } (H : ∀ (m : Π (i : fin n), (λ (i : fin n), G) i), f m C * ∏ (i : fin n), m i) (v : fin k → G) :
(f.restr s hk z) v (C * z ^ (n - k)) * ∏ (i : fin k), v i

Given a multilinear map in `n` variables, if one restricts it to `k` variables putting `z` on the other coordinates, then the resulting restricted function satisfies an inequality `∥f.restr v∥ ≤ C * ∥z∥^(n-k) * Π ∥v i∥` if the original function satisfies `∥f v∥ ≤ C * Π ∥v i∥`.

### Continuous multilinear maps #

We define the norm `∥f∥` of a continuous multilinear map `f` in finitely many variables as the smallest number such that `∥f m∥ ≤ ∥f∥ * ∏ i, ∥m i∥` for all `m`. We show that this defines a normed space structure on `continuous_multilinear_map 𝕜 E G`.

theorem continuous_multilinear_map.bound {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) :
∃ (C : ), 0 < C ∀ (m : Π (i : ι), E i), f m C * ∏ (i : ι), m i
def continuous_multilinear_map.op_norm {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) :

The operator norm of a continuous multilinear map is the inf of all its bounds.

Equations
@[instance]
def continuous_multilinear_map.has_op_norm {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] :
Equations
theorem continuous_multilinear_map.norm_def {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) :
f = Inf {c : | 0 c ∀ (m : Π (i : ι), E i), f m c * ∏ (i : ι), m i}
theorem continuous_multilinear_map.bounds_nonempty {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] {f : G} :
∃ (c : ), c {c : | 0 c ∀ (m : Π (i : ι), E i), f m c * ∏ (i : ι), m i}
theorem continuous_multilinear_map.bounds_bdd_below {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] {f : G} :
bdd_below {c : | 0 c ∀ (m : Π (i : ι), E i), f m c * ∏ (i : ι), m i}
theorem continuous_multilinear_map.op_norm_nonneg {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) :
theorem continuous_multilinear_map.le_op_norm {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) (m : Π (i : ι), E i) :
f m f * ∏ (i : ι), m i

The fundamental property of the operator norm of a continuous multilinear map: `∥f m∥` is bounded by `∥f∥` times the product of the `∥m i∥`.

theorem continuous_multilinear_map.le_of_op_norm_le {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) (m : Π (i : ι), E i) {C : } (h : f C) :
f m C * ∏ (i : ι), m i
theorem continuous_multilinear_map.ratio_le_op_norm {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) (m : Π (i : ι), E i) :
f m / ∏ (i : ι), m i f
theorem continuous_multilinear_map.unit_le_op_norm {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) (m : Π (i : ι), E i) (h : m 1) :

The image of the unit ball under a continuous multilinear map is bounded.

theorem continuous_multilinear_map.op_norm_le_bound {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) {M : } (hMp : 0 M) (hM : ∀ (m : Π (i : ι), E i), f m M * ∏ (i : ι), m i) :

If one controls the norm of every `f x`, then one controls the norm of `f`.

theorem continuous_multilinear_map.op_norm_add_le {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f g : G) :

The operator norm satisfies the triangle inequality.

theorem continuous_multilinear_map.op_norm_zero_iff {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) :
f = 0 f = 0

A continuous linear map is zero iff its norm vanishes.

theorem continuous_multilinear_map.op_norm_smul_le {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) {𝕜' : Type u_1} [ 𝕜] [ G] [ 𝕜 G] (c : 𝕜') :
theorem continuous_multilinear_map.op_norm_neg {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) :
@[instance]
def continuous_multilinear_map.to_normed_group {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] :

Continuous multilinear maps themselves form a normed space with respect to the operator norm.

Equations
@[instance]
def continuous_multilinear_map.to_normed_space {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] {𝕜' : Type u_1} [ 𝕜] [ G] [ 𝕜 G] :
G)
Equations
theorem continuous_multilinear_map.op_norm_prod {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] [normed_group G'] [ G'] (f : G) (g : G') :
theorem continuous_multilinear_map.norm_pi {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] {ι' : Type v'} [fintype ι'] {E' : ι' → Type wE'} [Π (i' : ι'), normed_group (E' i')] [Π (i' : ι'), (E' i')] (f : Π (i' : ι'), (E' i')) :
def continuous_multilinear_map.prodL (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) (G : Type wG) (G' : Type wG') [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] [normed_group G'] [ G'] :
≃ₗᵢ[𝕜] (G × G')

`continuous_multilinear_map.prod` as a `linear_isometry_equiv`.

Equations
def continuous_multilinear_map.piₗᵢ (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] {ι' : Type v'} [fintype ι'] {E' : ι' → Type wE'} [Π (i' : ι'), normed_group (E' i')] [Π (i' : ι'), (E' i')] :
(Π (i' : ι'), (E' i')) ≃ₗᵢ[𝕜] (Π (i : ι'), E' i)

`continuous_multilinear_map.pi` as a `linear_isometry_equiv`.

Equations
@[simp]
theorem continuous_multilinear_map.norm_restrict_scalars {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) {𝕜' : Type u_1} [ 𝕜] [ G] [ 𝕜 G] [Π (i : ι), (E i)] [∀ (i : ι), 𝕜 (E i)] :
def continuous_multilinear_map.restrict_scalars_linear {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (𝕜' : Type u_1) [ 𝕜] [ G] [ 𝕜 G] [Π (i : ι), (E i)] [∀ (i : ι), 𝕜 (E i)] :
→L[𝕜']

`continuous_multilinear_map.restrict_scalars` as a `continuous_multilinear_map`.

Equations
theorem continuous_multilinear_map.continuous_restrict_scalars {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] {𝕜' : Type u_1} [ 𝕜] [ G] [ 𝕜 G] [Π (i : ι), (E i)] [∀ (i : ι), 𝕜 (E i)] :
theorem continuous_multilinear_map.norm_image_sub_le' {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) (m₁ m₂ : Π (i : ι), E i) :
f m₁ - f m₂ f * ∑ (i : ι), ∏ (j : ι), ite (j = i) m₁ i - m₂ i (max m₁ j m₂ j)

The difference `f m₁ - f m₂` is controlled in terms of `∥f∥` and `∥m₁ - m₂∥`, precise version. For a less precise but more usable version, see `norm_image_sub_le`. The bound reads `∥f m - f m'∥ ≤ ∥f∥ * ∥m 1 - m' 1∥ * max ∥m 2∥ ∥m' 2∥ * max ∥m 3∥ ∥m' 3∥ * ... * max ∥m n∥ ∥m' n∥ + ...`, where the other terms in the sum are the same products where `1` is replaced by any `i`.

theorem continuous_multilinear_map.norm_image_sub_le {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) (m₁ m₂ : Π (i : ι), E i) :
f m₁ - f m₂ ((f * (fintype.card ι)) * max m₁ m₂ ^ - 1)) * m₁ - m₂

The difference `f m₁ - f m₂` is controlled in terms of `∥f∥` and `∥m₁ - m₂∥`, less precise version. For a more precise but less usable version, see `norm_image_sub_le'`. The bound is `∥f m - f m'∥ ≤ ∥f∥ * card ι * ∥m - m'∥ * (max ∥m∥ ∥m'∥) ^ (card ι - 1)`.

theorem continuous_multilinear_map.continuous_eval {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] :
continuous (λ (p : × Π (i : ι), E i), (p.fst) p.snd)

Applying a multilinear map to a vector is continuous in both coordinates.

theorem continuous_multilinear_map.continuous_eval_left {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (m : Π (i : ι), E i) :
continuous (λ (p : , p m)
theorem continuous_multilinear_map.has_sum_eval {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] {α : Type u_1} {p : α → } {q : G} (h : q) (m : Π (i : ι), E i) :
has_sum (λ (a : α), (p a) m) (q m)
@[instance]
def continuous_multilinear_map.complete_space {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G]  :

If the target space is complete, the space of continuous multilinear maps with its norm is also complete. The proof is essentially the same as for the space of continuous linear maps (modulo the addition of `finset.prod` where needed. The duplication could be avoided by deducing the linear case from the multilinear case via a currying isomorphism. However, this would mess up imports, and it is more satisfactory to have the simplest case as a standalone proof.

theorem multilinear_map.mk_continuous_norm_le {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) {C : } (hC : 0 C) (H : ∀ (m : Π (i : ι), E i), f m C * ∏ (i : ι), m i) :

If a continuous multilinear map is constructed from a multilinear map via the constructor `mk_continuous`, then its norm is bounded by the bound given to the constructor if it is nonnegative.

theorem multilinear_map.mk_continuous_norm_le' {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] (f : G) {C : } (H : ∀ (m : Π (i : ι), E i), f m C * ∏ (i : ι), m i) :
H max C 0

If a continuous multilinear map is constructed from a multilinear map via the constructor `mk_continuous`, then its norm is bounded by the bound given to the constructor if it is nonnegative.

def continuous_multilinear_map.restr {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] {k n : } (f : (λ (i : fin n), G) G') (s : finset (fin n)) (hk : s.card = k) (z : G) :
(λ (i : fin k), G) G'

Given a continuous multilinear map `f` on `n` variables (parameterized by `fin n`) and a subset `s` of `k` of these variables, one gets a new continuous multilinear map on `fin k` by varying these variables, and fixing the other ones equal to a given value `z`. It is denoted by `f.restr s hk z`, where `hk` is a proof that the cardinality of `s` is `k`. The implicit identification between `fin k` and `s` that we use is the canonical (increasing) bijection.

Equations
theorem continuous_multilinear_map.norm_restr {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] {k n : } (f : (λ (i : fin n), G) G') (s : finset (fin n)) (hk : s.card = k) (z : G) :
f.restr s hk z f * z ^ (n - k)
def continuous_multilinear_map.mk_pi_algebra (𝕜 : Type u) (ι : Type v) [decidable_eq ι] [fintype ι] (A : Type u_1) [ A] :
(λ (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
@[simp]
theorem continuous_multilinear_map.mk_pi_algebra_apply {𝕜 : Type u} {ι : Type v} [decidable_eq ι] [fintype ι] {A : Type u_1} [ A] (m : ι → A) :
= ∏ (i : ι), m i
theorem continuous_multilinear_map.norm_mk_pi_algebra_le {𝕜 : Type u} {ι : Type v} [decidable_eq ι] [fintype ι] {A : Type u_1} [ A] [nonempty ι] :
theorem continuous_multilinear_map.norm_mk_pi_algebra_of_empty {𝕜 : Type u} {ι : Type v} [decidable_eq ι] [fintype ι] {A : Type u_1} [ A] (h : ¬) :
@[simp]
theorem continuous_multilinear_map.norm_mk_pi_algebra {𝕜 : Type u} {ι : Type v} [decidable_eq ι] [fintype ι] {A : Type u_1} [ A]  :
def continuous_multilinear_map.mk_pi_algebra_fin (𝕜 : Type u) (n : ) (A : Type u_1) [normed_ring A] [ A] :
(λ (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: `multilinear_map.mk_pi_algebra`.

Equations
@[simp]
theorem continuous_multilinear_map.mk_pi_algebra_fin_apply {𝕜 : Type u} {n : } {A : Type u_1} [normed_ring A] [ A] (m : fin n → A) :
theorem continuous_multilinear_map.norm_mk_pi_algebra_fin_succ_le {𝕜 : Type u} {n : } {A : Type u_1} [normed_ring A] [ A] :
theorem continuous_multilinear_map.norm_mk_pi_algebra_fin_le_of_pos {𝕜 : Type u} {n : } {A : Type u_1} [normed_ring A] [ A] (hn : 0 < n) :
theorem continuous_multilinear_map.norm_mk_pi_algebra_fin_zero {𝕜 : Type u} {A : Type u_1} [normed_ring A] [ A] :
@[simp]
theorem continuous_multilinear_map.norm_mk_pi_algebra_fin {𝕜 : Type u} {n : } {A : Type u_1} [normed_ring A] [ A]  :
def continuous_multilinear_map.mk_pi_field (𝕜 : Type u) (ι : Type v) {G : Type wG} [decidable_eq ι] [fintype ι] [normed_group G] [ G] (z : G) :
(λ (i : ι), 𝕜) G

The canonical continuous multilinear map on `𝕜^ι`, associating to `m` the product of all the `m i` (multiplied by a fixed reference element `z` in the target module)

Equations
@[simp]
theorem continuous_multilinear_map.mk_pi_field_apply {𝕜 : Type u} {ι : Type v} {G : Type wG} [decidable_eq ι] [fintype ι] [normed_group G] [ G] (z : G) (m : ι → 𝕜) :
= (∏ (i : ι), m i) z
theorem continuous_multilinear_map.mk_pi_field_apply_one_eq_self {𝕜 : Type u} {ι : Type v} {G : Type wG} [decidable_eq ι] [fintype ι] [normed_group G] [ G] (f : (λ (i : ι), 𝕜) G) :
(f (λ (i : ι), 1)) = f
def continuous_multilinear_map.pi_field_equiv_aux (𝕜 : Type u) (ι : Type v) (G : Type wG) [decidable_eq ι] [fintype ι] [normed_group G] [ G] :
G ≃ₗ[𝕜] (λ (i : ι), 𝕜) G

Continuous multilinear maps on `𝕜^n` with values in `G` are in bijection with `G`, as such a continuous multilinear map is completely determined by its value on the constant vector made of ones. We register this bijection as a linear equivalence in `continuous_multilinear_map.pi_field_equiv_aux`. The continuous linear equivalence is `continuous_multilinear_map.pi_field_equiv`.

Equations
def continuous_multilinear_map.pi_field_equiv (𝕜 : Type u) (ι : Type v) (G : Type wG) [decidable_eq ι] [fintype ι] [normed_group G] [ G] :
G ≃L[𝕜] (λ (i : ι), 𝕜) G

Continuous multilinear maps on `𝕜^n` with values in `G` are in bijection with `G`, as such a continuous multilinear map is completely determined by its value on the constant vector made of ones. We register this bijection as a continuous linear equivalence in `continuous_multilinear_map.pi_field_equiv`.

Equations
theorem continuous_linear_map.norm_comp_continuous_multilinear_map_le {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] [normed_group G'] [ G'] (g : G →L[𝕜] G') (f : G) :
def continuous_linear_map.comp_continuous_multilinear_mapL {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] [normed_group G'] [ G'] :
(G →L[𝕜] G') →L[𝕜] →L[𝕜]

`continuous_linear_map.comp_continuous_multilinear_map` as a bundled continuous bilinear map.

Equations
• continuous_linear_map.comp_continuous_multilinear_mapL = continuous_linear_map.comp_continuous_multilinear_mapL._proof_8 continuous_linear_map.comp_continuous_multilinear_mapL._proof_9 continuous_linear_map.comp_continuous_multilinear_mapL._proof_10 continuous_linear_map.comp_continuous_multilinear_mapL._proof_11).mk_continuous₂ 1 continuous_linear_map.comp_continuous_multilinear_mapL._proof_12
def continuous_linear_map.flip_multilinear {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] [normed_group G'] [ G'] (f : G →L[𝕜] ) :
(G →L[𝕜] G')

Flip arguments in `f : G →L[𝕜] continuous_multilinear_map 𝕜 E G'` to get `continuous_multilinear_map 𝕜 E (G →L[𝕜] G')`

Equations
def multilinear_map.mk_continuous_linear {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] [normed_group G'] [ G'] (f : G →ₗ[𝕜] G') (C : ) (H : ∀ (x : G) (m : Π (i : ι), E i), (f x) m (C * x) * ∏ (i : ι), m i) :
G →L[𝕜]

Given a map `f : G →ₗ[𝕜] multilinear_map 𝕜 E G'` and an estimate `H : ∀ x m, ∥f x m∥ ≤ C * ∥x∥ * ∏ i, ∥m i∥`, construct a continuous linear map from `G` to `continuous_multilinear_map 𝕜 E G'`.

In order to lift, e.g., a map `f : (multilinear_map 𝕜 E G) →ₗ[𝕜] multilinear_map 𝕜 E' G'` to a map `(continuous_multilinear_map 𝕜 E G) →L[𝕜] continuous_multilinear_map 𝕜 E' G'`, one can apply this construction to `f.comp continuous_multilinear_map.to_multilinear_map_linear` which is a linear map from `continuous_multilinear_map 𝕜 E G` to `multilinear_map 𝕜 E' G'`.

Equations
theorem multilinear_map.mk_continuous_linear_norm_le' {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] [normed_group G'] [ G'] (f : G →ₗ[𝕜] G') (C : ) (H : ∀ (x : G) (m : Π (i : ι), E i), (f x) m (C * x) * ∏ (i : ι), m i) :
theorem multilinear_map.mk_continuous_linear_norm_le {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [normed_group G] [ G] [normed_group G'] [ G'] (f : G →ₗ[𝕜] G') {C : } (hC : 0 C) (H : ∀ (x : G) (m : Π (i : ι), E i), (f x) m (C * x) * ∏ (i : ι), m i) :
def multilinear_map.mk_continuous_multilinear {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {E : ι → Type wE} {E' : ι' → Type wE'} {G : Type wG} [decidable_eq ι] [fintype ι] [decidable_eq ι'] [fintype ι'] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [Π (i : ι'), normed_group (E' i)] [Π (i : ι'), (E' i)] [normed_group G] [ G] (f : E' G)) (C : ) (H : ∀ (m₁ : Π (i : ι), E i) (m₂ : Π (i : ι'), E' i), (f m₁) m₂ (C * ∏ (i : ι), m₁ i) * ∏ (i : ι'), m₂ i) :
G)

Given a map `f : multilinear_map 𝕜 E (multilinear_map 𝕜 E' G)` and an estimate `H : ∀ m m', ∥f m m'∥ ≤ C * ∏ i, ∥m i∥ * ∏ i, ∥m' i∥`, upgrade all `multilinear_map`s in the type to `continuous_multilinear_map`s.

Equations
@[simp]
theorem multilinear_map.mk_continuous_multilinear_apply {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {E : ι → Type wE} {E' : ι' → Type wE'} {G : Type wG} [decidable_eq ι] [fintype ι] [decidable_eq ι'] [fintype ι'] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [Π (i : ι'), normed_group (E' i)] [Π (i : ι'), (E' i)] [normed_group G] [ G] (f : E' G)) {C : } (H : ∀ (m₁ : Π (i : ι), E i) (m₂ : Π (i : ι'), E' i), (f m₁) m₂ (C * ∏ (i : ι), m₁ i) * ∏ (i : ι'), m₂ i) (m : Π (i : ι), E i) :
( H) m) = (f m)
theorem multilinear_map.mk_continuous_multilinear_norm_le' {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {E : ι → Type wE} {E' : ι' → Type wE'} {G : Type wG} [decidable_eq ι] [fintype ι] [decidable_eq ι'] [fintype ι'] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [Π (i : ι'), normed_group (E' i)] [Π (i : ι'), (E' i)] [normed_group G] [ G] (f : E' G)) (C : ) (H : ∀ (m₁ : Π (i : ι), E i) (m₂ : Π (i : ι'), E' i), (f m₁) m₂ (C * ∏ (i : ι), m₁ i) * ∏ (i : ι'), m₂ i) :
max C 0
theorem multilinear_map.mk_continuous_multilinear_norm_le {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {E : ι → Type wE} {E' : ι' → Type wE'} {G : Type wG} [decidable_eq ι] [fintype ι] [decidable_eq ι'] [fintype ι'] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [Π (i : ι'), normed_group (E' i)] [Π (i : ι'), (E' i)] [normed_group G] [ G] (f : E' G)) {C : } (hC : 0 C) (H : ∀ (m₁ : Π (i : ι), E i) (m₂ : Π (i : ι'), E' i), (f m₁) m₂ (C * ∏ (i : ι), m₁ i) * ∏ (i : ι'), m₂ i) :
C
theorem continuous_multilinear_map.norm_comp_continuous_linear_le {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [Π (i : ι), normed_group (E₁ i)] [Π (i : ι), (E₁ i)] [normed_group G] [ G] (g : G) (f : Π (i : ι), E i →L[𝕜] E₁ i) :
g * ∏ (i : ι), f i
def continuous_multilinear_map.comp_continuous_linear_mapL {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [Π (i : ι), normed_group (E₁ i)] [Π (i : ι), (E₁ i)] [normed_group G] [ G] (f : Π (i : ι), E i →L[𝕜] E₁ i) :
→L[𝕜]

`continuous_multilinear_map.comp_continuous_linear_map` as a bundled continuous linear map. This implementation fixes `f : Π i, E i →L[𝕜] E₁ i`.

TODO: Actually, the map is multilinear in `f` but an attempt to formalize this failed because of issues with class instances.

Equations
@[simp]
theorem continuous_multilinear_map.comp_continuous_linear_mapL_apply {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [Π (i : ι), normed_group (E₁ i)] [Π (i : ι), (E₁ i)] [normed_group G] [ G] (g : G) (f : Π (i : ι), E i →L[𝕜] E₁ i) :
theorem continuous_multilinear_map.norm_comp_continuous_linear_mapL_le {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} {G : Type wG} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] [Π (i : ι), normed_group (E₁ i)] [Π (i : ι), (E₁ i)] [normed_group G] [ G] (f : Π (i : ι), E i →L[𝕜] E₁ i) :
∏ (i : ι), f i

### Currying #

We associate to a continuous multilinear map in `n+1` variables (i.e., based on `fin n.succ`) two curried functions, named `f.curry_left` (which is a continuous linear map on `E 0` taking values in continuous multilinear maps in `n` variables) and `f.curry_right` (which is a continuous multilinear map in `n` variables taking values in continuous linear maps on `E (last n)`). The inverse operations are called `uncurry_left` and `uncurry_right`.

We also register continuous linear equiv versions of these correspondences, in `continuous_multilinear_curry_left_equiv` and `continuous_multilinear_curry_right_equiv`.

theorem continuous_linear_map.norm_map_tail_le {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : Ei 0 →L[𝕜] (λ (i : fin n), Ei i.succ) G) (m : Π (i : fin n.succ), Ei i) :
(f (m 0)) (fin.tail m) f * ∏ (i : fin n.succ), m i
theorem continuous_multilinear_map.norm_map_init_le {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : (λ (i : fin n), Ei (fin.cast_succ i)) (Ei (fin.last n) →L[𝕜] G)) (m : Π (i : fin n.succ), Ei i) :
(f (fin.init m)) (m (fin.last n)) f * ∏ (i : fin n.succ), m i
theorem continuous_multilinear_map.norm_map_cons_le {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : G) (x : Ei 0) (m : Π (i : fin n), Ei i.succ) :
f (fin.cons x m) (f * x) * ∏ (i : fin n), m i
theorem continuous_multilinear_map.norm_map_snoc_le {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : G) (m : Π (i : fin n), Ei ) (x : Ei (fin.last n)) :
f (fin.snoc m x) (f * ∏ (i : fin n), m i) * x

#### Left currying #

def continuous_linear_map.uncurry_left {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : Ei 0 →L[𝕜] (λ (i : fin n), Ei i.succ) G) :

Given a continuous linear map `f` from `E 0` to continuous multilinear maps on `n` variables, construct the corresponding continuous multilinear map on `n+1` variables obtained by concatenating the variables, given by `m ↦ f (m 0) (tail m)`

Equations
@[simp]
theorem continuous_linear_map.uncurry_left_apply {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : Ei 0 →L[𝕜] (λ (i : fin n), Ei i.succ) G) (m : Π (i : fin n.succ), Ei i) :
(f.uncurry_left) m = (f (m 0)) (fin.tail m)
def continuous_multilinear_map.curry_left {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : G) :
Ei 0 →L[𝕜] (λ (i : fin n), Ei i.succ) G

Given a continuous multilinear map `f` in `n+1` variables, split the first variable to obtain a continuous linear map into continuous multilinear maps in `n` variables, given by `x ↦ (m ↦ f (cons x m))`.

Equations
@[simp]
theorem continuous_multilinear_map.curry_left_apply {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : G) (x : Ei 0) (m : Π (i : fin n), Ei i.succ) :
((f.curry_left) x) m = f (fin.cons x m)
@[simp]
theorem continuous_linear_map.curry_uncurry_left {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : Ei 0 →L[𝕜] (λ (i : fin n), Ei i.succ) G) :
@[simp]
theorem continuous_multilinear_map.uncurry_curry_left {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : G) :
def continuous_multilinear_curry_left_equiv (𝕜 : Type u) {n : } (Ei : fin n.succType wEi) (G : Type wG) [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] :
(Ei 0 →L[𝕜] (λ (i : fin n), Ei i.succ) G) ≃ₗᵢ[𝕜]

The space of continuous multilinear maps on `Π(i : fin (n+1)), E i` is canonically isomorphic to the space of continuous linear maps from `E 0` to the space of continuous multilinear maps on `Π(i : fin n), E i.succ`, by separating the first variable. We register this isomorphism in `continuous_multilinear_curry_left_equiv 𝕜 E E₂`. The algebraic version (without topology) is given in `multilinear_curry_left_equiv 𝕜 E E₂`.

The direct and inverse maps are given by `f.uncurry_left` and `f.curry_left`. Use these unless you need the full framework of linear isometric equivs.

Equations
@[simp]
theorem continuous_multilinear_curry_left_equiv_apply {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : Ei 0 →L[𝕜] (λ (i : fin n), Ei i.succ) G) (v : Π (i : fin n.succ), Ei i) :
( f) v = (f (v 0)) (fin.tail v)
@[simp]
theorem continuous_multilinear_curry_left_equiv_symm_apply {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : G) (x : Ei 0) (v : Π (i : fin n), Ei i.succ) :
((.symm) f) x) v = f (fin.cons x v)
@[simp]
theorem continuous_multilinear_map.curry_left_norm {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : G) :
@[simp]
theorem continuous_linear_map.uncurry_left_norm {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : Ei 0 →L[𝕜] (λ (i : fin n), Ei i.succ) G) :

#### Right currying #

def continuous_multilinear_map.uncurry_right {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : (λ (i : fin n), Ei (fin.cast_succ i)) (Ei (fin.last n) →L[𝕜] G)) :

Given a continuous linear map `f` from continuous multilinear maps on `n` variables to continuous linear maps on `E 0`, construct the corresponding continuous multilinear map on `n+1` variables obtained by concatenating the variables, given by `m ↦ f (init m) (m (last n))`.

Equations
@[simp]
theorem continuous_multilinear_map.uncurry_right_apply {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : (λ (i : fin n), Ei (fin.cast_succ i)) (Ei (fin.last n) →L[𝕜] G)) (m : Π (i : fin n.succ), Ei i) :
def continuous_multilinear_map.curry_right {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : G) :
(λ (i : fin n), Ei (fin.cast_succ i)) (Ei (fin.last n) →L[𝕜] G)

Given a continuous multilinear map `f` in `n+1` variables, split the last variable to obtain a continuous multilinear map in `n` variables into continuous linear maps, given by `m ↦ (x ↦ f (snoc m x))`.

Equations
@[simp]
theorem continuous_multilinear_map.curry_right_apply {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : G) (m : Π (i : fin n), Ei ) (x : Ei (fin.last n)) :
((f.curry_right) m) x = f (fin.snoc m x)
@[simp]
theorem continuous_multilinear_map.curry_uncurry_right {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : (λ (i : fin n), Ei (fin.cast_succ i)) (Ei (fin.last n) →L[𝕜] G)) :
@[simp]
theorem continuous_multilinear_map.uncurry_curry_right {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : G) :
def continuous_multilinear_curry_right_equiv (𝕜 : Type u) {n : } (Ei : fin n.succType wEi) (G : Type wG) [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] :
(λ (i : fin n), Ei (fin.cast_succ i)) (Ei (fin.last n) →L[𝕜] G) ≃ₗᵢ[𝕜]

The space of continuous multilinear maps on `Π(i : fin (n+1)), Ei i` is canonically isomorphic to the space of continuous multilinear maps on `Π(i : fin n), Ei i.cast_succ` with values in the space of continuous linear maps on `Ei (last n)`, by separating the last variable. We register this isomorphism as a continuous linear equiv in `continuous_multilinear_curry_right_equiv 𝕜 Ei G`. The algebraic version (without topology) is given in `multilinear_curry_right_equiv 𝕜 Ei G`.

The direct and inverse maps are given by `f.uncurry_right` and `f.curry_right`. Use these unless you need the full framework of linear isometric equivs.

Equations
def continuous_multilinear_curry_right_equiv' (𝕜 : Type u) (n : ) (G : Type wG) (G' : Type wG') [normed_group G] [ G] [normed_group G'] [ G'] :
(λ (i : fin n), G) (G →L[𝕜] G') ≃ₗᵢ[𝕜] (λ (i : fin n.succ), G) G'

The space of continuous multilinear maps on `Π(i : fin (n+1)), G` is canonically isomorphic to the space of continuous multilinear maps on `Π(i : fin n), G` with values in the space of continuous linear maps on `G`, by separating the last variable. We register this isomorphism as a continuous linear equiv in `continuous_multilinear_curry_right_equiv' 𝕜 n G G'`. For a version allowing dependent types, see `continuous_multilinear_curry_right_equiv`. When there are no dependent types, use the primed version as it helps Lean a lot for unification.

The direct and inverse maps are given by `f.uncurry_right` and `f.curry_right`. Use these unless you need the full framework of linear isometric equivs.

Equations
@[simp]
theorem continuous_multilinear_curry_right_equiv_apply {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : (λ (i : fin n), Ei (fin.cast_succ i)) (Ei (fin.last n) →L[𝕜] G)) (v : Π (i : fin n.succ), Ei i) :
f) v = (f (fin.init v)) (v (fin.last n))
@[simp]
theorem continuous_multilinear_curry_right_equiv_symm_apply {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : G) (v : Π (i : fin n), Ei ) (x : Ei (fin.last n)) :
((.symm) f) v) x = f (fin.snoc v x)
@[simp]
theorem continuous_multilinear_curry_right_equiv_apply' {𝕜 : Type u} {n : } {G : Type wG} {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] (f : (λ (i : fin n), G) (G →L[𝕜] G')) (v : fin n.succ → G) :
( f) v = (f (fin.init v)) (v (fin.last n))
@[simp]
theorem continuous_multilinear_curry_right_equiv_symm_apply' {𝕜 : Type u} {n : } {G : Type wG} {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] (f : (λ (i : fin n.succ), G) G') (v : fin n → G) (x : G) :
(( G').symm) f) v) x = f (fin.snoc v x)
@[simp]
theorem continuous_multilinear_map.curry_right_norm {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : G) :
@[simp]
theorem continuous_multilinear_map.uncurry_right_norm {𝕜 : Type u} {n : } {Ei : fin n.succType wEi} {G : Type wG} [Π (i : fin n.succ), normed_group (Ei i)] [Π (i : fin n.succ), (Ei i)] [normed_group G] [ G] (f : (λ (i : fin n), Ei (fin.cast_succ i)) (Ei (fin.last n) →L[𝕜] G)) :

#### Currying with `0` variables #

The space of multilinear maps with `0` variables is trivial: such a multilinear map is just an arbitrary constant (note that multilinear maps in `0` variables need not map `0` to `0`!). Therefore, the space of continuous multilinear maps on `(fin 0) → G` with values in `E₂` is isomorphic (and even isometric) to `E₂`. As this is the zeroth step in the construction of iterated derivatives, we register this isomorphism.

def continuous_multilinear_map.uncurry0 {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] (f : (λ (i : fin 0), G) G') :
G'

Associating to a continuous multilinear map in `0` variables the unique value it takes.

Equations
def continuous_multilinear_map.curry0 (𝕜 : Type u) (G : Type wG) {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] (x : G') :
(λ (i : fin 0), G) G'

Associating to an element `x` of a vector space `E₂` the continuous multilinear map in `0` variables taking the (unique) value `x`

Equations
@[simp]
theorem continuous_multilinear_map.curry0_apply (𝕜 : Type u) {G : Type wG} {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] (x : G') (m : fin 0 → G) :
m = x
@[simp]
theorem continuous_multilinear_map.uncurry0_apply {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] (f : (λ (i : fin 0), G) G') :
@[simp]
theorem continuous_multilinear_map.apply_zero_curry0 {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] (f : (λ (i : fin 0), G) G') {x : fin 0 → G} :
(f x) = f
theorem continuous_multilinear_map.uncurry0_curry0 {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] (f : (λ (i : fin 0), G) G') :
@[simp]
theorem continuous_multilinear_map.curry0_uncurry0 (𝕜 : Type u) (G : Type wG) {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] (x : G') :
@[simp]
theorem continuous_multilinear_map.curry0_norm (𝕜 : Type u) (G : Type wG) {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] (x : G') :
@[simp]
theorem continuous_multilinear_map.fin0_apply_norm {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] (f : (λ (i : fin 0), G) G') {x : fin 0 → G} :
theorem continuous_multilinear_map.uncurry0_norm {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] (f : (λ (i : fin 0), G) G') :
def continuous_multilinear_curry_fin0 (𝕜 : Type u) (G : Type wG) (G' : Type wG') [normed_group G] [ G] [normed_group G'] [ G'] :
(λ (i : fin 0), G) G' ≃ₗᵢ[𝕜] G'

The continuous linear isomorphism between elements of a normed space, and continuous multilinear maps in `0` variables with values in this normed space.

The direct and inverse maps are `uncurry0` and `curry0`. Use these unless you need the full framework of linear isometric equivs.

Equations
@[simp]
theorem continuous_multilinear_curry_fin0_apply {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] (f : (λ (i : fin 0), G) G') :
f = f 0
@[simp]
theorem continuous_multilinear_curry_fin0_symm_apply {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] (x : G') (v : fin 0 → G) :
( G').symm) x) v = x

#### With 1 variable #

def continuous_multilinear_curry_fin1 (𝕜 : Type u) (G : Type wG) (G' : Type wG') [normed_group G] [ G] [normed_group G'] [ G'] :
(λ (i : fin 1), G) G' ≃ₗᵢ[𝕜] G →L[𝕜] G'

Continuous multilinear maps from `G^1` to `G'` are isomorphic with continuous linear maps from `G` to `G'`.

Equations
@[simp]
theorem continuous_multilinear_curry_fin1_apply {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] (f : (λ (i : fin 1), G) G') (x : G) :
( f) x = f (fin.snoc 0 x)
@[simp]
theorem continuous_multilinear_curry_fin1_symm_apply {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] (f : G →L[𝕜] G') (v : fin 1 → G) :
( G').symm) f) v = f (v 0)
def continuous_multilinear_map.dom_dom_congr (𝕜 : Type u) {ι : Type v} {ι' : Type v'} (G : Type wG) (G' : Type wG') [decidable_eq ι] [fintype ι] [decidable_eq ι'] [fintype ι'] [normed_group G] [ G] [normed_group G'] [ G'] (σ : ι ι') :
(λ (_x : ι), G) G' ≃ₗᵢ[𝕜] (λ (_x : ι'), G) G'

An equivalence of the index set defines a linear isometric equivalence between the spaces of multilinear maps.

Equations
def continuous_multilinear_map.curry_sum {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {G : Type wG} {G' : Type wG'} [decidable_eq ι] [fintype ι] [decidable_eq ι'] [fintype ι'] [normed_group G] [ G] [normed_group G'] [ G'] [decidable_eq ι')] (f : (λ (x : ι ι'), G) G') :
(λ (x : ι), G) (λ (x : ι'), G) G')

A continuous multilinear map with variables indexed by `ι ⊕ ι'` defines a continuous multilinear map with variables indexed by `ι` taking values in the space of continuous multilinear maps with variables indexed by `ι'`.

Equations
@[simp]
theorem continuous_multilinear_map.curry_sum_apply {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {G : Type wG} {G' : Type wG'} [decidable_eq ι] [fintype ι] [decidable_eq ι'] [fintype ι'] [normed_group G] [ G] [normed_group G'] [ G'] [decidable_eq ι')] (f : (λ (x : ι ι'), G) G') (m : ι → G) (m' : ι' → G) :
((f.curry_sum) m) m' = f (sum.elim m m')
def continuous_multilinear_map.uncurry_sum {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {G : Type wG} {G' : Type wG'} [decidable_eq ι] [fintype ι] [decidable_eq ι'] [fintype ι'] [normed_group G] [ G] [normed_group G'] [ G'] [decidable_eq ι')] (f : (λ (x : ι), G) (λ (x : ι'), G) G')) :
(λ (x : ι ι'), G) G'

A continuous multilinear map with variables indexed by `ι` taking values in the space of continuous multilinear maps with variables indexed by `ι'` defines a continuous multilinear map with variables indexed by `ι ⊕ ι'`.

Equations
@[simp]
theorem continuous_multilinear_map.uncurry_sum_apply {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {G : Type wG} {G' : Type wG'} [decidable_eq ι] [fintype ι] [decidable_eq ι'] [fintype ι'] [normed_group G] [ G] [normed_group G'] [ G'] [decidable_eq ι')] (f : (λ (x : ι), G) (λ (x : ι'), G) G')) (m : ι ι' → G) :
def continuous_multilinear_map.curry_sum_equiv (𝕜 : Type u) (ι : Type v) (ι' : Type v') (G : Type wG) (G' : Type wG') [decidable_eq ι] [fintype ι] [decidable_eq ι'] [fintype ι'] [normed_group G] [ G] [normed_group G'] [ G'] [decidable_eq ι')] :
(λ (x : ι ι'), G) G' ≃ₗᵢ[𝕜] (λ (x : ι), G) (λ (x : ι'), G) G')

Linear isometric equivalence between the space of continuous multilinear maps with variables indexed by `ι ⊕ ι'` and the space of continuous multilinear maps with variables indexed by `ι` taking values in the space of continuous multilinear maps with variables indexed by `ι'`.

The forward and inverse functions are `continuous_multilinear_map.curry_sum` and `continuous_multilinear_map.uncurry_sum`. Use this definition only if you need some properties of `linear_isometry_equiv`.

Equations
def continuous_multilinear_map.curry_fin_finset (𝕜 : Type u) (G : Type wG) (G' : Type wG') [normed_group G] [ G] [normed_group G'] [ G'] {k l n : } {s : finset (fin n)} (hk : s.card = k) (hl : s.card = l) :
(λ (i : fin n), G) G' ≃ₗᵢ[𝕜] (λ (i : fin k), G) (λ (i : fin l), G) G')

If `s : finset (fin n)` is a finite set of cardinality `k` and its complement has cardinality `l`, then the space of continuous multilinear maps `G [×n]→L[𝕜] G'` of `n` variables is isomorphic to the space of continuous multilinear maps `G [×k]→L[𝕜] G [×l]→L[𝕜] G'` of `k` variables taking values in the space of continuous multilinear maps of `l` variables.

Equations
@[simp]
theorem continuous_multilinear_map.curry_fin_finset_apply {𝕜 : Type u} {n : } {G : Type wG} {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] {k l : } {s : finset (fin n)} (hk : s.card = k) (hl : s.card = l) (f : (λ (i : fin n), G) G') (mk : fin k → G) (ml : fin l → G) :
(( hl) f) mk) ml = f (λ (i : fin n), sum.elim mk ml ( hl).symm) i))
@[simp]
theorem continuous_multilinear_map.curry_fin_finset_symm_apply {𝕜 : Type u} {n : } {G : Type wG} {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] {k l : } {s : finset (fin n)} (hk : s.card = k) (hl : s.card = l) (f : (λ (i : fin k), G) (λ (i : fin l), G) G')) (m : fin n → G) :
( hk hl).symm) f) m = (f (λ (i : fin k), m ( hl) (sum.inl i)))) (λ (i : fin l), m ( hl) (sum.inr i)))
@[simp]
theorem continuous_multilinear_map.curry_fin_finset_symm_apply_piecewise_const {𝕜 : Type u} {n : } {G : Type wG} {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] {k l : } {s : finset (fin n)} (hk : s.card = k) (hl : s.card = l) (f : (λ (i : fin k), G) (λ (i : fin l), G) G')) (x y : G) :
( hk hl).symm) f) (s.piecewise (λ (_x : fin n), x) (λ (_x : fin n), y)) = (f (λ (_x : fin k), x)) (λ (_x : fin l), y)
@[simp]
theorem continuous_multilinear_map.curry_fin_finset_symm_apply_const {𝕜 : Type u} {n : } {G : Type wG} {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] {k l : } {s : finset (fin n)} (hk : s.card = k) (hl : s.card = l) (f : (λ (i : fin k), G) (λ (i : fin l), G) G')) (x : G) :
( hk hl).symm) f) (λ (_x : fin n), x) = (f (λ (_x : fin k), x)) (λ (_x : fin l), x)
@[simp]
theorem continuous_multilinear_map.curry_fin_finset_apply_const {𝕜 : Type u} {n : } {G : Type wG} {G' : Type wG'} [normed_group G] [ G] [normed_group G'] [ G'] {k l : } {s : finset (fin n)} (hk : s.card = k) (hl : s.card = l) (f : (λ (i : fin n), G) G') (x y : G) :
(( hl) f) (λ (_x : fin k), x)) (λ (_x : fin l), y) = f (s.piecewise (λ (_x : fin n), x) (λ (_x : fin n), y))