English
The source of the map expMap on the fundamental cone is all of real space.
Русский
Область определения expMap на фундаментальном коне равна всему пространству действительных чисел.
LaTeX
$$$\\operatorname{expMap}.\\mathrm{source} = (\\mathbb{R}^{\\text{realSpace}}) = \\mathrm{Set.univ}$$$
Lean4
/-- The component of `expMap` at the place `w`.
-/
@[simps]
def expMap_single (w : InfinitePlace K) : OpenPartialHomeomorph ℝ ℝ
where
toFun := fun x ↦ Real.exp ((w.mult : ℝ)⁻¹ * x)
invFun := fun x ↦ w.mult * Real.log x
source := Set.univ
target := Set.Ioi 0
open_source := isOpen_univ
open_target := isOpen_Ioi
map_source' _ _ := Real.exp_pos _
map_target' _ _ := trivial
left_inv' _ _ := by simp only [Real.log_exp, mul_inv_cancel_left₀ mult_coe_ne_zero]
right_inv' _ h := by simp only [inv_mul_cancel_left₀ mult_coe_ne_zero, Real.exp_log h]
continuousOn_toFun := (continuousOn_const.mul continuousOn_id).rexp
continuousOn_invFun := continuousOn_const.mul (Real.continuousOn_log.mono (by aesop))
