English
The base embedding is strictly increasing: if x < y in its domain, then baseEmbedding(x) < baseEmbedding(y).
Русский
Базовое вложение строго возрастает: если x < y в области определения, то baseEmbedding(x) < baseEmbedding(y).
LaTeX
$$$\\text{StrictMono}(seed.baseEmbedding) $$$$
Lean4
theorem baseEmbedding_pos {x : seed.baseEmbedding.domain} (hx : 0 < x) : 0 < seed.baseEmbedding x := by
-- decompose `x` to sum of `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
have hfpos : 0 < (f.sum fun _ x ↦ x.val) := by
rw [hf]
simpa using hx
have hsupport : f.support.Nonempty := by
obtain hne := hfpos.ne.symm
contrapose! hne with hempty
apply DFinsupp.sum_eq_zero
intro c
simpa using DFinsupp.notMem_support_iff.mp (forall_not_of_not_exists hempty c)
have htop : f.support.min' hsupport ≠ ⊤ := by
by_contra! h
have h : ⊤ ∈ f.support := h ▸ f.support.min'_mem hsupport
rw [DFinsupp.mem_support_iff] at h
contrapose! h
rw [← Submodule.coe_eq_zero, ← Submodule.mem_bot K]
convert ← (f ⊤).prop
simp
-- The dictating term for `HahnSeries` < is at the lowest archimedean class of `f.support`
refine (HahnSeries.lt_iff _ _).mpr ⟨⟨f.support.min' hsupport, htop⟩, ?_, ?_⟩
· intro j hj
rw [seed.coeff_baseEmbedding hf.symm]
rw [DFinsupp.notMem_support_iff.mp ?_]
· simp
contrapose! hj
rw [← Subtype.coe_le_coe, Subtype.coe_mk]
exact Finset.min'_le f.support _ hj
rw [seed.coeff_baseEmbedding hf.symm]
suffices
(seed.coeff (f.support.min' hsupport)) 0 < (seed.coeff (f.support.min' hsupport)) (f (f.support.min' hsupport)) by
simpa using this
suffices 0 < (f (f.support.min' hsupport)).val
by
apply (seed.strictMono_coeff (f.support.min' hsupport))
simpa using this
apply pos_of_pos_of_mk_lt hfpos
rw [mk_sub_comm]
have hferase :
(f.sum fun _ x ↦ x.val) - (f (f.support.min' hsupport)).val =
∑ x ∈ f.support.erase (f.support.min' hsupport), (f x).val :=
sub_eq_of_eq_add (Finset.sum_erase_add _ _ (Finset.min'_mem _ hsupport)).symm
rw [hferase]
-- Now both sides are `mk (∑ ...)`
-- We rewrite them to `mk (dominating term)`
have hmono : StrictMonoOn (fun x ↦ ArchimedeanClass.mk (f x).val) f.support :=
by
intro c hc d hd h
simp only
rw [seed.archimedeanClassMk_of_mem_stratum (f c).prop (by simpa using hc)]
rw [seed.archimedeanClassMk_of_mem_stratum (f d).prop (by simpa using hd)]
exact h
rw [DFinsupp.sum, mk_sum hsupport hmono]
rw [seed.archimedeanClassMk_of_mem_stratum (f _).prop (by simpa using f.support.min'_mem hsupport)]
by_cases hsupport' : (f.support.erase (f.support.min' hsupport)).Nonempty
· rw [mk_sum hsupport' (hmono.mono (by simp))]
rw [seed.archimedeanClassMk_of_mem_stratum (f _).prop
(by simpa using (Finset.mem_erase.mp <| (f.support.erase _).min'_mem hsupport').2)]
apply Finset.min'_lt_of_mem_erase_min'
apply Finset.min'_mem _ _
· -- special case: `f` has a single term, and becomes 0 after removing it
have : f.support.erase (f.support.min' hsupport) = ∅ := Finset.not_nonempty_iff_eq_empty.mp hsupport'
simpa [this] using lt_top_iff_ne_top.mpr htop
