AI 中文总结
该论文解决了Lyons和White关于二面体群上随机游走速率单调性的猜想，证明对所有正整数$m,n$，$(D_n,2m)$是速率单调的，且推广到含广义二面体群等的群族，还证明非偶整数$p\geq1$时$(D_n,p)$非速率单调，结果已在Lean中形式化验证。
AI 中文摘要
设$D_n$为阶数为$2n$的二面体群。考虑$D_n$上由任意对称速率驱动的连续时间随机游走，其支撑集生成$D_n$。对于$p\in[1,\infty]$，若对每个固定时刻$t$，随机游走在时刻$t$的分布与均匀分布之间的$\ell^p$距离随速率单调递减，则称对$(D_n,p)$是速率单调的。Lyons和White证明了$(D_n,2)$和$(D_n,\infty)$是速率单调的，且出人意料地发现若干$p\in[1,1.997]\cup[2.001,3.999]\cup[4.001,5.995]$的对$(D_n,p)$不是速率单调的，并询问是否存在$p=4$或$p=6$的此类对。我们解决了他们的问题，证明对所有正整数$m$和$n$，$(D_n,2m)$是速率单调的。事实上，我们将该结果推广到更广泛的群族，包括广义二面体群、双循环群和广义四元数群。另一方面，我们证明对每个不偶整数的实数$p\geq1$，存在正整数$n$使得$(D_n,p)$不是速率单调的。本文的结果由AxiomProver在Lean中基于标准文献形式化验证。
英文摘要
Let $D_n$ be the dihedral group of order $2n$. Consider a continuous-time random walk on $D_n$ driven by arbitrary symmetric rates whose support generates $D_n$. For $p\in[1,\infty]$, we say the pair $(D_n,p)$ is rate-monotonic if for each fixed time $t$, the $\ell^p$-distance between the random walk's distribution at time $t$ and the uniform distribution is monotonically decreasing as a function of the rates. Lyons and White proved that $(D_n,2)$ and $(D_n,\infty)$ are rate-monotonic. Somewhat counterintuitively, they found several pairs $(D_n,p)$ with ${p\in[1,1.997]\cup[2.001,3.999]\cup[4.001,5.995]}$ that are not rate-monotonic, and they asked whether any such pairs exist with $p=4$ or $p=6$. We resolve their question, proving that $(D_n,2m)$ is rate-monotonic for all positive integers $m$ and $n$. In fact, we prove a generalization of this result to a broader family of groups that includes generalized dihedral groups, dicyclic groups, and generalized quaternion groups. In the other direction, we prove that for every real $p\geq 1$ that is not an even integer, there exists a positive integer $n$ such that $(D_n,p)$ is not rate-monotonic. The results of this paper were formally verified in Lean by AxiomProver assuming standard literature.
Comments13 pages
