English
convexBodyLT' is a convex set in the real vector space sense.
Русский
convexBodyLT' выпукло в смысле вещественного вектора пространства.
LaTeX
$$$$ \operatorname{Convex}_{\mathbb{R}}(\operatorname{convexBodyLT'}(K,f,w_0)). $$$$
Lean4
theorem convexBodyLT'_mem {x : K} :
mixedEmbedding K x ∈ convexBodyLT' K f w₀ ↔
(∀ w : InfinitePlace K, w ≠ w₀ → w x < f w) ∧
|(w₀.val.embedding x).re| < 1 ∧ |(w₀.val.embedding x).im| < (f w₀ : ℝ) ^ 2 :=
by
simp_rw [mixedEmbedding, RingHom.prod_apply, Set.mem_prod, Set.mem_pi, Set.mem_univ, forall_true_left,
Pi.ringHom_apply, mem_ball_zero_iff, ← Complex.norm_real, embedding_of_isReal_apply, norm_embedding_eq,
Subtype.forall]
refine ⟨fun ⟨h₁, h₂⟩ ↦ ⟨fun w h_ne ↦ ?_, ?_⟩, fun ⟨h₁, h₂⟩ ↦ ⟨fun w hw ↦ ?_, fun w hw ↦ ?_⟩⟩
· by_cases hw : IsReal w
· exact norm_embedding_eq w _ ▸ h₁ w hw
· specialize h₂ w (not_isReal_iff_isComplex.mp hw)
rw [apply_ite (w.embedding x ∈ ·), Set.mem_setOf_eq, mem_ball_zero_iff, norm_embedding_eq] at h₂
rwa [if_neg (by exact Subtype.coe_ne_coe.1 h_ne)] at h₂
· simpa [if_true] using h₂ w₀.val w₀.prop
· exact h₁ w (ne_of_isReal_isComplex hw w₀.prop)
· by_cases h_ne : w = w₀
· simpa [h_ne]
· rw [if_neg (by exact Subtype.coe_ne_coe.1 h_ne)]
rw [mem_ball_zero_iff, norm_embedding_eq]
exact h₁ w h_ne
