Kronecker's theorem for linear flows on tori

For a finite index type ι, a line t ↦ θ + t ν in the torus (ℝ / pℤ)^ι is an orbit of a linear flow. Its velocity ν is nonresonant if no nonzero integer vector k satisfies ∑ i, k i * ν i = 0. Kronecker's theorem (TauCeti.AddCircle.denseRange_coe_add_mul_iff) states that the line is dense exactly when ν is nonresonant. For a resonance k, the character x ↦ exp (2πi ⟪k, x⟫ / p) is constant along the line but not on the torus, so the line is not dense.

Density of a nonresonant line follows from Weyl's equidistribution theorem for linear flows (TauCeti.UnitAddTorus.tendsto_inv_smul_intervalIntegral): on the unit torus, the time averages T⁻¹ ∫₀ᵀ f (θ + t ν) dt of a continuous function f tend to its integral ∫ f. For a monomial mFourier n this is a direct computation: along the line it is a constant multiple of t ↦ exp (2πi ⟪n, ν⟫ t) (TauCeti.UnitAddTorus.mFourier_coe_add_mul), and its integral vanishes for n ≠ 0 (TauCeti.UnitAddTorus.integral_mFourier). It extends to every continuous function because the trigonometric polynomials are uniformly dense. A continuous bump function supported in an open set missed by the line has positive integral but vanishing time averages, so no such open set exists.

These statements decide when an orbit of a completely integrable system, which is a line on an invariant torus in action–angle coordinates, fills that torus densely.

Main results

• TauCeti.UnitAddTorus.integral_mFourier: ∫ mFourier n is 1 for n = 0 and 0 otherwise.
• TauCeti.UnitAddTorus.tendsto_inv_smul_intervalIntegral: Weyl's theorem, time averages along a nonresonant line tend to the space average.
• TauCeti.AddCircle.denseRange_coe_add_mul_iff: Kronecker's theorem, a line in (ℝ / pℤ)^ι is dense exactly when its velocity is nonresonant.

References

• H. Weyl, Über die Gleichverteilung von Zahlen mod. Eins, Mathematische Annalen 77 (1916), 313–352.
• V. I. Arnold, Mathematical Methods of Classical Mechanics, second edition, Graduate Texts in Mathematics 60, Springer, 1989, Section 51 (time and space averages on the torus).

@[simp]

theorem TauCeti.UnitAddTorus.integral_mFourier {d : Type u_1} [Fintype d] (n : d → ℤ) : ∫ (x : UnitAddTorus d), (UnitAddTorus.mFourier n) x = if n = 0 then 1 else 0

The integral of the monomial mFourier n over the unit torus is 1 for n = 0 and 0 otherwise.

theorem TauCeti.UnitAddTorus.mFourier_coe_add_mul {d : Type u_1} [Fintype d] (n : d → ℤ) (θ ν : d → ℝ) (t : ℝ) : ((UnitAddTorus.mFourier n) fun (i : d) => ↑(θ i + ν i * t)) = Complex.exp (2 * ↑Real.pi * Complex.I * ∑ i : d, ↑(n i) * ↑(θ i)) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑(∑ i : d, ↑(n i) * ν i) * ↑t)

Along the line t ↦ θ + t ν of the unit torus, the monomial mFourier n is the product of its value at θ with the exponential exp (2πi ⟪n, ν⟫ t).

theorem TauCeti.UnitAddTorus.tendsto_inv_smul_intervalIntegral {d : Type u_1} [Fintype d] {ν : d → ℝ} (hν : ∀ (k : d → ℤ), ∑ i : d, ↑(k i) * ν i = 0 → k = 0) (θ : d → ℝ) (f : C(UnitAddTorus d, ℂ)) : Filter.Tendsto (fun (T : ℝ) => T⁻¹ • ∫ (t : ℝ) in 0..T, f fun (i : d) => ↑(θ i + ν i * t)) Filter.atTop (nhds (∫ (x : UnitAddTorus d), f x))

Weyl's equidistribution theorem for linear flows. If the velocity ν is nonresonant, that is ⟪k, ν⟫ ≠ 0 for every nonzero k ∈ ℤ^d, then along every line t ↦ θ + t ν of the unit torus the time averages T⁻¹ ∫₀ᵀ f (θ + t ν) dt of a continuous function f tend to its space average ∫ f.

theorem TauCeti.AddCircle.denseRange_coe_add_mul_iff {ι : Type u_1} [Fintype ι] {p : ℝ} (hp : p ≠ 0) (θ ν : ι → ℝ) : (DenseRange fun (t : ℝ) (i : ι) => ↑(θ i + ν i * t)) ↔ ∀ (k : ι → ℤ), ∑ i : ι, ↑(k i) * ν i = 0 → k = 0

Kronecker's theorem for linear flows on tori. A line t ↦ θ + t ν in the torus (ℝ / pℤ)^ι is dense exactly when its velocity ν is nonresonant: ∑ i, k i * ν i ≠ 0 for every nonzero integer vector k.