injectiveSeminorm_le_projectiveSeminorm

English

For a simple tensor x = (v_i) with v_i ∈ E_i, the injective seminorm is bounded by the product of norms of v_i.

Русский

Для простого тензора x = \\otimes_i v_i нормированность инъективна ограничена произведением норм векторов v_i.

LaTeX

$$injectiveSeminorm (tprod i, v_i) ≤ ∏ i, ‖v_i‖$$

Lean4

theorem injectiveSeminorm_le_projectiveSeminorm : injectiveSeminorm (𝕜 := 𝕜) (E := E) ≤ projectiveSeminorm :=
  by
  rw [injectiveSeminorm]
  refine csSup_le ?_ ?_
  · existsi 0
    simp only [Set.mem_setOf_eq]
    existsi PUnit, inferInstance, inferInstance
    ext x
    simp only [Seminorm.zero_apply, Seminorm.comp_apply, coe_normSeminorm]
    rw [Subsingleton.elim (toDualContinuousMultilinearMap PUnit x) 0, norm_zero]
  · intro p hp
    simp only [Set.mem_setOf_eq] at hp
    obtain ⟨G, _, _, h⟩ := hp
    rw [h]; intro x; simp only [Seminorm.comp_apply, coe_normSeminorm]
    exact toDualContinuousMultilinearMap_le_projectiveSeminorm _

Похожие утверждения