convexBodyLT — Mathlib

English

The convex body LT is the product of unit balls in the real and complex infinite places, scaled by f.

Русский

Выпуклое тело LT есть произведение шаров единичного радиуса в реальных и комплексных местах, масштабируемое f.

LaTeX

$$$$\text{convexBodyLT}(K,f) = \Big(\prod_{w\in \{ w\text{ real} \}} B(0,f(w))\Big) \times \Big(\prod_{w\in \{ w\text{ complex} \}} B(0,f(w))\Big).$$$$

Lean4

/-- The convex body defined by `f`: the set of points `x : E` such that `‖x w‖ < f w` for all
infinite places `w`. -/
abbrev convexBodyLT : Set (mixedSpace K) :=
  (Set.univ.pi (fun w : { w : InfinitePlace K // IsReal w } => ball 0 (f w))) ×ˢ
    (Set.univ.pi (fun w : { w : InfinitePlace K // IsComplex w } => ball 0 (f w)))

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