Section 2: Elementary lattice and torus facts

This file was automatically generated by Claude.

Formalization of blueprint Section 2, "Elementary lattice and torus facts" (sec:lattices, lines 254-362) of blueprint/formalization_blueprint.tex.

theorem TrilinearHT.Auto.reducedBasis_weighted_coordinate_bound {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (hb : IsShortestProjectionBasis b) (hr : IsSizeReducedBasis b) (i : Fin n) (x : E) : ‖b i‖ * |(b.repr x) i| ≤ 8 ^ n * ‖x‖

The reduced-basis estimates imply a uniform bound on each coefficient weighted by its basis-vector length; used in blueprint lem:lattice-box.

noncomputable def TrilinearHT.Auto.latticeBoxSideLength {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (i : Fin n) : ℤ

The printed floored side length; zero lengths will be discarded.

Equations

• TrilinearHT.Auto.latticeBoxSideLength b i = ⌊(4 * ↑n * ‖b i‖)⁻¹⌋

noncomputable def TrilinearHT.Auto.latticeBoxIndices {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) : Finset (Fin n)

The part of the lattice basis retained in the coefficient box.

Equations

• TrilinearHT.Auto.latticeBoxIndices b = {i : Fin n | 0 < TrilinearHT.Auto.latticeBoxSideLength b i}

def TrilinearHT.Auto.integerCoefficientBox {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (I : Finset (Fin n)) (L : Fin n → ℤ) : Set E

An integer coefficient box on the selected part of a basis.

Equations

• TrilinearHT.Auto.integerCoefficientBox b I L = {x : E | ∃ (z : Fin n → ℤ), (∀ i ∉ I, z i = 0) ∧ (∀ i ∈ I, |z i| ≤ L i) ∧ ∑ i : Fin n, z i • b i = x}

theorem TrilinearHT.Auto.latticeBoxSideLength_nonneg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) (i : Fin n) : 0 ≤ latticeBoxSideLength b i

theorem TrilinearHT.Auto.latticeBoxSideLength_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) {i : Fin n} (hi : i ∈ latticeBoxIndices b) : 1 ≤ latticeBoxSideLength b i

theorem TrilinearHT.Auto.latticeBoxSideLength_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) {i : Fin n} (hi : i ∉ latticeBoxIndices b) : latticeBoxSideLength b i = 0

theorem TrilinearHT.Auto.latticeBoxSideLength_weight_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (hn : 0 < n) (b : Module.Basis (Fin n) ℝ E) (i : Fin n) : ↑(latticeBoxSideLength b i) * ‖b i‖ ≤ (4 * ↑n)⁻¹

theorem TrilinearHT.Auto.latticeBoxSideLength_sum_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (hn : 0 < n) (b : Module.Basis (Fin n) ℝ E) : ∑ i : Fin n, ↑(latticeBoxSideLength b i) * ‖b i‖ ≤ 1 / 4

Blueprint lem:lattice-box, line 336: the total length budget is 1/4.

noncomputable def TrilinearHT.Auto.latticeBoxRadius (n : ℕ) : ℝ

The explicit radius (100d)^(-10d) from blueprint lem:lattice-box.

Equations

• TrilinearHT.Auto.latticeBoxRadius n = ((100 * ↑n) ^ (10 * n))⁻¹

theorem TrilinearHT.Auto.latticeBoxRadius_scaled_le {n : ℕ} (hn : 0 < n) : 4 * ↑n * 8 ^ n * latticeBoxRadius n ≤ 1

