Hey everyone,
I’m working on a formalization of Bochner's Theorem using a "profinite" approach (inverse limits of finite cyclic groups) rather than the standard analytic route. I believe this method constructs a Locally Compact Abelian (LCA) proof for the circle group \mathbb{T} that could generalize. The current file is a bit rough (some AI comments need cleaning), but the core logic is taking shape.
I'm using the term "profinite" to describe these inverse limits—if that is non-standard in this context, please correct me.
Here is the proof strategy I have implemented so far:
1. Density of Roots of Unity: I have proven that the roots of unity \mu_{p^n} = \{z \mid z^{p^n} = 1\} are dense in \mathbb{T} as n \to \infty.
2. Finite Approximation via Characters: I represent functions on \mathbb{T} via approximation by characters on these finite subgroups. Specifically, I define a sequence of finite approximations f_{n,j} = f(\chi_{n,j}) where \chi_{n,j} are characters of \mathbb{Z}/p^n\mathbb{Z}. I have proven in Lean that this converges pointwise to f on the dense subset.
3. Profinite Continuity: I defined a notion of "profinite continuity" (continuity with respect to the inverse limit topology) and proved that for functions on \mathbb{T}, this coincides with standard \epsilon-\delta continuity due to density.
4. Positive Definiteness: I show that the positive-definite condition on f implies that the finite approximations (Gram matrices) in step 2 are non-negative definite.
The Goal:
I am aiming for the standard statement of Bochner's Theorem: For a continuous positive-definite function f on a group G, there exists a unique finite non-negative Radon measure \mu on the dual group \hat{G} such that f is the Fourier transform of \mu.
Current Status:
I have formalized steps 1–4. The final bridge is using the Riesz-Markov-Kakutani theorem to extract the measure \mu from the linear functional defined by these finite approximations. I have uploaded an updated file with ~4k lines of code implementing this tower.
Any feedback on this "profinite" architecture or the connection to general LCA methods would be very welcome!