truncLT_mem_range_baseEmbedding — Mathlib

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

Похожие утверждения