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_continuousasserts that, iffis continuous, then there existsC > 0with‖f m‖ ≤ C * ∏ i, ‖m i‖for allm.continuous_of_bound, conversely, asserts that this bound implies continuity.mkContinuousconstructs 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 allm.le_op_norm f masserts the fundamental inequality‖f m‖ ≤ ‖f‖ * ∏ i, ‖m i‖.norm_image_sub_le f m₁ m₂gives a control of the differencef 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.curryLeft and f.curryRight respectively (with inverses f.uncurryLeft and
f.uncurryRight). 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
continuousMultilinearCurryLeftEquiv and continuousMultilinearCurryRightEquiv.
Implementation notes #
We mostly follow the API (and the proofs) of OperatorNorm.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:
𝕜: aNontriviallyNormedField;ι,ι': finite index types with decidable equality;E,E₁: families of normed vector spaces over𝕜indexed byi : ι;E': a family of normed vector spaces over𝕜indexed byi' : ι';Ei: a family of normed vector spaces over𝕜indexed byi : 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
MultilinearMap.bound_of_shell
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : MultilinearMap 𝕜 E 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 * Finset.prod Finset.univ fun i => ‖m i‖)
(m : (i : ι) → E 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
MultilinearMap.exists_bound_of_continuous
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : MultilinearMap 𝕜 E G)
(hf : Continuous ↑f)
:
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
MultilinearMap.norm_image_sub_le_of_bound'
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : MultilinearMap 𝕜 E G)
[DecidableEq ι]
{C : ℝ}
(hC : 0 ≤ C)
(H : ∀ (m : (i : ι) → E i), ‖↑f m‖ ≤ C * Finset.prod Finset.univ fun i => ‖m i‖)
(m₁ : (i : ι) → E i)
(m₂ : (i : ι) → E i)
:
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
MultilinearMap.norm_image_sub_le_of_bound
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : MultilinearMap 𝕜 E G)
{C : ℝ}
(hC : 0 ≤ C)
(H : ∀ (m : (i : ι) → E i), ‖↑f m‖ ≤ C * Finset.prod Finset.univ fun i => ‖m i‖)
(m₁ : (i : ι) → E i)
(m₂ : (i : ι) → E i)
:
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
MultilinearMap.continuous_of_bound
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : MultilinearMap 𝕜 E G)
(C : ℝ)
(H : ∀ (m : (i : ι) → E i), ‖↑f m‖ ≤ C * Finset.prod Finset.univ fun i => ‖m i‖)
:
Continuous ↑f
If a multilinear map satisfies an inequality ‖f m‖ ≤ C * ∏ i, ‖m i‖, then it is
continuous.
def
MultilinearMap.mkContinuous
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : MultilinearMap 𝕜 E G)
(C : ℝ)
(H : ∀ (m : (i : ι) → E i), ‖↑f m‖ ≤ C * Finset.prod Finset.univ fun i => ‖m i‖)
:
ContinuousMultilinearMap 𝕜 E G
Constructing a continuous multilinear map from a multilinear map satisfying a boundedness condition.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
MultilinearMap.coe_mkContinuous
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : MultilinearMap 𝕜 E G)
(C : ℝ)
(H : ∀ (m : (i : ι) → E i), ‖↑f m‖ ≤ C * Finset.prod Finset.univ fun i => ‖m i‖)
:
↑(MultilinearMap.mkContinuous f C H) = ↑f
theorem
MultilinearMap.restr_norm_le
{𝕜 : Type u}
{G : Type wG}
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
{k : ℕ}
{n : ℕ}
(f : MultilinearMap 𝕜 (fun x => G) G')
(s : Finset (Fin n))
(hk : Finset.card s = k)
(z : G)
{C : ℝ}
(H : ∀ (m : Fin n → G), ‖↑f m‖ ≤ C * Finset.prod Finset.univ fun i => ‖m i‖)
(v : Fin k → G)
:
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 ContinuousMultilinearMap 𝕜 E G.
theorem
ContinuousMultilinearMap.bound
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G)
:
def
ContinuousMultilinearMap.opNorm
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G)
:
The operator norm of a continuous multilinear map is the inf of all its bounds.
Equations
Instances For
instance
ContinuousMultilinearMap.hasOpNorm
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
:
Norm (ContinuousMultilinearMap 𝕜 E G)
Equations
- ContinuousMultilinearMap.hasOpNorm = { norm := ContinuousMultilinearMap.opNorm }
instance
ContinuousMultilinearMap.hasOpNorm'
{𝕜 : Type u}
{ι : Type v}
{G : Type wG}
{G' : Type wG'}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
:
Norm (ContinuousMultilinearMap 𝕜 (fun x => G) G')
An alias of ContinuousMultilinearMap.hasOpNorm with non-dependent types to help typeclass
search.
Equations
- ContinuousMultilinearMap.hasOpNorm' = ContinuousMultilinearMap.hasOpNorm
theorem
ContinuousMultilinearMap.norm_def
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G)
:
theorem
ContinuousMultilinearMap.bounds_nonempty
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : ContinuousMultilinearMap 𝕜 E G}
:
theorem
ContinuousMultilinearMap.bounds_bddBelow
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : ContinuousMultilinearMap 𝕜 E G}
:
theorem
ContinuousMultilinearMap.isLeast_op_norm
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G)
:
theorem
ContinuousMultilinearMap.op_norm_nonneg
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G)
:
theorem
ContinuousMultilinearMap.le_op_norm
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G)
(m : (i : ι) → E 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
ContinuousMultilinearMap.le_mul_prod_of_le_op_norm_of_le
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : ContinuousMultilinearMap 𝕜 E G}
{m : (i : ι) → E i}
{C : ℝ}
{b : ι → ℝ}
(hC : ‖f‖ ≤ C)
(hm : ∀ (i : ι), ‖m i‖ ≤ b i)
:
‖↑f m‖ ≤ C * Finset.prod Finset.univ fun i => b i
theorem
ContinuousMultilinearMap.le_op_norm_mul_prod_of_le
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G)
{m : (i : ι) → E i}
{b : ι → ℝ}
(hm : ∀ (i : ι), ‖m i‖ ≤ b i)
:
theorem
ContinuousMultilinearMap.le_op_norm_mul_pow_card_of_le
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G)
{m : (i : ι) → E i}
{b : ℝ}
(hm : ‖m‖ ≤ b)
:
theorem
ContinuousMultilinearMap.le_op_norm_mul_pow_of_le
{𝕜 : Type u}
{n : ℕ}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{Ei : Fin n → Type u_1}
[(i : Fin n) → NormedAddCommGroup (Ei i)]
[(i : Fin n) → NormedSpace 𝕜 (Ei i)]
(f : ContinuousMultilinearMap 𝕜 Ei G)
{m : (i : Fin n) → Ei i}
{b : ℝ}
(hm : ‖m‖ ≤ b)
:
theorem
ContinuousMultilinearMap.le_of_op_norm_le
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : ContinuousMultilinearMap 𝕜 E G}
(m : (i : ι) → E i)
{C : ℝ}
(h : ‖f‖ ≤ C)
:
theorem
ContinuousMultilinearMap.ratio_le_op_norm
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G)
(m : (i : ι) → E i)
:
theorem
ContinuousMultilinearMap.unit_le_op_norm
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G)
(m : (i : ι) → E i)
(h : ‖m‖ ≤ 1)
:
The image of the unit ball under a continuous multilinear map is bounded.
theorem
ContinuousMultilinearMap.op_norm_le_bound
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G)
{M : ℝ}
(hMp : 0 ≤ M)
(hM : ∀ (m : (i : ι) → E i), ‖↑f m‖ ≤ M * Finset.prod Finset.univ fun i => ‖m i‖)
:
If one controls the norm of every f x, then one controls the norm of f.
theorem
ContinuousMultilinearMap.op_norm_le_iff
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G)
{C : ℝ}
(hC : 0 ≤ C)
:
theorem
ContinuousMultilinearMap.op_norm_add_le
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G)
(g : ContinuousMultilinearMap 𝕜 E G)
:
The operator norm satisfies the triangle inequality.
theorem
ContinuousMultilinearMap.op_norm_zero
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
:
theorem
ContinuousMultilinearMap.op_norm_zero_iff
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G)
:
A continuous linear map is zero iff its norm vanishes.
theorem
ContinuousMultilinearMap.op_norm_smul_le
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G)
{𝕜' : Type u_1}
[NormedField 𝕜']
[NormedSpace 𝕜' G]
[SMulCommClass 𝕜 𝕜' G]
(c : 𝕜')
:
theorem
ContinuousMultilinearMap.op_norm_neg
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G)
:
instance
ContinuousMultilinearMap.normedAddCommGroup
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
:
Continuous multilinear maps themselves form a normed space with respect to the operator norm.
Equations
- One or more equations did not get rendered due to their size.
instance
ContinuousMultilinearMap.normedAddCommGroup'
{𝕜 : Type u}
{ι : Type v}
{G : Type wG}
{G' : Type wG'}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
:
NormedAddCommGroup (ContinuousMultilinearMap 𝕜 (fun x => G) G')
An alias of ContinuousMultilinearMap.normedAddCommGroup with non-dependent types to help
typeclass search.
Equations
- ContinuousMultilinearMap.normedAddCommGroup' = ContinuousMultilinearMap.normedAddCommGroup
instance
ContinuousMultilinearMap.normedSpace
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{𝕜' : Type u_1}
[NormedField 𝕜']
[NormedSpace 𝕜' G]
[SMulCommClass 𝕜 𝕜' G]
:
NormedSpace 𝕜' (ContinuousMultilinearMap 𝕜 E G)
instance
ContinuousMultilinearMap.normedSpace'
{𝕜 : Type u}
{ι : Type v}
{G : Type wG}
{G' : Type wG'}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
{𝕜' : Type u_1}
[NormedField 𝕜']
[NormedSpace 𝕜' G]
[SMulCommClass 𝕜 𝕜' G]
:
NormedSpace 𝕜' (ContinuousMultilinearMap 𝕜 (fun x => G') G)
An alias of ContinuousMultilinearMap.normedSpace with non-dependent types to help typeclass
search.
Equations
- ContinuousMultilinearMap.normedSpace' = ContinuousMultilinearMap.normedSpace
theorem
ContinuousMultilinearMap.le_op_nnnorm
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G)
(m : (i : ι) → E 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‖, nnnorm version.
theorem
ContinuousMultilinearMap.le_of_op_nnnorm_le
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G)
(m : (i : ι) → E i)
{C : NNReal}
(h : ‖f‖₊ ≤ C)
:
theorem
ContinuousMultilinearMap.op_nnnorm_le_iff
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G)
{C : NNReal}
:
theorem
ContinuousMultilinearMap.isLeast_op_nnnorm
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G)
:
theorem
ContinuousMultilinearMap.op_nnnorm_prod
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
{G' : Type wG'}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(f : ContinuousMultilinearMap 𝕜 E G)
(g : ContinuousMultilinearMap 𝕜 E G')
:
theorem
ContinuousMultilinearMap.op_norm_prod
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
{G' : Type wG'}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(f : ContinuousMultilinearMap 𝕜 E G)
(g : ContinuousMultilinearMap 𝕜 E G')
:
theorem
ContinuousMultilinearMap.op_nnnorm_pi
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
{ι' : Type v'}
[Fintype ι']
{E' : ι' → Type wE'}
[(i' : ι') → NormedAddCommGroup (E' i')]
[(i' : ι') → NormedSpace 𝕜 (E' i')]
(f : (i' : ι') → ContinuousMultilinearMap 𝕜 E (E' i'))
:
theorem
ContinuousMultilinearMap.op_norm_pi
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
{ι' : Type v'}
[Fintype ι']
{E' : ι' → Type wE'}
[(i' : ι') → NormedAddCommGroup (E' i')]
[(i' : ι') → NormedSpace 𝕜 (E' i')]
(f : (i' : ι') → ContinuousMultilinearMap 𝕜 E (E' i'))
:
theorem
ContinuousMultilinearMap.norm_ofSubsingleton_le
(𝕜 : Type u)
{ι : Type v}
(G : Type wG)
[Fintype ι]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[Subsingleton ι]
(i' : ι)
:
@[simp]
theorem
ContinuousMultilinearMap.norm_ofSubsingleton
(𝕜 : Type u)
{ι : Type v}
(G : Type wG)
[Fintype ι]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[Subsingleton ι]
[Nontrivial G]
(i' : ι)
:
theorem
ContinuousMultilinearMap.nnnorm_ofSubsingleton_le
(𝕜 : Type u)
{ι : Type v}
(G : Type wG)
[Fintype ι]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[Subsingleton ι]
(i' : ι)
:
@[simp]
theorem
ContinuousMultilinearMap.nnnorm_ofSubsingleton
(𝕜 : Type u)
{ι : Type v}
(G : Type wG)
[Fintype ι]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[Subsingleton ι]
[Nontrivial G]
(i' : ι)
:
@[simp]
theorem
ContinuousMultilinearMap.norm_constOfIsEmpty
(𝕜 : Type u)
{ι : Type v}
(E : ι → Type wE)
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[IsEmpty ι]
(x : G)
:
@[simp]
theorem
ContinuousMultilinearMap.nnnorm_constOfIsEmpty
(𝕜 : Type u)
{ι : Type v}
(E : ι → Type wE)
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[IsEmpty ι]
(x : G)
:
def
ContinuousMultilinearMap.prodL
(𝕜 : Type u)
{ι : Type v}
(E : ι → Type wE)
(G : Type wG)
(G' : Type wG')
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
:
ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G' ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 E (G × G')
ContinuousMultilinearMap.prod as a LinearIsometryEquiv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
ContinuousMultilinearMap.piₗᵢ
(𝕜 : Type u)
{ι : Type v}
(E : ι → Type wE)
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
{ι' : Type v'}
[Fintype ι']
{E' : ι' → Type wE'}
[(i' : ι') → NormedAddCommGroup (E' i')]
[(i' : ι') → NormedSpace 𝕜 (E' i')]
:
((i' : ι') → ContinuousMultilinearMap 𝕜 E (E' i')) ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 E ((i : ι') → E' i)
ContinuousMultilinearMap.pi as a LinearIsometryEquiv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
ContinuousMultilinearMap.norm_restrictScalars
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G)
{𝕜' : Type u_1}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜' 𝕜]
[NormedSpace 𝕜' G]
[IsScalarTower 𝕜' 𝕜 G]
[(i : ι) → NormedSpace 𝕜' (E i)]
[∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)]
:
def
ContinuousMultilinearMap.restrictScalarsₗᵢ
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(𝕜' : Type u_1)
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜' 𝕜]
[NormedSpace 𝕜' G]
[IsScalarTower 𝕜' 𝕜 G]
[(i : ι) → NormedSpace 𝕜' (E i)]
[∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)]
:
ContinuousMultilinearMap 𝕜 E G →ₗᵢ[𝕜'] ContinuousMultilinearMap 𝕜' E G
ContinuousMultilinearMap.restrictScalars as a LinearIsometry.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
ContinuousMultilinearMap.restrictScalarsLinear
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(𝕜' : Type u_1)
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜' 𝕜]
[NormedSpace 𝕜' G]
[IsScalarTower 𝕜' 𝕜 G]
[(i : ι) → NormedSpace 𝕜' (E i)]
[∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)]
:
ContinuousMultilinearMap 𝕜 E G →L[𝕜'] ContinuousMultilinearMap 𝕜' E G
ContinuousMultilinearMap.restrictScalars as a ContinuousLinearMap.
Equations
Instances For
theorem
ContinuousMultilinearMap.continuous_restrictScalars
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{𝕜' : Type u_1}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜' 𝕜]
[NormedSpace 𝕜' G]
[IsScalarTower 𝕜' 𝕜 G]
[(i : ι) → NormedSpace 𝕜' (E i)]
[∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)]
:
theorem
ContinuousMultilinearMap.norm_image_sub_le'
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G)
[DecidableEq ι]
(m₁ : (i : ι) → E i)
(m₂ : (i : ι) → E i)
:
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
ContinuousMultilinearMap.norm_image_sub_le
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G)
(m₁ : (i : ι) → E i)
(m₂ : (i : ι) → E i)
:
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
ContinuousMultilinearMap.continuous_eval
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
:
Continuous fun p => ↑p.fst p.snd
Applying a multilinear map to a vector is continuous in both coordinates.
theorem
ContinuousMultilinearMap.continuous_eval_left
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(m : (i : ι) → E i)
:
Continuous fun p => ↑p m
theorem
ContinuousMultilinearMap.hasSum_eval
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{α : Type u_1}
{p : α → ContinuousMultilinearMap 𝕜 E G}
{q : ContinuousMultilinearMap 𝕜 E G}
(h : HasSum p q)
(m : (i : ι) → E i)
:
HasSum (fun a => ↑(p a) m) (↑q m)
theorem
ContinuousMultilinearMap.tsum_eval
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{α : Type u_1}
{p : α → ContinuousMultilinearMap 𝕜 E G}
(hp : Summable p)
(m : (i : ι) → E i)
:
↑(∑' (a : α), p a) m = ∑' (a : α), ↑(p a) m
instance
ContinuousMultilinearMap.completeSpace
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[CompleteSpace 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
MultilinearMap.mkContinuous_norm_le
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : MultilinearMap 𝕜 E G)
{C : ℝ}
(hC : 0 ≤ C)
(H : ∀ (m : (i : ι) → E i), ‖↑f m‖ ≤ C * Finset.prod Finset.univ fun i => ‖m i‖)
:
‖MultilinearMap.mkContinuous f C H‖ ≤ C
If a continuous multilinear map is constructed from a multilinear map via the constructor
mkContinuous, then its norm is bounded by the bound given to the constructor if it is
nonnegative.
theorem
MultilinearMap.mkContinuous_norm_le'
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : MultilinearMap 𝕜 E G)
{C : ℝ}
(H : ∀ (m : (i : ι) → E i), ‖↑f m‖ ≤ C * Finset.prod Finset.univ fun i => ‖m i‖)
:
‖MultilinearMap.mkContinuous f C H‖ ≤ max C 0
If a continuous multilinear map is constructed from a multilinear map via the constructor
mkContinuous, then its norm is bounded by the bound given to the constructor if it is
nonnegative.
def
ContinuousMultilinearMap.restr
{𝕜 : Type u}
{G : Type wG}
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
{k : ℕ}
{n : ℕ}
(f : ContinuousMultilinearMap 𝕜 (fun i => G) G')
(s : Finset (Fin n))
(hk : Finset.card s = k)
(z : G)
:
ContinuousMultilinearMap 𝕜 (fun i => 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
- One or more equations did not get rendered due to their size.
Instances For
theorem
ContinuousMultilinearMap.norm_restr
{𝕜 : Type u}
{G : Type wG}
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
{k : ℕ}
{n : ℕ}
(f : ContinuousMultilinearMap 𝕜 (fun i => G) G')
(s : Finset (Fin n))
(hk : Finset.card s = k)
(z : G)
:
@[simp]
theorem
ContinuousMultilinearMap.norm_mkPiAlgebra_le
{𝕜 : Type u}
{ι : Type v}
[Fintype ι]
[NontriviallyNormedField 𝕜]
{A : Type u_1}
[NormedCommRing A]
[NormedAlgebra 𝕜 A]
[Nonempty ι]
:
theorem
ContinuousMultilinearMap.norm_mkPiAlgebra_of_empty
{𝕜 : Type u}
{ι : Type v}
[Fintype ι]
[NontriviallyNormedField 𝕜]
{A : Type u_1}
[NormedCommRing A]
[NormedAlgebra 𝕜 A]
[IsEmpty ι]
:
@[simp]
theorem
ContinuousMultilinearMap.norm_mkPiAlgebra
{𝕜 : Type u}
{ι : Type v}
[Fintype ι]
[NontriviallyNormedField 𝕜]
{A : Type u_1}
[NormedCommRing A]
[NormedAlgebra 𝕜 A]
[NormOneClass A]
:
theorem
ContinuousMultilinearMap.norm_mkPiAlgebraFin_succ_le
{𝕜 : Type u}
{n : ℕ}
[NontriviallyNormedField 𝕜]
{A : Type u_1}
[NormedRing A]
[NormedAlgebra 𝕜 A]
:
theorem
ContinuousMultilinearMap.norm_mkPiAlgebraFin_le_of_pos
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
{A : Type u_1}
[NormedRing A]
[NormedAlgebra 𝕜 A]
(hn : 0 < n)
:
theorem
ContinuousMultilinearMap.norm_mkPiAlgebraFin_zero
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{A : Type u_1}
[NormedRing A]
[NormedAlgebra 𝕜 A]
:
@[simp]
theorem
ContinuousMultilinearMap.norm_mkPiAlgebraFin
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
{A : Type u_1}
[NormedRing A]
[NormedAlgebra 𝕜 A]
[NormOneClass A]
:
def
ContinuousMultilinearMap.mkPiField
(𝕜 : Type u)
(ι : Type v)
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(z : G)
:
ContinuousMultilinearMap 𝕜 (fun x => 𝕜) 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
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
ContinuousMultilinearMap.mkPiField_apply
{𝕜 : Type u}
{ι : Type v}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(z : G)
(m : ι → 𝕜)
:
↑(ContinuousMultilinearMap.mkPiField 𝕜 ι z) m = (Finset.prod Finset.univ fun i => m i) • z
theorem
ContinuousMultilinearMap.mkPiField_apply_one_eq_self
{𝕜 : Type u}
{ι : Type v}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 (fun x => 𝕜) G)
:
ContinuousMultilinearMap.mkPiField 𝕜 ι (↑f fun x => 1) = f
@[simp]
theorem
ContinuousMultilinearMap.norm_mkPiField
{𝕜 : Type u}
{ι : Type v}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(z : G)
:
theorem
ContinuousMultilinearMap.mkPiField_eq_iff
{𝕜 : Type u}
{ι : Type v}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{z₁ : G}
{z₂ : G}
:
ContinuousMultilinearMap.mkPiField 𝕜 ι z₁ = ContinuousMultilinearMap.mkPiField 𝕜 ι z₂ ↔ z₁ = z₂
theorem
ContinuousMultilinearMap.mkPiField_zero
{𝕜 : Type u}
{ι : Type v}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
:
ContinuousMultilinearMap.mkPiField 𝕜 ι 0 = 0
theorem
ContinuousMultilinearMap.mkPiField_eq_zero_iff
{𝕜 : Type u}
{ι : Type v}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(z : G)
:
ContinuousMultilinearMap.mkPiField 𝕜 ι z = 0 ↔ z = 0
def
ContinuousMultilinearMap.piFieldEquiv
(𝕜 : Type u)
(ι : Type v)
(G : Type wG)
[Fintype ι]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
:
G ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun x => 𝕜) 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 isometry in
ContinuousMultilinearMap.piFieldEquiv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ContinuousLinearMap.norm_compContinuousMultilinearMap_le
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
{G' : Type wG'}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(g : G →L[𝕜] G')
(f : ContinuousMultilinearMap 𝕜 E G)
:
def
ContinuousLinearMap.compContinuousMultilinearMapL
(𝕜 : Type u)
{ι : Type v}
(E : ι → Type wE)
(G : Type wG)
(G' : Type wG')
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
:
(G →L[𝕜] G') →L[𝕜] ContinuousMultilinearMap 𝕜 E G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
ContinuousLinearMap.compContinuousMultilinearMap as a bundled continuous bilinear map.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
ContinuousLinearEquiv.compContinuousMultilinearMapL
{𝕜 : Type u}
{ι : Type v}
(E : ι → Type wE)
{G : Type wG}
{G' : Type wG'}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(g : G ≃L[𝕜] G')
:
ContinuousMultilinearMap 𝕜 E G ≃L[𝕜] ContinuousMultilinearMap 𝕜 E G'
ContinuousLinearMap.compContinuousMultilinearMap as a bundled
continuous linear equiv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
ContinuousLinearEquiv.compContinuousMultilinearMapL_symm
{𝕜 : Type u}
{ι : Type v}
(E : ι → Type wE)
{G : Type wG}
{G' : Type wG'}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(g : G ≃L[𝕜] G')
:
@[simp]
theorem
ContinuousLinearEquiv.compContinuousMultilinearMapL_apply
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
{G' : Type wG'}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(g : G ≃L[𝕜] G')
(f : ContinuousMultilinearMap 𝕜 E G)
:
@[simp]
theorem
ContinuousLinearMap.flipMultilinear_apply_apply
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
{G' : Type wG'}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G')
(m : (i : ι) → E i)
(x : G)
:
↑(↑(ContinuousLinearMap.flipMultilinear f) m) x = ↑(↑f x) m
def
ContinuousLinearMap.flipMultilinear
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
{G' : Type wG'}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G')
:
ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')
Flip arguments in f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G' to get
ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LinearIsometry.norm_compContinuousMultilinearMap
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
{G' : Type wG'}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(g : G →ₗᵢ[𝕜] G')
(f : ContinuousMultilinearMap 𝕜 E G)
:
def
MultilinearMap.mkContinuousLinear
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
{G' : Type wG'}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(f : G →ₗ[𝕜] MultilinearMap 𝕜 E G')
(C : ℝ)
(H : ∀ (x : G) (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * Finset.prod Finset.univ fun i => ‖m i‖)
:
G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
Given a map f : G →ₗ[𝕜] MultilinearMap 𝕜 E G' and an estimate
H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖, construct a continuous linear
map from G to ContinuousMultilinearMap 𝕜 E G'.
In order to lift, e.g., a map f : (MultilinearMap 𝕜 E G) →ₗ[𝕜] MultilinearMap 𝕜 E' G'
to a map (ContinuousMultilinearMap 𝕜 E G) →L[𝕜] ContinuousMultilinearMap 𝕜 E' G',
one can apply this construction to f.comp ContinuousMultilinearMap.toMultilinearMapLinear
which is a linear map from ContinuousMultilinearMap 𝕜 E G to MultilinearMap 𝕜 E' G'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MultilinearMap.mkContinuousLinear_norm_le'
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
{G' : Type wG'}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(f : G →ₗ[𝕜] MultilinearMap 𝕜 E G')
(C : ℝ)
(H : ∀ (x : G) (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * Finset.prod Finset.univ fun i => ‖m i‖)
:
‖MultilinearMap.mkContinuousLinear f C H‖ ≤ max C 0
theorem
MultilinearMap.mkContinuousLinear_norm_le
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
{G' : Type wG'}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(f : G →ₗ[𝕜] MultilinearMap 𝕜 E G')
{C : ℝ}
(hC : 0 ≤ C)
(H : ∀ (x : G) (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * Finset.prod Finset.univ fun i => ‖m i‖)
:
‖MultilinearMap.mkContinuousLinear f C H‖ ≤ C
def
MultilinearMap.mkContinuousMultilinear
{𝕜 : Type u}
{ι : Type v}
{ι' : Type v'}
{E : ι → Type wE}
{E' : ι' → Type wE'}
{G : Type wG}
[Fintype ι]
[Fintype ι']
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[(i : ι') → NormedAddCommGroup (E' i)]
[(i : ι') → NormedSpace 𝕜 (E' i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G))
(C : ℝ)
(H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i),
‖↑(↑f m₁) m₂‖ ≤ (C * Finset.prod Finset.univ fun i => ‖m₁ i‖) * Finset.prod Finset.univ fun i => ‖m₂ i‖)
:
ContinuousMultilinearMap 𝕜 E (ContinuousMultilinearMap 𝕜 E' G)
Given a map f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G) and an estimate
H : ∀ m m', ‖f m m'‖ ≤ C * ∏ i, ‖m i‖ * ∏ i, ‖m' i‖, upgrade all MultilinearMaps in the type to
ContinuousMultilinearMaps.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
MultilinearMap.mkContinuousMultilinear_apply
{𝕜 : Type u}
{ι : Type v}
{ι' : Type v'}
{E : ι → Type wE}
{E' : ι' → Type wE'}
{G : Type wG}
[Fintype ι]
[Fintype ι']
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[(i : ι') → NormedAddCommGroup (E' i)]
[(i : ι') → NormedSpace 𝕜 (E' i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G))
{C : ℝ}
(H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i),
‖↑(↑f m₁) m₂‖ ≤ (C * Finset.prod Finset.univ fun i => ‖m₁ i‖) * Finset.prod Finset.univ fun i => ‖m₂ i‖)
(m : (i : ι) → E i)
:
↑(↑(MultilinearMap.mkContinuousMultilinear f C H) m) = ↑(↑f m)
theorem
MultilinearMap.mkContinuousMultilinear_norm_le'
{𝕜 : Type u}
{ι : Type v}
{ι' : Type v'}
{E : ι → Type wE}
{E' : ι' → Type wE'}
{G : Type wG}
[Fintype ι]
[Fintype ι']
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[(i : ι') → NormedAddCommGroup (E' i)]
[(i : ι') → NormedSpace 𝕜 (E' i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G))
(C : ℝ)
(H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i),
‖↑(↑f m₁) m₂‖ ≤ (C * Finset.prod Finset.univ fun i => ‖m₁ i‖) * Finset.prod Finset.univ fun i => ‖m₂ i‖)
:
‖MultilinearMap.mkContinuousMultilinear f C H‖ ≤ max C 0
theorem
MultilinearMap.mkContinuousMultilinear_norm_le
{𝕜 : Type u}
{ι : Type v}
{ι' : Type v'}
{E : ι → Type wE}
{E' : ι' → Type wE'}
{G : Type wG}
[Fintype ι]
[Fintype ι']
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[(i : ι') → NormedAddCommGroup (E' i)]
[(i : ι') → NormedSpace 𝕜 (E' i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G))
{C : ℝ}
(hC : 0 ≤ C)
(H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i),
‖↑(↑f m₁) m₂‖ ≤ (C * Finset.prod Finset.univ fun i => ‖m₁ i‖) * Finset.prod Finset.univ fun i => ‖m₂ i‖)
:
theorem
ContinuousMultilinearMap.norm_compContinuousLinearMap_le
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{E₁ : ι → Type wE₁}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[(i : ι) → NormedAddCommGroup (E₁ i)]
[(i : ι) → NormedSpace 𝕜 (E₁ i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(g : ContinuousMultilinearMap 𝕜 E₁ G)
(f : (i : ι) → E i →L[𝕜] E₁ i)
:
‖ContinuousMultilinearMap.compContinuousLinearMap g f‖ ≤ ‖g‖ * Finset.prod Finset.univ fun i => ‖f i‖
theorem
ContinuousMultilinearMap.norm_compContinuous_linearIsometry_le
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{E₁ : ι → Type wE₁}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[(i : ι) → NormedAddCommGroup (E₁ i)]
[(i : ι) → NormedSpace 𝕜 (E₁ i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(g : ContinuousMultilinearMap 𝕜 E₁ G)
(f : (i : ι) → E i →ₗᵢ[𝕜] E₁ i)
:
theorem
ContinuousMultilinearMap.norm_compContinuous_linearIsometryEquiv
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{E₁ : ι → Type wE₁}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[(i : ι) → NormedAddCommGroup (E₁ i)]
[(i : ι) → NormedSpace 𝕜 (E₁ i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(g : ContinuousMultilinearMap 𝕜 E₁ G)
(f : (i : ι) → E i ≃ₗᵢ[𝕜] E₁ i)
:
‖ContinuousMultilinearMap.compContinuousLinearMap g fun i => ↑(ContinuousLinearEquiv.mk (f i).toLinearEquiv)‖ = ‖g‖
def
ContinuousMultilinearMap.compContinuousLinearMapL
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{E₁ : ι → Type wE₁}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[(i : ι) → NormedAddCommGroup (E₁ i)]
[(i : ι) → NormedSpace 𝕜 (E₁ i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : (i : ι) → E i →L[𝕜] E₁ i)
:
ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G
ContinuousMultilinearMap.compContinuousLinearMap 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
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
ContinuousMultilinearMap.compContinuousLinearMapL_apply
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{E₁ : ι → Type wE₁}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[(i : ι) → NormedAddCommGroup (E₁ i)]
[(i : ι) → NormedSpace 𝕜 (E₁ i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(g : ContinuousMultilinearMap 𝕜 E₁ G)
(f : (i : ι) → E i →L[𝕜] E₁ i)
:
theorem
ContinuousMultilinearMap.norm_compContinuousLinearMapL_le
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{E₁ : ι → Type wE₁}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[(i : ι) → NormedAddCommGroup (E₁ i)]
[(i : ι) → NormedSpace 𝕜 (E₁ i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : (i : ι) → E i →L[𝕜] E₁ i)
:
‖ContinuousMultilinearMap.compContinuousLinearMapL f‖ ≤ Finset.prod Finset.univ fun i => ‖f i‖
def
ContinuousMultilinearMap.compContinuousLinearMapEquivL
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{E₁ : ι → Type wE₁}
(G : Type wG)
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[(i : ι) → NormedAddCommGroup (E₁ i)]
[(i : ι) → NormedSpace 𝕜 (E₁ i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : (i : ι) → E i ≃L[𝕜] E₁ i)
:
ContinuousMultilinearMap 𝕜 E₁ G ≃L[𝕜] ContinuousMultilinearMap 𝕜 E G
ContinuousMultilinearMap.compContinuousLinearMap as a bundled continuous linear equiv,
given f : Π i, E i ≃L[𝕜] E₁ i.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
ContinuousMultilinearMap.compContinuousLinearMapEquivL_symm
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{E₁ : ι → Type wE₁}
(G : Type wG)
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[(i : ι) → NormedAddCommGroup (E₁ i)]
[(i : ι) → NormedSpace 𝕜 (E₁ i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : (i : ι) → E i ≃L[𝕜] E₁ i)
:
@[simp]
theorem
ContinuousMultilinearMap.compContinuousLinearMapEquivL_apply
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{E₁ : ι → Type wE₁}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[(i : ι) → NormedAddCommGroup (E₁ i)]
[(i : ι) → NormedSpace 𝕜 (E₁ i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(g : ContinuousMultilinearMap 𝕜 E₁ G)
(f : (i : ι) → E i ≃L[𝕜] E₁ i)
:
↑(ContinuousMultilinearMap.compContinuousLinearMapEquivL G f) g = ContinuousMultilinearMap.compContinuousLinearMap g fun i => ↑(f i)
instance
continuousConstSMul
{𝕜 : Type u}
{ι : Type v}
{E : ι → Type wE}
{G : Type wG}
[Fintype ι]
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{R : Type u_1}
[Semiring R]
[Module R G]
[SMulCommClass 𝕜 R G]
[ContinuousConstSMul R G]
:
ContinuousConstSMul R (ContinuousMultilinearMap 𝕜 E G)
Currying #
We associate to a continuous multilinear map in n+1 variables (i.e., based on Fin n.succ) two
curried functions, named f.curryLeft (which is a continuous linear map on E 0 taking values
in continuous multilinear maps in n variables) and f.curryRight (which is a continuous
multilinear map in n variables taking values in continuous linear maps on E (last n)).
The inverse operations are called uncurryLeft and uncurryRight.
We also register continuous linear equiv versions of these correspondences, in
continuousMultilinearCurryLeftEquiv and continuousMultilinearCurryRightEquiv.
theorem
ContinuousLinearMap.norm_map_tail_le
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei (Fin.succ i)) G)
(m : (i : Fin (Nat.succ n)) → Ei i)
:
theorem
ContinuousMultilinearMap.norm_map_init_le
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 (fun i => Ei (Fin.castSucc i)) (Ei (Fin.last n) →L[𝕜] G))
(m : (i : Fin (Nat.succ n)) → Ei i)
:
theorem
ContinuousMultilinearMap.norm_map_cons_le
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 Ei G)
(x : Ei 0)
(m : (i : Fin n) → Ei (Fin.succ i))
:
theorem
ContinuousMultilinearMap.norm_map_snoc_le
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 Ei G)
(m : (i : Fin n) → Ei (Fin.castSucc i))
(x : Ei (Fin.last n))
:
Left currying #
def
ContinuousLinearMap.uncurryLeft
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei (Fin.succ i)) G)
:
ContinuousMultilinearMap 𝕜 Ei G
Given a continuous linear map f from E 0 to continuous multilinear maps on n variables,
construct the corresponding continuous multilinear map on n+1 variables obtained by concatenating
the variables, given by m ↦ f (m 0) (tail m)
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
ContinuousLinearMap.uncurryLeft_apply
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei (Fin.succ i)) G)
(m : (i : Fin (Nat.succ n)) → Ei i)
:
↑(ContinuousLinearMap.uncurryLeft f) m = ↑(↑f (m 0)) (Fin.tail m)
def
ContinuousMultilinearMap.curryLeft
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 Ei G)
:
Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei (Fin.succ i)) G
Given a continuous multilinear map f in n+1 variables, split the first variable to obtain
a continuous linear map into continuous multilinear maps in n variables, given by
x ↦ (m ↦ f (cons x m)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
ContinuousMultilinearMap.curryLeft_apply
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 Ei G)
(x : Ei 0)
(m : (i : Fin n) → Ei (Fin.succ i))
:
↑(↑(ContinuousMultilinearMap.curryLeft f) x) m = ↑f (Fin.cons x m)
@[simp]
theorem
ContinuousLinearMap.curry_uncurryLeft
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei (Fin.succ i)) G)
:
@[simp]
theorem
ContinuousMultilinearMap.uncurry_curryLeft
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 Ei G)
:
def
continuousMultilinearCurryLeftEquiv
(𝕜 : Type u)
{n : ℕ}
(Ei : Fin (Nat.succ n) → Type wEi)
(G : Type wG)
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
:
(Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei (Fin.succ i)) G) ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 Ei G
The space of continuous multilinear maps on Π(i : Fin (n+1)), E i is canonically isomorphic to
the space of continuous linear maps from E 0 to the space of continuous multilinear maps on
Π(i : Fin n), E i.succ, by separating the first variable. We register this isomorphism in
continuousMultilinearCurryLeftEquiv 𝕜 E E₂. The algebraic version (without topology) is given
in multilinearCurryLeftEquiv 𝕜 E E₂.
The direct and inverse maps are given by f.uncurryLeft and f.curryLeft. Use these
unless you need the full framework of linear isometric equivs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
continuousMultilinearCurryLeftEquiv_apply
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei (Fin.succ i)) G)
(v : (i : Fin (Nat.succ n)) → Ei i)
:
↑(↑(continuousMultilinearCurryLeftEquiv 𝕜 Ei G) f) v = ↑(↑f (v 0)) (Fin.tail v)
@[simp]
theorem
continuousMultilinearCurryLeftEquiv_symm_apply
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 Ei G)
(x : Ei 0)
(v : (i : Fin n) → Ei (Fin.succ i))
:
↑(↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 Ei G)) f) x) v = ↑f (Fin.cons x v)
@[simp]
theorem
ContinuousMultilinearMap.curryLeft_norm
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 Ei G)
:
@[simp]
theorem
ContinuousLinearMap.uncurryLeft_norm
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei (Fin.succ i)) G)
:
Right currying #
def
ContinuousMultilinearMap.uncurryRight
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 (fun i => Ei (Fin.castSucc i)) (Ei (Fin.last n) →L[𝕜] G))
:
ContinuousMultilinearMap 𝕜 Ei G
Given a continuous linear map f from continuous multilinear maps on n variables to
continuous linear maps on E 0, construct the corresponding continuous multilinear map on n+1
variables obtained by concatenating the variables, given by m ↦ f (init m) (m (last n)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
ContinuousMultilinearMap.uncurryRight_apply
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 (fun i => Ei (Fin.castSucc i)) (Ei (Fin.last n) →L[𝕜] G))
(m : (i : Fin (Nat.succ n)) → Ei i)
:
↑(ContinuousMultilinearMap.uncurryRight f) m = ↑(↑f (Fin.init m)) (m (Fin.last n))
def
ContinuousMultilinearMap.curryRight
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 Ei G)
:
ContinuousMultilinearMap 𝕜 (fun i => Ei (Fin.castSucc i)) (Ei (Fin.last n) →L[𝕜] G)
Given a continuous multilinear map f in n+1 variables, split the last variable to obtain
a continuous multilinear map in n variables into continuous linear maps, given by
m ↦ (x ↦ f (snoc m x)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
ContinuousMultilinearMap.curryRight_apply
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 Ei G)
(m : (i : Fin n) → Ei (Fin.castSucc i))
(x : Ei (Fin.last n))
:
↑(↑(ContinuousMultilinearMap.curryRight f) m) x = ↑f (Fin.snoc m x)
@[simp]
theorem
ContinuousMultilinearMap.curry_uncurryRight
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 (fun i => Ei (Fin.castSucc i)) (Ei (Fin.last n) →L[𝕜] G))
:
@[simp]
theorem
ContinuousMultilinearMap.uncurry_curryRight
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 Ei G)
:
def
continuousMultilinearCurryRightEquiv
(𝕜 : Type u)
{n : ℕ}
(Ei : Fin (Nat.succ n) → Type wEi)
(G : Type wG)
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
:
ContinuousMultilinearMap 𝕜 (fun i => Ei (Fin.castSucc i)) (Ei (Fin.last n) →L[𝕜] G) ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 Ei G
The space of continuous multilinear maps on Π(i : Fin (n+1)), Ei i is canonically isomorphic to
the space of continuous multilinear maps on Π(i : Fin n), Ei <| castSucc i with values in the
space of continuous linear maps on Ei (last n), by separating the last variable. We register this
isomorphism as a continuous linear equiv in continuousMultilinearCurryRightEquiv 𝕜 Ei G.
The algebraic version (without topology) is given in multilinearCurryRightEquiv 𝕜 Ei G.
The direct and inverse maps are given by f.uncurryRight and f.curryRight. Use these
unless you need the full framework of linear isometric equivs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
continuousMultilinearCurryRightEquiv'
(𝕜 : Type u)
(n : ℕ)
(G : Type wG)
(G' : Type wG')
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
:
ContinuousMultilinearMap 𝕜 (fun i => G) (G →L[𝕜] G') ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun i => G) G'
The space of continuous multilinear maps on Π(i : Fin (n+1)), G is canonically isomorphic to
the space of continuous multilinear maps on Π(i : Fin n), G with values in the space
of continuous linear maps on G, by separating the last variable. We register this
isomorphism as a continuous linear equiv in continuousMultilinearCurryRightEquiv' 𝕜 n G G'.
For a version allowing dependent types, see continuousMultilinearCurryRightEquiv. When there
are no dependent types, use the primed version as it helps Lean a lot for unification.
The direct and inverse maps are given by f.uncurryRight and f.curryRight. Use these
unless you need the full framework of linear isometric equivs.
Equations
- continuousMultilinearCurryRightEquiv' 𝕜 n G G' = continuousMultilinearCurryRightEquiv 𝕜 (fun x => G) G'
Instances For
@[simp]
theorem
continuousMultilinearCurryRightEquiv_apply
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 (fun i => Ei (Fin.castSucc i)) (Ei (Fin.last n) →L[𝕜] G))
(v : (i : Fin (Nat.succ n)) → Ei i)
:
↑(↑(continuousMultilinearCurryRightEquiv 𝕜 Ei G) f) v = ↑(↑f (Fin.init v)) (v (Fin.last n))
@[simp]
theorem
continuousMultilinearCurryRightEquiv_symm_apply
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 Ei G)
(v : (i : Fin n) → Ei (Fin.castSucc i))
(x : Ei (Fin.last n))
:
↑(↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv 𝕜 Ei G)) f) v) x = ↑f (Fin.snoc v x)
@[simp]
theorem
continuousMultilinearCurryRightEquiv_apply'
{𝕜 : Type u}
{n : ℕ}
{G : Type wG}
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(f : ContinuousMultilinearMap 𝕜 (fun i => G) (G →L[𝕜] G'))
(v : Fin (n + 1) → G)
:
↑(↑(continuousMultilinearCurryRightEquiv' 𝕜 n G G') f) v = ↑(↑f (Fin.init v)) (v (Fin.last n))
@[simp]
theorem
continuousMultilinearCurryRightEquiv_symm_apply'
{𝕜 : Type u}
{n : ℕ}
{G : Type wG}
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(f : ContinuousMultilinearMap 𝕜 (fun i => G) G')
(v : Fin n → G)
(x : G)
:
↑(↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n G G')) f) v) x = ↑f (Fin.snoc v x)
@[simp]
theorem
ContinuousMultilinearMap.curryRight_norm
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 Ei G)
:
@[simp]
theorem
ContinuousMultilinearMap.uncurryRight_norm
{𝕜 : Type u}
{n : ℕ}
{Ei : Fin (Nat.succ n) → Type wEi}
{G : Type wG}
[NontriviallyNormedField 𝕜]
[(i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)]
[(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 (fun i => Ei (Fin.castSucc 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
ContinuousMultilinearMap.uncurry0
{𝕜 : Type u}
{G : Type wG}
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(f : ContinuousMultilinearMap 𝕜 (fun x => G) G')
:
G'
Associating to a continuous multilinear map in 0 variables the unique value it takes.
Equations
Instances For
def
ContinuousMultilinearMap.curry0
(𝕜 : Type u)
(G : Type wG)
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(x : G')
:
ContinuousMultilinearMap 𝕜 (fun i => 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
- ContinuousMultilinearMap.curry0 𝕜 G x = ContinuousMultilinearMap.constOfIsEmpty 𝕜 (fun i => G) x
Instances For
@[simp]
theorem
ContinuousMultilinearMap.curry0_apply
(𝕜 : Type u)
{G : Type wG}
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(x : G')
(m : Fin 0 → G)
:
↑(ContinuousMultilinearMap.curry0 𝕜 G x) m = x
@[simp]
theorem
ContinuousMultilinearMap.uncurry0_apply
{𝕜 : Type u}
{G : Type wG}
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(f : ContinuousMultilinearMap 𝕜 (fun i => G) G')
:
@[simp]
theorem
ContinuousMultilinearMap.apply_zero_curry0
{𝕜 : Type u}
{G : Type wG}
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(f : ContinuousMultilinearMap 𝕜 (fun i => G) G')
{x : Fin 0 → G}
:
ContinuousMultilinearMap.curry0 𝕜 G (↑f x) = f
theorem
ContinuousMultilinearMap.uncurry0_curry0
{𝕜 : Type u}
{G : Type wG}
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(f : ContinuousMultilinearMap 𝕜 (fun i => G) G')
:
theorem
ContinuousMultilinearMap.curry0_uncurry0
(𝕜 : Type u)
(G : Type wG)
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(x : G')
:
@[simp]
theorem
ContinuousMultilinearMap.curry0_norm
(𝕜 : Type u)
(G : Type wG)
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(x : G')
:
@[simp]
theorem
ContinuousMultilinearMap.fin0_apply_norm
{𝕜 : Type u}
{G : Type wG}
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(f : ContinuousMultilinearMap 𝕜 (fun i => G) G')
{x : Fin 0 → G}
:
theorem
ContinuousMultilinearMap.uncurry0_norm
{𝕜 : Type u}
{G : Type wG}
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(f : ContinuousMultilinearMap 𝕜 (fun i => G) G')
:
def
continuousMultilinearCurryFin0
(𝕜 : Type u)
(G : Type wG)
(G' : Type wG')
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
:
ContinuousMultilinearMap 𝕜 (fun i => G) G' ≃ₗᵢ[𝕜] G'
The continuous linear isomorphism between elements of a normed space, and continuous multilinear
maps in 0 variables with values in this normed space.
The direct and inverse maps are uncurry0 and curry0. Use these unless you need the full
framework of linear isometric equivs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
continuousMultilinearCurryFin0_apply
{𝕜 : Type u}
{G : Type wG}
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(f : ContinuousMultilinearMap 𝕜 (fun i => G) G')
:
↑(continuousMultilinearCurryFin0 𝕜 G G') f = ↑f 0
@[simp]
theorem
continuousMultilinearCurryFin0_symm_apply
{𝕜 : Type u}
{G : Type wG}
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(x : G')
(v : Fin 0 → G)
:
↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 G G')) x) v = x
With 1 variable #
def
continuousMultilinearCurryFin1
(𝕜 : Type u)
(G : Type wG)
(G' : Type wG')
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
:
ContinuousMultilinearMap 𝕜 (fun i => G) G' ≃ₗᵢ[𝕜] G →L[𝕜] G'
Continuous multilinear maps from G^1 to G' are isomorphic with continuous linear maps from
G to G'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
continuousMultilinearCurryFin1_apply
{𝕜 : Type u}
{G : Type wG}
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(f : ContinuousMultilinearMap 𝕜 (fun i => G) G')
(x : G)
:
↑(↑(continuousMultilinearCurryFin1 𝕜 G G') f) x = ↑f (Fin.snoc 0 x)
@[simp]
theorem
continuousMultilinearCurryFin1_symm_apply
{𝕜 : Type u}
{G : Type wG}
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(f : G →L[𝕜] G')
(v : Fin 1 → G)
:
↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 G G')) f) v = ↑f (v 0)
@[simp]
theorem
ContinuousMultilinearMap.norm_domDomCongr
(𝕜 : Type u)
{ι : Type v}
{ι' : Type v'}
(G : Type wG)
(G' : Type wG')
[Fintype ι]
[Fintype ι']
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(σ : ι ≃ ι')
(f : ContinuousMultilinearMap 𝕜 (fun x => G) G')
:
def
ContinuousMultilinearMap.domDomCongrₗᵢ
(𝕜 : Type u)
{ι : Type v}
{ι' : Type v'}
(G : Type wG)
(G' : Type wG')
[Fintype ι]
[Fintype ι']
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(σ : ι ≃ ι')
:
ContinuousMultilinearMap 𝕜 (fun x => G) G' ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun x => G) G'
An equivalence of the index set defines a linear isometric equivalence between the spaces of multilinear maps.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
ContinuousMultilinearMap.currySum
{𝕜 : Type u}
{ι : Type v}
{ι' : Type v'}
{G : Type wG}
{G' : Type wG'}
[Fintype ι]
[Fintype ι']
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(f : ContinuousMultilinearMap 𝕜 (fun x => G) G')
:
ContinuousMultilinearMap 𝕜 (fun x => G) (ContinuousMultilinearMap 𝕜 (fun x => G) G')
A continuous multilinear map with variables indexed by ι ⊕ ι' defines a continuous
multilinear map with variables indexed by ι taking values in the space of continuous multilinear
maps with variables indexed by ι'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
ContinuousMultilinearMap.currySum_apply
{𝕜 : Type u}
{ι : Type v}
{ι' : Type v'}
{G : Type wG}
{G' : Type wG'}
[Fintype ι]
[Fintype ι']
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(f : ContinuousMultilinearMap 𝕜 (fun x => G) G')
(m : ι → G)
(m' : ι' → G)
:
↑(↑(ContinuousMultilinearMap.currySum f) m) m' = ↑f (Sum.elim m m')
def
ContinuousMultilinearMap.uncurrySum
{𝕜 : Type u}
{ι : Type v}
{ι' : Type v'}
{G : Type wG}
{G' : Type wG'}
[Fintype ι]
[Fintype ι']
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(f : ContinuousMultilinearMap 𝕜 (fun x => G) (ContinuousMultilinearMap 𝕜 (fun x => G) G'))
:
ContinuousMultilinearMap 𝕜 (fun x => G) G'
A continuous multilinear map with variables indexed by ι taking values in the space of
continuous multilinear maps with variables indexed by ι' defines a continuous multilinear map with
variables indexed by ι ⊕ ι'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
ContinuousMultilinearMap.uncurrySum_apply
{𝕜 : Type u}
{ι : Type v}
{ι' : Type v'}
{G : Type wG}
{G' : Type wG'}
[Fintype ι]
[Fintype ι']
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
(f : ContinuousMultilinearMap 𝕜 (fun x => G) (ContinuousMultilinearMap 𝕜 (fun x => G) G'))
(m : ι ⊕ ι' → G)
:
↑(ContinuousMultilinearMap.uncurrySum f) m = ↑(↑f (m ∘ Sum.inl)) (m ∘ Sum.inr)
def
ContinuousMultilinearMap.currySumEquiv
(𝕜 : Type u)
(ι : Type v)
(ι' : Type v')
(G : Type wG)
(G' : Type wG')
[Fintype ι]
[Fintype ι']
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
:
ContinuousMultilinearMap 𝕜 (fun x => G) G' ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun x => G) (ContinuousMultilinearMap 𝕜 (fun x => G) G')
Linear isometric equivalence between the space of continuous multilinear maps with variables
indexed by ι ⊕ ι' and the space of continuous multilinear maps with variables indexed by ι
taking values in the space of continuous multilinear maps with variables indexed by ι'.
The forward and inverse functions are ContinuousMultilinearMap.currySum
and ContinuousMultilinearMap.uncurrySum. Use this definition only if you need
some properties of LinearIsometryEquiv.
Instances For
def
ContinuousMultilinearMap.curryFinFinset
(𝕜 : Type u)
(G : Type wG)
(G' : Type wG')
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
{k : ℕ}
{l : ℕ}
{n : ℕ}
{s : Finset (Fin n)}
(hk : Finset.card s = k)
(hl : Finset.card sᶜ = l)
:
ContinuousMultilinearMap 𝕜 (fun i => G) G' ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun i => G) (ContinuousMultilinearMap 𝕜 (fun i => G) G')
If s : Finset (Fin n) is a finite set of cardinality k and its complement has cardinality
l, then the space of continuous multilinear maps G [×n]→L[𝕜] G' of n variables is isomorphic
to the space of continuous multilinear maps G [×k]→L[𝕜] G [×l]→L[𝕜] G' of k variables taking
values in the space of continuous multilinear maps of l variables.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
ContinuousMultilinearMap.curryFinFinset_apply
{𝕜 : Type u}
{n : ℕ}
{G : Type wG}
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
{k : ℕ}
{l : ℕ}
{s : Finset (Fin n)}
(hk : Finset.card s = k)
(hl : Finset.card sᶜ = l)
(f : ContinuousMultilinearMap 𝕜 (fun i => G) G')
(mk : Fin k → G)
(ml : Fin l → G)
:
↑(↑(↑(ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl) f) mk) ml = ↑f fun i => Sum.elim mk ml (↑(finSumEquivOfFinset hk hl).symm i)
@[simp]
theorem
ContinuousMultilinearMap.curryFinFinset_symm_apply
{𝕜 : Type u}
{n : ℕ}
{G : Type wG}
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
{k : ℕ}
{l : ℕ}
{s : Finset (Fin n)}
(hk : Finset.card s = k)
(hl : Finset.card sᶜ = l)
(f : ContinuousMultilinearMap 𝕜 (fun i => G) (ContinuousMultilinearMap 𝕜 (fun i => G) G'))
(m : Fin n → G)
:
↑(↑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl)) f) m = ↑(↑f fun i => m (↑(finSumEquivOfFinset hk hl) (Sum.inl i))) fun i => m (↑(finSumEquivOfFinset hk hl) (Sum.inr i))
theorem
ContinuousMultilinearMap.curryFinFinset_symm_apply_piecewise_const
{𝕜 : Type u}
{n : ℕ}
{G : Type wG}
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
{k : ℕ}
{l : ℕ}
{s : Finset (Fin n)}
(hk : Finset.card s = k)
(hl : Finset.card sᶜ = l)
(f : ContinuousMultilinearMap 𝕜 (fun i => G) (ContinuousMultilinearMap 𝕜 (fun i => G) G'))
(x : G)
(y : G)
:
↑(↑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl)) f)
(Finset.piecewise s (fun x => x) fun x => y) = ↑(↑f fun x => x) fun x => y
@[simp]
theorem
ContinuousMultilinearMap.curryFinFinset_symm_apply_const
{𝕜 : Type u}
{n : ℕ}
{G : Type wG}
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
{k : ℕ}
{l : ℕ}
{s : Finset (Fin n)}
(hk : Finset.card s = k)
(hl : Finset.card sᶜ = l)
(f : ContinuousMultilinearMap 𝕜 (fun i => G) (ContinuousMultilinearMap 𝕜 (fun i => G) G'))
(x : G)
:
(↑(↑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl)) f) fun x => x) = ↑(↑f fun x => x) fun x => x
theorem
ContinuousMultilinearMap.curryFinFinset_apply_const
{𝕜 : Type u}
{n : ℕ}
{G : Type wG}
{G' : Type wG'}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup G']
[NormedSpace 𝕜 G']
{k : ℕ}
{l : ℕ}
{s : Finset (Fin n)}
(hk : Finset.card s = k)
(hl : Finset.card sᶜ = l)
(f : ContinuousMultilinearMap 𝕜 (fun i => G) G')
(x : G)
(y : G)
:
(↑(↑(↑(ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl) f) fun x => x) fun x => y) = ↑f (Finset.piecewise s (fun x => x) fun x => y)