projectiveSeminorm — Mathlib

English

For a pure tensor m, projectiveSeminorm(m) ≤ ∏_i ∥m_i∥.

Русский

Для чистого тензора m: projectiveSeminorm(m) ≤ ∏_i ∥m_i∥.

LaTeX

$$$ \\mathrm{projectiveSeminorm}(\\otimes_i m_i) \\leq \\prod_i \\|m_i\\| $$$

Lean4

/-- The projective seminorm on `⨂[𝕜] i, Eᵢ`. It sends an element `x` of `⨂[𝕜] i, Eᵢ` to the
infimum over all expressions of `x` as `∑ j, ⨂ₜ[𝕜] mⱼ i` (with the `mⱼ` ∈ `Π i, Eᵢ`)
of `∑ j, Π i, ‖mⱼ i‖`.
-/
noncomputable def projectiveSeminorm : Seminorm 𝕜 (⨂[𝕜] i, E i) :=
  by
  refine Seminorm.ofSMulLE (fun x ↦ iInf (fun (p : lifts x) ↦ projectiveSeminormAux p.1)) ?_ ?_ ?_
  · refine le_antisymm ?_ ?_
    · refine ciInf_le_of_le (bddBelow_projectiveSemiNormAux (0 : ⨂[𝕜] i, E i)) ⟨0, lifts_zero⟩ ?_
      rfl
    · letI : Nonempty (lifts 0) := ⟨0, lifts_zero (R := 𝕜) (s := E)⟩
      exact le_ciInf (fun p ↦ projectiveSeminormAux_nonneg p.1)
  · intro x y
    letI := nonempty_subtype.mpr (nonempty_lifts x); letI := nonempty_subtype.mpr (nonempty_lifts y)
    exact
      le_ciInf_add_ciInf
        (fun p q ↦
          ciInf_le_of_le (bddBelow_projectiveSemiNormAux _) ⟨p.1 + q.1, lifts_add p.2 q.2⟩
            (projectiveSeminormAux_add_le p.1 q.1))
  · intro a x
    letI := nonempty_subtype.mpr (nonempty_lifts x)
    rw [Real.mul_iInf_of_nonneg (norm_nonneg _)]
    refine le_ciInf ?_
    intro p
    rw [← projectiveSeminormAux_smul]
    exact
      ciInf_le_of_le (bddBelow_projectiveSemiNormAux _) ⟨(p.1.map (fun y ↦ (a * y.1, y.2))), lifts_smul p.2 a⟩
        (le_refl _)

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