convexBodyLT' — Mathlib

English

There exists a variant g of f with controlled product at all places.

Русский

Существует вариант g для f с контролируемым произведением по всем местам.

LaTeX

$$$$ \exists g: InfinitePlace(K) \to NNReal, (\forall w, w \neq w_1 \to g(w)=f(w)) \land \prod_w g(w)^{mult(w)} = B. $$$$

Lean4

/-- A version of `convexBodyLT` with an additional condition at a fixed complex place. This is
needed to ensure the element constructed is not real, see for example
`exists_primitive_element_lt_of_isComplex`.
-/
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 } ↦
        if w = w₀ then {x | |x.re| < 1 ∧ |x.im| < (f w : ℝ) ^ 2} else ball 0 (f w)))

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