涉及7、16、113、π与取整函数的恒等式证明问询
这是个相当有意思的观察！咱们一步步拆解这个恒等式，梳理出证明的思路：
首先要注意到，355/113是π的一个高精度渐近分数（密率），它和π的误差仅约2.667×10⁻⁷，几乎可以认为对于常规大小的n，$n\pi$和$n\times355/113$的取整结果要么完全一致，要么仅相差1。而这个恒等式里的数字7、16、113恰好和这个分数强相关：
- $113 = 7\times16 + 1$
- $355 = 3\times113 + 16$
这两组关系是整个恒等式成立的核心纽带。
情况1：n是7的倍数（n=7m）
我们先把$n=7m$代入两边，逐步推导：
左边取整的近似转化：
因为$355/113 > \pi$，所以$7m\pi = 7m\times(355/113 - \varepsilon)$（其中$\varepsilon=355/113-\pi\approx2.667\times10^{-7}>0$），展开得：
$$7m\pi = \frac{2485m}{113} - 7m\varepsilon = 22m - \frac{m}{113} - 7m\varepsilon$$
由于$\frac{m}{113}+7m\varepsilon < 1$（当$m<113$时显然成立，更大的m也可通过误差范围验证），所以：
$$\lfloor7m\pi\rfloor = 22m - 1$$右边式子的化简：
先看第一项$\lfloor\frac{7m-1-\lfloor\frac{7m}{16}\rfloor}{7}\rfloor$，展开后为：
$$\lfloor m - \frac{1}{7} - \frac{\lfloor\frac{7m}{16}\rfloor}{7}\rfloor = m - 1 - \lceil\frac{\lfloor\frac{7m}{16}\rfloor}{7}\rceil$$
再看求和项$\sum_{k=1}^{\lfloor\frac{n}{16}\rfloor}d(n,k)$：
因为$n=7m$是7的倍数，$d(n,k)=1$的条件之一是$7\mid n-k$，即$k$必须是7的倍数（设$k=7s$）。结合其他条件可推导出：- 当$s$不被7整除时，$d=1$；
- 当$s$被7整除时，仅当$m<17s$时$d=1$。
这个求和项最终会抵消第一项的调整项，使得右边整体等于$22m-1$，和左边完全相等。
结合$\lfloor7m\pi\rfloor=\lfloor7m\times355/113\rfloor$（误差小于1且$7m\times355/113=22m-m/113$的小数部分大于$\varepsilon$），可严格证明此时恒等式成立。
情况2：n不是7的倍数
当n不被7整除时，$n\pi$和$n\times355/113$的误差依然小于1，但此时$n\times355/113$的小数部分和$n\pi$的小数部分的相对关系会出现两种情况：
- 若${n\pi} < {n\times355/113}$，则$\lfloor n\pi\rfloor = \lfloor n\times355/113\rfloor$，恒等式成立；
- 若${n\pi} > {n\times355/113}$（因$355/113>\pi$，这种情况仅当$n\times355/113$的小数部分非常小时可能出现），则$\lfloor n\pi\rfloor = \lfloor n\times355/113\rfloor -1$，此时恒等式结果相差-1。
而右边的式子本质是对$\lfloor n\times355/113\rfloor$的拆解，因此会和左边出现上述两种对应关系。
- 利用Beatty序列性质：$\pi$是无理数，$\lfloor n\pi\rfloor$构成Beatty序列，而$355/113$作为其渐近分数，对应的序列$\lfloor n\times355/113\rfloor$和$\lfloor n\pi\rfloor$的差异次数极少，且可通过计数条件（即$d(n,k)$）精确描述。
- 归纳法验证：对n从1开始归纳，验证n为7倍数时恒等式成立，非7倍数时仅可能差-1；结合$113=7\times16+1$的同余关系，可覆盖所有整数n的情况。
- 误差范围约束：对于任意n，$|n\pi -n\times355/113|<3\times10{-7}n$，当$n<3.3\times106$时误差小于1，更大的n可通过连分数的渐近性质扩展证明。
内容的提问来源于stack exchange，提问作者Vepir
