English
If y and z lie near x within c, then the corresponding coefficients of f.val y and f.val z in all d ≤ c agree.
Русский
Если y и z близки к x в пределах c, то соответствующие коэффициенты f.val y и f.val z в всх d ≤ c совпадают.
LaTeX
$$$\forall d\le c\, ,\ (ofLex (f.val y)).coeff d = (ofLex (f.val z)).coeff d$$$
Lean4
/-- For `x` within a ball of Archimedean class `c`, `f.val x`'coefficient at `d` vanishes
for `d ≤ c`. -/
theorem coeff_eq_zero_of_mem [IsOrderedAddMonoid R] [Archimedean R] {c : ArchimedeanClass M} {x : f.val.domain}
(hx : x.val ∈ ball K c) {d : FiniteArchimedeanClass M} (hd : d.val ≤ c) : (ofLex (f.val x)).coeff d = 0 :=
by
by_cases hc : c = ⊤
· rw [hc] at hx
have hx : x = 0 := by simpa using hx
simp [hx]
apply HahnSeries.coeff_eq_zero_of_lt_orderTop
apply_fun FiniteArchimedeanClass.withTopOrderIso _
rw [orderTop_eq_archimedeanClassMk, FiniteArchimedeanClass.withTopOrderIso_apply_coe]
apply lt_of_le_of_lt hd
simpa [hc] using hx
