Section 9, part 1: lem:return-splitting and lem:weyl

This file was automatically generated by Claude.

Formalization of blueprint Section 9, "Weyl splitting and progression separation" (sec:charts), part 1: lem:return-splitting and lem:weyl (lines 1244-1335) of blueprint/formalization_blueprint.tex.

theorem TrilinearHT.Auto.quadraticReturnFrequency_pairing {d k : ℕ} (C : Matrix (Fin d) (Fin d) ℝ) (V : Matrix (Fin d) (Fin k) ℝ) (Λ : Matrix (Fin k) (Fin k) ℝ) (hΛ : Λ.IsSymm) (h h' : Fin k → ℝ) (m m' : Fin d → ℝ) : h' ⬝ᵥ quadraticReturnFrequency C V Λ h m - h ⬝ᵥ quadraticReturnFrequency C V Λ h' m' = (V.mulVec h' - m') ⬝ᵥ (C - C.transpose).mulVec (V.mulVec h - m) - m' ⬝ᵥ (C - C.transpose).mulVec m

theorem TrilinearHT.Auto.scaled_integer_skew_pairing {d : ℕ} (C : Matrix (Fin d) (Fin d) ℝ) (P : ℤ) (hC : ∀ (i j : Fin d), ∃ (z : ℤ), ↑P * C i j = ↑z) (n n' : Fin d → ℤ) : ∃ (z : ℤ), ((fun (i : Fin d) => ↑P * ↑(n' i)) ⬝ᵥ (C - C.transpose).mulVec fun (i : Fin d) => ↑P * ↑(n i)) = ↑z

theorem TrilinearHT.Auto.abs_dotProduct_euclidean_le {d : ℕ} (x y : Fin d → ℝ) : |x ⬝ᵥ y| ≤ ‖WithLp.toLp 2 x‖ * ‖WithLp.toLp 2 y‖

theorem TrilinearHT.Auto.quadraticReturnFrequency_pairing_bound {d k : ℕ} (C : Matrix (Fin d) (Fin d) ℝ) (V : Matrix (Fin d) (Fin k) ℝ) (Λ : Matrix (Fin k) (Fin k) ℝ) (hΛ : Λ.IsSymm) (h h' : Fin k → ℝ) (m m' : Fin d → ℝ) {a M : ℝ} (ha : 0 ≤ a) (hh : ‖WithLp.toLp 2 h‖ ≤ a) (hh' : ‖WithLp.toLp 2 h'‖ ≤ a) (hd : ‖WithLp.toLp 2 (V.mulVec h - m)‖ ≤ a) (hd' : ‖WithLp.toLp 2 (V.mulVec h' - m')‖ ≤ a) (hO : ‖WithLp.toLp 2 (quadraticReturnFrequency C V Λ h m)‖ ≤ M) (hO' : ‖WithLp.toLp 2 (quadraticReturnFrequency C V Λ h' m')‖ ≤ M) : |m' ⬝ᵥ (C - C.transpose).mulVec m| ≤ a ^ 2 * ‖realMatrixOperator (C - C.transpose)‖ + 2 * a * M

theorem TrilinearHT.Auto.shortReturnRadius_bound {a M N : ℝ} (ha : 0 < a) (hM : 0 ≤ M) (hN : 0 ≤ N) : have r := min a (100 * (M + N + 1))⁻¹; 0 < r ∧ r ≤ a ∧ r ^ 2 * N + 2 * r * M < 1

theorem TrilinearHT.Auto.quadratic_short_returns_isotropic {d k : ℕ} (C : Matrix (Fin d) (Fin d) ℝ) (V : Matrix (Fin d) (Fin k) ℝ) (Λ : Matrix (Fin k) (Fin k) ℝ) (hΛ : Λ.IsSymm) (P : ℤ) (hC : ∀ (i j : Fin d), ∃ (z : ℤ), ↑P * C i j = ↑z) {a M : ℝ} (ha : 0 < a) (hM : 0 ≤ M) (hΩ : ∀ (h : Fin k → ℝ) (n : Fin d → ℤ), ‖WithLp.toLp 2 h‖ + ‖WithLp.toLp 2 (V.mulVec h - fun (i : Fin d) => ↑P * ↑(n i))‖ ≤ a → ‖WithLp.toLp 2 (quadraticReturnFrequency C V Λ h fun (i : Fin d) => ↑P * ↑(n i))‖ ≤ M) : have r := min a (100 * (M + ‖realMatrixOperator (C - C.transpose)‖ + 1))⁻¹; ∀ (h h' : Fin k → ℝ) (n n' : Fin d → ℤ), ‖WithLp.toLp 2 h‖ + ‖WithLp.toLp 2 (V.mulVec h - fun (i : Fin d) => ↑P * ↑(n i))‖ ≤ r → ‖WithLp.toLp 2 h'‖ + ‖WithLp.toLp 2 (V.mulVec h' - fun (i : Fin d) => ↑P * ↑(n' i))‖ ≤ r → ((fun (i : Fin d) => ↑P * ↑(n' i)) ⬝ᵥ (C - C.transpose).mulVec fun (i : Fin d) => ↑P * ↑(n i)) = 0

Blueprint lem:return-splitting, lines 1265-1269: after the specified radius reduction, all scaled integer short returns pair to zero under the skew form.

theorem TrilinearHT.Auto.quadratic_lattice_return_phase {d k : ℕ} (C : Matrix (Fin d) (Fin d) ℝ) (V : Matrix (Fin d) (Fin k) ℝ) (Λ : Matrix (Fin k) (Fin k) ℝ) (hΛ : Λ.IsSymm) (ell z h : Fin k → ℝ) (n m : Fin d → ℝ) : have e := V.mulVec h - m; (z + h) ⬝ᵥ Λ.mulVec (z + h) + ell ⬝ᵥ (z + h) + V.mulVec (z + h) ⬝ᵥ C.mulVec (V.mulVec (z + h) - (n + m)) = z ⬝ᵥ Λ.mulVec z + ell ⬝ᵥ z + V.mulVec z ⬝ᵥ C.mulVec (V.mulVec z - n) + z ⬝ᵥ quadraticReturnFrequency C V Λ h m + (h ⬝ᵥ Λ.mulVec h + ell ⬝ᵥ h + V.mulVec h ⬝ᵥ C.mulVec e) + e ⬝ᵥ C.mulVec (V.mulVec z - n) - m ⬝ᵥ C.mulVec n

The exact quadratic-lattice phase increment in the Weyl return identity (blueprint lem:weyl, lines 1323–1332), before discarding an integer phase.

