Operator norm on the space of continuous alternating maps

In this file we show that continuous alternating maps from a seminormed space to a (semi)normed space form a (semi)normed space. We also prove basic facts about this norm and define bundled versions of some operations on continuous alternating maps.

Most proofs just invoke the corresponding fact about continuous multilinear maps.

Type variables

We use the following type variables in this file:

• 𝕜 : a nontrivially normed field;
• ι: a finite index type;
• E, F, G: (semi)normed vector spaces over 𝕜.

instance ContinuousAlternatingMap.instContinuousEval {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} [NormedField 𝕜] [Finite ι] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace F] [AddCommGroup F] [IsTopologicalAddGroup F] [Module 𝕜 F] : ContinuousEval (E [⋀^ι]→L[𝕜] F) (ι → E) F

Applying a continuous alternating map to a vector is continuous in the pair (map, vector).

Continuity in in the vector holds by definition and continuity in the map holds if both the domain and the codomain are topological vector spaces. However, continuity in the pair (map, vector) needs the domain to be a locally bounded TVS. We have no typeclass for a locally bounded TVS, so we require it to be a seminormed space instead.

Continuity properties of alternating maps

We relate continuity of alternating 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 AlternatingMap.norm_map_coord_zero {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E [⋀^ι]→ₗ[𝕜] F) (hf : Continuous ⇑f) {m : ι → E} {i : ι} (hi : ‖m i‖ = 0) : ‖f m‖ = 0

If f is a continuous alternating map on E and m is an element of ι → E such that one of the m i has norm 0, then f m has norm 0.

Note that we cannot drop the continuity assumption. Indeed, let ℝ₀ be a copy or ℝ with zero norm and indiscrete topology. Then f : (Unit → ℝ₀) → ℝ given by f x = x () sends vector 1 with zero norm to number 1 with nonzero norm.

