English
There is a linear map realSpaceToLogSpace from realSpace(K) to the space of functions on {w ≠ w0} given by a specific coordinatewise formula involving x, mult, and the dimension finrank(K/ℚ).
Русский
Существует линейное отображение realSpaceToLogSpace: realSpace(K) → {w ≠ w0} → ℝ, заданное по координатам через x, mult и размерности finrank(ℚ, K).
LaTeX
$$$\text{realSpaceToLogSpace}: \mathrm{realSpace}(K) \to (\{ w : \mathrm{InfinitePlace}(K) \setminus \{w_0\} \}) \to \mathbb{R}$ with
(toFun)\,x\,w = x(w) - w.1.mult \cdot \Big(\sum_{w'} x(w')\Big) \cdot (\operatorname{finrank} \mathbb{Q} K)^{-1}$$$
Lean4
/-- An auxiliary map from `realSpace K` to `logSpace K` used to prove that `completeFamily` is
linearly independent, see `linearIndependent_completeFamily`.
-/
def realSpaceToLogSpace : realSpace K →ₗ[ℝ] { w : InfinitePlace K // w ≠ w₀ } → ℝ
where
toFun := fun x w ↦ x w.1 - w.1.mult * (∑ w', x w') * (Module.finrank ℚ K : ℝ)⁻¹
map_add' := fun _ _ ↦ funext fun _ ↦ by simpa [sum_add_distrib] using by ring
map_smul' := fun _ _ ↦ funext fun _ ↦ by simpa [← mul_sum] using by ring
