English
Let F be a filter on an index set, and let f: I → R be such that R is a conditionally complete linear order, with a constant c ∈ R. If f is cobounded from below and bounded from below under the relation ≥ along F, then liminf over F of (f(i) − c) equals (liminf over F of f(i)) − c. In words, liminf commutes with subtraction by a constant under suitable boundedness assumptions.
Русский
Пусть F — фильтр на индексном множестве I, а функция f: I → R реализует переходы в частично упорядоченном кольце R, где c ∈ R. Пусть f ограничена снизу в смысле coboundedness и ограничена снизу условиями bdd_below относительно отношения ≥ вдоль F. Тогда liminf_i→F (f(i) − c) = (liminf_i→F f(i)) − c. Говоря простей, лиминфимум сохраняет сдвиг на константу при допустимых ограничениях.
LaTeX
$$$\\forall F f c \; [NeBot F] \\, [\\text{IsCoboundedUnder} (\\ge) f F] \\, [\\text{IsBoundedUnder} (\\ge) f F] \\,\\; \\operatorname{Filter.liminf}(\\lambda i. f(i) - c) F = \\operatorname{Filter.liminf}(f) F - c$$$
Lean4
/-- `liminf (xᵢ - c) = (liminf xᵢ) - c`. -/
theorem liminf_sub_const (F : Filter ι) [NeBot F] [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R]
(f : ι → R) (c : R) (cobdd : F.IsCoboundedUnder (· ≥ ·) f) (bdd_below : F.IsBoundedUnder (· ≥ ·) f) :
Filter.liminf (fun i ↦ f i - c) F = Filter.liminf f F - c :=
(Monotone.map_limsInf_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ x - c) (fun _ _ h ↦ tsub_le_tsub_right h c)
(continuous_sub_right c).continuousAt cobdd bdd_below).symm
