English
If f.eval x = f.val y for some y ∈ f.val.domain, then for every z ∈ f.val.domain, the Archimedean class mk(x − z) is bounded above by mk(x − y).
Русский
Если f.eval x = f.val y для некоторого y ∈ домена f, тогда для любого z ∈ домена f величина ArchimedeanClass.mk(х − z) не превосходит mk(х − y).
LaTeX
$$$\\forall z\\in f.val.domain,\; \\operatorname{mk}(x-z) \\le \\operatorname{mk}(x-y)$ при $f.eval x = f.val y$, $y\\in f.val.domain$.$$
Lean4
/-- If `f.eval x = f.val y`, then for any `z` in the domain, `x - z` can't be closer than `x - y`
in terms of Archimedean classes. -/
theorem archimedeanClassMk_le_of_eval_eq [IsOrderedAddMonoid R] [Archimedean R] {x : M} {y : f.val.domain}
(h : f.eval x = f.val y) (z : f.val.domain) : mk (x - z.val) ≤ mk (x - y.val) :=
by
have : x - y.val = x - z.val + (z.val - y.val) := by abel
rw [this]
apply mk_left_le_mk_add
by_cases hyz : z.val - y.val = 0
· simp [hyz]
have h1 (c : FiniteArchimedeanClass M) (hc : c.val < mk (x - z.val)) :
(ofLex (f.eval x)).coeff c = (ofLex (f.val z)).coeff c :=
by
rw [mk_sub_comm] at hc
simp_rw [eval, ofLex_toLex]
apply evalCoeff_eq
simpa [c.prop] using hc
have h2 : ∀ c : FiniteArchimedeanClass M, c.val < mk (x - z.val) → (ofLex (f.val (z - y))).coeff c = 0 :=
by
intro c hc
rw [LinearPMap.map_sub, ofLex_sub, HahnSeries.coeff_sub, sub_eq_zero, ← h]
exact (h1 c hc).symm
contrapose! h2
exact ⟨FiniteArchimedeanClass.mk (z.val - y.val) hyz, h2, coeff_ne_zero _ _⟩
