English
If f ≠ 0 and f(m) = 0 for all m < n, then n ≤ order(ofSuppBddBelow f (forallLTEqZero_supp_BddBelow f n hn)).
Русский
Если f не равно нулю и для всех m < n имеет f(m) = 0, то n ≤ order(ofSuppBddBelow f (forallLTEqZero_supp_BddBelow f n hn)).
LaTeX
$$n ≤ order (ofSuppBddBelow f (forallLTEqZero_supp_BddBelow f n hn))$$
Lean4
theorem order_ofForallLtEqZero [Zero Γ] (f : Γ → R) (hf : f ≠ 0) (n : Γ) (hn : ∀ (m : Γ), m < n → f m = 0) :
n ≤ order (ofSuppBddBelow f (forallLTEqZero_supp_BddBelow f n hn)) :=
by
dsimp only [order]
by_cases h : ofSuppBddBelow f (forallLTEqZero_supp_BddBelow f n hn) = 0
cases h
· exact (hf rfl).elim
simp_all only [dite_false]
rw [Set.IsWF.le_min_iff]
intro m hm
rw [HahnSeries.support, Function.mem_support, ne_eq] at hm
exact not_lt.mp (mt (hn m) hm)
