structure ProjectionTheory.EuclideanProjectionData : Type

Data bundle for the Euclidean projection bound theorem: a scale parameter R > 1, a point set X of cardinality cardX, a direction set D of cardinality cardD, a uniform projection bound S = max_{θ ∈ D} |π_θ(X)|, and local covering numbers nX r, nD ρ measuring the maximum number of points of X (resp. directions of D) in any ball of radius r (resp. ρ), each bounded above by cardX, cardD.

• R : ℝ
• hR : 1 < self.R
• cardX : ℕ
• hcardX : 0 < self.cardX
• cardD : ℕ
• hcardD : 0 < self.cardD
• S : ℕ
• hS : 0 < self.S
• nX : ℝ → ℕ
• nD : ℝ → ℕ
• hnX_le (r : ℝ) : ↑(self.nX r) ≤ ↑self.cardX
• hnD_le (ρ : ℝ) : ↑(self.nD ρ) ≤ ↑self.cardD

noncomputable def ProjectionTheory.numDyadicScales (d : EuclideanProjectionData) : ℕ

Number of dyadic scales 1 ≤ r ≤ R used in the wave packet decomposition; explicitly ⌊log₂ ⌈R⌉⌋ + 1.

theorem ProjectionTheory.wave_packet_construction (d : EuclideanProjectionData) : ∃ (L2_energy : ℝ) (per_scale : Fin (numDyadicScales d) → ℝ) (f_values : Fin d.cardX → ℝ), (∀ (i : Fin d.cardX), f_values i ≥ ↑d.cardD) ∧ L2_energy = ∑ i : Fin d.cardX, f_values i ^ 2 ∧ L2_energy = Finset.univ.sum per_scale ∧ ∀ (k : Fin (numDyadicScales d)), per_scale k ≤ ↑d.S * ↑d.cardD * d.R * ⨆ r ∈ Set.Icc 1 d.R, ↑(d.nX r) * ↑(d.nD (r / d.R)) / r ^ 2

Existence of the wave packet decomposition f = ∑ₖ fₖ underlying the Euclidean projection bound. Produces a total L²-energy together with per-scale energies and pointwise values such that:

• f(i) ≥ |D| at every point of X (the projection lower bound),
• the total energy equals both ∑ᵢ f(i)² and the sum of per-scale energies, and
• each per-scale energy is bounded by S · |D| · R · max_{r ∈ [1,R]} (N_X(r) · N_D(r/R) / r²).

noncomputable def ProjectionTheory.wave_packet_L2_energy (d : EuclideanProjectionData) : ℝ

The total L²-energy of the wave packet decomposition extracted from wave_packet_construction.

noncomputable def ProjectionTheory.wave_packet_per_scale_energy (d : EuclideanProjectionData) : Fin (numDyadicScales d) → ℝ

The per-scale L²-energies ‖fₖ‖² extracted from wave_packet_construction.

noncomputable def ProjectionTheory.wave_packet_f_values (d : EuclideanProjectionData) : Fin d.cardX → ℝ

The pointwise values f(i) of the wave packet at the points of X, extracted from wave_packet_construction.

theorem ProjectionTheory.wave_packet_construction_props (d : EuclideanProjectionData) : (∀ (i : Fin d.cardX), wave_packet_f_values d i ≥ ↑d.cardD) ∧ wave_packet_L2_energy d = ∑ i : Fin d.cardX, wave_packet_f_values d i ^ 2 ∧ wave_packet_L2_energy d = Finset.univ.sum (wave_packet_per_scale_energy d) ∧ ∀ (k : Fin (numDyadicScales d)), wave_packet_per_scale_energy d k ≤ ↑d.S * ↑d.cardD * d.R * ⨆ r ∈ Set.Icc 1 d.R, ↑(d.nX r) * ↑(d.nD (r / d.R)) / r ^ 2

Bundles the defining properties of the wave packet construction: pointwise lower bound f(i) ≥ |D|, the two energy identities, and the per-scale energy bound.

theorem ProjectionTheory.wave_packet_pointwise_bound (d : EuclideanProjectionData) : ∃ (f_values : Fin d.cardX → ℝ), (∀ (i : Fin d.cardX), f_values i ≥ ↑d.cardD) ∧ wave_packet_L2_energy d = ∑ i : Fin d.cardX, f_values i ^ 2

