English
If f is IsRestricted with parameter c, then the set convergenceSet(c,f) is bounded above.
Русский
Если f ограничено по c, множество convergenceSet(c,f) ограничено сверху.
LaTeX
$$$\mathrm{IsRestricted}(c,f) \Rightarrow \mathrm{BddAbove}(\mathrm{convergenceSet}(c,f))$$$
Lean4
theorem convergenceSet_BddAbove {f : PowerSeries R} (hf : IsRestricted c f) : BddAbove (convergenceSet c f) :=
by
simp_rw [isRestricted_iff] at hf
obtain ⟨N, hf⟩ := by simpa using (hf 1)
rw [bddAbove_def, convergenceSet]
use max 1 (max' (image (fun i ↦ ‖coeff i f‖ * c ^ i) (range (N + 1))) (by simp))
simp only [Set.mem_setOf_eq, le_sup_iff, forall_exists_index, forall_apply_eq_imp_iff]
intro i
rcases le_total i N with h | h
· right
apply le_max'
simp only [mem_image, mem_range]
exact ⟨i, by omega, rfl⟩
· left
calc
_ ≤ ‖(coeff i) f‖ * |c ^ i| := by bound
_ ≤ 1 := by simpa using (hf i h).le
