@[reducible, inline]

abbrev FrequencyDecomposition.ℝ2 : Type

Short alias for the Euclidean plane $\mathbb{R}^2$.

structure FrequencyDecomposition.Tube : Type

A $1 \times R$ tube in $\mathbb{R}^2$: an oriented rectangle of length $R \geq 1$ and width $1$, specified by its center and direction angle.

• center : ℝ2
• direction : ℝ
• R : ℝ
• hR : 1 ≤ self.R

structure FrequencyDecomposition.WideTube : Type

A generic axis-aligned-along-direction rectangle in $\mathbb{R}^2$, with arbitrary halfWidth and halfLength, used to contain bundles of $1 \times R$ tubes.

• center : ℝ2
• direction : ℝ
• halfWidth : ℝ
• halfLength : ℝ

def FrequencyDecomposition.Tube.toSet (T : Tube) : Set ℝ2

Realize a tube $T$ as the rectangle of half-length $R/2$ along direction $\theta$ and half-width $1/2$ along the perpendicular.

def FrequencyDecomposition.WideTube.toSet (W : WideTube) : Set ℝ2

Realize a WideTube as the corresponding rectangle in $\mathbb{R}^2$.

def FrequencyDecomposition.Tube.containedIn (T : Tube) (W : WideTube) : Prop

A tube $T$ is contained in a wide tube $W$ if the rectangle of $T$ lies inside $W$.

noncomputable def FrequencyDecomposition.dyadicRange (R : ℝ) : Finset ℝ

The dyadic scales up to $R$: $\{2^k : k \in \mathbb{N}, 2^k \leq R\}$ as a Finset.

noncomputable def FrequencyDecomposition.tubeCoveringNumber (𝒯 : Finset Tube) (R r : ℝ) : ℕ

Tube covering number $N_\mathcal{T}(r) = \max_W |\{T \in \mathcal{T} : T \subseteq W\}|$, maximizing over $r \times R$ wide tubes $W$.

noncomputable def FrequencyDecomposition.l2NormSq (f : ℝ2 → ℂ) : ℝ

The $L^2$ norm squared $\|f\|_{L^2}^2 = \int_{\mathbb{R}^2} |f(x)|^2\, dx$.

def FrequencyDecomposition.fourierSupport (f : ℝ2 → ℂ) : Set ℝ2

The support of the Fourier transform of f in $\mathbb{R}^2$.

noncomputable def FrequencyDecomposition.cumulativeFreqProj (f : ℝ2 → ℂ) (r : ℝ) : ℝ2 → ℂ

The cumulative frequency projection $P_{\leq 1/r} f$: the inverse Fourier transform of $\hat f(\xi) \cdot \mathbf{1}_{|\xi| \leq 1/r}$.

noncomputable def FrequencyDecomposition.littlewoodPaleyPieceK (f : ℝ2 → ℂ) (K k : ℕ) (x : ℝ2) : ℂ

The $k$-th Littlewood–Paley piece of $f$ at depth $K$: $\Delta_k f = P_{\leq 2^{-k}} f - P_{\leq 2^{-(k+1)}} f$ for $k < K$, and the final endpoint $P_{\leq 2^{-K}} f$ when $k = K$ (with $f$ itself when $k = 0$).

theorem FrequencyDecomposition.littlewoodPaleyPieceK_sum (f : ℝ2 → ℂ) (K : ℕ) (x : ℝ2) : ∑ k ∈ Finset.range (K + 1), littlewoodPaleyPieceK f K k x = f x

Littlewood–Paley telescoping identity: $f(x) = \sum_{k=0}^{K} \Delta_k f(x)$.

theorem FrequencyDecomposition.nat_log_two_pow (k : ℕ) : Nat.log 2 ⌊2 ^ k⌋₊ = k

The natural logarithm base 2 of $\lfloor 2^k \rfloor$ equals $k$.

theorem FrequencyDecomposition.two_pow_le_of_mem_range (k : ℕ) (R : ℝ) (hR : 1 ≤ R) (hk : k < Nat.log 2 ⌊R⌋₊ + 1) : 2 ^ k ≤ R

If $k \leq \log_2 \lfloor R \rfloor$ then $2^k \leq R$.

theorem FrequencyDecomposition.two_pow_injective : Function.Injective fun (k : ℕ) => 2 ^ k

Injectivity of $k \mapsto 2^k$ on $\mathbb{N}$ (viewed in $\mathbb{R}$).

noncomputable def FrequencyDecomposition.littlewoodPaleyPiece (𝒯 : Finset Tube) (φ : Tube → ℝ2 → ℂ) (R r : ℝ) : ℝ2 → ℂ

