The perpendicular direction in $\mathbb{R}^2$: rotates a vector $(e_0, e_1)$ to $(-e_1, e_0)$.
Instances For
The rectangle in $\mathbb{R}^2$ centered at center with major axis along dir,
of half-length halfLength along dir and half-width halfWidth along perpDir dir.
Instances For
A $1 \times R$ tube in $\mathbb{R}^2$: a long, thin rectangle with unit direction
vector, length R ≥ 1, and width $1$.
- R : ℝ
- center : EuclideanSpace ℝ (Fin 2)
- direction : EuclideanSpace ℝ (Fin 2)
Instances For
Realize a Tube as the set $\{x \in \mathbb{R}^2 : |\langle x - c, d\rangle| \leq R/2, \ |\langle x - c, d^\perp\rangle| \leq 1/2\}$.
Instances For
The two-dimensional Fourier transform $\hat f(\xi) = \int f(x) e^{-2\pi i \langle x, \xi\rangle}\, dx$ of a real-valued function on $\mathbb{R}^2$, returning a complex value.
Instances For
The set of dyadic scales between $1$ and $R$: $\{2^k : k \in \mathbb{N}, 1 \leq 2^k \leq R\}$.
Instances For
A collection of $1 \times R$ tubes in $\mathbb{R}^2$ together with smooth bump functions $\psi_i$ adapted to each tube and a (compactly supported) Fourier bound. This is the data $f = \sum_T \psi_T$ used in the real-version Main Lemma 2R.
- R : ℝ
- ι : Type
- ψ : self.ι → EuclideanSpace ℝ (Fin 2) → ℝ
- ψ_integrable (i : self.ι) : MeasureTheory.Integrable (self.ψ i) MeasureTheory.volume
- fourierSupportBound : ℝ
- ψ_fourier_compact_support (i : self.ι) (ξ : EuclideanSpace ℝ (Fin 2)) : ‖ξ‖ > self.fourierSupportBound → fourierTransformR2 (self.ψ i) ξ = 0
Instances For
The index type of a TubeCollection is a Fintype.
The aggregated tube sum $f(x) = \sum_i \psi_i(x)$.
Instances For
The number of tubes in S contained in the $r \times R$ rectangle with center c
and direction d.
Instances For
The multiplicity at scale $r$: the maximum, over all $r \times R$ rectangles, of the
number of tubes of S contained in that rectangle.
Instances For
A frequency decomposition $f = \sum_{r} f_r$ of the tube sum into pieces with Fourier support in $\{|\xi| \leq 1/r\}$, satisfying a near-orthogonality $L^2$ bound.
- f_r : ℝ → EuclideanSpace ℝ (Fin 2) → ℝ
Instances For
Plancherel for the 2D Fourier transform of a real-valued function: $\int |f(x)|^2\, dx = \int |\hat f(\xi)|^2\, d\xi$.
Bilinear Plancherel/Parseval identity: $\int f(x) g(x)\, dx = \mathrm{Re}\,\int \hat f(\xi) \overline{\hat g(\xi)}\, d\xi$.
Pointwise bounded overlap on the Fourier side. For a decomposition $f = \sum_r f_r$ with $\hat{f_r}$ supported in $\{|\xi| \leq 1/r\}$, there is a constant $C$ such that the dyadic Fourier supports overlap with bounded multiplicity: $\sum_r |\hat{f_r}(\xi)|^2 \leq C |\hat f(\xi)|^2$ for every $\xi$.
Integrated bounded overlap on the Fourier side. Integrating the pointwise inequality gives $\sum_r \int |\hat{f_r}|^2 \leq C \int |\hat f|^2$.
Littlewood–Paley square function estimate. Combining Plancherel with bounded overlap on the Fourier side yields the spatial estimate $\sum_r \int |f_r|^2 \leq C \int |f|^2$.
Expanding the $L^2$ norm of a finite sum as a sum of pairwise integrals: $\int (\sum_i \varphi_i)^2 = \sum_{i,j} \int \varphi_i \varphi_j$.
Per-tube row sum bound: each row $\sum_j |\langle \varphi_i, \varphi_j\rangle|$ is
controlled by multiplicity r (the count of $\varphi_j$ that can interact with
$\varphi_i$) times the diagonal bound $R/r$.
Per-scale $L^2$ bound: given a tube-localized representation $f_r = \sum_i \varphi_i$ with per-tube energy $\leq R/r$ and bounded multiplicity at scale $r$, we obtain $\int f_r^2 \leq |S.\iota| \cdot \mathrm{mult}(r) \cdot (R/r)$.
Cauchy–Schwarz via the AM–GM inequality: if $\int f^2, \int g^2 \leq A$ then $|\int fg| \leq A$.
Existence of a smooth frequency partition: each tube bump $\psi_i$ splits as $\psi_i = \sum_{r \in \text{scales}} \eta_{r,i}$ where each piece has Fourier support inside $\{|\xi| \leq 1/r\}$, and similarly for the sum $\sum_i \eta_{r,i}$.
Basic Littlewood–Paley decomposition of the tube sum, together with a tube-wise representation $f_r = \sum_i \varphi_i$ on each scale.
Per-tube $L^2$ bound at scale $r$: $\int |\varphi_i|^2 \leq R/r$.
Amplitude wrapper: packages the per-tube $L^2$ bound as the existence of nonnegative dominating functions $g_i \geq \varphi_i^2$ with $\int g_i \leq R/r$.
Recover a per-tube $L^2$ bound $\int \varphi_i^2 \leq R/r$ from a pointwise domination by integrable amplitudes $g_i$ with $\int g_i \leq R/r$.
Angular Fourier disjointness: if the directions of tubes $i, j$ make a large enough angle (so $|\langle d_i, d_j\rangle| < 1 - (r/R)^2/2$), then the Fourier supports of their pieces $\varphi_i$ and $\varphi_j$ are disjoint.
Refined Littlewood–Paley construction including per-tube $L^2$ bounds and angular Fourier disjointness for non-aligned tubes.
Spatial orthogonality from Fourier-side disjointness: when the angle between tubes $i, j$ is large, $\int \varphi_i \varphi_j = 0$ via Plancherel and disjoint supports.
Spatial decay vanishing: when the tubes $i, j$ are nearly parallel but tube $j$ is not contained in the $r \times R$ rectangle around tube $i$, the interaction integral $\int \varphi_i \varphi_j = 0$.
Contrapositive of spatial decay: if the interaction $\int \varphi_i \varphi_j$ is nonzero and the tubes are nearly parallel, then tube $j$ must be contained in the $r \times R$ rectangle centred at tube $i$.
Frequency-localization of nonzero interactions: for each tube $i$ there is a rectangle (centred at the tube) outside of which every tube $j$ has zero interaction with $\varphi_i$.
Sparsity bound from orthogonality: for each tube $i$, the number of $j$ with $\int \varphi_i \varphi_j \ne 0$ is at most $\mathrm{mult}(r)$, the maximum tube multiplicity inside any $r \times R$ rectangle.
Full Littlewood–Paley construction packaging together: tube decomposition, per-tube $L^2$ bounds, and sparsity of nonzero pairwise interactions.
The final tube decomposition: each scale piece $f_r = \sum_i \varphi_i$ has absolutely bounded pairwise interactions $|\int \varphi_i \varphi_j| \leq R/r$ (by Cauchy–Schwarz) and bounded multiplicity.
Main Lemma 2R (real Fourier method, $1 \times R$ tubes). Let $\mathcal{T}$ be a set of $1 \times R$ tubes in $\mathbb{R}^2$ and $f = \sum_T \psi_T$ the associated tube sum. There exists a frequency decomposition $f = \sum_{r \in \text{scales}} f_r$ into dyadic pieces, with $\hat{f_r}$ supported in $\{|\xi| \leq 1/r\}$, near-orthogonality $\sum_r \int f_r^2 \lesssim \int f^2$, and the per-scale estimate $\int f_r^2 \leq C \cdot |\mathcal{T}| \cdot \mathrm{mult}(r) \cdot (R/r)$.