English
The Lex-truncated image of f.eval x lies in the range of the extended map f.extendFun hx.
Русский
Изображение усечения в Lex принадлежит диапазону расширенного отображения f.extendFun hx.
LaTeX
$$$\\mathrm{toLex}(\\ HahnSeries.truncLTLinearMap\\ K c\\ (ofLex (f\\!\\left(x\\right)))) \\in \\mathrm{range}(f.extendFun\\; hx).toFun$$$
Lean4
theorem truncLT_eval_mem_range_extendFun [IsOrderedAddMonoid R] [Archimedean R] {x : M} (hx : x ∉ f.val.domain)
(c : FiniteArchimedeanClass M) :
toLex (HahnSeries.truncLTLinearMap K c (ofLex (f.eval x))) ∈ LinearMap.range (f.extendFun hx).toFun :=
by
rw [extendFun, LinearMap.mem_range]
by_cases h : ∃ y : f.val.domain, y.val - x ∈ ball K c
· -- if `x` is not isolated within `c`, the truncation at `c` equals to truncating
-- a nearby `y` in the domain
obtain ⟨y, hy⟩ := h
obtain ⟨z, hz⟩ := LinearMap.mem_range.mp (f.prop.truncLT_mem_range y c)
refine ⟨⟨z.val, by simpa using Submodule.mem_sup_left z.prop⟩, ?_⟩
rw [LinearPMap.toFun_eq_coe] at hz
rw [LinearPMap.toFun_eq_coe, LinearPMap.supSpanSingleton_apply_mk_of_mem _ _ _ z.prop]
rw [hz, toLex_inj]
ext d
obtain hdc | hdc := lt_or_ge d c
· simp_rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_lt hdc]
refine (f.evalCoeff_eq (Set.mem_of_mem_of_subset hy ?_)).symm
simpa using ball_antitone K hdc.le
· simp_rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_le hdc]
· -- if `x` is isolated within c, truncating has no effect because the trailing coefficients
-- are already 0
refine ⟨⟨x, by simpa using Submodule.mem_sup_right (Submodule.mem_span_singleton_self x)⟩, ?_⟩
apply_fun ofLex
rw [ofLex_toLex, LinearPMap.toFun_eq_coe, LinearPMap.supSpanSingleton_apply_self]
ext d
obtain hdc | hdc := lt_or_ge d c
· rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_lt hdc]
rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_le hdc, eval, ofLex_toLex]
apply f.evalCoeff_eq_zero
contrapose! h
obtain ⟨y, hy⟩ := h
exact ⟨y, Set.mem_of_mem_of_subset hy (by simpa using ball_antitone K hdc)⟩
