English
In the Partial setting, coefficients agree for all d when y and z are sufficiently close to x.
Русский
В частичном контексте коэффициенты совпадают для всех d при достаточной близости y и z к x.
LaTeX
$$$ (\forall d).\ (ofLex (f.val y)).coeff d = (ofLex (f.val z)).coeff d $$$
Lean4
/-- Evaluate coefficients of the `HahnSeries` given an arbitrary input that's not necessarily in
`f`'s domain. The coefficient is picked from `y` that is "close enough" to `x` (their difference
is in a higher `ArchimedeanClass`). If no such `y` exists (in other words, x is "isolated"), set the
coefficient to 0.
This doesn't immediately extend `f`'s domain to the entire module in a consistent way. Such
extension isn't necessarily linear.
-/
noncomputable def evalCoeff (x : M) (c : FiniteArchimedeanClass M) : R :=
open Classical in if h : ∃ y : f.val.domain, y.val - x ∈ ball K c then (ofLex (f.val h.choose)).coeff c else 0
