English
There is eventual equality of coefficient values: for each f in a Cauchy filter, the coefficient functions stabilize on all d below a bound D.
Русский
Существует момент перехода: для каждого f в фильтре Cauchy коэффициентные функции стабилизируются на всех d ниже порога D.
LaTeX
$$$\forall f \text{ in } \mathcal F, \forall d, d < D, \text{coeff}(h_f,d) = f.d$$$
Lean4
theorem coeff_eventually_equal {ℱ : Filter K⸨X⸩} (hℱ : Cauchy ℱ) {D : ℤ} :
∀ᶠ f : K⸨X⸩ in ℱ, ∀ d, d < D → coeff hℱ d = f.coeff d := by
-- `φ` sends `d` to the set of Laurent Series having `d`th coefficient equal to `ℱ.coeff`.
let φ : ℤ → Set K⸨X⸩ := fun d ↦ {f | coeff hℱ d = f.coeff d}
have intersec₁ : (⋂ n ∈ Set.Iio D, φ n) ⊆ {x : K⸨X⸩ | ∀ d : ℤ, d < D → coeff hℱ d = x.coeff d} :=
by
intro _ hf
simpa only [Set.mem_iInter] using hf
let ℓ := (exists_lb_coeff_ne hℱ).choose
let N := max ℓ D
have intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ (⋂ n ∈ Set.Icc ℓ N, φ n) :=
by
simp only [Set.mem_Iio, Set.mem_Icc, Set.subset_iInter_iff]
intro i hi x hx
simp only [Set.mem_inter_iff, Set.mem_iInter, and_imp] at hx
by_cases H : i < ℓ
exacts [hx.1 _ H, hx.2 _ (le_of_not_gt H) <| le_of_lt <| lt_max_of_lt_right hi]
suffices (⋂ n ∈ Set.Iio ℓ, φ n) ∩ (⋂ n ∈ Set.Icc ℓ N, φ n) ∈ ℱ by
exact ℱ.sets_of_superset this <| intersec₂.trans intersec₁
· simp only [Set.mem_Iio, inter_mem_iff]
constructor
· have := (exists_lb_coeff_ne hℱ).choose_spec
rw [Filter.eventually_iff] at this
convert this
ext
simp only [Set.mem_iInter, Set.mem_setOf_eq]; rfl
· rw [biInter_mem (Set.finite_Icc ℓ N)]
intro _ _
apply coeff_tendsto hℱ
simp only [principal_singleton, mem_pure]; rfl
