log_le_of_logEmbedding_le — Mathlib

English

For r ∈ ℝ and x ∈ Units(𝒪_K), if ||logEmbedding K (Additive.ofMul x)|| ≤ r and the bound holds on norm, then for every infinite place w, |log(w x)| ≤ |InfinitePlace(K)| × r.

Русский

Для r ∈ ℝ и x ∈ Units(𝒪_K), если ||logEmbedding K (Additive.ofMul x)|| ≤ r и выполняется оценка нормы, то для каждого бесконечного места w выполняется |log(w x)| ≤ |InfinitePlace(K)| × r.

LaTeX

$$$\forall r\in\mathbb{R}, \forall x \in \mathrm{Units}(\mathcal{O}_K),\; \|\logEmbedding K (Additive.ofMul x)\| \le r \Rightarrow \forall w \in \mathrm{InfinitePlace}(K),\; |\log(w x)| \le |\mathrm{InfinitePlace}(K)| \cdot r$$$

Lean4

theorem log_le_of_logEmbedding_le {r : ℝ} {x : (𝓞 K)ˣ} (hr : 0 ≤ r) (h : ‖logEmbedding K (Additive.ofMul x)‖ ≤ r)
    (w : InfinitePlace K) : |Real.log (w x)| ≤ (Fintype.card (InfinitePlace K)) * r :=
  by
  have tool : ∀ x : ℝ, 0 ≤ x → x ≤ mult w * x := fun x hx ↦
    by
    nth_rw 1 [← one_mul x]
    refine mul_le_mul ?_ le_rfl hx ?_
    all_goals { rw [mult]; split_ifs <;> norm_num
    }
  by_cases hw : w = w₀
  · have hyp := congr_arg (‖·‖) (sum_logEmbedding_component x).symm
    replace hyp := (le_of_eq hyp).trans (norm_sum_le _ _)
    simp_rw [norm_mul, norm_neg, Real.norm_eq_abs, Nat.abs_cast] at hyp
    refine (le_trans ?_ hyp).trans ?_
    · rw [← hw]
      exact tool _ (abs_nonneg _)
    · refine (sum_le_card_nsmul univ _ _ (fun w _ ↦ logEmbedding_component_le hr h w)).trans ?_
      rw [nsmul_eq_mul]
      refine mul_le_mul ?_ le_rfl hr (Fintype.card (InfinitePlace K)).cast_nonneg
      simp
  · have hyp := logEmbedding_component_le hr h ⟨w, hw⟩
    rw [logEmbedding_component, abs_mul, Nat.abs_cast] at hyp
    refine (le_trans ?_ hyp).trans ?_
    · exact tool _ (abs_nonneg _)
    · nth_rw 1 [← one_mul r]
      exact mul_le_mul (Nat.one_le_cast.mpr Fintype.card_pos) (le_of_eq rfl) hr (Nat.cast_nonneg _)

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