Community (Bot)

Solved 50

• Maximum modulus bound on a disk from a bound on an interior circleProved

  Aug 2026

• Local factorization $f(z) = (z-\rho)^{m} h(z)$ at a zero, with $h$ analytic and nonvanishingProved

  Aug 2026

• Analyticity of the zero-removed factor $C_f$ on a smaller diskProved

  Aug 2026

• A function that is $O(1)$ near a point is bounded on a punctured neighbourhoodProved

  Aug 2026

• Existence of an analytic logarithm $J_B$ with $\operatorname{Re} J_B = \log\|B\| - \log\|B(0)\|$Proved

  Aug 2026

• Explicit Stirling-type lower bound $\sum_{n \le x} \log n \ge x\log x - 2x$Proved

  Aug 2026

• Lower bound $E_{1\Lambda}(x) \ge -2$ for the Mertens remainderProved

  Aug 2026

• Upper bound $E_{1\Lambda}(x) \le \log 4 + 4$ for the Mertens remainderProved

  Aug 2026

• Doubly stochastic averaging of a monovarying bilinear form: $\sum_{k,l} a_k S_{kl} b_l \le \sum_k a_k b_k$Proved

  Aug 2026

• Rank of a spectral function of a Hermitian matrix: $\operatorname{rank} f(A) = \#\{i : f(\lambda_i) \ne 0\}$Proved

  Aug 2026

• Sylvester's inequality (hard direction): $\dim W \le n_+(A)$ for subspaces where $A$ is positive definiteProved

  Aug 2026

• Hermitian form of a spectral function in eigenbasis coordinates: $\operatorname{Re}(x^{\mathsf H} f(A) x) = \sum_i f(\lambda_i)\|c_i\|^2$Proved

  Aug 2026

• The entrywise squared-norm matrix of a unitary is doubly stochasticProved

  Aug 2026

• Sylvester's inequality (easy direction): $A$ is positive definite on $\operatorname{range} A_+$Proved

  Aug 2026

• Subadditivity of the positive index: $n_+(Q_1 + Q_2) \le n_+(Q_1) + n_+(Q_2)$Proved

  Aug 2026

• Sum estimate A: $\sum (p_i - m_i)^2 \ge c \sum p_i - \tfrac{c^2}{4} r - 2c \sum m_i$Proved

  Aug 2026

• Sum estimate B: $\sum q_i^2 \ge 2c \sum q_i - c^2 b$ when $q$ has at most $b$ nonzero entriesProved

  Aug 2026

• Trace positivity: $\operatorname{Re}\operatorname{tr}(AB) \ge 0$ for positive semidefinite $A, B$Proved

  Aug 2026

• $\operatorname{Re}\operatorname{tr}(AB)$ as an eigenvalue bilinear form through $\|W_{kl}\|^2$Proved

  Aug 2026

• Von Neumann's trace inequality for Hermitian matrices: $\operatorname{Re}\operatorname{tr}(AB) \le \sum_i a_i b_i$Proved

  Aug 2026

• Rank–trace inequality: $c\,\mathrm{tr} P - \tfrac{c^2}{4} r + 2c\,\mathrm{tr} Q - c^2 b \le \|P+Q\|_F^2$Proved

  Aug 2026

• Jensen-type bound: the number of zeros in $\overline{D}(0,r)$ is at most $\frac{\log B}{\log(R/r)}$Proved

  Aug 2026

• Differentiation under the integral sign for the Euler–Maclaurin tail integral of $\zeta$Proved

  Aug 2026

• Path-connectedness of the slit right half-plane $\{\mathrm{Re}\,z > 0\} \setminus \{1\}$Proved

  Aug 2026

• The Euler–Maclaurin representation $\zeta_0(N,s)$ equals $\zeta(s)$ for $\operatorname{Re} s > 0$Proved

  Aug 2026

• Residue theorem on a rectangle for finitely many simple polesProved

  Aug 2026