theorem TrilinearHT.Auto.fourier_first_moment_lipschitz {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {f : E → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hm : MeasureTheory.Integrable (fun (x : E) => ‖x‖ * ‖f x‖) MeasureTheory.volume) (ξ η : E) : ‖FourierTransform.fourier f ξ - FourierTransform.fourier f η‖ ≤ (2 * Real.pi * ∫ (x : E), ‖x‖ * ‖f x‖) * ‖ξ - η‖

A finite first absolute moment bounds the derivative of the Fourier integral, hence its global Lipschitz constant. Used in lem:weyl, line 1333.

theorem TrilinearHT.Auto.fourier_sub_norm_le_integral {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {f g : E → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (ξ : E) : ‖FourierTransform.fourier f ξ - FourierTransform.fourier g ξ‖ ≤ ∫ (x : E), ‖f x - g x‖

The integral Fourier transform is L1-Lipschitz in its input.

theorem TrilinearHT.Auto.fourier_translate_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (f : E → ℂ) (h ξ : E) : ‖FourierTransform.fourier (fun (x : E) => f (x + h)) ξ‖ = ‖FourierTransform.fourier f ξ‖

Translation of the argument changes only the Fourier phase.

theorem TrilinearHT.Auto.fourier_return_lower {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {f : E → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (h ω ξ : E) (c : ℝ) : ‖FourierTransform.fourier f ξ‖ - ∫ (x : E), ‖f (x + h) - ↑(Real.fourierChar (c + inner ℝ x ω)) * f x‖ ≤ ‖FourierTransform.fourier f (ξ - ω)‖

A translation-modulation error bounds the loss of Fourier magnitude along the corresponding frequency step. Source: lem:weyl, line 1333.

theorem TrilinearHT.Auto.separated_balls_sq_mass {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {g : E → ℂ} (hg : MeasureTheory.Integrable (fun (x : E) => ‖g x‖ ^ 2) μ) (M : ℕ) (p : ℕ → E) {ρ c : ℝ} (hsep : ∀ i < M, ∀ j < M, i ≠ j → 2 * ρ ≤ dist (p i) (p j)) (hc : ∀ j < M, ∀ x ∈ Metric.ball (p j) ρ, c ≤ ‖g x‖) (hc0 : 0 ≤ c) : ↑M * (μ.real (Metric.ball 0 ρ) * c ^ 2) ≤ ∫ (x : E), ‖g x‖ ^ 2 ∂μ

Square mass on separated balls: if a square-integrable function has size at least c on M balls of radius ρ whose centers are 2ρ-separated, then its total square mass is at least M times the ball volume times c². Used in lem:weyl, line 1333.

theorem TrilinearHT.Auto.euclidean_ball_volume_lower {k : ℕ} {ρ : ℝ} (hρ : 0 < ρ) : (2 * (ρ / (↑k + 1))) ^ k ≤ MeasureTheory.volume.real (Metric.ball 0 ρ)

Euclidean balls contain an explicit coordinate cube, giving the volume lower bound (2ρ/(k+1))^k. Used in lem:weyl, line 1333.

theorem TrilinearHT.Auto.fourier_progression_step_small {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {f : E → ℂ} (hf1 : MeasureTheory.Integrable f MeasureTheory.volume) (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) {L δ S : ℝ} (hL : 0 < L) (hδ : 0 < δ) (hLip : ∀ (ξ η : E), ‖FourierTransform.fourier f ξ - FourierTransform.fourier f η‖ ≤ L * ‖ξ - η‖) (hS : ∫ (x : E), ‖f x‖ ^ 2 ≤ S) (M : ℕ) (hM : S < ↑M * (MeasureTheory.volume.real (Metric.ball 0 (min (1 / 2) (δ / (6 * L)))) * (δ / 3) ^ 2)) (ω ξ : E) (hlarge : ∀ j < M, δ / 2 ≤ ‖FourierTransform.fourier f (ξ - j • ω)‖) : ‖ω‖ < 1

The Fourier half of the Weyl alternative: a Lipschitz Fourier transform cannot stay large on M points of a progression with step of size at least one, once M balls of the explicit radius exceed the Plancherel mass. Source: lem:weyl, line 1333.

instance TrilinearHT.Auto.euclideanDualLattice_span_discrete {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) : DiscreteTopology ↥(euclideanDualLattice (Submodule.span ℤ (Set.range ⇑b)))

instance TrilinearHT.Auto.euclideanDualLattice_span_isZLattice {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) : IsZLattice ℝ (euclideanDualLattice (Submodule.span ℤ (Set.range ⇑b)))

theorem TrilinearHT.Auto.successiveMinimum_attained_fullLattice {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hK : IsSymmetricConvexBody K) (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {j : ℕ} (hj : 0 < j) (hjn : j ≤ Module.finrank ℝ E) : 0 < successiveMinimum K L j ∧ ∃ (w : Fin j → E), IndependentLatticeTuple L w ∧ ∀ (i : Fin j), w i ∈ successiveMinimum K L j • K

Basis-free version of attainment for every full lattice.

def TrilinearHT.Auto.euclideanCoordinateCube (d : ℕ) : Set (EuclideanSpace ℝ (Fin d))

Coordinate cube with every Euclidean coordinate between minus one and one.

Equations

• TrilinearHT.Auto.euclideanCoordinateCube d = WithLp.toLp 2 '' Set.Icc (fun (x : Fin d) => -1) fun (x : Fin d) => 1

theorem TrilinearHT.Auto.mem_euclideanCoordinateCube {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) : x ∈ euclideanCoordinateCube d ↔ ∀ (i : Fin d), |x.ofLp i| ≤ 1

theorem TrilinearHT.Auto.euclideanCoordinateCube_compact (d : ℕ) : IsCompact (euclideanCoordinateCube d)

theorem TrilinearHT.Auto.euclideanCoordinateCube_convex (d : ℕ) : Convex ℝ (euclideanCoordinateCube d)

theorem TrilinearHT.Auto.euclideanCoordinateCube_zero (d : ℕ) : 0 ∈ euclideanCoordinateCube d

theorem TrilinearHT.Auto.euclideanCoordinateCube_neg {d : ℕ} {x : EuclideanSpace ℝ (Fin d)} (hx : x ∈ euclideanCoordinateCube d) : -x ∈ euclideanCoordinateCube d

theorem TrilinearHT.Auto.euclideanCoordinateCube_zero_interior (d : ℕ) : 0 ∈ interior (euclideanCoordinateCube d)

noncomputable def TrilinearHT.Auto.shortReturnBody {d k : ℕ} (V : EuclideanSpace ℝ (Fin k) →L[ℝ] EuclideanSpace ℝ (Fin d)) (P : ℝ) : Set (EuclideanSpace ℝ (Fin d))

Minkowski sum of the scaled image cube and the ambient coordinate cube.

Equations

• TrilinearHT.Auto.shortReturnBody V P = ⇑(P⁻¹ • V) '' TrilinearHT.Auto.euclideanCoordinateCube k + TrilinearHT.Auto.euclideanCoordinateCube d

theorem TrilinearHT.Auto.shortReturnBody_cube_subset {d k : ℕ} (V : EuclideanSpace ℝ (Fin k) →L[ℝ] EuclideanSpace ℝ (Fin d)) (P : ℝ) : euclideanCoordinateCube d ⊆ shortReturnBody V P

theorem TrilinearHT.Auto.shortReturnBody_symmetricConvexBody {d k : ℕ} (V : EuclideanSpace ℝ (Fin k) →L[ℝ] EuclideanSpace ℝ (Fin d)) (P : ℝ) : IsSymmetricConvexBody (shortReturnBody V P)

Blueprint lem:return-splitting, lines 1271-1275: the sum of the image of the coordinate cube and the ambient coordinate cube is a symmetric compact convex body with the origin in its interior.

theorem TrilinearHT.Auto.mem_shortReturnBody {d k : ℕ} (V : EuclideanSpace ℝ (Fin k) →L[ℝ] EuclideanSpace ℝ (Fin d)) (P : ℝ) (x : EuclideanSpace ℝ (Fin d)) : x ∈ shortReturnBody V P ↔ ∃ (h : EuclideanSpace ℝ (Fin k)) (w : EuclideanSpace ℝ (Fin d)), (∀ (j : Fin k), |h.ofLp j| ≤ 1) ∧ (∀ (i : Fin d), |w.ofLp i| ≤ 1) ∧ P⁻¹ • V h + w = x

theorem TrilinearHT.Auto.finite_list_interval_gap {d : ℕ} (x : Fin d → ℝ) (b : ℕ → ℝ) (hb : Antitone b) : ∃ (j : Fin (d + 1)), ∀ (i : Fin d), x i ∉ Set.Ioc (b (↑j + 1)) (b ↑j)

theorem TrilinearHT.Auto.geometric_interval_gap {d : ℕ} (x : Fin d → ℝ) {B L : ℝ} (hB : 0 < B) (hL : 1 < L) : ∃ (b : ℝ), 0 < b ∧ b ≤ B ∧ b⁻¹ ≤ B⁻¹ * L ^ (d + 1) ∧ ∀ (i : Fin d), x i ≤ b ∨ L * b < x i

theorem TrilinearHT.Auto.successiveMinimum_geometric_gap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : Set E) (Λ : Submodule ℤ E) (d : ℕ) {B L : ℝ} (hB : 0 < B) (hL : 1 < L) : ∃ (b : ℝ), 0 < b ∧ b ≤ B ∧ b⁻¹ ≤ B⁻¹ * L ^ (d + 1) ∧ ∀ (j : ℕ), 0 < j → j ≤ d → successiveMinimum K Λ j ≤ b ∨ L * b < successiveMinimum K Λ j

Blueprint lem:return-splitting, lines 1275-1279: one geometric interval avoids all successive minima up to index d, with a controlled reciprocal scale.

theorem TrilinearHT.Auto.mem_smul_shortReturnBody_representation {d k : ℕ} (V : EuclideanSpace ℝ (Fin k) →L[ℝ] EuclideanSpace ℝ (Fin d)) (P : ℝ) {s : ℝ} (hs : 0 ≤ s) {x : EuclideanSpace ℝ (Fin d)} (hx : x ∈ s • shortReturnBody V P) : ∃ (h : EuclideanSpace ℝ (Fin k)) (w : EuclideanSpace ℝ (Fin d)), (∀ (j : Fin k), |h.ofLp j| ≤ s) ∧ (∀ (i : Fin d), |w.ofLp i| ≤ s) ∧ P⁻¹ • V h + w = x

theorem TrilinearHT.Auto.euclidean_norm_le_coordinate_bound {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) {s : ℝ} (hx : ∀ (i : Fin d), |x.ofLp i| ≤ s) : ‖x‖ ≤ ↑d * s

theorem TrilinearHT.Auto.scaled_shortReturnBody_gives_return {d k : ℕ} (V : EuclideanSpace ℝ (Fin k) →L[ℝ] EuclideanSpace ℝ (Fin d)) {P s : ℝ} (hP : 0 < P) (hs : 0 ≤ s) {x : EuclideanSpace ℝ (Fin d)} (hx : x ∈ s • shortReturnBody V P) : ∃ (h : EuclideanSpace ℝ (Fin k)), ‖h‖ + ‖V h - P • x‖ ≤ (↑k + P * ↑d) * s

noncomputable def TrilinearHT.Auto.coordinateIntegerLattice (d : ℕ) : Submodule ℤ (EuclideanSpace ℝ (Fin d))

Integer span of the standard Euclidean coordinate basis.

Equations

• TrilinearHT.Auto.coordinateIntegerLattice d = Submodule.span ℤ (Set.range ⇑(EuclideanSpace.basisFun (Fin d) ℝ).toBasis)

theorem TrilinearHT.Auto.mem_coordinateIntegerLattice {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) : x ∈ coordinateIntegerLattice d ↔ ∀ (i : Fin d), ∃ (n : ℤ), ↑n = x.ofLp i

theorem TrilinearHT.Auto.coordinateIntegerLattice_coordinates {d : ℕ} {x : EuclideanSpace ℝ (Fin d)} (hx : x ∈ coordinateIntegerLattice d) : ∃ (n : Fin d → ℤ), x = WithLp.toLp 2 fun (i : Fin d) => ↑(n i)

theorem TrilinearHT.Auto.bilinear_vanishes_on_span {E : Type u_1} [AddCommGroup E] [Module ℝ E] (B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (S : Set E) (hB : ∀ x ∈ S, ∀ y ∈ S, (B x) y = 0) (x : E) : x ∈ Submodule.span ℝ S → ∀ y ∈ Submodule.span ℝ S, (B x) y = 0

noncomputable def TrilinearHT.Auto.shortReturnLatticeSpan {d k : ℕ} (V : EuclideanSpace ℝ (Fin k) →L[ℝ] EuclideanSpace ℝ (Fin d)) (P s : ℝ) : Submodule ℝ (EuclideanSpace ℝ (Fin d))

Real span of integer lattice points inside the scaled short-return body.

Equations

• TrilinearHT.Auto.shortReturnLatticeSpan V P s = Submodule.span ℝ (↑(TrilinearHT.Auto.coordinateIntegerLattice d) ∩ s • TrilinearHT.Auto.shortReturnBody V P)

theorem TrilinearHT.Auto.shortReturnLatticeSpan_isotropic_of_returns {d k : ℕ} (V : EuclideanSpace ℝ (Fin k) →L[ℝ] EuclideanSpace ℝ (Fin d)) (B : EuclideanSpace ℝ (Fin d) →ₗ[ℝ] EuclideanSpace ℝ (Fin d) →ₗ[ℝ] ℝ) {P s r : ℝ} (hP : 0 < P) (hs : 0 ≤ s) (hscale : (↑k + P * ↑d) * s ≤ r) (hiso : ∀ (h h' : EuclideanSpace ℝ (Fin k)) (n n' : Fin d → ℤ), ‖h‖ + ‖V h - P • WithLp.toLp 2 fun (i : Fin d) => ↑(n i)‖ ≤ r → ‖h'‖ + ‖V h' - P • WithLp.toLp 2 fun (i : Fin d) => ↑(n' i)‖ ≤ r → (B (P • WithLp.toLp 2 fun (i : Fin d) => ↑(n i))) (P • WithLp.toLp 2 fun (i : Fin d) => ↑(n' i)) = 0) (x : EuclideanSpace ℝ (Fin d)) : x ∈ shortReturnLatticeSpan V P s → ∀ y ∈ shortReturnLatticeSpan V P s, (B x) y = 0

theorem TrilinearHT.Auto.shortReturn_scale_bound (d k : ℕ) {P s r : ℝ} (hP : 1 ≤ P) (hs : 0 ≤ s) (hb : s ≤ r / (100 * P * (↑d + ↑k + 1))) : (↑k + P * ↑d) * s ≤ r

theorem TrilinearHT.Auto.shortReturnLatticeSpan_isotropic {d k : ℕ} (C : Matrix (Fin d) (Fin d) ℝ) (V : Matrix (Fin d) (Fin k) ℝ) (Λ : Matrix (Fin k) (Fin k) ℝ) (hΛ : Λ.IsSymm) (P : ℤ) (hP : 1 ≤ P) (hC : ∀ (i j : Fin d), ∃ (z : ℤ), ↑P * C i j = ↑z) {a M s : ℝ} (ha : 0 < a) (hM : 0 ≤ M) (hs : 0 ≤ s) (hΩ : ∀ (h : Fin k → ℝ) (n : Fin d → ℤ), ‖WithLp.toLp 2 h‖ + ‖WithLp.toLp 2 (V.mulVec h - fun (i : Fin d) => ↑P * ↑(n i))‖ ≤ a → ‖WithLp.toLp 2 ((2 • Λ + V.transpose * C * V).mulVec h - (V.transpose * (C - C.transpose)).mulVec fun (i : Fin d) => ↑P * ↑(n i))‖ ≤ M) : have r := min a (100 * (M + ‖LinearMap.toContinuousLinearMap (Matrix.toEuclideanLin (C - C.transpose))‖ + 1))⁻¹; s ≤ r / (100 * ↑P * (↑d + ↑k + 1)) → ∀ x ∈ shortReturnLatticeSpan (LinearMap.toContinuousLinearMap (Matrix.toEuclideanLin V)) (↑P) s, ∀ y ∈ shortReturnLatticeSpan (LinearMap.toContinuousLinearMap (Matrix.toEuclideanLin V)) (↑P) s, y.ofLp ⬝ᵥ (C - C.transpose).mulVec x.ofLp = 0

Blueprint lem:return-splitting, lines 1279-1281: the real span of the integer points in the chosen return body is isotropic for C-C^T.

noncomputable def TrilinearHT.Auto.latticeBodySpan {E : Type u_1} [AddCommGroup E] [Module ℝ E] (K : Set E) (L : Submodule ℤ E) (b : ℝ) : Submodule ℝ E

Real span of lattice points in the dilation b • K.

Equations

• TrilinearHT.Auto.latticeBodySpan K L b = Submodule.span ℝ (↑L ∩ b • K)

theorem TrilinearHT.Auto.latticeBodySpan_successiveMinimum_gt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hK : IsSymmetricConvexBody K) (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {b : ℝ} (hb : 0 < b) (hr : Module.finrank ℝ ↥(latticeBodySpan K L b) < Module.finrank ℝ E) : b < successiveMinimum K L (Module.finrank ℝ ↥(latticeBodySpan K L b) + 1)

theorem TrilinearHT.Auto.latticeBodySpan_rank_gap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hK : IsSymmetricConvexBody K) (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {b A : ℝ} (hb : 0 < b) (hgap : ∀ (j : ℕ), 0 < j → j ≤ Module.finrank ℝ E → successiveMinimum K L j ≤ b ∨ A * b < successiveMinimum K L j) (hr : Module.finrank ℝ ↥(latticeBodySpan K L b) < Module.finrank ℝ E) : A * b < successiveMinimum K L (Module.finrank ℝ ↥(latticeBodySpan K L b) + 1)

theorem TrilinearHT.Auto.short_dual_vector_mem_orthogonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : Set E) (L : Submodule ℤ E) {b t : ℝ} (hb : 0 ≤ b) (ht : 0 ≤ t) (hbt : b * t < 1) {q : E} (hq : q ∈ euclideanDualLattice L) (hqt : q ∈ t • euclideanPolar K) : q ∈ (latticeBodySpan K L b)ᗮ

theorem TrilinearHT.Auto.latticeBodySpan_small_dual_basis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hK : IsSymmetricConvexBody K) {n : ℕ} (v : Module.Basis (Fin n) ℝ E) {b C A : ℝ} (hb : 0 < b) (hC : ↑n * 16 ^ n ≤ C) (hCA : C < A) (hgap : ∀ (j : ℕ), 0 < j → j ≤ n → successiveMinimum K (Submodule.span ℤ (Set.range ⇑v)) j ≤ b ∨ A * b < successiveMinimum K (Submodule.span ℤ (Set.range ⇑v)) j) (hr : Module.finrank ℝ ↥(latticeBodySpan K (Submodule.span ℤ (Set.range ⇑v)) b) < n) : have U := latticeBodySpan K (Submodule.span ℤ (Set.range ⇑v)) b; ∃ (q : Fin (n - Module.finrank ℝ ↥U) → E), LinearIndependent ℝ q ∧ (∀ (i : Fin (n - Module.finrank ℝ ↥U)), q i ∈ euclideanDualLattice (Submodule.span ℤ (Set.range ⇑v))) ∧ (∀ (i : Fin (n - Module.finrank ℝ ↥U)), q i ∈ (C / (A * b)) • euclideanPolar K) ∧ Submodule.span ℝ (Set.range q) = Uᗮ

A gap in the primal minima produces a short dual basis for the orthogonal complement of the span of the small primal lattice points.

theorem TrilinearHT.Auto.coordinateIntegerLattice_dual (d : ℕ) : euclideanDualLattice (coordinateIntegerLattice d) = coordinateIntegerLattice d

theorem TrilinearHT.Auto.shortReturnLatticeSpan_dual_basis {d k : ℕ} (V : EuclideanSpace ℝ (Fin k) →L[ℝ] EuclideanSpace ℝ (Fin d)) (P : ℝ) {b : ℝ} (hb : 0 < b) (hgap : ∀ (j : ℕ), 0 < j → j ≤ d → successiveMinimum (shortReturnBody V P) (coordinateIntegerLattice d) j ≤ b ∨ 16 * (100 * ↑d) ^ (10 * d) * b < successiveMinimum (shortReturnBody V P) (coordinateIntegerLattice d) j) (hr : Module.finrank ℝ ↥(shortReturnLatticeSpan V P b) < d) : ∃ (q : Fin (d - Module.finrank ℝ ↥(shortReturnLatticeSpan V P b)) → EuclideanSpace ℝ (Fin d)), LinearIndependent ℝ q ∧ (∀ (i : Fin (d - Module.finrank ℝ ↥(shortReturnLatticeSpan V P b))), q i ∈ coordinateIntegerLattice d) ∧ (∀ (i : Fin (d - Module.finrank ℝ ↥(shortReturnLatticeSpan V P b))), q i ∈ ((100 * ↑d) ^ (10 * d) / (16 * (100 * ↑d) ^ (10 * d) * b)) • euclideanPolar (shortReturnBody V P)) ∧ Submodule.span ℝ (Set.range q) = (shortReturnLatticeSpan V P b)ᗮ

The short dual vectors in the return-splitting proof span precisely the orthogonal complement of the short-return subspace.

theorem TrilinearHT.Auto.euclideanCoordinateCube_basis_mem {d : ℕ} (i : Fin d) : (EuclideanSpace.basisFun (Fin d) ℝ) i ∈ euclideanCoordinateCube d

theorem TrilinearHT.Auto.shortReturnBody_scaled_image_mem {d k : ℕ} (V : EuclideanSpace ℝ (Fin k) →L[ℝ] EuclideanSpace ℝ (Fin d)) (P : ℝ) {h : EuclideanSpace ℝ (Fin k)} (hh : h ∈ euclideanCoordinateCube k) : P⁻¹ • V h ∈ shortReturnBody V P

theorem TrilinearHT.Auto.shortReturnBody_polar_coordinates {d k : ℕ} (V : EuclideanSpace ℝ (Fin k) →L[ℝ] EuclideanSpace ℝ (Fin d)) {P t : ℝ} (hP : 0 < P) (ht : 0 ≤ t) {q : EuclideanSpace ℝ (Fin d)} (hq : q ∈ t • euclideanPolar (shortReturnBody V P)) : (∀ (i : Fin d), |q.ofLp i| ≤ t) ∧ ∀ (j : Fin k), |inner ℝ q (V ((EuclideanSpace.basisFun (Fin k) ℝ) j))| ≤ P * t

theorem TrilinearHT.Auto.finite_torus_close_pair {d N : ℕ} (hN : 0 < N) (x : Fin (N ^ d + 1) → Fin d → ℝ) : ∃ (i : Fin (N ^ d + 1)) (j : Fin (N ^ d + 1)), i < j ∧ ∀ (l : Fin d), |Int.fract (x j l) - Int.fract (x i l)| ≤ 1 / ↑N

Finite torus pigeonholing with an explicit cubical grid.

theorem TrilinearHT.Auto.finite_grid_line_return {d N : ℕ} (hN : 0 < N) (v : Fin d → ℝ) {b : ℝ} (hb : 0 < b) : ∃ (t : ℝ) (n : Fin d → ℤ), b / ↑N ^ d ≤ t ∧ t ≤ b ∧ ∀ (l : Fin d), |t * v l - ↑(n l)| ≤ 1 / ↑N

theorem TrilinearHT.Auto.small_line_lattice_return {d : ℕ} (v : Fin d → ℝ) {b : ℝ} (hb : 0 < b) : ∃ (M : ℕ) (t : ℝ) (n : Fin d → ℤ), 0 < M ∧ ↑M ≤ (1 + 4 / b) ^ d ∧ b / ↑M ≤ t ∧ t ≤ b ∧ ∀ (l : Fin d), |t * v l - ↑(n l)| ≤ b / 4

theorem TrilinearHT.Auto.mem_smul_shortReturnBody_of_representation {d k : ℕ} (V : EuclideanSpace ℝ (Fin k) →L[ℝ] EuclideanSpace ℝ (Fin d)) (P : ℝ) {b : ℝ} (hb : 0 < b) {x : EuclideanSpace ℝ (Fin d)} (h : EuclideanSpace ℝ (Fin k)) (w : EuclideanSpace ℝ (Fin d)) (hh : ∀ (j : Fin k), |h.ofLp j| ≤ b) (hw : ∀ (i : Fin d), |w.ofLp i| ≤ b) (he : P⁻¹ • V h + w = x) : x ∈ b • shortReturnBody V P

theorem TrilinearHT.Auto.shortReturnBody_coordinate_return {d k : ℕ} (V : EuclideanSpace ℝ (Fin k) →L[ℝ] EuclideanSpace ℝ (Fin d)) {P b : ℝ} (hP : 0 < P) (hb : 0 < b) (j : Fin k) : ∃ (M : ℕ) (t : ℝ) (n : Fin d → ℤ), 0 < M ∧ ↑M ≤ (1 + 4 / b) ^ d ∧ b / ↑M ≤ t ∧ t ≤ b ∧ (WithLp.toLp 2 fun (i : Fin d) => ↑(n i)) ∈ b • shortReturnBody V P ∧ (P • WithLp.toLp 2 fun (i : Fin d) => ↑(n i)) ∈ shortReturnLatticeSpan V P b ∧ (∀ (i : Fin d), |(V (t • (EuclideanSpace.basisFun (Fin k) ℝ) j) - P • WithLp.toLp 2 fun (i : Fin d) => ↑(n i)).ofLp i| ≤ P * b / 4) ∧ ‖t • (EuclideanSpace.basisFun (Fin k) ℝ) j‖ + ‖V (t • (EuclideanSpace.basisFun (Fin k) ℝ) j) - P • WithLp.toLp 2 fun (i : Fin d) => ↑(n i)‖ ≤ (1 + P * ↑d) * b

Quantitative returns along every coordinate axis, with the returning integer vector in the short-return span.

theorem TrilinearHT.Auto.shortReturnLatticeSpan_dual_coordinates {d k : ℕ} (V : EuclideanSpace ℝ (Fin k) →L[ℝ] EuclideanSpace ℝ (Fin d)) {P b : ℝ} (hP : 0 < P) (hb : 0 < b) (hgap : ∀ (j : ℕ), 0 < j → j ≤ d → successiveMinimum (shortReturnBody V P) (coordinateIntegerLattice d) j ≤ b ∨ 16 * (100 * ↑d) ^ (10 * d) * b < successiveMinimum (shortReturnBody V P) (coordinateIntegerLattice d) j) : ∃ r ≤ d, ∃ (q : Fin r → EuclideanSpace ℝ (Fin d)), LinearIndependent ℝ q ∧ (∀ (i : Fin r), q i ∈ coordinateIntegerLattice d) ∧ (∀ (i : Fin r) (j : Fin d), |(q i).ofLp j| ≤ b⁻¹) ∧ (∀ (i : Fin r) (j : Fin k), |inner ℝ (q i) (V ((EuclideanSpace.basisFun (Fin k) ℝ) j))| ≤ P * b⁻¹) ∧ Submodule.span ℝ (Set.range q) = (shortReturnLatticeSpan V P b)ᗮ

Integer generators of the orthogonal complement of the short-return span, including the full-rank case. Coordinate and velocity-pairing bounds depend only on the reciprocal return scale.

theorem TrilinearHT.Auto.shortReturnSplittingBudget_quasipolynomial : QuasipolynomialBound shortReturnSplittingBudget

theorem TrilinearHT.Auto.shortReturnRowBudget_two_le {t : ℝ} (ht : 2 ≤ t) : 2 ≤ shortReturnRowBudget t

theorem TrilinearHT.Auto.shortReturnGramBudget_two_le {t : ℝ} (ht : 2 ≤ t) : 2 ≤ shortReturnGramBudget t

theorem TrilinearHT.Auto.shortReturnSlowBudget_two_le {t : ℝ} (ht : 2 ≤ t) : 2 ≤ shortReturnSlowBudget t

theorem TrilinearHT.Auto.shortReturnRadius_reciprocal_bound {t a M N : ℝ} (ht : 2 ≤ t) (ha : 0 < a) (hM0 : 0 ≤ M) (hN0 : 0 ≤ N) (haT : a⁻¹ ≤ t) (hM : M ≤ t) (hN : N ≤ shortReturnAlternatingBudget t) : have r := min a (100 * (M + N + 1))⁻¹; 0 < r ∧ r ≤ a ∧ r⁻¹ ≤ shortReturnRadiusBudget t

theorem TrilinearHT.Auto.shortReturnInitialScale_reciprocal_bound {t P r : ℝ} (ht : 2 ≤ t) (hP : 0 < P) (hr : 0 < r) (hPt : P ≤ t) (hrT : r⁻¹ ≤ shortReturnRadiusBudget t) {d k : ℕ} (hd : ↑d ≤ logarithmicSize t) (hk : k ≤ 3) : have b := min (1 / 100) (r / (100 * P * (↑d + ↑k + 1))); 0 < b ∧ b⁻¹ ≤ shortReturnInitialScaleBudget t

theorem TrilinearHT.Auto.shortReturnGapBudget_one_le {t : ℝ} (ht : 2 ≤ t) : 1 ≤ shortReturnGapBudget t

theorem TrilinearHT.Auto.shortReturnGapBudget_bound {t : ℝ} (ht : 2 ≤ t) {d : ℕ} (hd : ↑d ≤ logarithmicSize t) : 16 * (100 * ↑d) ^ (10 * d) ≤ shortReturnGapBudget t

theorem TrilinearHT.Auto.shortReturnScale_reciprocal_bound {t c g b : ℝ} (ht : 2 ≤ t) (hg0 : 0 ≤ g) {d : ℕ} (hd : ↑d ≤ logarithmicSize t) (hcT : c⁻¹ ≤ shortReturnInitialScaleBudget t) (hgT : g ≤ shortReturnGapBudget t) (hb : b⁻¹ ≤ c⁻¹ * g ^ (d + 1)) : b⁻¹ ≤ shortReturnScaleBudget t

theorem TrilinearHT.Auto.shortReturnProjectionBudget_bound {t B : ℝ} (ht : 2 ≤ t) (hB : 2 ≤ B) (hBT : B ≤ shortReturnRowBudget t) {d : ℕ} (hd : ↑d ≤ logarithmicSize t) : Real.exp (8 * (↑d + 1) ^ 4 * Real.log (2 * B)) ≤ shortReturnProjectionBudget t

theorem TrilinearHT.Auto.shortReturnGramBudget_bound {t : ℝ} (ht : 2 ≤ t) {d : ℕ} (hd : ↑d ≤ logarithmicSize t) : max 2 (↑d * shortReturnRowBudget t ^ 2) ≤ shortReturnGramBudget t

theorem TrilinearHT.Auto.shortReturnGram_exponential_bound {t : ℝ} (ht : 2 ≤ t) {r d : ℕ} (hr : r ≤ d) (hd : ↑d ≤ logarithmicSize t) : Real.exp (2 * (↑r + 1) ^ 4 * Real.log (2 * max 2 (↑d * shortReturnRowBudget t ^ 2))) ≤ (2 * shortReturnGramBudget t) ^ (2 * (logarithmicSize t + 1) ^ 4)

theorem TrilinearHT.Auto.shortReturnSlowBudget_bound {t : ℝ} (ht : 2 ≤ t) {r d k : ℕ} (hr : r ≤ d) (hd : ↑d ≤ logarithmicSize t) (hk : k ≤ 3) : ↑d * ↑r * shortReturnRowBudget t * (↑r * ↑r * Real.exp (2 * (↑r + 1) ^ 4 * Real.log (2 * max 2 (↑d * shortReturnRowBudget t ^ 2))) * (↑r * ↑k * (t * shortReturnRowBudget t))) ≤ shortReturnSlowBudget t

theorem TrilinearHT.Auto.shortReturnTimeInverseBudget_bound {t b : ℝ} (ht : 2 ≤ t) (hb : 0 < b) (hbT : b⁻¹ ≤ shortReturnScaleBudget t) {d : ℕ} (hd : ↑d ≤ logarithmicSize t) : (1 + 4 / b) ^ d / b ≤ shortReturnTimeInverseBudget t

theorem TrilinearHT.Auto.shortReturnQuadraticBudget_bound {t a M s : ℝ} (ht : 2 ≤ t) (ha : 0 ≤ a) (ha1 : a ≤ 1) (hM : 0 ≤ M) (hMt : M ≤ t) (hs : 0 < s) (hsT : s⁻¹ ≤ shortReturnTimeInverseBudget t) {d k : ℕ} (hd : ↑d ≤ logarithmicSize t) (hk : k ≤ 3) : ↑k * ↑k * ((M + ↑k * ↑d * shortReturnSlowBudget t * (shortReturnAlternatingBudget t * (shortReturnSlowBudget t * a)) + ↑k * ↑d * shortReturnSlowBudget t * (shortReturnAlternatingBudget t * a)) / s) ≤ shortReturnQuadraticBudget t

theorem TrilinearHT.Auto.shortReturnSplittingBudget_dominates {t : ℝ} (ht : 2 ≤ t) : shortReturnProjectionBudget t ≤ shortReturnSplittingBudget t ∧ shortReturnSlowBudget t ≤ shortReturnSplittingBudget t ∧ shortReturnQuadraticBudget t ≤ shortReturnSplittingBudget t

theorem TrilinearHT.Auto.shortReturnParameter_product_bounds {H P a M : ℝ} (hH : 2 ≤ H) (hP : 1 ≤ P) (ha : 0 < a) (ha1 : a ≤ 1) (hM : 1 ≤ M) : have t := H * P * a⁻¹ * M; 2 ≤ t ∧ H ≤ t ∧ P ≤ t ∧ a⁻¹ ≤ t ∧ M ≤ t ∧ logarithmicSize t = 1 + Real.log H + Real.log P + Real.log (1 / a) + Real.log M

theorem TrilinearHT.Auto.shortReturnSplittingBudget_uniform : ∃ (D : ℕ), 1 ≤ D ∧ ∀ (H P a M : ℝ), 2 ≤ H → 1 ≤ P → 0 < a → a ≤ 1 → 1 ≤ M → shortReturnSplittingBudget (H * P * a⁻¹ * M) ≤ Real.exp (↑D * (1 + Real.log H + Real.log P + Real.log (1 / a) + Real.log M) ^ D)

theorem TrilinearHT.Auto.chartMatrixPhase_eq_dotProduct {d : ℕ} (C : Matrix (Fin d) (Fin d) ℚ) (u w : Fin d → ℝ) : chartMatrixPhase C u w = u ⬝ᵥ (C.map fun (q : ℚ) => ↑q).mulVec w

Bilinear matrix phase in dot-product notation.

noncomputable def TrilinearHT.Auto.multivariableChartPhase {k d : ℕ} (A : MultivariableQuadraticChartData k d) (z : Fin k → ℝ) (n : Fin d → ℤ) : ℝ

The complete phase of one lattice summand of a several-variable chart.

Equations

• One or more equations did not get rendered due to their size.

theorem TrilinearHT.Auto.multivariableQuadraticChartAtom_eq_tsum {k d : ℕ} (A : MultivariableQuadraticChartData k d) (z : Fin k → ℝ) : multivariableQuadraticChartAtom A z = ∑' (n : Fin d → ℤ), A.amplitude (A.horizontal.mulVec z - fun (i : Fin d) => ↑(n i)) * ↑(Real.fourierChar (multivariableChartPhase A z n))

theorem TrilinearHT.Auto.multivariableQuadraticChart_return_identity {k d : ℕ} (A : MultivariableQuadraticChartData k d) (z h : Fin k → ℝ) (m : Fin d → ℤ) (hint : ∀ (i j : Fin d), ∃ (q : ℤ), ↑q = ↑(m i) * ↑(A.matrix i j)) : have e := A.horizontal.mulVec h - fun (i : Fin d) => ↑(m i); have C := A.matrix.map fun (q : ℚ) => ↑q; have ω := (2 • A.quadratic + A.horizontal.transpose * C * A.horizontal).mulVec h - (A.horizontal.transpose * (C - C.transpose)).mulVec fun (i : Fin d) => ↑(m i); have c := h ⬝ᵥ A.quadratic.mulVec h + A.linear ⬝ᵥ h + chartMatrixPhase A.matrix (A.horizontal.mulVec h) e; multivariableQuadraticChartAtom A (z + h) = ↑(Real.fourierChar (c + z ⬝ᵥ ω)) * ∑' (n : Fin d → ℤ), A.amplitude ((A.horizontal.mulVec z - fun (i : Fin d) => ↑(n i)) + e) * ↑(Real.fourierChar (chartMatrixPhase A.matrix e (A.horizontal.mulVec z - fun (i : Fin d) => ↑(n i)))) * ↑(Real.fourierChar (multivariableChartPhase A z n))

Exact reindexing and modulation for a chart return. The residual amplitude is shifted only by the return defect; its phase involves that defect rather than the unrestricted horizontal velocity. Source: lem:weyl, lines 1321–1331.

theorem TrilinearHT.Auto.chart_integer_period_coefficients {d : ℕ} (C : Matrix (Fin d) (Fin d) ℚ) (P : ℤ) (hPC : ∀ (i j : Fin d), ∃ (z : ℤ), ↑P * C i j = ↑z) (n : Fin d → ℤ) (i j : Fin d) : ∃ (z : ℤ), ↑z = ↑(P * n i) * ↑(C i j)

A clearing period makes every lattice return eligible for exact reindexing.

theorem TrilinearHT.Auto.chart_fourierChar_sub_one_norm_le (x : ℝ) : ‖↑(Real.fourierChar x) - 1‖ ≤ 2 * Real.pi * |x|

theorem TrilinearHT.Auto.multivariableChart_amplitude_difference {k d c₀ : ℕ} {H : ℝ} {A : MultivariableQuadraticChartData k d} (hA : MultivariableQuadraticChartComplexity c₀ H A) (hc : 1 ≤ c₀) (x y : Fin d → ℝ) : ‖A.amplitude y - A.amplitude x‖ ≤ H ^ (4 * c₀) * 2 ^ (2 * c₀) * ‖y - x‖

A global first-derivative estimate for the actual chart cutoff.

theorem TrilinearHT.Auto.chart_modulated_amplitude_error {d : ℕ} (C : Matrix (Fin d) (Fin d) ℚ) (χ : (Fin d → ℝ) → ℂ) {B K L R : ℝ} (hB : 0 ≤ B) (hK : 0 ≤ K) (hR : 0 ≤ R) (hC : ∀ (i j : Fin d), |↑(C i j)| ≤ B) (hχ : ∀ (w : Fin d → ℝ), ‖χ w‖ ≤ K) (hsupp : ∀ (w : Fin d → ℝ), χ w ≠ 0 → ‖w‖ ≤ R) (hLip : ∀ (x y : Fin d → ℝ), ‖χ y - χ x‖ ≤ L * ‖y - x‖) (w e : Fin d → ℝ) : ‖χ (w + e) * ↑(Real.fourierChar (chartMatrixPhase C e w)) - χ w‖ ≤ (L + K * (2 * Real.pi * ↑d ^ 2 * B * R)) * ‖e‖

Shifting a compact amplitude and multiplying by the small defect phase costs linearly in the defect, uniformly in the horizontal location.

theorem TrilinearHT.Auto.chart_lattice_modulation_error {d : ℕ} (C : Matrix (Fin d) (Fin d) ℚ) (χ : (Fin d → ℝ) → ℂ) {B K L R : ℝ} (hB : 0 ≤ B) (hK : 0 ≤ K) (hL : 0 ≤ L) (hR : 0 ≤ R) (hC : ∀ (i j : Fin d), |↑(C i j)| ≤ B) (hχ : ∀ (w : Fin d → ℝ), ‖χ w‖ ≤ K) (hsupp : ∀ (w : Fin d → ℝ), χ w ≠ 0 → ∀ (i : Fin d), |w i| ≤ R) (hLip : ∀ (x y : Fin d → ℝ), ‖χ y - χ x‖ ≤ L * ‖y - x‖) (u e : Fin d → ℝ) (φ : (Fin d → ℤ) → ℂ) (hφ : ∀ (n : Fin d → ℤ), ‖φ n‖ ≤ 1) : ‖∑' (n : Fin d → ℤ), χ ((u - fun (i : Fin d) => ↑(n i)) + e) * ↑(Real.fourierChar (chartMatrixPhase C e (u - fun (i : Fin d) => ↑(n i)))) * φ n - ∑' (n : Fin d → ℤ), χ (u - fun (i : Fin d) => ↑(n i)) * φ n‖ ≤ 2 * (2 * R + 3) ^ d * (L + K * (2 * Real.pi * ↑d ^ 2 * B * R)) * ‖e‖

A lattice sum inherits the defect estimate with only the uniform number of terms meeting the original or shifted amplitude support.

theorem TrilinearHT.Auto.multivariableQuadraticChart_norm_le {k d c₀ : ℕ} {H : ℝ} {A : MultivariableQuadraticChartData k d} (hA : MultivariableQuadraticChartComplexity c₀ H A) (z : Fin k → ℝ) : ‖multivariableQuadraticChartAtom A z‖ ≤ (2 * H + 3) ^ d * H ^ c₀

theorem TrilinearHT.Auto.multivariableQuadraticChart_return_error {k d c₀ : ℕ} {H : ℝ} {A : MultivariableQuadraticChartData k d} (hA : MultivariableQuadraticChartComplexity c₀ H A) (hc : 1 ≤ c₀) (z h : Fin k → ℝ) (m : Fin d → ℤ) (hint : ∀ (i j : Fin d), ∃ (q : ℤ), ↑q = ↑(m i) * ↑(A.matrix i j)) : have e := A.horizontal.mulVec h - fun (i : Fin d) => ↑(m i); have C := A.matrix.map fun (q : ℚ) => ↑q; have ω := (2 • A.quadratic + A.horizontal.transpose * C * A.horizontal).mulVec h - (A.horizontal.transpose * (C - C.transpose)).mulVec fun (i : Fin d) => ↑(m i); have c := h ⬝ᵥ A.quadratic.mulVec h + A.linear ⬝ᵥ h + chartMatrixPhase A.matrix (A.horizontal.mulVec h) e; ‖multivariableQuadraticChartAtom A (z + h) - ↑(Real.fourierChar (c + z ⬝ᵥ ω)) * multivariableQuadraticChartAtom A z‖ ≤ 2 * (2 * H + 3) ^ d * (H ^ (4 * c₀) * 2 ^ (2 * c₀) + H ^ c₀ * (2 * Real.pi * ↑d ^ 2 * H * H)) * ‖e‖

The return error for the actual several-variable atom is uniform in the horizontal and ordinary quadratic parameters. Source: eq:return.

theorem TrilinearHT.Auto.multivariableQuadraticChartAtom_measurable {k d : ℕ} (A : MultivariableQuadraticChartData k d) : Measurable (multivariableQuadraticChartAtom A)

theorem TrilinearHT.Auto.localized_modulation_error {E : Type u_1} [NormedAddCommGroup E] (θ Q : E → ℂ) (z h : E) (p : ℂ) {K L B D η : ℝ} (hK : 0 ≤ K) (hL : 0 ≤ L) (hB : 0 ≤ B) (hD : 0 ≤ D) (hη : 0 ≤ η) (hθ : ‖θ z‖ ≤ K) (hθh : ‖θ (z + h) - θ z‖ ≤ L * ‖h‖) (hQ : ‖Q (z + h)‖ ≤ B) (herr : ‖Q (z + h) - p * Q z‖ ≤ D * η) : ‖θ (z + h) * Q (z + h) - p * (θ z * Q z)‖ ≤ (L * B + K * D) * (‖h‖ + η)

Localization adds only the cutoff's translation error to a modulation error.

theorem TrilinearHT.Auto.bounded_supported_integral_norm {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {f : X → ℂ} {S : Set X} {B : ℝ} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hS : MeasurableSet S) (hSf : μ S ≠ ⊤) (hbound : ∀ (x : X), ‖f x‖ ≤ B) (hsupp : ∀ x ∉ S, f x = 0) : MeasureTheory.Integrable f μ ∧ ∫ (x : X), ‖f x‖ ∂μ ≤ μ.real S * B

An explicitly bounded measurable function supported in a finite-measure set is integrable, with its L1 norm bounded by size times measure.

theorem TrilinearHT.Auto.bounded_box_integral_norm {k : ℕ} {f : (Fin k → ℝ) → ℂ} {R B : ℝ} (hf : Measurable f) (hR : 0 ≤ R) (hbound : ∀ (x : Fin k → ℝ), ‖f x‖ ≤ B) (hsupp : ∀ (x : Fin k → ℝ), f x ≠ 0 → ∀ (i : Fin k), |x i| ≤ R) : MeasureTheory.Integrable f MeasureTheory.volume ∧ ∫ (x : Fin k → ℝ), ‖f x‖ ≤ (2 * R) ^ k * B

The preceding bound with the exact volume of a coordinate box.

noncomputable def TrilinearHT.Auto.chartReturnErrorConstant (c₀ d : ℕ) (H : ℝ) : ℝ

Explicit defect constant in the chart return estimate.

Equations

• TrilinearHT.Auto.chartReturnErrorConstant c₀ d H = 2 * (2 * H + 3) ^ d * (H ^ (4 * c₀) * 2 ^ (2 * c₀) + H ^ c₀ * (2 * Real.pi * ↑d ^ 2 * H * H))

noncomputable def TrilinearHT.Auto.localizedReturnErrorConstant (c₀ d k : ℕ) (H R : ℝ) : ℝ

The localization constant includes the volume of the enlarged fixed box.

Equations

• TrilinearHT.Auto.localizedReturnErrorConstant c₀ d k H R = (1 + (2 * (R + 1)) ^ k) * (H * ((2 * H + 3) ^ d * H ^ c₀) + H * TrilinearHT.Auto.chartReturnErrorConstant c₀ d H)

theorem TrilinearHT.Auto.localized_multivariableChart_return_error {k d c₀ : ℕ} {H R : ℝ} {A : MultivariableQuadraticChartData k d} (hA : MultivariableQuadraticChartComplexity c₀ H A) (hc : 1 ≤ c₀) (θ : (Fin k → ℝ) → ℂ) (hθm : Measurable θ) (hR : 0 ≤ R) (hθ : ∀ (z : Fin k → ℝ), ‖θ z‖ ≤ H) (hθLip : ∀ (x y : Fin k → ℝ), ‖θ y - θ x‖ ≤ H * ‖y - x‖) (hθsupp : ∀ (z : Fin k → ℝ), θ z ≠ 0 → ∀ (i : Fin k), |z i| ≤ R) (h : Fin k → ℝ) (hh : ‖h‖ ≤ 1) (m : Fin d → ℤ) (hint : ∀ (i j : Fin d), ∃ (q : ℤ), ↑q = ↑(m i) * ↑(A.matrix i j)) : have e := A.horizontal.mulVec h - fun (i : Fin d) => ↑(m i); have C := A.matrix.map fun (q : ℚ) => ↑q; have ω := (2 • A.quadratic + A.horizontal.transpose * C * A.horizontal).mulVec h - (A.horizontal.transpose * (C - C.transpose)).mulVec fun (i : Fin d) => ↑(m i); have c := h ⬝ᵥ A.quadratic.mulVec h + A.linear ⬝ᵥ h + chartMatrixPhase A.matrix (A.horizontal.mulVec h) e; have E := fun (z : Fin k → ℝ) => θ (z + h) * multivariableQuadraticChartAtom A (z + h) - ↑(Real.fourierChar (c + z ⬝ᵥ ω)) * (θ z * multivariableQuadraticChartAtom A z); MeasureTheory.Integrable E MeasureTheory.volume ∧ ∀ (z : Fin k → ℝ), (∫ (x : Fin k → ℝ), ‖E x‖) + ‖E z‖ ≤ localizedReturnErrorConstant c₀ d k H R * (‖h‖ + ‖e‖)

Blueprint eq:return: the genuine localized error is integrable and its L1 norm plus every pointwise norm is bounded linearly in the return size. The constant has no dependence on the unrestricted velocity or phase.

theorem TrilinearHT.Auto.bounded_box_L2_and_moment {k : ℕ} {f : (Fin k → ℝ) → ℂ} {R B : ℝ} (hf : Measurable f) (hR : 0 ≤ R) (hB : 0 ≤ B) (hbound : ∀ (x : Fin k → ℝ), ‖f x‖ ≤ B) (hsupp : ∀ (x : Fin k → ℝ), f x ≠ 0 → ∀ (i : Fin k), |x i| ≤ R) : MeasureTheory.MemLp f 2 MeasureTheory.volume ∧ ∫ (x : Fin k → ℝ), ‖f x‖ ^ 2 ≤ (2 * R) ^ k * B ^ 2 ∧ MeasureTheory.Integrable (fun (x : Fin k → ℝ) => ‖x‖ * ‖f x‖) MeasureTheory.volume ∧ ∫ (x : Fin k → ℝ), ‖x‖ * ‖f x‖ ≤ (2 * R) ^ k * R * B

A bounded box-supported function has explicit L2 mass and first-moment bounds, as needed before the Weyl Fourier argument.

theorem TrilinearHT.Auto.localized_multivariableChart_size {k d c₀ : ℕ} {H R : ℝ} {A : MultivariableQuadraticChartData k d} (hA : MultivariableQuadraticChartComplexity c₀ H A) (θ : (Fin k → ℝ) → ℂ) (hθm : Measurable θ) (hR : 0 ≤ R) (hθ : ∀ (z : Fin k → ℝ), ‖θ z‖ ≤ H) (hθsupp : ∀ (z : Fin k → ℝ), θ z ≠ 0 → ∀ (i : Fin k), |z i| ≤ R) : have F := fun (z : Fin k → ℝ) => θ z * multivariableQuadraticChartAtom A z; have B := H * ((2 * H + 3) ^ d * H ^ c₀); Measurable F ∧ (∀ (z : Fin k → ℝ), ‖F z‖ ≤ B) ∧ (∀ (z : Fin k → ℝ), F z ≠ 0 → ∀ (i : Fin k), |z i| ≤ R) ∧ MeasureTheory.Integrable F MeasureTheory.volume ∧ ∫ (z : Fin k → ℝ), ‖F z‖ ≤ (2 * R) ^ k * B ∧ MeasureTheory.MemLp F 2 MeasureTheory.volume ∧ ∫ (z : Fin k → ℝ), ‖F z‖ ^ 2 ≤ (2 * R) ^ k * B ^ 2 ∧ MeasureTheory.Integrable (fun (z : Fin k → ℝ) => ‖z‖ * ‖F z‖) MeasureTheory.volume ∧ ∫ (z : Fin k → ℝ), ‖z‖ * ‖F z‖ ≤ (2 * R) ^ k * R * B

All analytic size assumptions on F=θQ in the Weyl proof follow from the actual chart complexity and the fixed support box of θ.

theorem TrilinearHT.Auto.euclidean_norm_le_dimension_mul_pi_norm {k : ℕ} (x : Fin k → ℝ) : ‖WithLp.toLp 2 x‖ ≤ ↑k * ‖x‖

Coordinate sup norm and Euclidean norm comparisons, including dimension zero.

theorem TrilinearHT.Auto.coordinate_lift_first_moment {k : ℕ} {f : (Fin k → ℝ) → ℂ} (hf : Measurable f) (hm : MeasureTheory.Integrable (fun (x : Fin k → ℝ) => ‖x‖ * ‖f x‖) MeasureTheory.volume) : MeasureTheory.Integrable (fun (x : EuclideanSpace ℝ (Fin k)) => ‖x‖ * ‖f x.ofLp‖) MeasureTheory.volume ∧ ∫ (x : EuclideanSpace ℝ (Fin k)), ‖x‖ * ‖f x.ofLp‖ ≤ ↑k * ∫ (x : Fin k → ℝ), ‖x‖ * ‖f x‖

Passing from coordinate functions to Euclidean space preserves volume and costs at most the dimension in the first absolute moment.

theorem TrilinearHT.Auto.localized_multivariableChart_euclidean_size {k d c₀ : ℕ} {H R : ℝ} {A : MultivariableQuadraticChartData k d} (hA : MultivariableQuadraticChartComplexity c₀ H A) (θ : (Fin k → ℝ) → ℂ) (hθm : Measurable θ) (hR : 0 ≤ R) (hθ : ∀ (z : Fin k → ℝ), ‖θ z‖ ≤ H) (hθsupp : ∀ (z : Fin k → ℝ), θ z ≠ 0 → ∀ (i : Fin k), |z i| ≤ R) : have F := fun (z : EuclideanSpace ℝ (Fin k)) => θ z.ofLp * multivariableQuadraticChartAtom A z.ofLp; have B := H * ((2 * H + 3) ^ d * H ^ c₀); Measurable F ∧ (∀ (z : EuclideanSpace ℝ (Fin k)), ‖F z‖ ≤ B) ∧ MeasureTheory.Integrable F MeasureTheory.volume ∧ ∫ (z : EuclideanSpace ℝ (Fin k)), ‖F z‖ ≤ (2 * R) ^ k * B ∧ MeasureTheory.MemLp F 2 MeasureTheory.volume ∧ ∫ (z : EuclideanSpace ℝ (Fin k)), ‖F z‖ ^ 2 ≤ (2 * R) ^ k * B ^ 2 ∧ MeasureTheory.Integrable (fun (z : EuclideanSpace ℝ (Fin k)) => ‖z‖ * ‖F z‖) MeasureTheory.volume ∧ ∫ (z : EuclideanSpace ℝ (Fin k)), ‖z‖ * ‖F z‖ ≤ ↑k * ((2 * R) ^ k * R * B)

The analytic input to the Weyl argument on Euclidean space, with the standard Lebesgue measure and the Euclidean first absolute moment.

theorem TrilinearHT.Auto.localized_multivariableChart_fourier_lipschitz {k d c₀ : ℕ} {H R : ℝ} {A : MultivariableQuadraticChartData k d} (hA : MultivariableQuadraticChartComplexity c₀ H A) (θ : (Fin k → ℝ) → ℂ) (hθm : Measurable θ) (hR : 0 ≤ R) (hθ : ∀ (z : Fin k → ℝ), ‖θ z‖ ≤ H) (hθsupp : ∀ (z : Fin k → ℝ), θ z ≠ 0 → ∀ (i : Fin k), |z i| ≤ R) (ξ η : EuclideanSpace ℝ (Fin k)) : have F := fun (z : EuclideanSpace ℝ (Fin k)) => θ z.ofLp * multivariableQuadraticChartAtom A z.ofLp; ‖FourierTransform.fourier F ξ - FourierTransform.fourier F η‖ ≤ 2 * Real.pi * (↑k * ((2 * R) ^ k * R * (H * ((2 * H + 3) ^ d * H ^ c₀)))) * ‖ξ - η‖

The localized chart Fourier transform is quantitatively Lipschitz, without any bound on its unrestricted horizontal or quadratic parameters.

theorem TrilinearHT.Auto.localized_multivariableChart_fourier_return_lower {k d c₀ : ℕ} {H R : ℝ} {A : MultivariableQuadraticChartData k d} (hA : MultivariableQuadraticChartComplexity c₀ H A) (hc : 1 ≤ c₀) (θ : (Fin k → ℝ) → ℂ) (hθm : Measurable θ) (hR : 0 ≤ R) (hθ : ∀ (z : Fin k → ℝ), ‖θ z‖ ≤ H) (hθLip : ∀ (x y : Fin k → ℝ), ‖θ y - θ x‖ ≤ H * ‖y - x‖) (hθsupp : ∀ (z : Fin k → ℝ), θ z ≠ 0 → ∀ (i : Fin k), |z i| ≤ R) (h : Fin k → ℝ) (hh : ‖h‖ ≤ 1) (m : Fin d → ℤ) (hint : ∀ (i j : Fin d), ∃ (q : ℤ), ↑q = ↑(m i) * ↑(A.matrix i j)) (ξ : EuclideanSpace ℝ (Fin k)) : have e := A.horizontal.mulVec h - fun (i : Fin d) => ↑(m i); have C := A.matrix.map fun (q : ℚ) => ↑q; have ω := (2 • A.quadratic + A.horizontal.transpose * C * A.horizontal).mulVec h - (A.horizontal.transpose * (C - C.transpose)).mulVec fun (i : Fin d) => ↑(m i); have F := fun (z : EuclideanSpace ℝ (Fin k)) => θ z.ofLp * multivariableQuadraticChartAtom A z.ofLp; ‖FourierTransform.fourier F ξ‖ - localizedReturnErrorConstant c₀ d k H R * (‖h‖ + ‖e‖) ≤ ‖FourierTransform.fourier F (ξ - WithLp.toLp 2 ω)‖

The actual chart return error propagates Fourier magnitude by one return frequency. This is the quantitative input for the multiple-return argument.

theorem TrilinearHT.Auto.localized_multivariableChart_fourier_progression {k d c₀ : ℕ} {H R : ℝ} {A : MultivariableQuadraticChartData k d} (hA : MultivariableQuadraticChartComplexity c₀ H A) (hc : 1 ≤ c₀) (θ : (Fin k → ℝ) → ℂ) (hθm : Measurable θ) (hR : 0 ≤ R) (hθ : ∀ (z : Fin k → ℝ), ‖θ z‖ ≤ H) (hθLip : ∀ (x y : Fin k → ℝ), ‖θ y - θ x‖ ≤ H * ‖y - x‖) (hθsupp : ∀ (z : Fin k → ℝ), θ z ≠ 0 → ∀ (i : Fin k), |z i| ≤ R) (h : Fin k → ℝ) (hh : ‖h‖ ≤ 1) (m : Fin d → ℤ) (hint : ∀ (i j : Fin d), ∃ (q : ℤ), ↑q = ↑(m i) * ↑(A.matrix i j)) (ξ : EuclideanSpace ℝ (Fin k)) (j : ℕ) : have e := A.horizontal.mulVec h - fun (i : Fin d) => ↑(m i); have C := A.matrix.map fun (q : ℚ) => ↑q; have ω := (2 • A.quadratic + A.horizontal.transpose * C * A.horizontal).mulVec h - (A.horizontal.transpose * (C - C.transpose)).mulVec fun (i : Fin d) => ↑(m i); have F := fun (z : EuclideanSpace ℝ (Fin k)) => θ z.ofLp * multivariableQuadraticChartAtom A z.ofLp; ‖FourierTransform.fourier F ξ‖ - ↑j * (localizedReturnErrorConstant c₀ d k H R * (‖h‖ + ‖e‖)) ≤ ‖FourierTransform.fourier F (ξ - j • WithLp.toLp 2 ω)‖

The source progression of large Fourier values follows by iterating the verified one-return estimate; no new return hypotheses are assumed.

theorem TrilinearHT.Auto.shortReturn_projection_budget {d k : ℕ} (V : Matrix (Fin d) (Fin k) ℝ) {P b t : ℝ} (ht : 2 ≤ t) (hP : 0 < P) (hPt : P ≤ t) (hb : 0 < b) (hbT : b⁻¹ ≤ shortReturnScaleBudget t) (hd : ↑d ≤ logarithmicSize t) (hk : k ≤ 3) (hgap : ∀ (j : ℕ), 0 < j → j ≤ d → successiveMinimum (shortReturnBody (realMatrixOperator V) P) (coordinateIntegerLattice d) j ≤ b ∨ 16 * (100 * ↑d) ^ (10 * d) * b < successiveMinimum (shortReturnBody (realMatrixOperator V) P) (coordinateIntegerLattice d) j) : let U := shortReturnLatticeSpan (realMatrixOperator V) P b; ∃ (Q : Matrix (Fin d) (Fin d) ℚ), realMatrixOperator (Q.map fun (q : ℚ) => ↑q) = Uᗮ.starProjection ∧ realMatrixOperator ((1 - Q).map fun (q : ℚ) => ↑q) = U.starProjection ∧ (∀ (i j : Fin d), ↑(rationalHeight (Q i j)) ≤ shortReturnProjectionBudget t) ∧ (∀ (i j : Fin d), ↑(rationalHeight ((1 - Q) i j)) ≤ shortReturnProjectionBudget t) ∧ ‖realMatrixOperator ((Q.map fun (q : ℚ) => ↑q) * V)‖ ≤ shortReturnSlowBudget t

The rational slow projection supplied by the return-body gap has simultaneously bounded height and velocity, without a bound on V.

theorem TrilinearHT.Auto.shortReturnSplitting_explicit {d k : ℕ} (hk1 : 1 ≤ k) (hk3 : k ≤ 3) (C : Matrix (Fin d) (Fin d) ℚ) (V : Matrix (Fin d) (Fin k) ℝ) (Λ : Matrix (Fin k) (Fin k) ℝ) (hΛ : Λ.IsSymm) (P : ℤ) (hP : 1 ≤ P) (hPC : ∀ (i j : Fin d), ∃ (z : ℤ), ↑P * C i j = ↑z) {t a M : ℝ} (ht : 2 ≤ t) (hPt : ↑P ≤ t) (hd : ↑d ≤ logarithmicSize t) (hC : ∀ (i j : Fin d), ↑(rationalHeight (C i j)) ≤ t) (ha : 0 < a) (ha1 : a ≤ 1) (hat : a⁻¹ ≤ t) (hM : 0 ≤ M) (hMt : M ≤ t) (hΩ : ∀ (h : Fin k → ℝ) (n : Fin d → ℤ), ‖WithLp.toLp 2 h‖ + ‖WithLp.toLp 2 (V.mulVec h - fun (i : Fin d) => ↑P * ↑(n i))‖ ≤ a → ‖WithLp.toLp 2 (quadraticReturnFrequency (C.map fun (q : ℚ) => ↑q) V Λ h fun (i : Fin d) => ↑P * ↑(n i))‖ ≤ M) : ∃ (U : Submodule ℝ (EuclideanSpace ℝ (Fin d))) (Q : Matrix (Fin d) (Fin d) ℚ), realMatrixOperator (Q.map fun (q : ℚ) => ↑q) = Uᗮ.starProjection ∧ realMatrixOperator ((1 - Q).map fun (q : ℚ) => ↑q) = U.starProjection ∧ (∀ x ∈ U, ∀ y ∈ U, inner ℝ y ((realMatrixOperator ((C.map fun (q : ℚ) => ↑q) - (C.map fun (q : ℚ) => ↑q).transpose)) x) = 0) ∧ (∀ (i j : Fin d), ↑(rationalHeight (Q i j)) ≤ shortReturnSplittingBudget t) ∧ (∀ (i j : Fin d), ↑(rationalHeight ((1 - Q) i j)) ≤ shortReturnSplittingBudget t) ∧ ‖realMatrixOperator ((Q.map fun (q : ℚ) => ↑q) * V)‖ ≤ shortReturnSplittingBudget t ∧ ‖realMatrixOperator (effectiveReturnQuadratic (C.map fun (q : ℚ) => ↑q) Λ V (((1 - Q).map fun (q : ℚ) => ↑q) * V) ((Q.map fun (q : ℚ) => ↑q) * V))‖ ≤ shortReturnSplittingBudget t

Blueprint lem:return-splitting, lines 1245–1302, with the explicit common budget. Both complementary projections are rational, the fast space is isotropic, and the slow velocity and effective quadratic form are bounded.

theorem TrilinearHT.Auto.shortReturnSplitting : ∃ (D : ℕ), 1 ≤ D ∧ ∀ {d k : ℕ}, 1 ≤ k → k ≤ 3 → ∀ (H : ℝ), Real.exp 2 ≤ H → ↑d ≤ Real.log H → ∀ (C : Matrix (Fin d) (Fin d) ℚ), (∀ (i j : Fin d), ↑(rationalHeight (C i j)) ≤ H) → ∀ (V : Matrix (Fin d) (Fin k) ℝ) (Λ : Matrix (Fin k) (Fin k) ℝ), Λ.IsSymm → ∀ (P : ℤ), 1 ≤ P → (∀ (i j : Fin d), ∃ (z : ℤ), ↑P * C i j = ↑z) → ∀ (a M : ℝ), 0 < a → a < 1 → 1 ≤ M → (∀ (h : Fin k → ℝ) (n : Fin d → ℤ), ‖WithLp.toLp 2 h‖ + ‖WithLp.toLp 2 (V.mulVec h - fun (i : Fin d) => ↑P * ↑(n i))‖ ≤ a → ‖WithLp.toLp 2 (quadraticReturnFrequency (C.map fun (q : ℚ) => ↑q) V Λ h fun (i : Fin d) => ↑P * ↑(n i))‖ ≤ M) → have B := Real.exp (↑D * (1 + Real.log H + Real.log ↑P + Real.log (1 / a) + Real.log M) ^ D); ∃ (U : Submodule ℝ (EuclideanSpace ℝ (Fin d))) (Q : Matrix (Fin d) (Fin d) ℚ), realMatrixOperator (Q.map fun (q : ℚ) => ↑q) = Uᗮ.starProjection ∧ realMatrixOperator ((1 - Q).map fun (q : ℚ) => ↑q) = U.starProjection ∧ (∀ x ∈ U, ∀ y ∈ U, inner ℝ y ((realMatrixOperator ((C.map fun (q : ℚ) => ↑q) - (C.map fun (q : ℚ) => ↑q).transpose)) x) = 0) ∧ (∀ (i j : Fin d), ↑(rationalHeight (Q i j)) ≤ B) ∧ (∀ (i j : Fin d), ↑(rationalHeight ((1 - Q) i j)) ≤ B) ∧ ‖realMatrixOperator ((Q.map fun (q : ℚ) => ↑q) * V)‖ ≤ B ∧ ‖realMatrixOperator (effectiveReturnQuadratic (C.map fun (q : ℚ) => ↑q) Λ V (((1 - Q).map fun (q : ℚ) => ↑q) * V) ((Q.map fun (q : ℚ) => ↑q) * V))‖ ≤ B

Blueprint lem:return-splitting (lines 1245–1302): an absolute constant and degree control both rational projection heights, the slow velocity, and the effective symmetric quadratic form. The rational matrix Q is the slow projection; 1-Q projects onto the isotropic rational fast subspace U. There is no size assumption on V or on the symmetric matrix Λ.

theorem TrilinearHT.Auto.sup_norm_le_euclidean {k : ℕ} (x : Fin k → ℝ) : ‖x‖ ≤ ‖WithLp.toLp 2 x‖

theorem TrilinearHT.Auto.weyl_return_frequency_lt_one {k d c₀ : ℕ} {H R : ℝ} {A : MultivariableQuadraticChartData k d} (hA : MultivariableQuadraticChartComplexity c₀ H A) (hc : 1 ≤ c₀) (θ : (Fin k → ℝ) → ℂ) (hθm : Measurable θ) (hR : 0 ≤ R) (hθ : ∀ (z : Fin k → ℝ), ‖θ z‖ ≤ H) (hθLip : ∀ (x y : Fin k → ℝ), ‖θ y - θ x‖ ≤ H * ‖y - x‖) (hθsupp : ∀ (z : Fin k → ℝ), θ z ≠ 0 → ∀ (i : Fin k), |z i| ≤ R) (P : ℤ) (hPC : ∀ (i j : Fin d), ∃ (z : ℤ), ↑P * A.matrix i j = ↑z) {δ a : ℝ} (hδ : 0 < δ) (ha1 : a ≤ 1) (M : ℕ) (ξ : EuclideanSpace ℝ (Fin k)) (hξ : 3 * δ / 4 ≤ ‖FourierTransform.fourier (fun (z : EuclideanSpace ℝ (Fin k)) => θ z.ofLp * multivariableQuadraticChartAtom A z.ofLp) ξ‖) (hM : (2 * R) ^ k * (H * ((2 * H + 3) ^ d * H ^ c₀)) ^ 2 < ↑M * (MeasureTheory.volume.real (Metric.ball 0 (min (1 / 2) (δ / (6 * (2 * Real.pi * (↑k * ((2 * R) ^ k * R * (H * ((2 * H + 3) ^ d * H ^ c₀)))) + 1))))) * (δ / 3) ^ 2)) (haM : ↑M * (localizedReturnErrorConstant c₀ d k H R * (2 * a)) ≤ δ / 4) (h : Fin k → ℝ) (n : Fin d → ℤ) (hret : ‖WithLp.toLp 2 h‖ + ‖WithLp.toLp 2 (A.horizontal.mulVec h - fun (i : Fin d) => ↑P * ↑(n i))‖ ≤ a) : ‖WithLp.toLp 2 (quadraticReturnFrequency (A.matrix.map fun (q : ℚ) => ↑q) A.horizontal A.quadratic h fun (i : Fin d) => ↑P * ↑(n i))‖ < 1

Blueprint lem:weyl, line 1333: once the return threshold a makes the accumulated progression error at most δ/4 over M steps, and M balls exceed the Plancherel mass, every short return has frequency of norm below one.

theorem TrilinearHT.Auto.seven_le_exp_two : 7 ≤ Real.exp 2

e² ≥ 7.

theorem TrilinearHT.Auto.weyl_constants_le_power {c₀ d k : ℕ} {H R : ℝ} (hH : Real.exp 2 ≤ H) (hd : ↑d ≤ Real.log H) (hR : 0 ≤ R) (hk : k ≤ 3) : have Z := 5 * (R + 2) * H; have N := 4 * c₀ + 3 * d + 20; have B := H * ((2 * H + 3) ^ d * H ^ c₀); 70 ≤ Z ∧ 2 * Real.pi * (↑k * ((2 * R) ^ k * R * B)) + 1 ≤ Z ^ N ∧ (2 * R) ^ k * B ^ 2 ≤ Z ^ N ∧ localizedReturnErrorConstant c₀ d k H R ≤ Z ^ N

All analytic constants of the localized chart in the Weyl argument are bounded by one explicit power of Z = 5 (R + 2) H. Source: lem:weyl, line 1333.

theorem TrilinearHT.Auto.weyl_threshold_lower {S' V0 K δ W : ℝ} (hW : 70 ≤ W) (hδ : 0 < δ) (hδW : 1 ≤ δ * W) (hS : S' ≤ W) (hK0 : 0 ≤ K) (hK : K ≤ W) (hS0 : 0 ≤ S') (hV : (1 / (12 * W)) ^ 3 ≤ V0) : have M := ⌈9 * S' / (V0 * δ ^ 2)⌉₊ + 1; (W ^ 16)⁻¹ ≤ min (1 / 2) (δ / (8 * (K + 1) * ↑M))

The return threshold a in the Weyl argument is at least W^(-16), where W dominates all localized chart constants and δ⁻¹.

theorem TrilinearHT.Auto.weyl_log_budget {c₀ d : ℕ} {H R δ P a : ℝ} (hH : Real.exp 2 ≤ H) (hd : ↑d ≤ Real.log H) (hR : 0 ≤ R) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (hP : 1 ≤ P) (hPH : P ≤ H ^ d ^ 2) (ha : 0 < a) (haW : (((5 * (R + 2) * H) ^ (4 * c₀ + 3 * d + 20) / δ) ^ 16)⁻¹ ≤ a) : 1 + Real.log H + Real.log P + Real.log (1 / a) + Real.log 1 ≤ (18 + 16 * (4 * ↑c₀ + 23) * (Real.log (5 * (R + 2)) + 1)) * (1 + Real.log H + Real.log δ⁻¹) ^ 3

Logarithmic budget of the Weyl alternative: the parameters fed to the short-return splitting have total logarithmic size at most κ T³.

theorem TrilinearHT.Auto.weylSplitting (c₀ : ℕ) (hc : 1 ≤ c₀) (R : ℝ) (hR : 0 ≤ R) : ∃ (D : ℕ), 1 ≤ D ∧ ∀ {d k : ℕ}, 1 ≤ k → k ≤ 3 → ∀ (H : ℝ) (A : MultivariableQuadraticChartData k d), MultivariableQuadraticChartComplexity c₀ H A → ∀ (θ : (Fin k → ℝ) → ℂ), Measurable θ → (∀ (z : Fin k → ℝ), ‖θ z‖ ≤ H) → (∀ (x y : Fin k → ℝ), ‖θ y - θ x‖ ≤ H * ‖y - x‖) → (∀ (z : Fin k → ℝ), θ z ≠ 0 → ∀ (i : Fin k), |z i| ≤ R) → ∀ (δ : ℝ), 0 < δ → (∀ t < δ, ∃ (ξ : EuclideanSpace ℝ (Fin k)), t < ‖FourierTransform.fourier (fun (z : EuclideanSpace ℝ (Fin k)) => θ z.ofLp * multivariableQuadraticChartAtom A z.ofLp) ξ‖) → have B := Real.exp (↑D * (1 + Real.log H + Real.log (max 1 δ⁻¹)) ^ D); ∃ (U : Submodule ℝ (EuclideanSpace ℝ (Fin d))) (Q : Matrix (Fin d) (Fin d) ℚ), realMatrixOperator (Q.map fun (q : ℚ) => ↑q) = Uᗮ.starProjection ∧ realMatrixOperator ((1 - Q).map fun (q : ℚ) => ↑q) = U.starProjection ∧ (∀ x ∈ U, ∀ y ∈ U, inner ℝ y ((realMatrixOperator ((A.matrix.map fun (q : ℚ) => ↑q) - (A.matrix.map fun (q : ℚ) => ↑q).transpose)) x) = 0) ∧ (∀ (i j : Fin d), ↑(rationalHeight (Q i j)) ≤ B) ∧ (∀ (i j : Fin d), ↑(rationalHeight ((1 - Q) i j)) ≤ B) ∧ ‖realMatrixOperator ((Q.map fun (q : ℚ) => ↑q) * A.horizontal)‖ ≤ B ∧ ‖realMatrixOperator (effectiveReturnQuadratic (A.matrix.map fun (q : ℚ) => ↑q) A.quadratic A.horizontal (((1 - Q).map fun (q : ℚ) => ↑q) * A.horizontal) ((Q.map fun (q : ℚ) => ↑q) * A.horizontal))‖ ≤ B

Blueprint lem:weyl (Weyl alternative), lines 1304–1333. Let θ be supported in the fixed box [-R,R]^k with supremum and Lipschitz norms at most H, and let Q be a several-variable quadratic chart of complexity H (fixed Gevrey order c₀). If sup_ξ |∫ θ(z) Q(z) e(-ξ·z) dz| ≥ δ > 0, there is a rational subspace U with orthogonal projections P_f = 1 - Q onto U and P_s = Q onto Uᗮ such that the skew part of the chart matrix vanishes on U × U, ‖V_s‖ ≤ H' and ‖Λ_*‖ ≤ H', where Λ_* is the effective quadratic form Λ + ½VᵀC_syV + sym(V_fᵀC_skV_s). The projection heights and H' are quasipolynomial in H and δ⁻¹: all are bounded by exp(D (1 + log H + log max(1, δ⁻¹))^D), with D depending only on c₀ and the box. As in the trilinear setting, 1 ≤ k ≤ 3.

theorem TrilinearHT.Auto.dotProduct_transpose_mulVec_comm {d : ℕ} (C : Matrix (Fin d) (Fin d) ℝ) (x y : Fin d → ℝ) : x ⬝ᵥ C.transpose.mulVec y = y ⬝ᵥ C.mulVec x

Transposed bilinear pairings in dot-product form.

theorem TrilinearHT.Auto.effectiveReturnQuadratic_form {d k : ℕ} (C : Matrix (Fin d) (Fin d) ℝ) (Λ : Matrix (Fin k) (Fin k) ℝ) (V F S : Matrix (Fin d) (Fin k) ℝ) (z : Fin k → ℝ) : z ⬝ᵥ (effectiveReturnQuadratic C Λ V F S).mulVec z = z ⬝ᵥ Λ.mulVec z + 1 / 2 * V.mulVec z ⬝ᵥ (realSymmetricPart C).mulVec (V.mulVec z) + F.mulVec z ⬝ᵥ (realSkewPart C).mulVec (S.mulVec z)

The quadratic form of the effective matrix Λ_* in eq:effective.

def TrilinearHT.Auto.separatedPhaseMatrix {d : ℕ} (C Q : Matrix (Fin d) (Fin d) ℚ) : Matrix (Fin d) (Fin d) ℚ

The rational matrix of the separated quadratic phase.

Equations

• TrilinearHT.Auto.separatedPhaseMatrix C Q = (1 / 4) • (C + C.transpose) + (1 - Q).transpose * (1 / 2) • (C - C.transpose) * Q

theorem TrilinearHT.Auto.separatedPhaseMatrix_cast {d : ℕ} (C Q : Matrix (Fin d) (Fin d) ℚ) : ((separatedPhaseMatrix C Q).map fun (q : ℚ) => ↑q) = (1 / 2) • realSymmetricPart (C.map fun (q : ℚ) => ↑q) + (1 - Q.map fun (q : ℚ) => ↑q).transpose * realSkewPart (C.map fun (q : ℚ) => ↑q) * Q.map fun (q : ℚ) => ↑q

theorem TrilinearHT.Auto.phase_height_budget {H X : ℝ} {d Dw : ℕ} (hDw : 1 ≤ Dw) (hH1 : 1 ≤ H) (hHX : Real.log H ≤ X) (hX3 : 3 ≤ X) (hdX : ↑d ≤ X) : have B := Real.exp (↑Dw * X ^ Dw); 4 * H ^ d ^ 2 * (B ^ d ^ 2) ^ 2 * (H + ↑d ^ 2 * ((1 + B) * H * B) + 1) ≤ Real.exp (9 * (1 + ↑Dw) * X ^ (Dw + 2))

theorem TrilinearHT.Auto.exp_compose_budget {X Xs : ℝ} {Dw Ds : ℕ} (hXs0 : 0 ≤ Xs) (hXs : Xs ≤ (1 + ↑Dw) * X ^ Dw) : Real.exp (↑Ds * Xs ^ Ds) ≤ Real.exp (↑Ds * (1 + ↑Dw) ^ Ds * X ^ (Dw * Ds))

Quasipolynomial composition: a bound quasipolynomial in X_s = 1 + log H + log B, where B = exp(D_w X^{D_w}), is quasipolynomial in X.