noncomputable def OrthogonalityTubes.perp (d : EuclideanSpace ℝ (Fin 2)) : EuclideanSpace ℝ (Fin 2)

The perpendicular vector in $\mathbb{R}^2$: $\mathrm{perp}(d_0, d_1) = (-d_1, d_0)$.

def OrthogonalityTubes.rectangleCarrier (c d : EuclideanSpace ℝ (Fin 2)) (w l : ℝ) : Set (EuclideanSpace ℝ (Fin 2))

Underlying point set of a rectangle with centre $c$, axis-direction $d$, width $w$ and length $l$: the set of $x$ with $|\langle x - c, d\rangle| \le l/2$ and $|\langle x - c, d^\perp\rangle| \le w/2$.

structure OrthogonalityTubes.Tube (R : ℝ) : Type

A tube of length $R$ in $\mathbb{R}^2$: an oriented $1 \times R$ rectangle parameterised by a centre point and a unit direction vector.

• center : EuclideanSpace ℝ (Fin 2)
• direction : EuclideanSpace ℝ (Fin 2)
• direction_unit : ‖self.direction‖ = 1

def OrthogonalityTubes.Tube.carrier {R : ℝ} (T : Tube R) : Set (EuclideanSpace ℝ (Fin 2))

The underlying point set of a tube $T$: the $1 \times R$ rectangle with axis along T.direction centred at T.center.

def OrthogonalityTubes.Tube.rNeighborhood {R : ℝ} (T : Tube R) (r : ℝ) : Set (EuclideanSpace ℝ (Fin 2))

The open $r$-thickening of a tube's carrier (the set of points within distance $r$).

structure OrthogonalityTubes.Rectangle (width length : ℝ) : Type

An oriented rectangle in $\mathbb{R}^2$ of given width and length, parameterised by a centre and a unit direction (the axis of the rectangle).

• center : EuclideanSpace ℝ (Fin 2)
• direction : EuclideanSpace ℝ (Fin 2)
• direction_unit : ‖self.direction‖ = 1

def OrthogonalityTubes.Rectangle.carrier {w l : ℝ} (rect : Rectangle w l) : Set (EuclideanSpace ℝ (Fin 2))

The underlying point set of a Rectangle: a $w \times l$ rectangle centred at rect.center with axis rect.direction.

def OrthogonalityTubes.Tube.containedIn {R : ℝ} (T : Tube R) {w l : ℝ} (rect : Rectangle w l) : Prop

A tube T is contained in a rectangle rect if its carrier is a subset of the rectangle's carrier.

noncomputable def OrthogonalityTubes.stdBilinR2 : EuclideanSpace ℝ (Fin 2) →ₗ[ℝ] EuclideanSpace ℝ (Fin 2) →ₗ[ℝ] ℝ

The standard bilinear pairing $(v, w) \mapsto \langle v, w\rangle$ on $\mathbb{R}^2$, packaged as a continuous bilinear map (used to define the Fourier transform on $\mathbb{R}^2$).

noncomputable def OrthogonalityTubes.fourierTransformR2 (f : EuclideanSpace ℝ (Fin 2) → ℂ) : EuclideanSpace ℝ (Fin 2) → ℂ

The Fourier transform on $\mathbb{R}^2$: $\widehat f(\xi) = \int_{\mathbb{R}^2} f(x)\, e^{-2\pi i \langle x, \xi\rangle}\, dx$.

def OrthogonalityTubes.freqAnnulus (r : ℝ) : Set (EuclideanSpace ℝ (Fin 2))

The frequency annulus at scale $r$: $\{\xi : r^{-1}/2 \le \|\xi\| \le 2 r^{-1}\}$.

noncomputable def OrthogonalityTubes.phiTubeFreqLoc (R r : ℝ) (T : Tube R) : EuclideanSpace ℝ (Fin 2) → ℂ

The frequency-localised wave packet $\phi_{T, r}$ associated to a tube $T$ at scale $r$: a function whose Fourier transform is concentrated in an angular cap of width $\sim r/R$ around the direction of $T$.

def OrthogonalityTubes.freqAngularCap (R r : ℝ) (T : Tube R) : Set (EuclideanSpace ℝ (Fin 2))

The frequency angular cap supporting $\widehat{\phi_{T, r}}$: frequencies in the annulus of scale $r$ that lie within angular distance $\lesssim r / R$ of the line $\mathbb{R} \cdot T.\mathrm{direction}$.

theorem OrthogonalityTubes.phiTubeFreqLoc_angularSupport (R r : ℝ) (hR : 1 ≤ R) (hr : 0 < r) (hrR : r ≤ R) (T : Tube R) (ξ : EuclideanSpace ℝ (Fin 2)) : ξ ∉ freqAngularCap R r T → fourierTransformR2 (phiTubeFreqLoc R r T) ξ = 0

Angular Fourier support of the tube wave packet: $\widehat{\phi_{T, r}}$ vanishes outside the frequency angular cap of $T$.

noncomputable def OrthogonalityTubes.l2Inner (f g : EuclideanSpace ℝ (Fin 2) → ℂ) : ℂ

