English
There exists a lower bound N such that for almost all Laurent series f in a Cauchy filter, f.coeff n = 0 for all n < N.
Русский
Существует нижняя граница N такая, что для почти всех Лаурентовых серий f в границе Cauchy, коэффициенты f.coeff n равны нулю для всех n < N.
LaTeX
$$$\exists N, \forall^{\!} f : K\langle\langle X \rangle\rangle \text{ in } \mathcal F, \forall n < N, f.coeff n = 0$$$
Lean4
theorem exists_lb_eventual_support {ℱ : Filter K⸨X⸩} (hℱ : Cauchy ℱ) :
∃ N, ∀ᶠ f : K⸨X⸩ in ℱ, ∀ n < N, f.coeff n = (0 : K) :=
by
let entourage : Set (K⸨X⸩ × K⸨X⸩) := {P : K⸨X⸩ × K⸨X⸩ | Valued.v (P.snd - P.fst) < 1}
let ζ := Units.mk0 (G₀ := ℤᵐ⁰) _ (WithZero.coe_ne_zero (a := 1))
obtain ⟨S, ⟨hS, ⟨T, ⟨hT, H⟩⟩⟩⟩ :=
mem_prod_iff.mp <|
Filter.le_def.mp hℱ.2 entourage <| (Valued.hasBasis_uniformity K⸨X⸩ ℤᵐ⁰).mem_of_mem (i := ζ) (by tauto)
obtain ⟨f, hf⟩ := forall_mem_nonempty_iff_neBot.mpr hℱ.1 (S ∩ T) (inter_mem_iff.mpr ⟨hS, hT⟩)
obtain ⟨N, hN⟩ : ∃ N : ℤ, ∀ g : K⸨X⸩, Valued.v (g - f) ≤ 1 → ∀ n < N, g.coeff n = 0 :=
by
by_cases hf : f = 0
· refine ⟨0, fun x hg ↦ ?_⟩
rw [hf, sub_zero] at hg
exact (valuation_le_iff_coeff_lt_eq_zero K).mp hg
· refine ⟨min (f.2.isWF.min (HahnSeries.support_nonempty_iff.mpr hf)) 0 - 1, fun _ hg n hn ↦ ?_⟩
rw [eq_coeff_of_valuation_sub_lt K hg (d := 0)]
·
exact
Function.notMem_support.mp fun h ↦
f.2.isWF.not_lt_min (HahnSeries.support_nonempty_iff.mpr hf) h <|
lt_trans hn <| Int.sub_one_lt_iff.mpr <| min_le_left _ _
exact lt_of_lt_of_le hn <| le_of_lt (Int.sub_one_lt_of_le <| min_le_right _ _)
use N
apply mem_of_superset (inter_mem hS hT)
intro g hg
have h_prod : (f, g) ∈ S ×ˢ T := by simp [hf.1, hg.2]
refine hN g (le_of_lt ?_)
simpa using H h_prod