The Littlewood–Paley piece $f_r$ at dyadic scale $r$ of the tube sum $f = \sum_T \varphi_T$, indexed by the integer $\log_2 r$.

structure FrequencyDecomposition.FrequencyDecompositionData (𝒯 : Finset Tube) (R : ℝ) : Type

Bundle of frequency-decomposition data for the tube sum $f = \sum_T \varphi_T$: the pieces $f_r$ at dyadic scales, Fourier support inside $\{|\xi| \leq 1/r\}$, and the per-scale $L^2$ estimate $\|f_r\|_{L^2}^2 \leq C \cdot N_\mathcal{T}(r) \cdot |\mathcal{T}| / r \cdot R$.

• φ : Tube → ℝ2 → ℂ
• f_r : ℝ → ℝ2 → ℂ
• f : ℝ2 → ℂ
• decomposition (x : ℝ2) : self.f x = ∑ r ∈ dyadicRange R, self.f_r r x
• freq_support (r : ℝ) : r ∈ dyadicRange R → fourierSupport (self.f_r r) ⊆ Metric.closedBall 0 (1 / r)
• C : ℝ
• hC : 0 < self.C
• l2_estimate (r : ℝ) : r ∈ dyadicRange R → l2NormSq (self.f_r r) ≤ self.C * ↑(tubeCoveringNumber 𝒯 R r) * ↑𝒯.card * r⁻¹ * R

theorem FrequencyDecomposition.littlewoodPaley_decomposition (𝒯 : Finset Tube) (R : ℝ) (hR : 1 ≤ R) (φ : Tube → ℝ2 → ℂ) (hφ_smooth : ∀ T ∈ 𝒯, ContDiff ℝ ⊤ (φ T)) (hφ_integrable : ∀ T ∈ 𝒯, MeasureTheory.Integrable (φ T) MeasureTheory.volume) (hφ_support : ∀ T ∈ 𝒯, Function.support (φ T) ⊆ T.toSet) (x : ℝ2) : (fun (x : ℝ2) => ∑ T ∈ 𝒯, φ T x) x = ∑ r ∈ dyadicRange R, littlewoodPaleyPiece 𝒯 φ R r x

The tube sum reconstructs from its Littlewood–Paley pieces: $\sum_{T \in \mathcal{T}} \varphi_T(x) = \sum_{r \in \text{dyadicRange}(R)} f_r(x)$.

theorem FrequencyDecomposition.fourier_fourierInv (g : ℝ2 → ℂ) : FourierTransform.fourier (FourierTransformInv.fourierInv g) = g

Fourier inversion: $\mathcal{F}(\mathcal{F}^{-1}g) = g$.

theorem FrequencyDecomposition.fourierInv_sub' (g₁ g₂ : ℝ2 → ℂ) : (fun (x : ℝ2) => FourierTransformInv.fourierInv g₁ x - FourierTransformInv.fourierInv g₂ x) = FourierTransformInv.fourierInv (g₁ - g₂)

Linearity of the inverse Fourier transform under subtraction: $\mathcal{F}^{-1}g_1 - \mathcal{F}^{-1}g_2 = \mathcal{F}^{-1}(g_1 - g_2)$.

theorem FrequencyDecomposition.lp_piece_endpoint_as_fourierInv (f : ℝ2 → ℂ) (K k : ℕ) (hk : ¬k < K ∨ k = 0) : ∃ (g : ℝ2 → ℂ), Function.support g ⊆ Metric.closedBall 0 (1 / 2 ^ k) ∧ (fun (x : ℝ2) => littlewoodPaleyPieceK f K k x) = FourierTransformInv.fourierInv g

Endpoint case ($k \geq K$ or $k = 0$): the Littlewood–Paley piece can be written as the inverse Fourier transform of a function supported in the ball of radius $1/2^k$.

theorem FrequencyDecomposition.annular_support_in_ball (f : ℝ2 → ℂ) (k : ℕ) : (Function.support fun (ξ : ℝ2) => (FourierTransform.fourier f ξ * if dist ξ 0 ≤ 1 / 2 ^ k then 1 else 0) - FourierTransform.fourier f ξ * if dist ξ 0 ≤ 1 / 2 ^ (k + 1) then 1 else 0) ⊆ Metric.closedBall 0 (1 / 2 ^ k)

The annular difference $\hat f \cdot (\mathbf 1_{B_{1/2^k}} - \mathbf 1_{B_{1/2^{k+1}}})$ is supported in the ball of radius $1/2^k$.