theorem AlternatingMap.bound_of_shell_of_norm_map_coord_zero {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (f : E [⋀^ι]→ₗ[𝕜] F) (hf₀ : ∀ {m : ι → E} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0) {ε : ι → ℝ} {C : ℝ} (hε : ∀ (i : ι), 0 < ε i) {c : ι → 𝕜} (hc : ∀ (i : ι), 1 < ‖c i‖) (hf : ∀ (m : ι → E), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖) (m : ι → E) : ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖

If an alternating map in finitely many variables on seminormed spaces sends vectors with a component of norm zero to vectors of norm zero and 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.

The first assumption is automatically satisfied on normed spaces, see bound_of_shell below. For seminormed spaces, it follows from continuity of f, see lemma bound_of_shell_of_continuous below.

theorem AlternatingMap.bound_of_shell_of_continuous {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (f : E [⋀^ι]→ₗ[𝕜] F) (hfc : Continuous ⇑f) {ε C : ℝ} (hε : 0 < ε) {c : 𝕜} (hc : 1 < ‖c‖) (hf : ∀ (m : ι → E), (∀ (i : ι), ε / ‖c‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε) → ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖) (m : ι → E) : ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖

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

If the domain is a Hausdorff space, then the continuity assumption is reduntant, see bound_of_shell below.

theorem AlternatingMap.exists_bound_of_continuous {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (f : E [⋀^ι]→ₗ[𝕜] F) (hf : Continuous ⇑f) : ∃ (C : ℝ), 0 < C ∧ ∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖

If an alternating map in finitely many variables on a seminormed space is continuous, then it satisfies the inequality ‖f m‖ ≤ C * ∏ i, ‖m i‖, for some C which can be chosen to be positive.

theorem AlternatingMap.norm_image_sub_le_of_bound' {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] [DecidableEq ι] (f : E [⋀^ι]→ₗ[𝕜] F) {C : ℝ} (hC : 0 ≤ C) (H : ∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖) (m₁ m₂ : ι → E) : ‖f m₁ - f m₂‖ ≤ C * ∑ i : ι, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

If an alternating map 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 AlternatingMap.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 AlternatingMap.norm_image_sub_le_of_bound {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (f : E [⋀^ι]→ₗ[𝕜] F) {C : ℝ} (hC : 0 ≤ C) (H : ∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖) (m₁ m₂ : ι → E) : ‖f m₁ - f m₂‖ ≤ C * ↑(Fintype.card ι) * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖

If an alternating map 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 AlternatingMap.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 AlternatingMap.continuous_of_bound {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (f : E [⋀^ι]→ₗ[𝕜] F) (C : ℝ) (H : ∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖) : Continuous ⇑f

If an alternating map satisfies an inequality ‖f m‖ ≤ C * ∏ i, ‖m i‖, then it is continuous.

def AlternatingMap.mkContinuous {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (f : E [⋀^ι]→ₗ[𝕜] F) (C : ℝ) (H : ∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖) : E [⋀^ι]→L[𝕜] F

Construct a continuous alternating map from a alternating map satisfying a boundedness condition.

Equations

• f.mkContinuous C H = { toMultilinearMap := ↑f, cont := ⋯, map_eq_zero_of_eq' := ⋯ }

@[simp]

theorem AlternatingMap.coe_mkContinuous {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (f : E [⋀^ι]→ₗ[𝕜] F) (C : ℝ) (H : ∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖) : ⇑(f.mkContinuous C H) = ⇑f

Continuous alternating maps

We define the norm ‖f‖ of a continuous alternating map f in finitely many variables as the smallest nonnegative number such that ‖f m‖ ≤ ‖f‖ * ∏ i, ‖m i‖ for all m. We show that this defines a normed space structure on E [⋀^ι]→L[𝕜] F.

theorem ContinuousAlternatingMap.bound {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (f : E [⋀^ι]→L[𝕜] F) : ∃ (C : ℝ), 0 < C ∧ ∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖

instance ContinuousAlternatingMap.instSeminormedAddCommGroup {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] : SeminormedAddCommGroup (E [⋀^ι]→L[𝕜] F)

Continuous alternating maps form a seminormed additive commutative group. We override projection to PseudoMetricSpace to ensure that instances commute in with_reducible_and_instances.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousAlternatingMap.norm_toContinuousMultilinearMap {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (f : E [⋀^ι]→L[𝕜] F) : ‖f.toContinuousMultilinearMap‖ = ‖f‖

@[simp]

theorem ContinuousAlternatingMap.nnnorm_toContinuousMultilinearMap {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (f : E [⋀^ι]→L[𝕜] F) : ‖f.toContinuousMultilinearMap‖₊ = ‖f‖₊

@[simp]

theorem ContinuousAlternatingMap.enorm_toContinuousMultilinearMap {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (f : E [⋀^ι]→L[𝕜] F) : ‖f.toContinuousMultilinearMap‖ₑ = ‖f‖ₑ

def ContinuousAlternatingMap.toContinuousMultilinearMapLI {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] : E [⋀^ι]→L[𝕜] F →ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) => E) F

The inclusion of E [⋀^ι]→L[𝕜] F into ContinuousMultilinearMap 𝕜 (fun _ : ι ↦ E) F as a linear isometry.

Equations

• ContinuousAlternatingMap.toContinuousMultilinearMapLI = { toLinearMap := ContinuousAlternatingMap.toContinuousMultilinearMapLinear, norm_map' := ⋯ }

@[simp]

theorem ContinuousAlternatingMap.toContinuousMultilinearMapLI_apply {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (self : E [⋀^ι]→L[𝕜] F) : toContinuousMultilinearMapLI self = self.toContinuousMultilinearMap

theorem ContinuousAlternatingMap.norm_def {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (f : E [⋀^ι]→L[𝕜] F) : ‖f‖ = sInf {c : ℝ | 0 ≤ c ∧ ∀ (m : ι → E), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖}

theorem ContinuousAlternatingMap.bounds_nonempty {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] {f : E [⋀^ι]→L[𝕜] F} : ∃ (c : ℝ), c ∈ {c : ℝ | 0 ≤ c ∧ ∀ (m : ι → E), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖}

theorem ContinuousAlternatingMap.bounds_bddBelow {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] {f : E [⋀^ι]→L[𝕜] F} : BddBelow {c : ℝ | 0 ≤ c ∧ ∀ (m : ι → E), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖}

theorem ContinuousAlternatingMap.isLeast_opNorm {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (f : E [⋀^ι]→L[𝕜] F) : IsLeast {c : ℝ | 0 ≤ c ∧ ∀ (m : ι → E), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖} ‖f‖

theorem ContinuousAlternatingMap.le_opNorm {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (f : E [⋀^ι]→L[𝕜] F) (m : ι → E) : ‖f m‖ ≤ ‖f‖ * ∏ i : ι, ‖m i‖

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

theorem ContinuousAlternatingMap.le_mul_prod_of_opNorm_le_of_le {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] {f : E [⋀^ι]→L[𝕜] F} {m : ι → E} {C : ℝ} {b : ι → ℝ} (hC : ‖f‖ ≤ C) (hm : ∀ (i : ι), ‖m i‖ ≤ b i) : ‖f m‖ ≤ C * ∏ i : ι, b i

theorem ContinuousAlternatingMap.le_opNorm_mul_prod_of_le {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] {m : ι → E} (f : E [⋀^ι]→L[𝕜] F) {b : ι → ℝ} (hm : ∀ (i : ι), ‖m i‖ ≤ b i) : ‖f m‖ ≤ ‖f‖ * ∏ i : ι, b i

theorem ContinuousAlternatingMap.le_opNorm_mul_pow_card_of_le {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (f : E [⋀^ι]→L[𝕜] F) {m : ι → E} {b : ℝ} (hm : ‖m‖ ≤ b) : ‖f m‖ ≤ ‖f‖ * b ^ Fintype.card ι

theorem ContinuousAlternatingMap.le_opNorm_mul_pow_of_le {𝕜 : Type u} {E : Type wE} {F : Type wF} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (f : E [⋀^Fin n]→L[𝕜] F) {m : Fin n → E} {b : ℝ} (hm : ‖m‖ ≤ b) : ‖f m‖ ≤ ‖f‖ * b ^ n

theorem ContinuousAlternatingMap.le_of_opNorm_le {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] {f : E [⋀^ι]→L[𝕜] F} {C : ℝ} (h : ‖f‖ ≤ C) (m : ι → E) : ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖

theorem ContinuousAlternatingMap.ratio_le_opNorm {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (f : E [⋀^ι]→L[𝕜] F) (m : ι → E) : ‖f m‖ / ∏ i : ι, ‖m i‖ ≤ ‖f‖

theorem ContinuousAlternatingMap.unit_le_opNorm {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] {m : ι → E} (f : E [⋀^ι]→L[𝕜] F) (h : ‖m‖ ≤ 1) : ‖f m‖ ≤ ‖f‖

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

theorem ContinuousAlternatingMap.opNorm_le_bound {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (f : E [⋀^ι]→L[𝕜] F) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ (m : ι → E), ‖f m‖ ≤ M * ∏ i : ι, ‖m i‖) : ‖f‖ ≤ M

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

theorem ContinuousAlternatingMap.opNorm_le_iff {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] {f : E [⋀^ι]→L[𝕜] F} {C : ℝ} (hC : 0 ≤ C) : ‖f‖ ≤ C ↔ ∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖

theorem ContinuousAlternatingMap.le_opNNNorm {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (f : E [⋀^ι]→L[𝕜] F) (m : ι → E) : ‖f m‖₊ ≤ ‖f‖₊ * ∏ i : ι, ‖m i‖₊

The fundamental property of the operator norm of a continuous alternating map: ‖f m‖ is bounded by ‖f‖ times the product of the ‖m i‖, nnnorm version.

theorem ContinuousAlternatingMap.le_of_opNNNorm_le {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] {f : E [⋀^ι]→L[𝕜] F} {C : NNReal} (h : ‖f‖₊ ≤ C) (m : ι → E) : ‖f m‖₊ ≤ C * ∏ i : ι, ‖m i‖₊

theorem ContinuousAlternatingMap.opNNNorm_le_iff {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] {f : E [⋀^ι]→L[𝕜] F} {C : NNReal} : ‖f‖₊ ≤ C ↔ ∀ (m : ι → E), ‖f m‖₊ ≤ C * ∏ i : ι, ‖m i‖₊

theorem ContinuousAlternatingMap.isLeast_opNNNorm {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (f : E [⋀^ι]→L[𝕜] F) : IsLeast {C : NNReal | ∀ (m : ι → E), ‖f m‖₊ ≤ C * ∏ i : ι, ‖m i‖₊} ‖f‖₊

theorem ContinuousAlternatingMap.opNNNorm_prod {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : E [⋀^ι]→L[𝕜] F) (g : E [⋀^ι]→L[𝕜] G) : ‖f.prod g‖₊ = max ‖f‖₊ ‖g‖₊

theorem ContinuousAlternatingMap.opNorm_prod {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : E [⋀^ι]→L[𝕜] F) (g : E [⋀^ι]→L[𝕜] G) : ‖f.prod g‖ = max ‖f‖ ‖g‖

theorem ContinuousAlternatingMap.opNNNorm_pi {𝕜 : Type u} {E : Type wE} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] {ι' : Type u_1} [Fintype ι'] {F : ι' → Type u_2} [(i' : ι') → SeminormedAddCommGroup (F i')] [(i' : ι') → NormedSpace 𝕜 (F i')] (f : (i' : ι') → E [⋀^ι]→L[𝕜] F i') : ‖pi f‖₊ = ‖f‖₊

theorem ContinuousAlternatingMap.opNorm_pi {𝕜 : Type u} {E : Type wE} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] {ι' : Type u_1} [Fintype ι'] {F : ι' → Type u_2} [(i' : ι') → SeminormedAddCommGroup (F i')] [(i' : ι') → NormedSpace 𝕜 (F i')] (f : (i' : ι') → E [⋀^ι]→L[𝕜] F i') : ‖pi f‖ = ‖f‖

instance ContinuousAlternatingMap.instNormedSpace {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] {𝕜' : Type u_1} [NormedField 𝕜'] [NormedSpace 𝕜' F] [SMulCommClass 𝕜 𝕜' F] : NormedSpace 𝕜' (E [⋀^ι]→L[𝕜] F)

Equations

• ContinuousAlternatingMap.instNormedSpace = { toModule := ContinuousAlternatingMap.instModule, norm_smul_le := ⋯ }

@[simp]

theorem ContinuousAlternatingMap.norm_ofSubsingleton {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] [Subsingleton ι] (i : ι) (f : E →L[𝕜] F) : ‖(ofSubsingleton 𝕜 E F i) f‖ = ‖f‖

@[simp]

theorem ContinuousAlternatingMap.nnnorm_ofSubsingleton {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] [Subsingleton ι] (i : ι) (f : E →L[𝕜] F) : ‖(ofSubsingleton 𝕜 E F i) f‖₊ = ‖f‖₊

def ContinuousAlternatingMap.ofSubsingletonLIE {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] [Subsingleton ι] (i : ι) : (E →L[𝕜] F) ≃ₗᵢ[𝕜] E [⋀^ι]→L[𝕜] F

ContinuousAlternatingMap.ofSubsingleton as a linear isometry.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousAlternatingMap.ofSubsingletonLIE_apply {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] [Subsingleton ι] (i : ι) (a✝ : E →L[𝕜] F) : (ofSubsingletonLIE i) a✝ = (ofSubsingleton 𝕜 E F i) a✝

@[simp]

theorem ContinuousAlternatingMap.ofSubsingletonLIE_symm_apply {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] [Subsingleton ι] (i : ι) (a✝ : E [⋀^ι]→L[𝕜] F) : (ofSubsingletonLIE i).symm a✝ = (ofSubsingleton 𝕜 E F i).symm a✝

theorem ContinuousAlternatingMap.norm_ofSubsingleton_id_le {𝕜 : Type u} {E : Type wE} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] [Subsingleton ι] (i : ι) : ‖(ofSubsingleton 𝕜 E E i) (ContinuousLinearMap.id 𝕜 E)‖ ≤ 1

theorem ContinuousAlternatingMap.nnnorm_ofSubsingleton_id_le {𝕜 : Type u} {E : Type wE} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] [Subsingleton ι] (i : ι) : ‖(ofSubsingleton 𝕜 E E i) (ContinuousLinearMap.id 𝕜 E)‖₊ ≤ 1

@[simp]

theorem ContinuousAlternatingMap.norm_constOfIsEmpty (𝕜 : Type u) (E : Type wE) {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] [IsEmpty ι] (x : F) : ‖constOfIsEmpty 𝕜 E ι x‖ = ‖x‖

@[simp]

theorem ContinuousAlternatingMap.nnnorm_constOfIsEmpty (𝕜 : Type u) (E : Type wE) {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] [IsEmpty ι] (x : F) : ‖constOfIsEmpty 𝕜 E ι x‖₊ = ‖x‖₊

def ContinuousAlternatingMap.prodLIE (𝕜 : Type u) (E : Type wE) (F : Type wF) (G : Type wG) {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] : E [⋀^ι]→L[𝕜] F × E [⋀^ι]→L[𝕜] G ≃ₗᵢ[𝕜] E [⋀^ι]→L[𝕜] (F × G)

ContinuousAlternatingMap.prod as a LinearIsometryEquiv.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousAlternatingMap.prodLIE_symm_apply (𝕜 : Type u) (E : Type wE) (F : Type wF) (G : Type wG) {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : E [⋀^ι]→L[𝕜] (F × G)) : (prodLIE 𝕜 E F G).symm f = ((ContinuousLinearMap.fst 𝕜 F G).compContinuousAlternatingMap f, (ContinuousLinearMap.snd 𝕜 F G).compContinuousAlternatingMap f)

@[simp]

theorem ContinuousAlternatingMap.prodLIE_apply (𝕜 : Type u) (E : Type wE) (F : Type wF) (G : Type wG) {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : E [⋀^ι]→L[𝕜] F × E [⋀^ι]→L[𝕜] G) : (prodLIE 𝕜 E F G) f = f.1.prod f.2

def ContinuousAlternatingMap.piLIE (𝕜 : Type u) (E : Type wE) {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] {ι' : Type u_1} [Fintype ι'] {F : ι' → Type u_2} [(i' : ι') → SeminormedAddCommGroup (F i')] [(i' : ι') → NormedSpace 𝕜 (F i')] : ((i' : ι') → E [⋀^ι]→L[𝕜] F i') ≃ₗᵢ[𝕜] E [⋀^ι]→L[𝕜] ((i : ι') → F i)

ContinuousAlternatingMap.pi as a LinearIsometryEquiv.

Equations

• ContinuousAlternatingMap.piLIE 𝕜 E = { toLinearEquiv := ContinuousAlternatingMap.piLinearEquiv, norm_map' := ⋯ }

@[simp]

theorem ContinuousAlternatingMap.piLIE_symm_apply_apply (𝕜 : Type u) (E : Type wE) {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] {ι' : Type u_1} [Fintype ι'] {F : ι' → Type u_2} [(i' : ι') → SeminormedAddCommGroup (F i')] [(i' : ι') → NormedSpace 𝕜 (F i')] (a✝ : E [⋀^ι]→L[𝕜] ((i : ι') → F i)) (i : ι') (a✝¹ : (i : ι) → (fun (x : ι) => E) i) : ((piLIE 𝕜 E).symm a✝ i) a✝¹ = a✝ a✝¹ i

@[simp]

theorem ContinuousAlternatingMap.piLIE_apply_apply (𝕜 : Type u) (E : Type wE) {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] {ι' : Type u_1} [Fintype ι'] {F : ι' → Type u_2} [(i' : ι') → SeminormedAddCommGroup (F i')] [(i' : ι') → NormedSpace 𝕜 (F i')] (a✝ : (i : ι') → E [⋀^ι]→L[𝕜] F i) (m : (i : ι) → (fun (x : ι) => E) i) (i : ι') : ((piLIE 𝕜 E) a✝) m i = (a✝ i) m

@[simp]

theorem ContinuousAlternatingMap.norm_restrictScalars {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] {f : E [⋀^ι]→L[𝕜] F} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [NormedSpace 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [NormedSpace 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] : ‖restrictScalars 𝕜' f‖ = ‖f‖

def ContinuousAlternatingMap.restrictScalarsLI {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (𝕜' : Type u_1) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [NormedSpace 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [NormedSpace 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] : E [⋀^ι]→L[𝕜] F →ₗᵢ[𝕜'] E [⋀^ι]→L[𝕜'] F

ContinuousAlternatingMap.restrictScalars as a LinearIsometry.

Equations

• ContinuousAlternatingMap.restrictScalarsLI 𝕜' = { toFun := ContinuousAlternatingMap.restrictScalars 𝕜', map_add' := ⋯, map_smul' := ⋯, norm_map' := ⋯ }

@[simp]

theorem ContinuousAlternatingMap.restrictScalarsLI_apply {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (𝕜' : Type u_1) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [NormedSpace 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [NormedSpace 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] (f : E [⋀^ι]→L[𝕜] F) : (restrictScalarsLI 𝕜') f = restrictScalars 𝕜' f

theorem ContinuousAlternatingMap.norm_image_sub_le' {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] [DecidableEq ι] (f : E [⋀^ι]→L[𝕜] F) (m₁ m₂ : ι → E) : ‖f m₁ - f m₂‖ ≤ ‖f‖ * ∑ i : ι, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else 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 ContinuousAlternatingMap.norm_image_sub_le {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (f : E [⋀^ι]→L[𝕜] F) (m₁ m₂ : ι → E) : ‖f m₁ - f m₂‖ ≤ ‖f‖ * ↑(Fintype.card ι) * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 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 AlternatingMap.mkContinuous_norm_le {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (f : E [⋀^ι]→ₗ[𝕜] F) {C : ℝ} (hC : 0 ≤ C) (H : ∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖) : ‖f.mkContinuous C H‖ ≤ C

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

theorem AlternatingMap.mkContinuous_norm_le' {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (f : E [⋀^ι]→ₗ[𝕜] F) {C : ℝ} (H : ∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖) : ‖f.mkContinuous C H‖ ≤ max C 0

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

theorem ContinuousLinearMap.norm_compContinuousAlternatingMap_le {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (g : F →L[𝕜] G) (f : E [⋀^ι]→L[𝕜] F) : ‖g.compContinuousAlternatingMap f‖ ≤ ‖g‖ * ‖f‖

def ContinuousLinearMap.compContinuousAlternatingMapCLM (𝕜 : Type u) (E : Type wE) (F : Type wF) (G : Type wG) {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] : (F →L[𝕜] G) →L[𝕜] E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G

ContinuousLinearMap.compContinuousAlternatingMap as a bundled continuous bilinear map.

Equations

• ContinuousLinearMap.compContinuousAlternatingMapCLM 𝕜 E F G = (ContinuousLinearMap.compContinuousAlternatingMapₗ 𝕜 E F G).mkContinuous₂ 1 ⋯

@[simp]

theorem ContinuousLinearMap.compContinuousAlternatingMapCLM_apply_apply (𝕜 : Type u) (E : Type wE) (F : Type wF) (G : Type wG) {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (x : F →L[𝕜] G) (f : E [⋀^ι]→L[𝕜] F) : ((compContinuousAlternatingMapCLM 𝕜 E F G) x) f = x.compContinuousAlternatingMap f

def ContinuousLinearEquiv.continuousAlternatingMapCongrRight {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (g : F ≃L[𝕜] G) : E [⋀^ι]→L[𝕜] F ≃L[𝕜] E [⋀^ι]→L[𝕜] G

ContinuousLinearMap.compContinuousAlternatingMap as a bundled continuous linear equiv.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousLinearEquiv.continuousAlternatingMapCongrRight_apply {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (g : F ≃L[𝕜] G) (a✝ : E [⋀^ι]→L[𝕜] F) : g.continuousAlternatingMapCongrRight a✝ = (↑g).compContinuousAlternatingMap a✝

@[simp]

theorem ContinuousLinearEquiv.continuousAlternatingMapCongrRight_symm {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (g : F ≃L[𝕜] G) : g.continuousAlternatingMapCongrRight.symm = g.symm.continuousAlternatingMapCongrRight

def ContinuousLinearMap.flipAlternating {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : F →L[𝕜] E [⋀^ι]→L[𝕜] G) : E [⋀^ι]→L[𝕜] (F →L[𝕜] G)

Flip arguments in f : F →L[𝕜] E [⋀^ι]→L[𝕜] G to get ⋀^ι⟮𝕜; E; F →L[𝕜] G⟯

Equations

• f.flipAlternating = { toContinuousMultilinearMap := ((ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜).comp f).flipMultilinear, map_eq_zero_of_eq' := ⋯ }

@[simp]

theorem ContinuousLinearMap.flipAlternating_apply_apply {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : F →L[𝕜] E [⋀^ι]→L[𝕜] G) (m : (i : ι) → (fun (x : ι) => E) i) (x : F) : (f.flipAlternating m) x = (f x) m

theorem LinearIsometry.norm_compContinuousAlternatingMap {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (g : F →ₗᵢ[𝕜] G) (f : E [⋀^ι]→L[𝕜] F) : ‖g.toContinuousLinearMap.compContinuousAlternatingMap f‖ = ‖f‖

theorem ContinuousAlternatingMap.norm_compContinuousLinearMap_le {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : F [⋀^ι]→L[𝕜] G) (g : E →L[𝕜] F) : ‖f.compContinuousLinearMap g‖ ≤ ‖f‖ * ‖g‖ ^ Fintype.card ι

def ContinuousAlternatingMap.compContinuousLinearMapCLM {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : E →L[𝕜] F) : F [⋀^ι]→L[𝕜] G →L[𝕜] E [⋀^ι]→L[𝕜] G

Composition of a continuous alternating map and a continuous linear map as a bundled continuous linear map.

Equations

• ContinuousAlternatingMap.compContinuousLinearMapCLM f = (ContinuousAlternatingMap.compContinuousLinearMapₗ f).mkContinuous (‖f‖ ^ Fintype.card ι) ⋯

def ContinuousLinearEquiv.continuousAlternatingMapCongrLeft {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : E ≃L[𝕜] F) : E [⋀^ι]→L[𝕜] G ≃L[𝕜] F [⋀^ι]→L[𝕜] G

Given a continuous linear isomorphism between the domains, generate a continuous linear isomorphism between the spaces of continuous alternating maps.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousLinearEquiv.continuousAlternatingMapCongrLeft_apply {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : E ≃L[𝕜] F) (g : E [⋀^ι]→L[𝕜] G) : f.continuousAlternatingMapCongrLeft g = g.compContinuousLinearMap ↑f.symm

def ContinuousLinearEquiv.continuousAlternatingMapCongr {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] {E' : Type u_1} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F' : Type u_2} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] (e : E ≃L[𝕜] E') (e' : F ≃L[𝕜] F') : E [⋀^ι]→L[𝕜] F ≃L[𝕜] E' [⋀^ι]→L[𝕜] F'

Continuous linear equivalences between the domains and the codomains generate a continuous linear equivalence between the spaces of continuous alternating maps.

Equations

• e.continuousAlternatingMapCongr e' = e.continuousAlternatingMapCongrLeft.trans e'.continuousAlternatingMapCongrRight

@[simp]

theorem ContinuousLinearEquiv.continuousAlternatingMapCongr_apply {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] {E' : Type u_1} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F' : Type u_2} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] (e : E ≃L[𝕜] E') (e' : F ≃L[𝕜] F') (a✝ : E [⋀^ι]→L[𝕜] F) : (e.continuousAlternatingMapCongr e') a✝ = (↑e').compContinuousAlternatingMap (a✝.compContinuousLinearMap ↑e.symm)

def AlternatingMap.mkContinuousLinear {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G) (C : ℝ) (H : ∀ (x : F) (m : ι → E), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖) : F →L[𝕜] E [⋀^ι]→L[𝕜] G

Given a map f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G and an estimate H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖, construct a continuous linear map from F to E [⋀^ι]→L[𝕜] G.

In order to lift, e.g., a map f : (E [⋀^ι]→ₗ[𝕜] F) →ₗ[𝕜] E' [⋀^ι]→ₗ[𝕜] G to a map (E [⋀^ι]→L[𝕜] F) →L[𝕜] E' [⋀^ι]→L[𝕜] G, one can apply this construction to f.comp ContinuousAlternatingMap.toAlternatingMapLinear which is a linear map from E [⋀^ι]→L[𝕜] F to E' [⋀^ι]→ₗ[𝕜] G.

Equations

• AlternatingMap.mkContinuousLinear f C H = { toFun := fun (x : F) => (f x).mkContinuous (C * ‖x‖) ⋯, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (max C 0) ⋯

theorem AlternatingMap.mkContinuousLinear_norm_le_max {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G) (C : ℝ) (H : ∀ (x : F) (m : ι → E), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖) : ‖mkContinuousLinear f C H‖ ≤ max C 0

theorem AlternatingMap.mkContinuousLinear_norm_le {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G) {C : ℝ} (hC : 0 ≤ C) (H : ∀ (x : F) (m : ι → E), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖) : ‖mkContinuousLinear f C H‖ ≤ C

def AlternatingMap.mkContinuousAlternating {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] {ι' : Type u_1} [Fintype ι'] (f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G) (C : ℝ) (H : ∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖) : E [⋀^ι]→L[𝕜] F [⋀^ι']→L[𝕜] G

Given a map f : E [⋀^ι]→ₗ[𝕜] (F [⋀^ι']→ₗ[𝕜] G) and an estimate H : ∀ m m', ‖f m m'‖ ≤ C * ∏ i, ‖m i‖ * ∏ i, ‖m' i‖, upgrade all AlternatingMaps in the type to ContinuousAlternatingMaps.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlternatingMap.mkContinuousAlternating_apply {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] {ι' : Type u_1} [Fintype ι'] (f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G) {C : ℝ} (H : ∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖) (m : ι → E) : ⇑((f.mkContinuousAlternating C H) m) = ⇑(f m)

theorem AlternatingMap.mkContinuousAlternating_norm_le_max {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] {ι' : Type u_1} [Fintype ι'] (f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G) {C : ℝ} (H : ∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖) : ‖f.mkContinuousAlternating C H‖ ≤ max C 0

theorem AlternatingMap.mkContinuousAlternating_norm_le {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] {ι' : Type u_1} [Fintype ι'] (f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G) {C : ℝ} (hC : 0 ≤ C) (H : ∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖) : ‖f.mkContinuousAlternating C H‖ ≤ C

Results that are only true if the target space is a NormedAddCommGroup (and not just a SeminormedAddCommGroup).

instance ContinuousAlternatingMap.instNormedAddCommGroup {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [Fintype ι] [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] : NormedAddCommGroup (E [⋀^ι]→L[𝕜] F)

Continuous alternating maps themselves form a normed group with respect to the operator norm.

Equations

• ContinuousAlternatingMap.instNormedAddCommGroup = NormedAddCommGroup.ofSeparation ⋯

theorem ContinuousAlternatingMap.norm_ofSubsingleton_id (𝕜 : Type u) (F : Type wF) {ι : Type v} [Fintype ι] [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [Subsingleton ι] [Nontrivial F] (i : ι) : ‖(ofSubsingleton 𝕜 F F i) (ContinuousLinearMap.id 𝕜 F)‖ = 1

theorem ContinuousAlternatingMap.nnnorm_ofSubsingleton_id (𝕜 : Type u) (F : Type wF) {ι : Type v} [Fintype ι] [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [Subsingleton ι] [Nontrivial F] (i : ι) : ‖(ofSubsingleton 𝕜 F F i) (ContinuousLinearMap.id 𝕜 F)‖₊ = 1

theorem AlternatingMap.bound_of_shell {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [Fintype ι] [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : F [⋀^ι]→ₗ[𝕜] E) {ε : ι → ℝ} {C : ℝ} {c : ι → 𝕜} (hε : ∀ (i : ι), 0 < ε i) (hc : ∀ (i : ι), 1 < ‖c i‖) (hf : ∀ (m : ι → F), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖) (m : ι → F) : ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖

If an alternating map in finitely many variables on a normed space 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.