theorem TrilinearHT.Auto.exists_integer_basis_coordinates {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (b : Module.Basis (Fin n) ℝ E) {v : E} (hv : v ∈ Submodule.span ℤ (Set.range ⇑b)) : ∃ (z : Fin n → ℤ), (∀ (i : Fin n), ↑(z i) = (b.repr v) i) ∧ ∑ i : Fin n, z i • b i = v

Integer coordinates in a real basis of its integer span.

theorem TrilinearHT.Auto.small_lattice_vector_mem_coefficientBox {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (hn : 0 < n) (b : Module.Basis (Fin n) ℝ E) (hb : IsShortestProjectionBasis b) (hr : IsSizeReducedBasis b) {v : E} (hv : v ∈ Submodule.span ℤ (Set.range ⇑b)) (hnorm : ‖v‖ ≤ latticeBoxRadius n) : v ∈ integerCoefficientBox b (latticeBoxIndices b) (latticeBoxSideLength b)

Blueprint lem:lattice-box, lines 337–342: every lattice vector with norm at most the explicit radius belongs to the selected coefficient box.

theorem TrilinearHT.Auto.coefficientBox_partial_sum_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (hn : 0 < n) (b : Module.Basis (Fin n) ℝ E) (z : Fin n → ℤ) (hz : ∀ i ∉ latticeBoxIndices b, z i = 0) (hbound : ∀ i ∈ latticeBoxIndices b, |z i| ≤ latticeBoxSideLength b i) (s : Finset (Fin n)) : ‖∑ i ∈ s, z i • b i‖ ≤ 1 / 4

Every partial coordinate sum in the selected coefficient box has norm at most 1/4, as required in blueprint lem:lattice-box.

theorem TrilinearHT.Auto.coefficientBox_subset_quarter_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (hn : 0 < n) (b : Module.Basis (Fin n) ℝ E) : integerCoefficientBox b (latticeBoxIndices b) (latticeBoxSideLength b) ⊆ Metric.closedBall 0 (1 / 4)

theorem TrilinearHT.Auto.smallBallCoefficientBox {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (hn : 0 < n) (b : Module.Basis (Fin n) ℝ E) : ∃ (c : Module.Basis (Fin n) ℝ E) (I : Finset (Fin n)) (L : Fin n → ℤ), Submodule.span ℤ (Set.range ⇑c) = Submodule.span ℤ (Set.range ⇑b) ∧ (∀ i ∈ I, 1 ≤ L i) ∧ Metric.closedBall 0 (latticeBoxRadius n) ∩ ↑(Submodule.span ℤ (Set.range ⇑b)) ⊆ integerCoefficientBox c I L ∧ integerCoefficientBox c I L ⊆ Metric.closedBall 0 (1 / 4) ∧ ∀ (z : Fin n → ℤ), (∀ i ∉ I, z i = 0) → (∀ i ∈ I, |z i| ≤ L i) → ∀ (s : Finset (Fin n)), ‖∑ i ∈ s, z i • c i‖ ≤ 1 / 4

Blueprint lem:lattice-box, complete statement: a part of a lattice basis with positive integer side lengths contains the closed radius (100d)^(-10d) lattice ball and lies in the closed radius 1/4 ball; every partial coordinate sum satisfies the same outer bound.

@[reducible, inline]

abbrev TrilinearHT.Auto.StandardTorus (d : ℕ) : Type

The standard real torus used in blueprint lem:torus-annihilator.

Equations

• TrilinearHT.Auto.StandardTorus d = (Fin d → AddCircle 1)

noncomputable def TrilinearHT.Auto.torusEvaluation {d : ℕ} (x : StandardTorus d) : (Fin d → ℤ) →ₗ[ℤ] AddCircle 1

Evaluation of an integer frequency at a torus point, before exponentiation.

Equations

• TrilinearHT.Auto.torusEvaluation x = ((Pi.basisFun ℤ (Fin d)).constr ℤ) x

noncomputable def TrilinearHT.Auto.torusPairing {d : ℕ} (n : Fin d → ℤ) (x : StandardTorus d) : AddCircle 1

Pair an integer character with a point of the standard torus.

Equations

• TrilinearHT.Auto.torusPairing n x = (TrilinearHT.Auto.torusEvaluation x) n

theorem TrilinearHT.Auto.torusPairing_eq_sum {d : ℕ} (n : Fin d → ℤ) (x : StandardTorus d) : torusPairing n x = ∑ i : Fin d, n i • x i

noncomputable def TrilinearHT.Auto.torusPairingMap {d : ℕ} (n : Fin d → ℤ) : StandardTorus d →ₗ[ℤ] AddCircle 1

Integer-linear character pairing on the standard torus.

Equations

• TrilinearHT.Auto.torusPairingMap n = { toFun := TrilinearHT.Auto.torusPairing n, map_add' := ⋯, map_smul' := ⋯ }

theorem TrilinearHT.Auto.continuous_torusPairing {d : ℕ} (n : Fin d → ℤ) : Continuous (torusPairing n)

noncomputable def TrilinearHT.Auto.torusAnnihilator {d : ℕ} (L : Submodule ℤ (Fin d → ℤ)) : Submodule ℤ (StandardTorus d)

The subgroup annihilating all frequencies in an integer submodule.

Equations

• TrilinearHT.Auto.torusAnnihilator L = ⨅ (n : ↥L), (TrilinearHT.Auto.torusPairingMap ↑n).ker

theorem TrilinearHT.Auto.mem_torusAnnihilator {d : ℕ} (L : Submodule ℤ (Fin d → ℤ)) (x : StandardTorus d) : x ∈ torusAnnihilator L ↔ ∀ n ∈ L, torusPairing n x = 0

noncomputable def TrilinearHT.Auto.torusBasisEquiv {d : ℕ} (b : Module.Basis (Fin d) ℤ (Fin d → ℤ)) : StandardTorus d ≃ₗ[ℤ] StandardTorus d

An integer basis acts on the torus by evaluating its basis frequencies.

Equations

• TrilinearHT.Auto.torusBasisEquiv b = (Pi.basisFun ℤ (Fin d)).constr ℤ ≪≫ₗ (b.constr ℤ).symm

theorem TrilinearHT.Auto.torusBasisEquiv_apply {d : ℕ} (b : Module.Basis (Fin d) ℤ (Fin d → ℤ)) (x : StandardTorus d) (i : Fin d) : (torusBasisEquiv b) x i = torusPairing (b i) x

theorem TrilinearHT.Auto.torusBasisEquiv_symm_apply {d : ℕ} (b : Module.Basis (Fin d) ℤ (Fin d → ℤ)) (x : StandardTorus d) (i : Fin d) : (torusBasisEquiv b).symm x i = ∑ j : Fin d, (b.repr ((Pi.basisFun ℤ (Fin d)) i)) j • x j

theorem TrilinearHT.Auto.continuous_torusBasisEquiv {d : ℕ} (b : Module.Basis (Fin d) ℤ (Fin d → ℤ)) : Continuous ⇑(torusBasisEquiv b)

theorem TrilinearHT.Auto.continuous_torusBasisEquiv_symm {d : ℕ} (b : Module.Basis (Fin d) ℤ (Fin d → ℤ)) : Continuous ⇑(torusBasisEquiv b).symm

theorem TrilinearHT.Auto.torusAnnihilator_basis_coordinates {d r : ℕ} (L : Submodule ℤ (Fin d → ℤ)) (b : Module.Basis (Fin d) ℤ (Fin d → ℤ)) (hb : Submodule.span ℤ (⇑b '' {i : Fin d | ↑i < r}) = L) (x : StandardTorus d) : x ∈ torusAnnihilator L ↔ ∀ (i : Fin d), ↑i < r → (torusBasisEquiv b) x i = 0

Blueprint lem:torus-annihilator, line 358: an adapted integer basis turns annihilation by its first basis vectors into zero coordinate conditions.

def TrilinearHT.Auto.coordinateTorus (d r : ℕ) : Submodule ℤ (StandardTorus d)

The coordinate torus with its first r coordinates equal to zero.

Equations

• TrilinearHT.Auto.coordinateTorus d r = { carrier := {x : TrilinearHT.Auto.StandardTorus d | ∀ (i : Fin d), ↑i < r → x i = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

noncomputable def TrilinearHT.Auto.coordinateTorusTailEquiv (d r : ℕ) : ↥(coordinateTorus d r) ≃ₗ[ℤ] { i : Fin d // r ≤ ↑i } → AddCircle 1

Identify the coordinate subtorus with its unrestricted tail coordinates.

Equations

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

theorem TrilinearHT.Auto.continuous_coordinateTorusTailEquiv (d r : ℕ) : Continuous ⇑(coordinateTorusTailEquiv d r)

theorem TrilinearHT.Auto.continuous_coordinateTorusTailEquiv_symm (d r : ℕ) : Continuous ⇑(coordinateTorusTailEquiv d r).symm

noncomputable def TrilinearHT.Auto.coordinateTorusTailHomeomorph (d r : ℕ) : ↥(coordinateTorus d r) ≃ₜ ({ i : Fin d // r ≤ ↑i } → AddCircle 1)

Homeomorphism identifying the coordinate subtorus with its tail coordinates.

Equations

• TrilinearHT.Auto.coordinateTorusTailHomeomorph d r = { toEquiv := (TrilinearHT.Auto.coordinateTorusTailEquiv d r).toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

noncomputable def TrilinearHT.Auto.torusAnnihilatorCoordinateEquiv {d r : ℕ} (L : Submodule ℤ (Fin d → ℤ)) (b : Module.Basis (Fin d) ℤ (Fin d → ℤ)) (hb : Submodule.span ℤ (⇑b '' {i : Fin d | ↑i < r}) = L) : ↥(torusAnnihilator L) ≃ₗ[ℤ] ↥(coordinateTorus d r)

Identify a lattice annihilator with a coordinate subtorus using the chosen integer basis.

Equations

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

noncomputable def TrilinearHT.Auto.torusAnnihilatorCoordinateHomeomorph {d r : ℕ} (L : Submodule ℤ (Fin d → ℤ)) (b : Module.Basis (Fin d) ℤ (Fin d → ℤ)) (hb : Submodule.span ℤ (⇑b '' {i : Fin d | ↑i < r}) = L) : ↥(torusAnnihilator L) ≃ₜ ↥(coordinateTorus d r)

Topological identification of a lattice annihilator with its coordinate subtorus.

Equations

• TrilinearHT.Auto.torusAnnihilatorCoordinateHomeomorph L b hb = { toEquiv := (TrilinearHT.Auto.torusAnnihilatorCoordinateEquiv L b hb).toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem TrilinearHT.Auto.saturatedAnnihilator_is_torus {d : ℕ} (L : Submodule ℤ (Fin d → ℤ)) (hL : IntegerSaturated L) : ∃ r ≤ d, Nonempty (↥(torusAnnihilator L) ≃ₗ[ℤ] { i : Fin d // r ≤ ↑i } → AddCircle 1) ∧ Nonempty (↥(torusAnnihilator L) ≃ₜ ({ i : Fin d // r ≤ ↑i } → AddCircle 1))

Blueprint lem:torus-annihilator: every saturated annihilator is isomorphic and homeomorphic to a finite product of circles.

theorem TrilinearHT.Auto.torusAnnihilator_isClosed {d : ℕ} (L : Submodule ℤ (Fin d → ℤ)) : IsClosed ↑(torusAnnihilator L)

instance TrilinearHT.Auto.torusAnnihilator_compactSpace {d : ℕ} (L : Submodule ℤ (Fin d → ℤ)) : CompactSpace ↥(torusAnnihilator L)

noncomputable def TrilinearHT.Auto.torusAnnihilatorHaar {d : ℕ} (L : Submodule ℤ (Fin d → ℤ)) : MeasureTheory.Measure ↥(torusAnnihilator L)

Haar probability on the compact annihilator subgroup.

Equations

• TrilinearHT.Auto.torusAnnihilatorHaar L = MeasureTheory.Measure.addHaarMeasure { carrier := Set.univ, isCompact' := ⋯, interior_nonempty' := ⋯ }

instance TrilinearHT.Auto.torusAnnihilatorHaar_isAddHaar {d : ℕ} (L : Submodule ℤ (Fin d → ℤ)) : (torusAnnihilatorHaar L).IsAddHaarMeasure

instance TrilinearHT.Auto.torusAnnihilatorHaar_probability {d : ℕ} (L : Submodule ℤ (Fin d → ℤ)) : MeasureTheory.IsProbabilityMeasure (torusAnnihilatorHaar L)

noncomputable def TrilinearHT.Auto.torusCharacter {d : ℕ} (n : Fin d → ℤ) (x : StandardTorus d) : ℂ

The character exp(2πi n·x) on the standard torus.

Equations

• TrilinearHT.Auto.torusCharacter n x = (fourier 1) (TrilinearHT.Auto.torusPairing n x)

theorem TrilinearHT.Auto.torusPairing_basis_inverse {d : ℕ} (b : Module.Basis (Fin d) ℤ (Fin d → ℤ)) (n : Fin d → ℤ) (y : StandardTorus d) : torusPairing n ((torusBasisEquiv b).symm y) = ∑ i : Fin d, (b.repr n) i • y i

theorem TrilinearHT.Auto.saturatedAnnihilator_half_period {d : ℕ} (L : Submodule ℤ (Fin d → ℤ)) (hL : IntegerSaturated L) {n : Fin d → ℤ} (hn : n ∉ L) : ∃ (x : ↥(torusAnnihilator L)), torusPairing n ↑x = ↑(1 / 2)

A frequency outside a saturated integer submodule has a half-period on its annihilator, giving the cancellation needed for its Haar integral.

theorem TrilinearHT.Auto.torusCharacter_add_half_period {d : ℕ} (n : Fin d → ℤ) {a : StandardTorus d} (ha : torusPairing n a = ↑(1 / 2)) (x : StandardTorus d) : torusCharacter n (x + a) = -torusCharacter n x

theorem TrilinearHT.Auto.saturatedAnnihilator_character_integral {d : ℕ} (L : Submodule ℤ (Fin d → ℤ)) (hL : IntegerSaturated L) (n : Fin d → ℤ) : ∫ (x : ↥(torusAnnihilator L)), torusCharacter n ↑x ∂torusAnnihilatorHaar L = if n ∈ L then 1 else 0

Blueprint lem:torus-annihilator: the Haar integral of a torus character over the annihilator of a saturated lattice is exactly its membership indicator.

theorem TrilinearHT.Auto.rationalAnnihilator_character_integral {d : ℕ} (V : Submodule ℚ (Fin d → ℚ)) (n : Fin d → ℤ) : ∫ (x : ↥(torusAnnihilator (rationalIntegerIntersection V))), torusCharacter n ↑x ∂torusAnnihilatorHaar (rationalIntegerIntersection V) = if n ∈ rationalIntegerIntersection V then 1 else 0

theorem TrilinearHT.Auto.saturatedAnnihilator_zsmul_surjective {d : ℕ} (L : Submodule ℤ (Fin d → ℤ)) (hL : IntegerSaturated L) {k : ℤ} (hk : k ≠ 0) : Function.Surjective fun (x : ↥(torusAnnihilator L)) => k • x

Nonzero integer multiplication is onto every saturated annihilator torus.

def TrilinearHT.Auto.progressionPairHom (G : Type u_1) [AddCommGroup G] (i j l : ℤ) : G × G →+ G × G

The two-coordinate progression map from blueprint lem:torus-annihilator.

Equations

• TrilinearHT.Auto.progressionPairHom G i j l = { toFun := fun (x : G × G) => (x.1 + (i - l) • x.2, x.1 + (j - l) • x.2), map_zero' := ⋯, map_add' := ⋯ }

theorem TrilinearHT.Auto.progressionPairHom_surjective {G : Type u_1} [AddCommGroup G] (hdiv : ∀ (k : ℤ), k ≠ 0 → Function.Surjective fun (x : G) => k • x) {i j : ℤ} (hij : i ≠ j) (l : ℤ) : Function.Surjective ⇑(progressionPairHom G i j l)

theorem TrilinearHT.Auto.saturatedAnnihilator_progression_surjective {d : ℕ} (L : Submodule ℤ (Fin d → ℤ)) (hL : IntegerSaturated L) {i j : ℤ} (hij : i ≠ j) (l : ℤ) : Function.Surjective ⇑(progressionPairHom (↥(torusAnnihilator L)) i j l)

theorem TrilinearHT.Auto.continuous_progressionPairHom {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (i j l : ℤ) : Continuous ⇑(progressionPairHom G i j l)

theorem TrilinearHT.Auto.saturatedAnnihilator_progression_measurePreserving {d : ℕ} (L : Submodule ℤ (Fin d → ℤ)) (hL : IntegerSaturated L) {i j : ℤ} (hij : i ≠ j) (l : ℤ) : MeasureTheory.MeasurePreserving (⇑(progressionPairHom (↥(torusAnnihilator L)) i j l)) ((torusAnnihilatorHaar L).prod (torusAnnihilatorHaar L)) ((torusAnnihilatorHaar L).prod (torusAnnihilatorHaar L))

Blueprint lem:torus-annihilator: the progression pair map preserves the product of the annihilator's Haar probabilities.

theorem TrilinearHT.Auto.rationalAnnihilator_progression_measurePreserving {d : ℕ} (V : Submodule ℚ (Fin d → ℚ)) {i j : ℤ} (hij : i ≠ j) (l : ℤ) : MeasureTheory.MeasurePreserving (⇑(progressionPairHom (↥(torusAnnihilator (rationalIntegerIntersection V))) i j l)) ((torusAnnihilatorHaar (rationalIntegerIntersection V)).prod (torusAnnihilatorHaar (rationalIntegerIntersection V))) ((torusAnnihilatorHaar (rationalIntegerIntersection V)).prod (torusAnnihilatorHaar (rationalIntegerIntersection V)))