Research proof index

For every bounded, finitely supported function $f$, almost every point $x$ admits a sequence of balls $B(c_i,r_i)$ that all contain $x$, whose radii tend to $0$ from above, and whose averages converge to $f(x)$:

$\dashint_{B(c_i,r_i)} f(y)\,dy\longrightarrow f(x).$

Existence theorem packaging the lexicographic construction. It produces a LinearOrder (Finset α) with two convenient properties: 1. Subset-monotonicity: A ⊆ B implies A ≤ B. 2. Singleton compatibility: comparing singleton finsets recovers the original order on α. API note: returning the order via ∃ lo allows users to avoid a global instance and...

A boundary Fourier identity for a Dirichlet series with a simple pole. Suppose $f\ge0$, the Dirichlet series $L(f,s)$ differs from $A/(s-1)$ by a function $G$ that extends continuously to $\operatorname{Re}s\ge1$, and $\psi$ is a compactly supported $C^2$ test function with nonnegative real Fourier transform. For $x>0$, $\sum_{n\ge1}\frac{f(n)}{n}\widehat\psi\!\left(\frac{1}{2\pi}\log\frac{n}{x}\right)-A\int_{-\log x}^{\infty}\widehat\psi\!\left(\frac{u}{2\pi}\right)du=\int_{\mathbb R}G(1+it)\psi(t)x^{it}\,dt.$

Convergence on a dense set of a collection of monotone function controls the limsup at a point if f is right continuous at a. We prove this under the assumption that α has both a bottom element and a top element. The bottom element is needed because otherwise limsup evaluated at the bottome element may give a junk value to break the inequality.

The min distance of a linear code equals the minimum of the weights of non-zero codewords.

A linear code is equal to the submodule spanned by the rows of the matrix whose rows form a basis of the code.