theorem FrequencyDecomposition.lp_piece_as_fourierInv (f : ℝ2 → ℂ) (K k : ℕ) : ∃ (g : ℝ2 → ℂ), Function.support g ⊆ Metric.closedBall 0 (1 / 2 ^ k) ∧ (fun (x : ℝ2) => littlewoodPaleyPieceK f K k x) = FourierTransformInv.fourierInv g

Every Littlewood–Paley piece is the inverse Fourier transform of some function supported in the ball of radius $1/2^k$, regardless of whether the piece is interior or an endpoint.

theorem FrequencyDecomposition.fourier_lp_piece_support (f : ℝ2 → ℂ) (K k : ℕ) : (fourierSupport fun (x : ℝ2) => littlewoodPaleyPieceK f K k x) ⊆ Metric.closedBall 0 (1 / 2 ^ k)

The Fourier transform of the $k$-th Littlewood–Paley piece is supported in the ball of radius $1/2^k$.

theorem FrequencyDecomposition.littlewoodPaley_freq_support (𝒯 : Finset Tube) (R : ℝ) (hR : 1 ≤ R) (φ : Tube → ℝ2 → ℂ) (hφ_smooth : ∀ T ∈ 𝒯, ContDiff ℝ ⊤ (φ T)) (hφ_integrable : ∀ T ∈ 𝒯, MeasureTheory.Integrable (φ T) MeasureTheory.volume) (hφ_support : ∀ T ∈ 𝒯, Function.support (φ T) ⊆ T.toSet) (r : ℝ) : r ∈ dyadicRange R → fourierSupport (littlewoodPaleyPiece 𝒯 φ R r) ⊆ Metric.closedBall 0 (1 / r)

Frequency support of each Littlewood–Paley piece $f_r$ lies in the ball $\{|\xi| \leq 1/r\}$.

theorem FrequencyDecomposition.pos_of_mem_dyadicRange {R r : ℝ} (hr : r ∈ dyadicRange R) : 0 < r

Every element of dyadicRange R is strictly positive (it is a power of $2$).

theorem FrequencyDecomposition.plancherel_fourierInv (g : ℝ2 → ℂ) (hg : MeasureTheory.Integrable (fun (x : ℝ2) => ‖FourierTransformInv.fourierInv g x‖ ^ 2) MeasureTheory.volume) : ∫ (x : ℝ2), ‖FourierTransformInv.fourierInv g x‖ ^ 2 = ∫ (ξ : ℝ2), ‖g ξ‖ ^ 2

Plancherel for the inverse Fourier transform on $\mathbb{R}^2$: $\int |\mathcal{F}^{-1}g|^2 = \int |g|^2$ whenever the LHS is integrable.

theorem FrequencyDecomposition.tube_freq_restricted_l2_bound_core (φ : ℝ2 → ℂ) (hsmooth : ContDiff ℝ ⊤ φ) (hint : MeasureTheory.Integrable φ MeasureTheory.volume) (T : Tube) (hsupp : Function.support φ ⊆ T.toSet) (R : ℝ) (hR : 1 ≤ R) (hTR : T.R = R) (r : ℝ) (hr_pos : 0 < r) (hr_le : r ≤ R) : ∫ (ξ : ℝ2), ‖FourierTransform.fourier φ ξ * if dist ξ 0 ≤ 1 / r then 1 else 0‖ ^ 2 ≤ r⁻¹ * R

Core frequency-side estimate: if $\varphi$ is a smooth integrable function supported in a $1 \times R$ tube $T$, then the $L^2$ mass of its Fourier transform restricted to the ball $\{|\xi| \leq 1/r\}$ is at most $R/r$.

theorem FrequencyDecomposition.tube_freq_loc_spatial_integrable (φ : ℝ2 → ℂ) (hsmooth : ContDiff ℝ ⊤ φ) (hint : MeasureTheory.Integrable φ MeasureTheory.volume) (T : Tube) (hsupp : Function.support φ ⊆ T.toSet) (R : ℝ) (hR : 1 ≤ R) (hTR : T.R = R) (r : ℝ) (hr_pos : 0 < r) (hr_le : r ≤ R) : MeasureTheory.Integrable (fun (x : ℝ2) => ‖cumulativeFreqProj φ r x‖ ^ 2) MeasureTheory.volume

$|P_{\leq 1/r}\varphi|^2$ is integrable on $\mathbb{R}^2$, where $\varphi$ is a smooth integrable tube-supported function.

