Density of nonresonant linear torus flows, proved through Fourier coefficients and closure.

@[instance_reducible]

noncomputable def KamProject.Arnold1963.densityUnitCircleMeasureSpace : MeasureTheory.MeasureSpace UnitAddCircle

Normalized Haar measure used in the Fourier proof of orbit density.

Equations

• KamProject.Arnold1963.densityUnitCircleMeasureSpace = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

theorem KamProject.Arnold1963.densityUnitCircleHaar : MeasureTheory.volume.IsAddHaarMeasure

theorem KamProject.Arnold1963.densityUnitCircleProbability : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

def KamProject.Arnold1963.unitTorusLine {n : ℕ} (v : RealSpace n) (t : ℝ) : UnitAddTorus (Fin n)

A uniform rotation on the unit-period real torus.

Equations

• KamProject.Arnold1963.unitTorusLine v t j = ↑(t * v j)

theorem KamProject.Arnold1963.unitTorusLine_add {n : ℕ} (v : RealSpace n) (s t : ℝ) : unitTorusLine v (s + t) = unitTorusLine v s + unitTorusLine v t

theorem KamProject.Arnold1963.mFourier_translate {n : ℕ} (k : FourierIndex n) (x y : UnitAddTorus (Fin n)) : (UnitAddTorus.mFourier k) (x + y) = (UnitAddTorus.mFourier k) x * (UnitAddTorus.mFourier k) y

theorem KamProject.Arnold1963.mFourier_unitTorusLine {n : ℕ} (k : FourierIndex n) (v : RealSpace n) (t : ℝ) : (UnitAddTorus.mFourier k) (unitTorusLine v t) = Complex.exp (2 * ↑Real.pi * Complex.I * ↑t * ↑(∑ j : Fin n, ↑(k j) * v j))

theorem KamProject.Arnold1963.invariant_under_nonresonant_line_constant {n : ℕ} (v : RealSpace n) (hnr : ∀ (k : FourierIndex n), k ≠ 0 → ∑ j : Fin n, ↑(k j) * v j ≠ 0) (f : C(UnitAddTorus (Fin n), ℂ)) (hi : ∀ (t : ℝ) (x : UnitAddTorus (Fin n)), f (unitTorusLine v t + x) = f x) (x y : UnitAddTorus (Fin n)) : f x = f y

theorem KamProject.Arnold1963.denseRange_unitTorusLine {n : ℕ} (v : RealSpace n) (hnr : ∀ (k : FourierIndex n), k ≠ 0 → ∑ j : Fin n, ↑(k j) * v j ≠ 0) : DenseRange (unitTorusLine v)

noncomputable def KamProject.Arnold1963.realTorusLine {n : ℕ} (v q : RealSpace n) (t : ℝ) : RealTorus n

A real-angle trajectory on the torus with period 2π.

Equations

• KamProject.Arnold1963.realTorusLine v q t j = ↑(q j + t * v j)

theorem KamProject.Arnold1963.denseRange_realTorusLine {n : ℕ} (v q : RealSpace n) (hnr : ∀ (k : FourierIndex n), k ≠ 0 → ∑ j : Fin n, ↑(k j) * v j ≠ 0) : DenseRange (realTorusLine v q)