English
If g: N→R is bounded in a suitable sense, then the tail behavior of x ↦ x • g(⌊x⌋₊) along real x agrees with the tail of n • g(n) along n.
Русский
Если функция g: N→R ограничена над некоторыми диапазонами, то поведение функций x ↦ x • g(⌊x⌋₊) совпадает с поведением n • g(n) вдоль x
LaTeX
$$$\text{Tendsto}(\lambda x:\K, x \cdot g(\lfloor x \rfloor_+))\;\text{от atTop к } t$ следует из $\text{Tendsto}(\lambda n: n \cdot g(n))$$$
Lean4
theorem tendsto_smul_comp_nat_floor_of_tendsto_nsmul [NormSMulClass ℤ K] [LinearOrder K] [IsStrictOrderedRing K]
[FloorSemiring K] [HasSolidNorm K] {g : ℕ → R} {t : R} (hg : Tendsto (fun n : ℕ ↦ n • g n) atTop (𝓝 t)) :
Tendsto (fun x : K ↦ x • g ⌊x⌋₊) atTop (𝓝 t) :=
by
replace hg : Tendsto (fun n : ℕ ↦ (n : K) • g n) atTop (𝓝 t) := mod_cast hg
apply tendsto_smul_congr_of_tendsto_left_cobounded_of_isBoundedUnder (hg.comp tendsto_nat_floor_atTop)
· exact tendsto_natCast_atTop_cobounded.comp tendsto_nat_floor_atTop
· apply isBoundedUnder_of_eventually_le (a := ‖(1 : K)‖)
apply Eventually.mono _ (fun x h ↦ norm_le_norm_of_abs_le_abs h)
simpa using ⟨0, fun _ h ↦ mod_cast Nat.abs_floor_sub_le h⟩