Pointwise lower bound for the wave packet: there exist values f(i) ≥ |D| whose squared sum equals the total L²-energy.

theorem ProjectionTheory.wave_packet_lp_orthogonality (d : EuclideanProjectionData) : wave_packet_L2_energy d = Finset.univ.sum (wave_packet_per_scale_energy d)

Near-orthogonality of the dyadic pieces: the total L²-energy equals the sum of the per-scale energies ∑ₖ ‖fₖ‖².

theorem ProjectionTheory.wave_packet_lower_bound (d : EuclideanProjectionData) : ↑d.cardD ^ 2 * ↑d.cardX ≤ wave_packet_L2_energy d

Lower bound on the wave packet L²-energy: since f(i) ≥ |D| at each of the |X| points, we have ‖f‖² ≥ |D|² · |X|.

theorem ProjectionTheory.wave_packet_decomposition_bound (d : EuclideanProjectionData) : wave_packet_L2_energy d ≤ Finset.univ.sum (wave_packet_per_scale_energy d)

Trivial inequality form of orthogonality: ‖f‖² ≤ ∑ₖ ‖fₖ‖².

theorem ProjectionTheory.wave_packet_per_scale_estimate (d : EuclideanProjectionData) (k : Fin (numDyadicScales d)) : wave_packet_per_scale_energy d k ≤ ↑d.S * ↑d.cardD * d.R * ⨆ r ∈ Set.Icc 1 d.R, ↑(d.nX r) * ↑(d.nD (r / d.R)) / r ^ 2

Per-scale L²-bound for the wave packet decomposition: ‖fₖ‖² ≤ S · |D| · R · max_{r ∈ [1,R]} (N_X(r) N_D(r/R) / r²).

theorem ProjectionTheory.dyadic_scale_count_le_log (d : EuclideanProjectionData) : ↑(numDyadicScales d) ≤ Real.logb 2 d.R + 2

The number of dyadic scales is at most log₂ R + 2, which produces the logarithmic factor in the final Euclidean projection bound.

theorem ProjectionTheory.wave_packet_upper_bound (d : EuclideanProjectionData) : wave_packet_L2_energy d ≤ ↑d.S * ↑d.cardD * d.R * (Real.logb 2 d.R + 2) * ⨆ r ∈ Set.Icc 1 d.R, ↑(d.nX r) * ↑(d.nD (r / d.R)) / r ^ 2

Upper bound on the wave packet L²-energy obtained by summing the per-scale estimates over the log₂ R + 2 dyadic scales: ‖f‖² ≤ S · |D| · R · (log₂ R + 2) · max_{r ∈ [1,R]} (N_X(r) N_D(r/R) / r²).

theorem ProjectionTheory.wave_packet_energy_bound (d : EuclideanProjectionData) : ↑d.cardD ^ 2 * ↑d.cardX ≤ ↑d.S * ↑d.cardD * d.R * (Real.logb 2 d.R + 2) * ⨆ r ∈ Set.Icc 1 d.R, ↑(d.nX r) * ↑(d.nD (r / d.R)) / r ^ 2

Combined energy estimate chaining the lower and upper bounds: |D|² · |X| ≤ S · |D| · R · (log₂ R + 2) · max_r (N_X(r) N_D(r/R) / r²).

theorem ProjectionTheory.euclidean_projection_bound (d : EuclideanProjectionData) : ∃ C > 0, ↑d.cardD ≤ C * (Real.logb 2 d.R + 2) * (↑d.S * d.R / ↑d.cardX) * ⨆ r ∈ Set.Icc 1 d.R, ↑(d.nX r) * ↑(d.nD (r / d.R)) / r ^ 2

Euclidean projection bound (the main theorem of the section): there is a constant C > 0 such that $$|D| \lessapprox \frac{S R}{|X|} \max_{1 \le r \le R} \frac{N_X(r)\, N_D(r/R)}{r^2}.$$ This is the Euclidean analogue of the Fourier projection bound (Theorem 2.3) and follows from canceling a factor of |D| in the wave packet energy estimate.