Real restrictions and descent to the physical angle torus, including representative independence and injectivity on the quotient.

theorem KamProject.Arnold1963.complexifyPhase_shift {n : ℕ} (k : FourierIndex n) (x : RealPhaseCover n) : complexifyPhase (realPhaseShift k x) = phaseShift k (complexifyPhase x)

theorem KamProject.Arnold1963.realPartPhase_shift {n : ℕ} (k : FourierIndex n) (x : ComplexPhaseSpace n) : realPartPhase (phaseShift k x) = realPhaseShift k (realPartPhase x)

noncomputable def KamProject.Arnold1963.generatingRealTransform {n : ℕ} (S : ComplexPhaseSpace n → ℂ) (G : Set (ComplexSpace n)) (ρ r : NNReal) (x : RealPhaseCover n) : RealPhaseCover n

The generating transformation restricted to unwrapped real phase coordinates.

Equations

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

noncomputable def KamProject.Arnold1963.generatingTorusTransform {n : ℕ} (S : ComplexPhaseSpace n → ℂ) (G : Set (ComplexSpace n)) (ρ r : NNReal) (x : RealPhaseSpace n) : RealPhaseSpace n

The generating transformation descended to real angles modulo 2π.

Equations

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

theorem KamProject.Arnold1963.complexifyPhase_mem_generatingTarget {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} (hρ : r + r + r ≤ ρ) {x : RealPhaseCover n} (hx : x.1 ∈ realSlice (erosion G (r + r))) : complexifyPhase x ∈ generatingTarget G (angleStrip n ρ) r

theorem KamProject.Arnold1963.AnalyticPhaseFunction.generatingTransform_real {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} {M : ℝ} (S : AnalyticPhaseFunction n G ρ) (d : GeneratingData S.toFun G (angleStrip n ρ) r M) (hρ : r + r + r ≤ ρ) {x : RealPhaseCover n} (hx : x.1 ∈ realSlice (erosion G (r + r))) : complexifyPhase (generatingRealTransform S.toFun G ρ r x) = generatingTransform S.toFun G (angleStrip n ρ) r (complexifyPhase x)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.generatingRealTransform_mapsTo {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} {M : ℝ} (S : AnalyticPhaseFunction n G ρ) (d : GeneratingData S.toFun G (angleStrip n ρ) r M) (hρ : r + r + r ≤ ρ) {x : RealPhaseCover n} (hx : x.1 ∈ realSlice (erosion G (r + r))) : (generatingRealTransform S.toFun G ρ r x).1 ∈ realSlice G

theorem KamProject.Arnold1963.AnalyticPhaseFunction.generatingRealTransform_shift {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} {M : ℝ} (S : AnalyticPhaseFunction n G ρ) (d : GeneratingData S.toFun G (angleStrip n ρ) r M) (hρ : r + r + r ≤ ρ) {x : RealPhaseCover n} (hx : x.1 ∈ realSlice (erosion G (r + r))) (k : FourierIndex n) : generatingRealTransform S.toFun G ρ r (realPhaseShift k x) = realPhaseShift k (generatingRealTransform S.toFun G ρ r x)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.generatingTorusTransform_projection {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} {M : ℝ} (S : AnalyticPhaseFunction n G ρ) (d : GeneratingData S.toFun G (angleStrip n ρ) r M) (hρ : r + r + r ≤ ρ) {x : RealPhaseCover n} (hx : x.1 ∈ realSlice (erosion G (r + r))) : generatingTorusTransform S.toFun G ρ r (torusProjection x) = torusProjection (generatingRealTransform S.toFun G ρ r x)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.generatingTorusTransform_mapsTo {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} {M : ℝ} (S : AnalyticPhaseFunction n G ρ) (d : GeneratingData S.toFun G (angleStrip n ρ) r M) (hρ : r + r + r ≤ ρ) : Set.MapsTo (generatingTorusTransform S.toFun G ρ r) (realSlice (erosion G (r + r)) ×ˢ Set.univ) (realSlice G ×ˢ Set.univ)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.generatingTorusTransform_injOn {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} {M : ℝ} (S : AnalyticPhaseFunction n G ρ) (d : GeneratingData S.toFun G (angleStrip n ρ) r M) (hρ : r + r + r ≤ ρ) : Set.InjOn (generatingTorusTransform S.toFun G ρ r) (realSlice (erosion G (r + r)) ×ˢ Set.univ)