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)))