logMap — Mathlib

English

There exists a nonzero a ∈ I with a bounded norm under a Minkowski-type bound in the convex body context.

Русский

Существуют не нулевые элементы a ∈ I с ограниченной нормой в рамках Минковского типа границ внутри выпуклого тела.

LaTeX

$$$\exists a \in I, a \neq 0 \land |\operatorname{Norm}_{\mathbb{Q}}(a)| \le \dots$$$

Lean4

/-- The map from the mixed space to `logSpace K` defined in such way that: 1) it factors the map
`logEmbedding`, see `logMap_eq_logEmbedding`; 2) it is constant on the sets
`{c • x | c ∈ ℝ, c ≠ 0}` if `norm x ≠ 0`, see `logMap_real_smul`. -/
def logMap (x : mixedSpace K) : logSpace K := fun w ↦
  mult w.val * (Real.log (normAtPlace w.val x) - Real.log (mixedEmbedding.norm x) * (finrank ℚ K : ℝ)⁻¹)

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