English
For any x in the base embedding domain and any finite Archimedean class c, the truncated left Hahn series built from ofLex (seed.baseEmbedding x) lies in the range of seed.baseEmbedding.toFun.
Русский
Для любого x в области определения базового вложения и любого конечного архимедова класса c отсечённая слева ряд Гохана, построенный из ofLex(seed.baseEmbedding x), лежит в диапазоне seed.baseEmbedding.toFun.
LaTeX
$$$\text{toLex}(\text{HahnSeries.truncLTLinearMap } K\ c\ (ofLex(seed.baseEmbedding x))) \in \text{LinearMap.range}(seed.baseEmbedding.toFun)$$$
Lean4
theorem truncLT_mem_range_baseEmbedding (x : seed.baseEmbedding.domain) (c : FiniteArchimedeanClass M) :
toLex (HahnSeries.truncLTLinearMap K c (ofLex (seed.baseEmbedding x))) ∈ LinearMap.range seed.baseEmbedding.toFun :=
by
-- decompose `x` to `stratum`
have hmem : x.val ∈ seed.baseEmbedding.domain := x.prop
simp_rw [seed.domain_baseEmbedding] at hmem
obtain ⟨f, hf⟩ := (Submodule.mem_iSup_iff_exists_dfinsupp' _ _).mp hmem
let f' : Π₀ (i : ArchimedeanClass M), seed.stratum i :=
DFinsupp.mk f.support fun d ↦ if c.val ≤ d.val then 0 else f d.val
refine ⟨⟨f'.sum fun d x ↦ x.val, ?_⟩, ?_⟩
· rw [seed.domain_baseEmbedding, ArchimedeanStrata.baseDomain, Submodule.mem_iSup_iff_exists_dfinsupp']
use f'
apply_fun ofLex
rw [ofLex_toLex, LinearPMap.toFun_eq_coe]
ext d
rw [seed.coeff_baseEmbedding rfl]
unfold f'
obtain hdc | hdc := lt_or_ge d c
· rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_lt hdc, seed.coeff_baseEmbedding hf.symm]
apply congrArg
have hcd : ¬c.val ≤ d.val := not_le_of_gt hdc
simp only [DFinsupp.mk_apply, hcd, ↓reduceIte]
aesop
· rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_le hdc]
have hcd : c.val ≤ d.val := hdc
simp only [DFinsupp.mk_apply, hcd, ↓reduceIte]
convert LinearMap.map_zero _
simp