English
If f.eval x = f.val y for some y ∈ f.val.domain, then for all z ∈ f.val.domain we have mk(x − z) ≤ mk(x − y).
Русский
Если f.eval x = f.val y для некоторого y ∈ f.val.domain, то для всех z ∈ f.val.domain выполняется mk(x − z) ≤ mk(x − y).
LaTeX
$$$\\forall z\\in f.val.domain:\\; \\operatorname{mk}(x-z) \\le \\operatorname{mk}(x-y)$, при $f.eval x = f.val y$.$$
Lean4
/-- For `x` not in `f`'s domain, `f.eval x` is consistent with `f`'s monotonicity. -/
theorem eval_lt [IsOrderedAddMonoid R] [Archimedean R] {x : M} (hx : x ∉ f.val.domain) (y : f.val.domain)
(h : x < y.val) : f.eval x < f.val y := by
-- Expand the definition of `HahnSeries`' order. We need to find the first coefficient that
-- dictates the < relation. This coefficient is exactly at the Archimedean class of `y - x`
rw [HahnSeries.lt_iff]
have hxy0 : y.val - x ≠ 0 := sub_ne_zero_of_ne h.ne.symm
refine ⟨FiniteArchimedeanClass.mk (y.val - x) hxy0, ?_, ?_⟩
· -- All coefficients before the dictating term are the same
intro j hj
apply evalCoeff_eq
simpa [j.prop] using hj
have hyxtop : mk (y.val - x) ≠ ⊤ := by simp [hxy0]
suffices
f.evalCoeff x (FiniteArchimedeanClass.mk (y.val - x) hxy0) <
(ofLex (f.val y)).coeff (FiniteArchimedeanClass.mk (y.val - x) hxy0)
by simpa [eval] using this
obtain ⟨z, hz⟩ := f.exists_sub_mem_ball hx y
have hz' : z.val - x ∈ ball K (FiniteArchimedeanClass.mk (y.val - x) hxy0).val := hz
rw [f.evalCoeff_eq hz']
have hzy : z < y := by
change z.val < y.val
refine (sub_lt_sub_iff_right x).mp <| lt_of_mk_lt_mk_of_nonneg ?_ (sub_nonneg_of_le h.le)
simpa [hyxtop] using hz
have hzyne : z.val - y.val ≠ 0 := by
apply sub_ne_zero_of_ne
simpa using hzy.ne
have hzyclass : FiniteArchimedeanClass.mk (y.val - x) hxy0 = FiniteArchimedeanClass.mk (z.val - y.val) hzyne :=
by
suffices mk (y.val - x) = mk (z.val - y.val) by simpa [Subtype.eq_iff] using this
have : y.val - z.val = y.val - x + (x - z.val) := by abel
rw [mk_sub_comm z.val y.val, this]
refine (mk_add_eq_mk_left ?_).symm
rw [mk_sub_comm x z.val]
simpa [hyxtop] using hz
rw [← f.prop.strictMono.lt_iff_lt, HahnSeries.lt_iff] at hzy
obtain ⟨i, hj, hi⟩ := hzy
have hieq : i = FiniteArchimedeanClass.mk (y.val - x) hxy0 :=
by
apply le_antisymm
· by_contra! hlt
obtain hj := sub_eq_zero_of_eq (hj (FiniteArchimedeanClass.mk (y.val - x) hxy0) hlt)
contrapose! hj
rw [← HahnSeries.coeff_sub, ← ofLex_sub, ← LinearPMap.map_sub, hzyclass]
apply f.coeff_ne_zero
· contrapose! hi
rw [hzyclass] at hi
have hzy : z.val - y.val ∈ ball K i.val := by simpa [i.prop] using hi
exact (f.coeff_eq_of_mem y.val (by simp) hzy (by simp)).le
exact hieq ▸ hi