theorem FrequencyDecomposition.tube_freq_loc_spatial_l2_bound (φ : ℝ2 → ℂ) (hsmooth : ContDiff ℝ ⊤ φ) (hint : MeasureTheory.Integrable φ MeasureTheory.volume) (T : Tube) (hsupp : Function.support φ ⊆ T.toSet) (R : ℝ) (hR : 1 ≤ R) (hTR : T.R = R) (r : ℝ) (hr_pos : 0 < r) (hr_le : r ≤ R) : ∫ (x : ℝ2), ‖cumulativeFreqProj φ r x‖ ^ 2 ≤ r⁻¹ * R

Spatial $L^2$ bound for the frequency-localized tube function: $\|P_{\leq 1/r}\varphi\|_{L^2}^2 \leq R/r$. Follows from the core frequency bound via Plancherel.

theorem FrequencyDecomposition.tube_fourier_restricted_l2_bound (φ : ℝ2 → ℂ) (hsmooth : ContDiff ℝ ⊤ φ) (hint : MeasureTheory.Integrable φ MeasureTheory.volume) (T : Tube) (hsupp : Function.support φ ⊆ T.toSet) (R : ℝ) (hR : 1 ≤ R) (hTR : T.R = R) (r : ℝ) (hr_pos : 0 < r) (hr_le : r ≤ R) : ∫ (ξ : ℝ2), ‖FourierTransform.fourier φ ξ * if dist ξ 0 ≤ 1 / r then 1 else 0‖ ^ 2 ≤ r⁻¹ * R

Equivalent frequency-side statement: $\int |\hat\varphi(\xi)|^2 \mathbf 1_{|\xi| \leq 1/r}\, d\xi \leq R/r$.

theorem FrequencyDecomposition.plancherel_bandlimited_tube_bound (φ : ℝ2 → ℂ) (hsmooth : ContDiff ℝ ⊤ φ) (hint : MeasureTheory.Integrable φ MeasureTheory.volume) (T : Tube) (hsupp : Function.support φ ⊆ T.toSet) (R : ℝ) (hR : 1 ≤ R) (hTR : T.R = R) (r : ℝ) (hr_pos : 0 < r) (hr_le : r ≤ R) (hInt : MeasureTheory.Integrable (fun (x : ℝ2) => ‖cumulativeFreqProj φ r x‖ ^ 2) MeasureTheory.volume) : ∫ (x : ℝ2), ‖cumulativeFreqProj φ r x‖ ^ 2 ≤ r⁻¹ * R

Plancherel-based reformulation of the spatial $L^2$ bound for the bandlimited tube projection.

theorem FrequencyDecomposition.freqLocalized_tube_l2_bound (T : Tube) (R : ℝ) (hR : 1 ≤ R) (hTR : T.R = R) (φ_T : ℝ2 → ℂ) (hsmooth : ContDiff ℝ ⊤ φ_T) (hint : MeasureTheory.Integrable φ_T MeasureTheory.volume) (hsupp : Function.support φ_T ⊆ T.toSet) (r : ℝ) (hr_pos : 0 < r) (hr_le : r ≤ R) : l2NormSq (cumulativeFreqProj φ_T r) ≤ r⁻¹ * R

Per-tube $L^2$ estimate: $\|P_{\leq 1/r}\varphi_T\|_{L^2}^2 \leq R/r$ for any smooth integrable bump $\varphi_T$ supported in the tube $T$.

theorem FrequencyDecomposition.l2NormSq_littlewoodPaleyPieceK_le_cumulativeFreqProj (f : ℝ2 → ℂ) (hf_int : MeasureTheory.Integrable f MeasureTheory.volume) (K k : ℕ) (hk_le : k ≤ K) : (l2NormSq fun (x : ℝ2) => littlewoodPaleyPieceK f K k x) ≤ l2NormSq (cumulativeFreqProj f (2 ^ k))

The $L^2$ norm of the $k$-th Littlewood–Paley piece is dominated by the cumulative frequency projection up to scale $2^k$.

theorem FrequencyDecomposition.cumulativeFreqProj_sum {ι : Type u_1} (s : Finset ι) (φ : ι → ℝ2 → ℂ) (hint : ∀ i ∈ s, MeasureTheory.Integrable (φ i) MeasureTheory.volume) (r : ℝ) : (fun (x : ℝ2) => ∑ i ∈ s, cumulativeFreqProj (φ i) r x) = cumulativeFreqProj (fun (x : ℝ2) => ∑ i ∈ s, φ i x) r

The cumulative frequency projection commutes with finite sums: $\sum_i P_{\leq 1/r}\varphi_i = P_{\leq 1/r}(\sum_i \varphi_i)$.

