Documentation

LeanPool.PoincareThreeBody.IrrationalTorusFlow

Irrational rotating flows on the two-torus #

The rotating Kepler frequency has the form (ω, -1). When ω is irrational, its flow is dense on the angle torus. This file proves directly that a continuous invariant of that flow is constant, using irrational rotations on a circle.

source
@[reducible, inline]
abbrev LeanPool.PoincareThreeBody.AngleCircle :
Type

The circle with the natural angular period 2π.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev LeanPool.PoincareThreeBody.AngleTorus :
    Type

    The two Delaunay angles.

    Equations
    Instances For
      source
      noncomputable def LeanPool.PoincareThreeBody.rotatingAngleFlow (ω time : ℝ) (angle : AngleTorus) :
      AngleTorus

      Translation by the rotating Kepler frequency (ω, -1) on the angle torus.

      Equations
      Instances For
        source
        theorem LeanPool.PoincareThreeBody.rotatingAngleFlow_zero (ω : ℝ) (angle : AngleTorus) :
        rotatingAngleFlow ω 0 angle = angle
        source
        theorem LeanPool.PoincareThreeBody.rotatingAngleFlow_add (ω first second : ℝ) (angle : AngleTorus) :
        rotatingAngleFlow ω (first + second) angle = rotatingAngleFlow ω second (rotatingAngleFlow ω first angle)
        source
        theorem LeanPool.PoincareThreeBody.denseRange_firstAngle_wholePeriods {ω : ℝ} (hω : Irrational ω) :
        DenseRange fun (n : ℤ) => n • ↑(2 * Real.pi * ω)

        On an irrational rotating Kepler torus, fixing the second angle and advancing through whole rotating periods gives a dense set of first angles.

        source
        theorem LeanPool.PoincareThreeBody.eq_of_same_second_of_rotatingAngleFlow_invariant {ω : ℝ} (hω : Irrational ω) {f : AngleTorus → ℝ} (hf : Continuous f) (hinvariant : ∀ (angle : AngleTorus) (time : ℝ), f (rotatingAngleFlow ω time angle) = f angle) (first second fixedSecond : AngleCircle) :
        f (first, fixedSecond) = f (second, fixedSecond)

        A continuous function invariant under the rotating flow is independent of the first angle when the Kepler frequency is irrational.

        source
        theorem LeanPool.PoincareThreeBody.eq_of_rotatingAngleFlow_invariant {ω : ℝ} (hω : Irrational ω) {f : AngleTorus → ℝ} (hf : Continuous f) (hinvariant : ∀ (angle : AngleTorus) (time : ℝ), f (rotatingAngleFlow ω time angle) = f angle) (first second : AngleTorus) :
        f first = f second

        A continuous invariant of an irrational rotating Kepler flow is constant on the entire two-torus.

        source
        theorem LeanPool.PoincareThreeBody.rotatingAngleFlow_invariant_eq_const {ω : ℝ} (hω : Irrational ω) {f : AngleTorus → ℝ} (hf : Continuous f) (hinvariant : ∀ (angle : AngleTorus) (time : ℝ), f (rotatingAngleFlow ω time angle) = f angle) (base : AngleTorus) :
        f = fun (x : AngleTorus) => f base

        Extensional form: every continuous invariant of an irrational rotating flow is a constant function.

        source
        theorem LeanPool.PoincareThreeBody.eq_of_continuous_family_rotatingAngleFlow_invariant {f : ℝ × AngleTorus → ℝ} (hf : Continuous f) (hinvariant : ∀ (ω : ℝ) (angle : AngleTorus) (time : ℝ), f (ω, rotatingAngleFlow ω time angle) = f (ω, angle)) (ω : ℝ) (first second : AngleTorus) :
        f (ω, first) = f (ω, second)

        For a jointly continuous family of invariants, angle-independence on the dense irrational frequencies extends to every frequency.

        source
        theorem LeanPool.PoincareThreeBody.continuous_family_rotatingAngleFlow_invariant_eq_base {f : ℝ × AngleTorus → ℝ} (hf : Continuous f) (hinvariant : ∀ (ω : ℝ) (angle : AngleTorus) (time : ℝ), f (ω, rotatingAngleFlow ω time angle) = f (ω, angle)) (base : AngleTorus) :
        f = fun (state : ℝ × AngleTorus) => f (state.1, base)

        Extensional form of angle-independence for a continuous family of rotating-flow invariants.

        source
        theorem LeanPool.PoincareThreeBody.Function.Periodic.continuous_lift {f : ℝ → ℝ} {period : ℝ} (hperiodic : Function.Periodic f period) (hcontinuous : Continuous f) :
        Continuous hperiodic.lift

        A continuous periodic real function descends continuously to the corresponding additive circle.

        source
        theorem LeanPool.PoincareThreeBody.eq_of_continuous_two_periods_of_irrational_ratio {f : ℝ → ℝ} {period shift : ℝ} (hcontinuous : Continuous f) (hperiod : Function.Periodic f period) (hshift : Function.Periodic f shift) (hirrational : Irrational (shift / period)) (first second : ℝ) :
        f first = f second

        A continuous real function with an ordinary period and an incommensurable second period is constant.

        source
        theorem LeanPool.PoincareThreeBody.eq_of_continuous_periodic_rotatingFlow_invariant {ω : ℝ} (hω : Irrational ω) {f : ℝ × ℝ → ℝ} (hf : Continuous f) (hmeanPeriod : ∀ (mean periapsis : ℝ), f (mean + 2 * Real.pi, periapsis) = f (mean, periapsis)) (hperiapsisPeriod : ∀ (mean periapsis : ℝ), f (mean, periapsis + 2 * Real.pi) = f (mean, periapsis)) (hinvariant : ∀ (mean periapsis time : ℝ), f (mean + ω * time, periapsis - time) = f (mean, periapsis)) (first second : ℝ × ℝ) :
        f first = f second

        Real-lift form of the irrational two-torus argument: a continuous function, periodic in both angles and invariant under (ω, -1) translation, is constant when ω is irrational.