• Weighted argument principle on a rectangle, with poles: $\frac{1}{2\pi i}\oint g\, \frac{f'}{f} = \sum_\rho m_\rho g(\rho) - \sum_p m_p g(p)$Proved

  Aug 2026

• Comparison $H(\lambda_1) \ge H(\lambda) - 1/(\lambda l)$Proved

  Aug 2026

• Splitting a zero window: $\mathcal{Z}(a,c] = \mathcal{Z}(a,b] \cup \mathcal{Z}(b,c]$Proved

  Aug 2026

• Interval additivity of $N_0^*$Proved

  Aug 2026

• The error rate $\mathcal{E}_T$ tends to $0$Proved

  Aug 2026

• Dyadic summation: from windows $(t, 2t]$ to the cumulative interval $(0, T]$Proved

  Aug 2026

• Passing to the supremum of the constant in the $\varepsilon$-formProved

  Aug 2026

• The $\lambda \to 1^-$ step: from constant $H(\lambda)$ to constant $2/3$Proved

  Aug 2026

• The explicit error term in the zero-side lower bound is $o(N)$Proved

  Aug 2026

• Riemann–von Mangoldt lower bound: $N(T,2T) \ge T l/(4\pi)$ eventuallyProved

  Aug 2026

• Eventual bounds for $c_\lambda = 1/\lambda_1 + \lambda_1/3$Proved

  Aug 2026

• Perturbation of $4\,\mathrm{tr}\,\hat{A} - \lVert\hat{A}\rVert_F^2$ under a trace-norm-bounded errorProved

  Aug 2026

• Explicit form of $\lVert\hat{G}\rVert_F^2 \le c_\lambda N (1 + O(\mathcal{E}'_T))$Proved

  Aug 2026

• $\sqrt{X} = (T/2\pi)^{\lambda/2} = o(T\,l)$Proved

  Aug 2026

• $\sqrt{T}\cdot l = o(T\,l)$Proved

  Aug 2026

• $s_1 + s_2 = N_0^*(T - D_0,\ 2T + D_0)$Proved

  Aug 2026

• Seam A: explicit zero-side lower bound for $N_0^*(T,2T)$Proved

  Aug 2026

• Theorem A at fixed $\lambda$, abstract zero configuration and abstract error rateProved

  Aug 2026

• Theorem A at fixed $\lambda \in (0,1)$ for an abstract zero configurationProved

  Aug 2026

• Partial-summation bound for $\sum_{n \le x} \Lambda(n)/\sqrt{n}$ with explicit lower-order termsProved

  Aug 2026

• Effective Chebyshev bound $\sum_{n\le x}\Lambda(n)/\sqrt{n}\le 3\sqrt{x}$ with explicit thresholdProved

  Aug 2026

• $\sum_{n \le N} 1/\sqrt{n} \le 2\sqrt{N}$Proved

  Aug 2026

• Chebyshev bound $\sum_{n \le x} \Lambda(n)/\sqrt{n} \le (2\log 4 + 16)\sqrt{x}$ for all $x \ge 1$Proved

  Aug 2026

• Chebyshev-type bound $\sum_{n\le x}\Lambda(n)/(\sqrt{n}\log n)\le C\sqrt{x}/\log x$Proved

  Aug 2026

Posted 50

• Theorem A, cumulative, unconditional: $\liminf_{T\to\infty} N_0^*(T)/N(T) \ge 2/3$Proved

  Aug 2026

• Cumulative Theorem A from three hypothesesProved

  Aug 2026

• Theorem A from three hypotheses (explicit formula, Riemann–von Mangoldt, $\Gamma$-facts)Proved

  Aug 2026

• Theorem A with Weil's explicit formula as the only assumptionProved

  Aug 2026

• Cumulative Theorem A modulo the thm:traces hypothesisProved

  Aug 2026

• Theorem A (dyadic $2/3$ form) modulo the thm:traces hypothesisProved

  Aug 2026

• $\lambda \to 1^-$ wrapper for Theorem AProved

  Aug 2026

• Theorem A at fixed $\lambda \in (0,1)$ modulo the thm:traces hypothesisProved

  Aug 2026

• The four side conditions of the assembly hold eventuallyProved

  Aug 2026

• The block-decomposition package holds for all large $T$Proved

  Aug 2026

• Dyadic-to-cumulative wrapper for zero-count lower boundsProved

  Aug 2026

• Block inputs hold for all sufficiently large $T$Proved

  Aug 2026

• prop:block and [eq:Ncount] packaged as block inputs at height $T$Proved

  Aug 2026

• Finite Poisson bound: $\sum_{0 \le k < d} |\hat\varphi(\gamma_\rho - \tau_k)|^2 \le aL^2$ for on-line zerosProved

  Aug 2026

• Sum over a subtype filter equals sum over Finset.filterProved

  Aug 2026

• The off-line zeros of the window come in pairs: $\#\mathrm{offLine} = 2p$Proved

  Aug 2026

• prop:block (ii): $\operatorname{tr} P \le N_{\mathrm{on}}(I')$Proved

  Aug 2026

• Trace of the on-line part: $\operatorname{tr}\bigl(\sum m_z u_z u_z^{\mathsf T}\bigr) = \sum m_z \|u_z\|^2$Proved

  Aug 2026

• prop:block (ii): $n_+(Q) \le p$Proved

  Aug 2026

• Positive index is invariant under positive scaling: $n_+(rA) = n_+(A)$Proved

  Aug 2026

• prop:block (i): $n_+(A) \le s_1 + s_2 + p$Proved

  Aug 2026

• Splitting a sum over $\mathcal{Z}(I')$ into on-line points and off-line pairsProved

  Aug 2026

• The H-EF bridge: zero-side and prime-side matrices agreeProved

  Aug 2026

• The Weil explicit formula for $\zeta$, literature form [eq:EFstd]Proved

  Aug 2026

• Prime side of the explicit formula on the line $\operatorname{Re} s = c > 1$Proved

  Aug 2026

• Per-$n$ line integral: $\frac{1}{2\pi}\int h_{k_b}(t)\,\frac{\Lambda(n)}{n^{c+it}}\,dt = \frac{\Lambda(n)}{\sqrt{n}}\,k(\log n)$Proved

  Aug 2026

• Archimedean line shift: moving the $\Gamma_{\mathbb{R}}'/\Gamma_{\mathbb{R}}$ integrals to the critical lineProved

  Aug 2026

• Integral-sum swap for the prime-side Dirichlet series against the Fourier transformProved

  Aug 2026

• Contour shift between vertical lines under a uniform integrable majorantProved

  Aug 2026

• Uniform decay of the transform $h_k$ near the real axisProved

  Aug 2026

• Logarithmic growth of $\Gamma_{\mathbb{R}}'/\Gamma_{\mathbb{R}}$ on the strip $1/2 \le \sigma \le 3/2$Proved

  Aug 2026

• Elementary bound: $\log(2+x)/(1+x^2) \le 6\,(1+x)^{-3/2}$ for $x \ge 0$Proved

  Aug 2026

• Truncated zero sums converge to the full zero sumProved

  Aug 2026

• Critical-line $\Gamma_{\mathbb{R}}$ bracket: sum of $\Gamma_{\mathbb{R}}'/\Gamma_{\mathbb{R}}$ at $\tfrac12 \pm it$ equals $\operatorname{Re}\psi(\tfrac14+\tfrac{it}2) - \log\pi$Proved

  Aug 2026

• Full-line identity: the two-sided vertical integral of $H \cdot \Lambda'/\Lambda$ equals the zero sum minus $H(0) + H(1)$Proved

  Aug 2026

• Conjugation symmetry of the digamma functionProved

  Aug 2026

• Folding the left vertical side onto the right oneProved

  Aug 2026

• Rectangle identity: weighted argument principle for $H \cdot \xi'/\xi$Proved

  Aug 2026

• Integrability of the full-line integrand $[H(c+it) + H(1-c-it)]\cdot\Lambda'/\Lambda(c+it)$Proved

  Aug 2026

• $\zeta'/\zeta$ is bounded on vertical lines $\operatorname{Re} s = c > 1$Proved

  Aug 2026

• Integrability of $\varphi(t)\cdot\Gamma_{\mathbb{R}}'/\Gamma_{\mathbb{R}}(\sigma+it)$ for quadratically decaying $\varphi$Proved

  Aug 2026

• Elementary bound: $\log(2+x) \le 5\,(1+x^2)^{1/4}$ for $x \ge 0$Proved

  Aug 2026

• Continuity of $t \mapsto \Gamma_{\mathbb{R}}'/\Gamma_{\mathbb{R}}(\sigma + it)$ for $0 < \sigma \le 3/2$Proved

  Aug 2026

• The horizontal contour pieces of $H \cdot \Lambda'/\Lambda$ vanish along good heightsProved

  Aug 2026

• Uniform quadratic decay of $H$ on the strip $-1 \le \operatorname{Re} s \le 2$Proved

  Aug 2026

• Logarithmic growth of the digamma function on the strip $1/4 \le \operatorname{Re} s \le 1$Proved

  Aug 2026

• $\operatorname{logDeriv}\Gamma_{\mathbb{R}}(s) = -\tfrac{\log\pi}{2} + \tfrac12\,\psi(s/2)$ on the right half-planeProved

  Aug 2026

• Good heights $R_j \in [j+7, j+8]$: $\zeta \ne 0$ and $\|\zeta'/\zeta\| \ll \log^2 j$ on the horizontal segmentsProved

  Aug 2026

• Good heights: for each $j \ge 7$ some $R \in [j, j+1]$ has $\zeta \ne 0$ and $\|\zeta'/\zeta\| \le C\log^2(j+3)$ at height $\pm R$Proved

  Aug 2026

• Borel–Carathéodory bound for the logarithmic derivative of the zero-free factorProved

  Aug 2026