English
If the real-valued function g on R and a floor-based scalar sequence produce a convergent product after scaling by floor and real scalar multiplication, then the limit is preserved under floor-sampled scaling.
Русский
Если произведение с использованием пола и floor сохраняет предельное поведение при масштабировании, то предел сохраняется.
LaTeX
$$$\text{Tendsto}(x \mapsto x \cdot g(\lfloor x \rfloor))\Rightarrow \text{Tendsto}(n \mapsto n \cdot g(n))$$$
Lean4
theorem tendsto_smul_comp_nat_floor_of_tendsto_mul [NormedRing K] [NormedRing R] [Module K R] [NoZeroSMulDivisors K R]
[NormSMulClass K R] [NormSMulClass ℤ K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] [HasSolidNorm K]
{g : ℕ → R} {t : R} (hg : Tendsto (fun n : ℕ ↦ (n : R) * g n) atTop (𝓝 t)) :
Tendsto (fun x : K ↦ x • g ⌊x⌋₊) atTop (𝓝 t) :=
tendsto_smul_comp_nat_floor_of_tendsto_nsmul (by simpa only [nsmul_eq_mul] using hg)