theorem FrequencyDecomposition.lp_piece_bounded_by_proj_sum (𝒯 : Finset Tube) (R : ℝ) (hR : 1 ≤ R) (φ : Tube → ℝ2 → ℂ) (hφ_smooth : ∀ T ∈ 𝒯, ContDiff ℝ ⊤ (φ T)) (hφ_integrable : ∀ T ∈ 𝒯, MeasureTheory.Integrable (φ T) MeasureTheory.volume) (r : ℝ) (hr : r ∈ dyadicRange R) : l2NormSq (littlewoodPaleyPiece 𝒯 φ R r) ≤ l2NormSq fun (x : ℝ2) => ∑ T ∈ 𝒯, cumulativeFreqProj (φ T) r x

$L^2$ norm of a Littlewood–Paley piece at scale $r$ is dominated by the $L^2$ norm of the sum of tube-wise cumulative frequency projections.

noncomputable def FrequencyDecomposition.tubeInteraction (g F : ℝ2 → ℂ) : ℝ

The pairwise interaction $\langle g, F\rangle_{\mathbb R} = \mathrm{Re} \int \overline{g(x)} F(x)\, dx$ between two complex-valued functions.

theorem FrequencyDecomposition.norm_sq_sum_eq_sum_re_tube (𝒯 : Finset Tube) (g : Tube → ℂ) : ‖∑ T ∈ 𝒯, g T‖ ^ 2 = ∑ T ∈ 𝒯, ((starRingEnd ℂ) (g T) * ∑ T' ∈ 𝒯, g T').re

Pointwise expansion of $\|\sum_T g(T)\|^2$ as $\sum_T \mathrm{Re}(\overline{g(T)} \sum_{T'} g(T'))$.

theorem FrequencyDecomposition.l2NormSq_sum_eq_sum_interaction (𝒯 : Finset Tube) (g : Tube → ℝ2 → ℂ) (hint : ∀ T ∈ 𝒯, MeasureTheory.Integrable (fun (x : ℝ2) => ((starRingEnd ℂ) (g T x) * ∑ T' ∈ 𝒯, g T' x).re) MeasureTheory.volume) : (l2NormSq fun (x : ℝ2) => ∑ T ∈ 𝒯, g T x) = ∑ T ∈ 𝒯, tubeInteraction (g T) fun (x : ℝ2) => ∑ T' ∈ 𝒯, g T' x

$L^2$ norm of a tube sum equals the sum of tube interactions: $\|\sum_T g_T\|_{L^2}^2 = \sum_T \langle g_T, \sum_{T'} g_{T'}\rangle$.

theorem FrequencyDecomposition.pairwise_freq_interaction_integrable (𝒯 : Finset Tube) (R : ℝ) (hR : 1 ≤ R) (φ : Tube → ℝ2 → ℂ) (hφ_smooth : ∀ T ∈ 𝒯, ContDiff ℝ ⊤ (φ T)) (hφ_integrable : ∀ T ∈ 𝒯, MeasureTheory.Integrable (φ T) MeasureTheory.volume) (hφ_support : ∀ T ∈ 𝒯, Function.support (φ T) ⊆ T.toSet) (r : ℝ) (T T' : Tube) (hT : T ∈ 𝒯) (hT' : T' ∈ 𝒯) : MeasureTheory.Integrable (fun (x : ℝ2) => ((starRingEnd ℂ) (cumulativeFreqProj (φ T) r x) * cumulativeFreqProj (φ T') r x).re) MeasureTheory.volume