The $L^2$ inner product $\langle f, g\rangle = \int f(x) \overline{g(x)}\, dx$ on $\mathbb{R}^2$.

noncomputable def OrthogonalityTubes.Tube.angle {R : ℝ} (T₁ T₂ : Tube R) : ℝ

A surrogate for the angle between two tubes: $\|T_1.\text{direction} - T_2.\text{direction}\|$ (which is comparable to $|\sin \theta|$ for the actual angle $\theta$ between the directions when both are unit vectors).

theorem OrthogonalityTubes.plancherel_l2Inner (f g : EuclideanSpace ℝ (Fin 2) → ℂ) : l2Inner f g = l2Inner (fourierTransformR2 f) (fourierTransformR2 g)

Plancherel's theorem on $\mathbb{R}^2$: $\langle f, g\rangle_{L^2} = \langle \widehat f, \widehat g\rangle_{L^2}$.

theorem OrthogonalityTubes.phiTubeFreqLoc_disjoint_fourierSupport {R : ℝ} (hR : 1 ≤ R) {r : ℝ} (hr : 0 < r) (hrR : r ≤ R) {ε : ℝ} (hε : 0 < ε) (T₁ T₂ : Tube R) (hangle : T₁.angle T₂ ≥ R ^ ε * (r / R)) (ξ : EuclideanSpace ℝ (Fin 2)) : fourierTransformR2 (phiTubeFreqLoc R r T₁) ξ = 0 ∨ fourierTransformR2 (phiTubeFreqLoc R r T₂) ξ = 0

If two tubes have angular separation $\ge R^\varepsilon \cdot r/R$ then the Fourier supports of their wave packets $\phi_{T_1, r}, \phi_{T_2, r}$ are disjoint: at every frequency $\xi$, at least one of the Fourier transforms vanishes.

theorem OrthogonalityTubes.l2Inner_eq_zero_of_pointwise_disjoint (f g : EuclideanSpace ℝ (Fin 2) → ℂ) (h : ∀ (ξ : EuclideanSpace ℝ (Fin 2)), f ξ = 0 ∨ g ξ = 0) : l2Inner f g = 0

If at every point $\xi$ either $f(\xi) = 0$ or $g(\xi) = 0$, then $\langle f, g\rangle = 0$ — the integrand vanishes identically.

theorem OrthogonalityTubes.orthogonality_tubes_case_angle {R : ℝ} (hR : 1 ≤ R) {r : ℝ} (hr : 1 ≤ r) (hrR : r ≤ R) {ε : ℝ} (hε : 0 < ε) (T₁ T₂ : Tube R) (hangle : T₁.angle T₂ ≥ R ^ ε * (r / R)) : l2Inner (phiTubeFreqLoc R r T₁) (phiTubeFreqLoc R r T₂) = 0

Orthogonality of tube wave packets (angular case): if the tubes have angular separation $\ge R^\varepsilon \cdot r/R$, then $\langle \phi_{T_1, r}, \phi_{T_2, r}\rangle = 0$ exactly. Proof: Plancherel plus disjoint Fourier supports.

theorem OrthogonalityTubes.Tube.carrier_nonempty {R : ℝ} (hR : 1 ≤ R) (T : Tube R) : T.carrier.Nonempty

For $R \ge 1$, the carrier of every tube is nonempty (the centre belongs to it).

theorem OrthogonalityTubes.disjoint_thickening_infDist {R : ℝ} (hR : 1 ≤ R) {r : ℝ} (T₁ T₂ : Tube R) (hdisjoint : Disjoint (T₁.rNeighborhood r) (T₂.rNeighborhood r)) (x : EuclideanSpace ℝ (Fin 2)) : r ≤ Metric.infDist x T₁.carrier ∨ r ≤ Metric.infDist x T₂.carrier

If the $r$-thickenings of two tubes are disjoint, then for every point $x$ at least one of the two tubes lies at distance $\ge r$ from $x$.

theorem OrthogonalityTubes.phiTubeFreqLoc_schwartz_bound (R r : ℝ) (hR : 1 ≤ R) (hr : 1 ≤ r) (hrR : r ≤ R) (T : Tube R) (N : ℝ) (hN : 0 < N) (x : EuclideanSpace ℝ (Fin 2)) : ‖phiTubeFreqLoc R r T x‖ ≤ r⁻¹ * (1 + Metric.infDist x T.carrier / r) ^ (-N)

Schwartz-type pointwise decay bound for the tube wave packet: $|\phi_{T, r}(x)| \le r^{-1} (1 + d(x, T) / r)^{-N}$ for every $N > 0$.

theorem OrthogonalityTubes.phiTubeFreqLoc_norm_integrable (R r : ℝ) (hR : 1 ≤ R) (hr : 1 ≤ r) (hrR : r ≤ R) (T : Tube R) : MeasureTheory.Integrable (fun (x : EuclideanSpace ℝ (Fin 2)) => ‖phiTubeFreqLoc R r T x‖) MeasureTheory.volume

