Conjugation and physical angle translation laws for the same selected inverse. No periodicity or real compatibility is required of arbitrary extensions outside the original domain.

noncomputable def KamProject.Arnold1963.phaseShift {n : ℕ} (k : FourierIndex n) (x : ComplexPhaseSpace n) : ComplexSpace n × ComplexSpace n

Translation of phase space by an integer angle-period shift.

Equations

• KamProject.Arnold1963.phaseShift k x = (x.1, x.2 + KamProject.Arnold1963.angleShift k)

theorem KamProject.Arnold1963.phaseShift_eq_add {n : ℕ} (k : FourierIndex n) (x : ComplexPhaseSpace n) : phaseShift k x = x + (0, angleShift k)

theorem KamProject.Arnold1963.phaseShift_mem_phaseDomain {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (k : FourierIndex n) (x : ComplexPhaseSpace n) : phaseShift k x ∈ phaseDomain G ρ ↔ x ∈ phaseDomain G ρ

theorem KamProject.Arnold1963.star_mem_erosion {E : Type u_1} [NormedAddCommGroup E] [StarAddMonoid E] [NormedStarGroup E] {V : Set E} (hc : ∀ x ∈ V, star x ∈ V) {r : NNReal} {x : E} (hx : x ∈ erosion V r) : star x ∈ erosion V r

theorem KamProject.Arnold1963.add_mem_erosion {E : Type u_1} [NormedAddCommGroup E] {V : Set E} {c : E} (hc : ∀ (z : E), z + c ∈ V ↔ z ∈ V) {r : NNReal} {x : E} (hx : x ∈ erosion V r) : x + c ∈ erosion V r

theorem KamProject.Arnold1963.conj_mem_phaseDomain {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (hG : ConjInvariant G) {x : ComplexPhaseSpace n} (hx : x ∈ phaseDomain G ρ) : conjPhase x ∈ phaseDomain G ρ

theorem KamProject.Arnold1963.fderiv_conjPhase {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {V : Set (ComplexPhaseSpace n)} {x : ComplexPhaseSpace n} (ha : AnalyticAt ℂ S x) (hc : ConjCompatibleOn S V) (hx : V ∈ nhds (conjPhase x)) (v : ComplexPhaseSpace n) : (fderiv ℂ S (conjPhase x)) (conjPhase v) = star ((fderiv ℂ S x) v)

theorem KamProject.Arnold1963.gradients_conj {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {V : Set (ComplexPhaseSpace n)} {x : ComplexPhaseSpace n} (ha : AnalyticAt ℂ S x) (hc : ConjCompatibleOn S V) (hx : V ∈ nhds (conjPhase x)) : pGradient S (conjPhase x) = conjVec (pGradient S x) ∧ qGradient S (conjPhase x) = conjVec (qGradient S x)

theorem KamProject.Arnold1963.gradients_periodic {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} (S : AnalyticPhaseFunction n G ρ) (hr : 0 < r) {x : ComplexPhaseSpace n} (hx : x ∈ erosion (phaseDomain G ρ) r) (k : FourierIndex n) : pGradient S.toFun (phaseShift k x) = pGradient S.toFun x ∧ qGradient S.toFun (phaseShift k x) = qGradient S.toFun x