Calderón sum formula for higher-dimensional Parseval wavelet frames

### What is the conjecture

Let $A, P \in \mathrm{GL}(d, \mathbb{R})$ and $\psi \in L^2(\mathbb{R}^d)$. Suppose that

$$\{|\det(A)|^{-j/2} \psi(A^j \cdot - Pk)\}_{j \in \mathbb{Z}, k \in \mathbb{Z}^d}$$

is an orthonormal basis, or more generally a Parseval frame, for $L^2(\mathbb{R}^d)$. Then the Calderón sum formula holds:

$$\sum_{j \in \mathbb{Z}} |\widehat{\psi}((A^t)^j \xi)|^2 = |\det(P)| \quad \text{for almost every } \xi \in \mathbb{R}^d.$$

**Context:** The Calderón sum formula is a central identity in wavelet theory that completely characterizes tight wavelet frames under additional assumptions on the dilation matrix $A$ (such as expansive dilations preserving $\mathbb{Z}^d$). Bownik (2017, Conjecture 1; 2020 Open Problem 3.3) and Speegle (2003) conjectured that the formula holds for arbitrary dilation matrices $A \in \mathrm{GL}(d, \mathbb{R})$ and translation lattices $P\mathbb{Z}^d$. Enstad and van Velthoven establish this formula under a mild Bessel orbit condition $\psi \in \mathcal{B}_\pi$, but the general case for all $\psi \in L^2(\mathbb{R}^d)$ remains an open problem.

* **Source Paper:** *On the Calderón sum formula for wavelet systems* ([arXiv:2602.10766v1](https://arxiv.org/abs/2602.10766v1), [HTML](https://arxiv.org/html/2602.10766v1), [PDF](https://arxiv.org/pdf/2602.10766v1))
* **Authors:** Ulrik Enstad, Jordy Timo van Velthoven
* **In-Paper Location:** [Conjecture 1 (Page 1)](https://arxiv.org/pdf/2602.10766v1#page=1) in Section 1 "Introduction"
* **OpenConjecture ID:** 440 ([OpenConjecture](https://github.com/davisrbr/conjectures-arxiv))

### Prerequisites needed

* **Fourier transform on Euclidean space:** [`Mathlib.Analysis.Fourier.FourierTransform`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Fourier/FourierTransform.html)
* **$L^2$ spaces and Lebesgue measure:** [`Mathlib.MeasureTheory.Function.L2Space`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Function/L2Space.html), [`Mathlib.MeasureTheory.Measure.Lebesgue.Basic`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.html)
* **General Linear Group $\mathrm{GL}(d, \mathbb{R})$:** [`Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.html)
* **Inner product spaces & Hilbert frames:** [`Mathlib.Analysis.InnerProductSpace.Basic`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/InnerProductSpace/Basic.html)

### Choose either option
- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

This issue was generated by an AI agent and reviewed by me.

Start by reading Conjecture 1 in the linked source paper, then review the listed Mathlib documentation for Fourier transforms, L2 spaces, Lebesgue measure, general linear groups, and Hilbert frames. Identify the repository's entry point and conventions for formalized conjectures; done means the stated higher-dimensional Calderón sum conjecture is added and the Lean project accepts it.

Written by the indexing model from the issue text.