English
Let f be a partial Hahn embedding. If there exists y in the domain of f with Archimedean class c = ArchimedeanClass(y − x), and there is no closer z to x whose difference has a higher Archimedean class, then the value f.eval(x) is given by a lexicographic truncation of a Hahn series associated to y; more precisely it equals toLex(HahnSeries.truncLTLinearMap(K, c, ofLex(f.val y))).
Русский
Пусть f — частичное отображение Хаана. Если существует y из области определения f и c = ArchimedeanClass(y − x), и не существует ближе к x z с разностью, имеющей более высокий Archimedeан класс, тогда значение f.eval(x) задаётся лексикографическим усечением соответствующей гамма-хаановой серии: f.eval(x) = toLex(HahnSeries.truncLTLinearMap(K, c, ofLex(f.val y))).
LaTeX
$$$\\forall [IsOrderedAddMonoid R] [Archimedean R] {x : M} {c : FiniteArchimedeanClass M} {y : f.val.domain} (hy : mk (y.val - x) = c.val) (h : ∀ z : f.val.domain, z.val - x \\notin ball K c),\\; f.eval x = toLex (HahnSeries.truncLTLinearMap K c (ofLex (f.val y)))$$$
Lean4
/-- If there is a `y` in `f`'s domain with `c = ArchimedeanClass (y - x)`, but there
is no closer `z` to `x` where the difference is of a higher `ArchimedeanClass`, then
`f.eval x` is simply `f.val y` truncated at `c`.
This doesn't mean every `x` can be evaluated this way: it is possible that one can find
an infinite chain of `y` that keeps getting closer to `x` in terms of Archimedean classes,
yet `x` is still isolated within a very high Archimedean class. In fact, in the next theorem,
we will show that there is always such chain for `x` not in `f`'s domain. -/
theorem eval_eq_truncLT [IsOrderedAddMonoid R] [Archimedean R] {x : M} {c : FiniteArchimedeanClass M} {y : f.val.domain}
(hy : mk (y.val - x) = c.val) (h : ∀ z : f.val.domain, z.val - x ∉ ball K c) :
f.eval x = toLex (HahnSeries.truncLTLinearMap K c (ofLex (f.val y))) :=
by
unfold eval
rw [toLex.injective.eq_iff]
ext d
simp only
obtain hd | hd := lt_or_ge d c
· rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_lt hd]
apply evalCoeff_eq
simpa [d.prop, hy] using hd
· rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_le hd]
apply evalCoeff_eq_zero
contrapose! h
obtain ⟨z, hz⟩ := h
exact ⟨z, ball_antitone K (by simpa using hd) hz⟩