The pairwise interaction $\langle P_{\leq 1/r}\varphi_T, P_{\leq 1/r}\varphi_{T'}\rangle$ between two tube projections is integrable.

theorem FrequencyDecomposition.cumulativeFreqProj_l2NormSq_comparable (𝒯 : Finset Tube) (R : ℝ) (hR : 1 ≤ R) (hR_eq : ∀ T ∈ 𝒯, T.R = R) (φ : Tube → ℝ2 → ℂ) (hφ_smooth : ∀ T ∈ 𝒯, ContDiff ℝ ⊤ (φ T)) (hφ_integrable : ∀ T ∈ 𝒯, MeasureTheory.Integrable (φ T) MeasureTheory.volume) (hφ_support : ∀ T ∈ 𝒯, Function.support (φ T) ⊆ T.toSet) (r : ℝ) (hr : r ∈ dyadicRange R) (T : Tube) (hT : T ∈ 𝒯) : l2NormSq (cumulativeFreqProj (φ T) r) ≤ r⁻¹ * R

Per-tube $L^2$ bound restated as a wrapper for tubes belonging to a collection: $\|P_{\leq 1/r}\varphi_T\|_{L^2}^2 \leq R/r$.

theorem FrequencyDecomposition.pairwise_interaction_cauchy_schwarz (𝒯 : Finset Tube) (R : ℝ) (hR : 1 ≤ R) (hR_eq : ∀ T ∈ 𝒯, T.R = R) (φ : Tube → ℝ2 → ℂ) (hφ_smooth : ∀ T ∈ 𝒯, ContDiff ℝ ⊤ (φ T)) (hφ_integrable : ∀ T ∈ 𝒯, MeasureTheory.Integrable (φ T) MeasureTheory.volume) (hφ_support : ∀ T ∈ 𝒯, Function.support (φ T) ⊆ T.toSet) (r : ℝ) (hr : r ∈ dyadicRange R) (T T' : Tube) (hT : T ∈ 𝒯) (hT' : T' ∈ 𝒯) (hcontained : ∃ (W : WideTube), W.halfWidth = r ∧ W.halfLength = R ∧ T.containedIn W ∧ T'.containedIn W) : tubeInteraction (cumulativeFreqProj (φ T) r) (cumulativeFreqProj (φ T') r) ≤ r⁻¹ * R

Cauchy–Schwarz bound on pairwise tube interactions (for neighbors): when both tubes lie in a common $r \times R$ wide tube, $|\langle P_{\leq 1/r}\varphi_T, P_{\leq 1/r}\varphi_{T'}\rangle| \leq R/r$.

theorem FrequencyDecomposition.non_neighbor_interaction_vanishes (𝒯 : Finset Tube) (R : ℝ) (hR : 1 ≤ R) (hR_eq : ∀ T ∈ 𝒯, T.R = R) (φ : Tube → ℝ2 → ℂ) (hφ_smooth : ∀ T ∈ 𝒯, ContDiff ℝ ⊤ (φ T)) (hφ_integrable : ∀ T ∈ 𝒯, MeasureTheory.Integrable (φ T) MeasureTheory.volume) (hφ_support : ∀ T ∈ 𝒯, Function.support (φ T) ⊆ T.toSet) (r : ℝ) (hr : r ∈ dyadicRange R) (T T' : Tube) (hT : T ∈ 𝒯) (hT' : T' ∈ 𝒯) (hnot_contained : ¬∃ (W : WideTube), W.halfWidth = r ∧ W.halfLength = R ∧ T.containedIn W ∧ T'.containedIn W) : tubeInteraction (cumulativeFreqProj (φ T) r) (cumulativeFreqProj (φ T') r) = 0

For tubes $T, T'$ that do not share any common $r \times R$ containing rectangle, the tube interaction vanishes.

theorem FrequencyDecomposition.negligible_interaction_non_neighbors (𝒯 : Finset Tube) (R : ℝ) (hR : 1 ≤ R) (hR_eq : ∀ T ∈ 𝒯, T.R = R) (φ : Tube → ℝ2 → ℂ) (hφ_smooth : ∀ T ∈ 𝒯, ContDiff ℝ ⊤ (φ T)) (hφ_integrable : ∀ T ∈ 𝒯, MeasureTheory.Integrable (φ T) MeasureTheory.volume) (hφ_support : ∀ T ∈ 𝒯, Function.support (φ T) ⊆ T.toSet) (r : ℝ) (hr : r ∈ dyadicRange R) (T T' : Tube) (hT : T ∈ 𝒯) (hT' : T' ∈ 𝒯) (hnot_contained : ¬∃ (W : WideTube), W.halfWidth = r ∧ W.halfLength = R ∧ T.containedIn W ∧ T'.containedIn W) : tubeInteraction (cumulativeFreqProj (φ T) r) (cumulativeFreqProj (φ T') r) ≤ 0

Non-positivity (in fact zero) of interactions for non-neighboring tube pairs.

theorem FrequencyDecomposition.wideTube_containment_through_shared_tube (T T' : Tube) (W W₀ : WideTube) (hWw : W.halfWidth = W₀.halfWidth) (hWl : W.halfLength = W₀.halfLength) (hTW₀ : T.containedIn W₀) (hTW : T.containedIn W) (hT'W : T'.containedIn W) : T'.containedIn W₀

Transitivity-of-containment for wide tubes of the same dimensions: if $T$ lies in both $W_0$ and $W$, and $T'$ also lies in $W$, then $T'$ lies in $W_0$.

theorem FrequencyDecomposition.neighbor_counting_bound (𝒯 : Finset Tube) (R r : ℝ) (hR : 1 ≤ R) (T : Tube) (hT : T ∈ 𝒯) : {T' ∈ 𝒯 | ∃ (W : WideTube), W.halfWidth = r ∧ W.halfLength = R ∧ T.containedIn W ∧ T'.containedIn W}.card ≤ tubeCoveringNumber 𝒯 R r

The number of tubes that share an $r \times R$ wide tube with T is at most the tube covering number $N_\mathcal{T}(r)$.

theorem FrequencyDecomposition.orthogonality_interaction_sum_bound (𝒯 : Finset Tube) (R : ℝ) (hR : 1 ≤ R) (hR_eq : ∀ T ∈ 𝒯, T.R = R) (φ : Tube → ℝ2 → ℂ) (hφ_smooth : ∀ T ∈ 𝒯, ContDiff ℝ ⊤ (φ T)) (hφ_integrable : ∀ T ∈ 𝒯, MeasureTheory.Integrable (φ T) MeasureTheory.volume) (hφ_support : ∀ T ∈ 𝒯, Function.support (φ T) ⊆ T.toSet) (r : ℝ) (hr : r ∈ dyadicRange R) (T : Tube) (hT : T ∈ 𝒯) : ∑ T' ∈ 𝒯, tubeInteraction (cumulativeFreqProj (φ T) r) (cumulativeFreqProj (φ T') r) ≤ ↑(tubeCoveringNumber 𝒯 R r) * (r⁻¹ * R)

Row-sum bound: for each tube $T$, $\sum_{T' \in \mathcal{T}} \langle P_{\leq 1/r}\varphi_T, P_{\leq 1/r}\varphi_{T'}\rangle \leq N_\mathcal{T}(r) \cdot (R/r)$. Combines orthogonality on non-neighbors with the Cauchy–Schwarz bound on neighbors.

theorem FrequencyDecomposition.per_tube_interaction_bound (𝒯 : Finset Tube) (R : ℝ) (hR : 1 ≤ R) (hR_eq : ∀ T ∈ 𝒯, T.R = R) (φ : Tube → ℝ2 → ℂ) (hφ_smooth : ∀ T ∈ 𝒯, ContDiff ℝ ⊤ (φ T)) (hφ_integrable : ∀ T ∈ 𝒯, MeasureTheory.Integrable (φ T) MeasureTheory.volume) (hφ_support : ∀ T ∈ 𝒯, Function.support (φ T) ⊆ T.toSet) (r : ℝ) (hr : r ∈ dyadicRange R) (T : Tube) (hT : T ∈ 𝒯) : (tubeInteraction (cumulativeFreqProj (φ T) r) fun (x : ℝ2) => ∑ T' ∈ 𝒯, cumulativeFreqProj (φ T') r x) ≤ ↑(tubeCoveringNumber 𝒯 R r) * (r⁻¹ * R)

Per-tube interaction bound: $\langle P_{\leq 1/r}\varphi_T, \sum_{T'} P_{\leq 1/r}\varphi_{T'}\rangle \leq N_\mathcal{T}(r) \cdot (R/r)$, obtained by expanding the right-hand side via linearity of integration.

theorem FrequencyDecomposition.interaction_integrable (𝒯 : Finset Tube) (R : ℝ) (hR : 1 ≤ R) (φ : Tube → ℝ2 → ℂ) (hφ_smooth : ∀ T ∈ 𝒯, ContDiff ℝ ⊤ (φ T)) (hφ_integrable : ∀ T ∈ 𝒯, MeasureTheory.Integrable (φ T) MeasureTheory.volume) (hφ_support : ∀ T ∈ 𝒯, Function.support (φ T) ⊆ T.toSet) (r : ℝ) (T : Tube) (hT : T ∈ 𝒯) : MeasureTheory.Integrable (fun (x : ℝ2) => ((starRingEnd ℂ) (cumulativeFreqProj (φ T) r x) * ∑ T' ∈ 𝒯, cumulativeFreqProj (φ T') r x).re) MeasureTheory.volume

Integrability of the interaction between a single tube projection and the sum of all tube projections.

theorem FrequencyDecomposition.orthogonality_counting_for_tubes (𝒯 : Finset Tube) (R : ℝ) (hR : 1 ≤ R) (hR_eq : ∀ T ∈ 𝒯, T.R = R) (φ : Tube → ℝ2 → ℂ) (hφ_smooth : ∀ T ∈ 𝒯, ContDiff ℝ ⊤ (φ T)) (hφ_integrable : ∀ T ∈ 𝒯, MeasureTheory.Integrable (φ T) MeasureTheory.volume) (hφ_support : ∀ T ∈ 𝒯, Function.support (φ T) ⊆ T.toSet) (r : ℝ) (hr : r ∈ dyadicRange R) : (l2NormSq fun (x : ℝ2) => ∑ T ∈ 𝒯, cumulativeFreqProj (φ T) r x) ≤ ↑(tubeCoveringNumber 𝒯 R r) * ↑𝒯.card * (r⁻¹ * R)

$L^2$ orthogonality counting bound: $\|\sum_T P_{\leq 1/r}\varphi_T\|_{L^2}^2 \leq N_\mathcal{T}(r) \cdot |\mathcal{T}| \cdot (R/r)$.

theorem FrequencyDecomposition.l2_orthogonality_counting (𝒯 : Finset Tube) (R : ℝ) (hR : 1 ≤ R) (hR_eq : ∀ T ∈ 𝒯, T.R = R) (φ : Tube → ℝ2 → ℂ) (hφ_smooth : ∀ T ∈ 𝒯, ContDiff ℝ ⊤ (φ T)) (hφ_integrable : ∀ T ∈ 𝒯, MeasureTheory.Integrable (φ T) MeasureTheory.volume) (hφ_support : ∀ T ∈ 𝒯, Function.support (φ T) ⊆ T.toSet) (r : ℝ) (hr : r ∈ dyadicRange R) (hint : MeasureTheory.Integrable (fun (x : ℝ2) => ‖littlewoodPaleyPiece 𝒯 φ R r x‖ ^ 2) MeasureTheory.volume) : l2NormSq (littlewoodPaleyPiece 𝒯 φ R r) ≤ ↑(tubeCoveringNumber 𝒯 R r) * ↑𝒯.card * (r⁻¹ * R)

Direct $L^2$ bound on the Littlewood–Paley piece $f_r$ via orthogonality counting: $\|f_r\|_{L^2}^2 \leq N_\mathcal{T}(r) \cdot |\mathcal{T}| \cdot (R/r)$.

theorem FrequencyDecomposition.littlewoodPaley_l2_estimate (𝒯 : Finset Tube) (R : ℝ) (hR : 1 ≤ R) (hR_eq : ∀ T ∈ 𝒯, T.R = R) (φ : Tube → ℝ2 → ℂ) (hφ_smooth : ∀ T ∈ 𝒯, ContDiff ℝ ⊤ (φ T)) (hφ_integrable : ∀ T ∈ 𝒯, MeasureTheory.Integrable (φ T) MeasureTheory.volume) (hφ_support : ∀ T ∈ 𝒯, Function.support (φ T) ⊆ T.toSet) (r : ℝ) : r ∈ dyadicRange R → l2NormSq (littlewoodPaleyPiece 𝒯 φ R r) ≤ 1 * ↑(tubeCoveringNumber 𝒯 R r) * ↑𝒯.card * r⁻¹ * R

Final per-scale $L^2$ estimate for the Littlewood–Paley pieces: $\|f_r\|_{L^2}^2 \leq N_\mathcal{T}(r) \cdot |\mathcal{T}| \cdot R / r$.

theorem FrequencyDecomposition.main_lemma_real (𝒯 : Finset Tube) (R : ℝ) (hR : 1 ≤ R) (hR_eq : ∀ T ∈ 𝒯, T.R = R) (φ : Tube → ℝ2 → ℂ) (hφ_smooth : ∀ T ∈ 𝒯, ContDiff ℝ ⊤ (φ T)) (hφ_integrable : ∀ T ∈ 𝒯, MeasureTheory.Integrable (φ T) MeasureTheory.volume) (hφ_support : ∀ T ∈ 𝒯, Function.support (φ T) ⊆ T.toSet) : ∃ (data : FrequencyDecompositionData 𝒯 R), data.φ = φ

Main Lemma (real version). Let $\mathcal{T}$ be a finite set of $1 \times R$ tubes in $\mathbb{R}^2$ and $\varphi_T$ a smooth integrable bump supported on each tube. Then there exists a Littlewood–Paley frequency decomposition $f = \sum_T \varphi_T = \sum_{r \in \text{dyadic}} f_r$ with $\hat{f_r}$ supported in $\{|\xi| \leq 1/r\}$ and the per-scale $L^2$ estimate $\|f_r\|_{L^2}^2 \leq N_\mathcal{T}(r) \cdot |\mathcal{T}| \cdot R / r$.