Algebraic foundations for the uniform Kronecker lemma

This file isolates the exact (non-quantitative) character-extension argument used in the paper. The remaining quantitative statement is developed on top of these declarations.

def Wallace.relationMap {G : Type u} [AddCommGroup G] {m : ℕ} (z : Fin m → G) : (Fin m → ℤ) →+ G

The homomorphism which evaluates an integer relation on a finite tuple.

Equations

• Wallace.relationMap z = { toFun := fun (a : Fin m → ℤ) => ∑ i : Fin m, a i • z i, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Wallace.relationMap_single {G : Type u} [AddCommGroup G] {m : ℕ} (z : Fin m → G) (i : Fin m) : (relationMap z) (Pi.single i 1) = z i

def Wallace.torusRelationMap {m : ℕ} (t : Fin m → UnitAddCircle) : (Fin m → ℤ) →+ UnitAddCircle

Evaluation of an integer vector on a tuple in the unit additive torus.

Equations

• Wallace.torusRelationMap t = Wallace.relationMap t

@[simp]

theorem Wallace.torusRelationMap_single {m : ℕ} (t : Fin m → UnitAddCircle) (i : Fin m) : (torusRelationMap t) (Pi.single i 1) = t i

@[reducible, inline]

abbrev Wallace.relationGroup {G : Type u} [AddCommGroup G] {m : ℕ} (z : Fin m → G) : AddSubgroup (Fin m → ℤ)

The subgroup of integer relations on a tuple.

Equations

• Wallace.relationGroup z = (Wallace.relationMap z).ker

def Wallace.RespectsRelations {G : Type u} [AddCommGroup G] {m : ℕ} (z : Fin m → G) (t : Fin m → UnitAddCircle) : Prop

A target tuple respects every relation of z.

Equations

• Wallace.RespectsRelations z t = ((Wallace.relationMap z).ker ≤ (Wallace.torusRelationMap t).ker)

theorem Wallace.respectsRelations_iff {G : Type u} [AddCommGroup G] {m : ℕ} (z : Fin m → G) (t : Fin m → UnitAddCircle) : RespectsRelations z t ↔ ∀ (a : Fin m → ℤ), ∑ i : Fin m, a i • z i = 0 → ∑ i : Fin m, a i • t i = 0

def Wallace.intVectorHeight {m : ℕ} (a : Fin m → ℤ) : ℕ

Supremum norm (height) of an integer vector with finite index type.

Equations

• Wallace.intVectorHeight a = Finset.univ.sup fun (i : Fin m) => (a i).natAbs

theorem Wallace.natAbs_le_intVectorHeight {m : ℕ} (a : Fin m → ℤ) (i : Fin m) : (a i).natAbs ≤ intVectorHeight a

def Wallace.RespectsRelationsUpTo {G : Type u} [AddCommGroup G] {m : ℕ} (q : ℕ) (z : Fin m → G) (t : Fin m → UnitAddCircle) : Prop

A target tuple respects all relations of height at most q.

Equations

• Wallace.RespectsRelationsUpTo q z t = ∀ (a : Fin m → ℤ), Wallace.intVectorHeight a ≤ q → (Wallace.relationMap z) a = 0 → (Wallace.torusRelationMap t) a = 0

def Wallace.IsUniformKroneckerBound (m : ℕ) (ε : ℝ) (q : ℕ) : Prop

q is a uniform Kronecker bound for tuples of length m and error ε.

Equations

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

noncomputable def Wallace.homOnTupleRange {G : Type u} [AddCommGroup G] {m : ℕ} (z : Fin m → G) (t : Fin m → UnitAddCircle) (h : RespectsRelations z t) : ↥(relationMap z).range →+ UnitAddCircle

A target which respects all relations defines a homomorphism on the range generated by the tuple.

Equations

• Wallace.homOnTupleRange z t h = ((Wallace.relationMap z).rangeRestrict.liftOfRightInverse (Function.surjInv ⋯) ⋯) ⟨Wallace.torusRelationMap t, ⋯⟩

theorem Wallace.homOnTupleRange_comp {G : Type u} [AddCommGroup G] {m : ℕ} (z : Fin m → G) (t : Fin m → UnitAddCircle) (h : RespectsRelations z t) : (homOnTupleRange z t h).comp (relationMap z).rangeRestrict = torusRelationMap t

theorem Wallace.exists_character_of_respectsRelations {G : Type u} [AddCommGroup G] {m : ℕ} (z : Fin m → G) (t : Fin m → UnitAddCircle) (h : RespectsRelations z t) : ∃ (χ : G →+ UnitAddCircle), ∀ (i : Fin m), χ (z i) = t i

Exact finite Kronecker extension: a target tuple which respects all integer relations is the restriction of a character of the ambient Abelian group.

Algebraic separation into the real unit circle

noncomputable def Wallace.rationalCircleToUnit : AddCircle 1 →+ UnitAddCircle

The embedding of the rational additive circle into the real additive circle.

Equations

• Wallace.rationalCircleToUnit = QuotientAddGroup.map (AddSubgroup.zmultiples 1) (AddSubgroup.zmultiples 1) (Rat.castHom ℝ).toAddMonoidHom Wallace.rationalCircleToUnit._proof_4

theorem Wallace.rationalCircleToUnit_injective : Function.Injective ⇑rationalCircleToUnit

theorem Wallace.exists_unit_character_apply_ne_zero {A : Type u} [AddCommGroup A] {a : A} (ha : a ≠ 0) : ∃ (c : A →+ UnitAddCircle), c a ≠ 0

Characters into the real unit circle separate points of every Abelian group. The CharacterModule theorem supplies a rational-circle character and the preceding embedding changes the codomain without losing its nonzero value.

Relation annihilators and their distance functions

def Wallace.integerAnnihilator {m : ℕ} (R : AddSubgroup (Fin m → ℤ)) : AddSubgroup (UnitAddTorus (Fin m))

The annihilator in the finite torus of a subgroup of integer relations.

Equations

• Wallace.integerAnnihilator R = { carrier := {x : UnitAddTorus (Fin m) | ∀ a ∈ R, (Wallace.torusRelationMap x) a = 0}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

theorem Wallace.isClosed_integerAnnihilator {m : ℕ} (R : AddSubgroup (Fin m → ℤ)) : IsClosed ↑(integerAnnihilator R)

noncomputable def Wallace.annihilatorDistance {m : ℕ} (R : AddSubgroup (Fin m → ℤ)) : BoundedContinuousFunction (UnitAddTorus (Fin m)) ℝ

Distance to the relation annihilator, as a bounded continuous real-valued function.

Equations

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

@[simp]

theorem Wallace.annihilatorDistance_apply {m : ℕ} (R : AddSubgroup (Fin m → ℤ)) (x : UnitAddTorus (Fin m)) : (annihilatorDistance R) x = Metric.infDist x ↑(integerAnnihilator R)

theorem Wallace.annihilatorDistance_lipschitz {m : ℕ} (R : AddSubgroup (Fin m → ℤ)) : LipschitzWith 1 ⇑(annihilatorDistance R)

theorem Wallace.exists_mem_integerAnnihilator_not_annihilate {m : ℕ} (R : AddSubgroup (Fin m → ℤ)) {a : Fin m → ℤ} (ha : a ∉ R) : ∃ x ∈ integerAnnihilator R, (torusRelationMap x) a ≠ 0

The algebraic double-annihilator direction needed below: if an integer vector is not in R, some point of R⁺ detects it.

theorem Wallace.mFourier_eq_toCircle_relation {m : ℕ} (a : Fin m → ℤ) (x : UnitAddTorus (Fin m)) : (UnitAddTorus.mFourier a) x = ↑(AddCircle.toCircle ((torusRelationMap x) a))

def Wallace.complexifyDistanceFunction {m : ℕ} (f : BoundedContinuousFunction (UnitAddTorus (Fin m)) ℝ) : C(UnitAddTorus (Fin m), ℂ)

Regard a bounded real-valued continuous function on the compact torus as a complex-valued continuous function.

Equations

• Wallace.complexifyDistanceFunction f = { toFun := fun (x : UnitAddTorus (Fin m)) => ↑(f x), continuous_toFun := ⋯ }

def Wallace.oneLipschitzHalfRangeFamily (m : ℕ) : Set (BoundedContinuousFunction (UnitAddTorus (Fin m)) ℝ)

The family occurring in the paper's uniform-frequency-set lemma: real-valued functions on the finite torus which are 1-Lipschitz and take their values in [0, 1 / 2].

Equations

• Wallace.oneLipschitzHalfRangeFamily m = {f : BoundedContinuousFunction (UnitAddTorus (Fin m)) ℝ | LipschitzWith 1 ⇑f ∧ ∀ (x : UnitAddTorus (Fin m)), f x ∈ Set.Icc 0 (1 / 2)}

theorem Wallace.isCompact_closure_oneLipschitzHalfRangeFamily (m : ℕ) : IsCompact (closure (oneLipschitzHalfRangeFamily m))

Arzelà--Ascoli compactness for the family in the uniform-frequency-set lemma. We retain the closure in the statement because that is exactly the form supplied by Mathlib's version of Arzelà--Ascoli; membership of the original family is enough for every application below.

theorem Wallace.exists_uniform_frequency_set (m : ℕ) {η : ℝ} (hη : 0 < η) : ∃ (S : Finset (Fin m → ℤ)), ∀ (f : BoundedContinuousFunction (UnitAddTorus (Fin m)) ℝ), LipschitzWith 1 ⇑f → (∀ (x : UnitAddTorus (Fin m)), f x ∈ Set.Icc 0 (1 / 2)) → ∃ (c : (Fin m → ℤ) →₀ ℂ), c.support ⊆ S ∧ ∀ (x : UnitAddTorus (Fin m)), ‖(c.sum fun (a : Fin m → ℤ) (z : ℂ) => z • UnitAddTorus.mFourier a) x - ↑(f x)‖ < η

Uniform finite frequency set (paper, Lemma uniform-frequency-set).

For every dimension and every positive error there is a finite set of integer frequencies such that every real-valued 1-Lipschitz function with values in [0, 1 / 2] is uniformly approximated by a trigonometric polynomial supported on that same set. The paper assumes 1 ≤ m; the formal statement is slightly stronger, since it also holds for m = 0.

theorem Wallace.exists_finite_frequency_approximation (m : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∃ (S : Finset (Fin m → ℤ)), ∀ (R : AddSubgroup (Fin m → ℤ)), ∃ (c : (Fin m → ℤ) →₀ ℂ), c.support ⊆ S ∧ ∀ (x : UnitAddTorus (Fin m)), ‖(c.sum fun (a : Fin m → ℤ) (z : ℂ) => z • UnitAddTorus.mFourier a) x - ↑((annihilatorDistance R) x)‖ < 2 * δ

Uniform finite Fourier approximation for all annihilator-distance functions of a fixed dimension. Compactness is used only here: it turns the frequency support, initially depending on the subgroup, into one finite set.

Averaging over a relation annihilator

theorem Wallace.infDist_integerAnnihilator_lt_of_finite_relations {m : ℕ} {δ : ℝ} {S : Finset (Fin m → ℤ)} (hS : ∀ (R : AddSubgroup (Fin m → ℤ)), ∃ (c : (Fin m → ℤ) →₀ ℂ), c.support ⊆ S ∧ ∀ (x : UnitAddTorus (Fin m)), ‖(c.sum fun (a : Fin m → ℤ) (z : ℂ) => z • UnitAddTorus.mFourier a) x - ↑((annihilatorDistance R) x)‖ < 2 * δ) (R : AddSubgroup (Fin m → ℤ)) (t : UnitAddTorus (Fin m)) (ht : ∀ a ∈ S, a ∈ R → (torusRelationMap t) a = 0) : Metric.infDist t ↑(integerAnnihilator R) ≤ 4 * δ

A target satisfying all frequencies in c.support is close to the corresponding annihilator. This is the quantitative conclusion extracted from the averaged finite Fourier approximation.

theorem Wallace.IsUniformKroneckerBound.mono {m q q' : ℕ} {ε : ℝ} (h : IsUniformKroneckerBound m ε q) (hqq' : q ≤ q') : IsUniformKroneckerBound m ε q'

A uniform Kronecker bound remains valid when the permitted relation height is increased.

theorem Wallace.exists_uniform_kronecker_bound (m : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ (q : ℕ), IsUniformKroneckerBound m ε q

Unconditional uniform finite-dimensional Kronecker theorem.

For every tuple length and every positive error, a single finite height bound detects enough integer relations to guarantee approximation by a character of every Abelian group.

theorem Wallace.exists_uniformKroneckerBound (m : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ (q : ℕ), IsUniformKroneckerBound m ε q

Camel-case compatibility spelling for downstream modules.