logEmbedding_component_le — Mathlib

English

If a real-valued bound holds for the sup-norm of the log-embedding of x, then each non-w0 component is bounded by the same bound.

Русский

Если сверху для x верно неравенство для нормы лог-отображения, то каждая компонентa, отличная от специалного места w0, также ограничена этим пределом.

LaTeX

$$$0 \le r \Rightarrow ( \|\logEmbedding K x\| \le r) \Rightarrow \forall w, w \neq w_0 \Rightarrow |\logEmbedding K(Additive.ofMul x) w| \le r$$$

Lean4

theorem logEmbedding_component_le {r : ℝ} {x : (𝓞 K)ˣ} (hr : 0 ≤ r) (h : ‖logEmbedding K x‖ ≤ r)
    (w : { w : InfinitePlace K // w ≠ w₀ }) : |logEmbedding K (Additive.ofMul x) w| ≤ r :=
  by
  lift r to NNReal using hr
  simp_rw [Pi.norm_def, NNReal.coe_le_coe, Finset.sup_le_iff, ← NNReal.coe_le_coe] at h
  exact h w (mem_univ _)

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