Theorems · Theorem · functional analysis

MultilinearMap.bound_of_shell

∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G) {ε : ι → ℝ} {C : ℝ}
  {c : ι → 𝕜},
  (∀ (i : ι), 0 < ε i) →
    (∀ (i : ι), 1 < ‖c i‖) →
      (∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖) →
        ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖

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

Defined in

Mathlib.Analysis.Normed.Module.Multilinear.Basic

Cited by

1 results in Mathlib

Foundations

Depth 124 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeNontriviallyNormedFieldNormedAddCommGroupNormedSpaceSeminormedAddCommGroupNormedSpace