projectiveSeminormAux — Mathlib

English

Define a lift of a product-like quantity on FreeAddMonoid to the real numbers, by summing over all expressions of a tensor as a product of norms.

Русский

Задаётся подъем (lift) проектной семиномормы на FreeAddMonoid, суммируя по выражениям тензора как произведение норм.

LaTeX

$$$ \\mathrm{projectiveSeminormAux} : FreeAddMonoid (𝕜 \\times \\Pi i, E_i) \\to \\mathbb{R} ,\\quad p \\mapsto \\sum (\\mathrm{norms\\ of\\ components}) $$$

Lean4

/-- A lift of the projective seminorm to `FreeAddMonoid (𝕜 × Π i, Eᵢ)`, useful to prove the
properties of `projectiveSeminorm`.
-/
def projectiveSeminormAux : FreeAddMonoid (𝕜 × Π i, E i) → ℝ := fun p =>
  (p.toList.map (fun p ↦ ‖p.1‖ * ∏ i, ‖p.2 i‖)).sum

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