The tube wave packet $\phi_{T, r}$ is absolutely integrable on $\mathbb{R}^2$ — its norm function lies in $L^1$.

theorem OrthogonalityTubes.phiTubeFreqLoc_l1_le (R r : ℝ) (hR : 1 ≤ R) (hr : 1 ≤ r) (hrR : r ≤ R) (T : Tube R) : ∫ (x : EuclideanSpace ℝ (Fin 2)), ‖phiTubeFreqLoc R r T x‖ ≤ R / 4

$L^1$ bound on the tube wave packet: $\int_{\mathbb{R}^2} |\phi_{T, r}(x)|\, dx \le R/4$.

theorem OrthogonalityTubes.phiTubeFreqLoc_product_integral_bound {R : ℝ} (hR : 1 ≤ R) {r : ℝ} (hr : 1 ≤ r) (hrR : r ≤ R) (T₁ T₂ : Tube R) (hdisjoint : Disjoint (T₁.rNeighborhood r) (T₂.rNeighborhood r)) : ∫ (x : EuclideanSpace ℝ (Fin 2)), ‖phiTubeFreqLoc R r T₁ x * (starRingEnd ℂ) (phiTubeFreqLoc R r T₂ x)‖ ≤ R ^ (-1000)

If two tubes are $r$-separated, then the pointwise product of their wave packets satisfies $\int_{\mathbb{R}^2} |\phi_{T_1, r}(x) \overline{\phi_{T_2, r}(x)}|\, dx \le R^{-1000}$ (rapid decay from Schwartz estimates plus the $r$-separation).

theorem OrthogonalityTubes.orthogonality_tubes_case_disjoint_support {R : ℝ} (hR : 1 ≤ R) {r : ℝ} (hr : 1 ≤ r) (hrR : r ≤ R) (T₁ T₂ : Tube R) (hdisjoint : Disjoint (T₁.rNeighborhood r) (T₂.rNeighborhood r)) : ‖l2Inner (phiTubeFreqLoc R r T₁) (phiTubeFreqLoc R r T₂)‖ ≤ R ^ (-1000)

Orthogonality of tube wave packets (spatial-disjointness case): if the $r$-thickenings of $T_1$ and $T_2$ are disjoint, then $|\langle \phi_{T_1, r}, \phi_{T_2, r}\rangle| \le R^{-1000}$.

theorem OrthogonalityTubes.tubes_fit_in_rect_of_close {R : ℝ} (hR : 1 ≤ R) {r : ℝ} (hr : 1 ≤ r) (hrR : r ≤ R) {ε : ℝ} (hε : 0 < ε) (T₁ T₂ : Tube R) (hangle : T₁.angle T₂ < R ^ ε * (r / R)) (hoverlap : ¬Disjoint (T₁.rNeighborhood r) (T₂.rNeighborhood r)) : ∃ (T_tilde : Rectangle (R ^ ε * r) (R ^ (1 + ε))), T₁.containedIn T_tilde ∧ T₂.containedIn T_tilde

Geometric covering lemma: if two tubes are angularly close ($\angle T_1, T_2 < R^\varepsilon \cdot r/R$) and their $r$-thickenings overlap, then they fit inside a common $R^\varepsilon r \times R^{1 + \varepsilon}$ rectangle.

theorem OrthogonalityTubes.geometric_dichotomy {R : ℝ} (hR : 1 ≤ R) {r : ℝ} (hr : 1 ≤ r) (hrR : r ≤ R) {ε : ℝ} (hε : 0 < ε) (T₁ T₂ : Tube R) (hnotRect : ¬∃ (T_tilde : Rectangle (R ^ ε * r) (R ^ (1 + ε))), T₁.containedIn T_tilde ∧ T₂.containedIn T_tilde) : T₁.angle T₂ ≥ R ^ ε * (r / R) ∨ Disjoint (T₁.rNeighborhood r) (T₂.rNeighborhood r)

Geometric dichotomy contrapositive of tubes_fit_in_rect_of_close: if no common covering $R^\varepsilon r \times R^{1 + \varepsilon}$ rectangle exists, then either the tubes have large angular separation, or their $r$-thickenings are disjoint.

theorem OrthogonalityTubes.orthogonality_tubes {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (R : ℝ), 1 ≤ R → ∀ (r : ℝ), 1 ≤ r → r ≤ R → ∀ (T₁ T₂ : Tube R), (¬∃ (T_tilde : Rectangle (R ^ ε * r) (R ^ (1 + ε))), T₁.containedIn T_tilde ∧ T₂.containedIn T_tilde) → ‖l2Inner (phiTubeFreqLoc R r T₁) (phiTubeFreqLoc R r T₂)‖ ≤ C * R ^ (-1000)

Orthogonality of tube wave packets (Lemma): if two $1 \times R$ tubes $T_1, T_2$ do not fit into a common $R^\varepsilon r \times R^{1 + \varepsilon}$ rectangle, then $|\langle \phi_{T_1, r}, \phi_{T_2, r}\rangle| \lesssim R^{-1000}$. The implicit constant $C$ is uniform in $R, r, T_1, T_2$.