convexBodyLT'Factor — Mathlib

English

The set convexBodyLT' is convex in the real sense for every fixed w0.

Русский

Для фиксированного w0 множество convexBodyLT' выпукло по отношению к вещественному полю.

LaTeX

$$$$ Convex_{\mathbb{R}}(convexBodyLT'(K,f,w_0)) $$$$

Lean4

/-- The fudge factor that appears in the formula for the volume of `convexBodyLT'`. -/
noncomputable abbrev convexBodyLT'Factor : ℝ≥0 :=
  (2 : ℝ≥0) ^ (nrRealPlaces K + 2) * NNReal.pi ^ (nrComplexPlaces K - 1)

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