Uniqueness on a fixed source yields conjugation compatibility and angle equivariance.

theorem KamProject.Arnold1963.AnalyticPhaseFunction.conj_generatingTarget {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} (S : AnalyticPhaseFunction n G ρ) {y : ComplexPhaseSpace n} (hy : y ∈ generatingTarget G (angleStrip n ρ) r) : conjPhase y ∈ generatingTarget G (angleStrip n ρ) r

theorem KamProject.Arnold1963.AnalyticPhaseFunction.shift_generatingTarget {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} {y : ComplexPhaseSpace n} (hy : y ∈ generatingTarget G (angleStrip n ρ) r) (k : FourierIndex n) : phaseShift k y ∈ generatingTarget G (angleStrip n ρ) r

theorem KamProject.Arnold1963.AnalyticPhaseFunction.conj_generatingSource {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} (S : AnalyticPhaseFunction n G ρ) {x : ComplexPhaseSpace n} (hx : x ∈ generatingSource G (angleStrip n ρ) r) : conjPhase x ∈ generatingSource G (angleStrip n ρ) r

theorem KamProject.Arnold1963.AnalyticPhaseFunction.shift_generatingSource {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} {x : ComplexPhaseSpace n} (hx : x ∈ generatingSource G (angleStrip n ρ) r) (k : FourierIndex n) : phaseShift k x ∈ generatingSource G (angleStrip n ρ) r

theorem KamProject.Arnold1963.AnalyticPhaseFunction.gradients_conj_on_source {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} {M : ℝ} (S : AnalyticPhaseFunction n G ρ) (d : GeneratingData S.toFun G (angleStrip n ρ) r M) {x : ComplexPhaseSpace n} (hx : x ∈ generatingSource G (angleStrip n ρ) r) : pGradient S.toFun (conjPhase x) = conjVec (pGradient S.toFun x) ∧ qGradient S.toFun (conjPhase x) = conjVec (qGradient S.toFun x)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.input_conj {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} {M : ℝ} (S : AnalyticPhaseFunction n G ρ) (d : GeneratingData S.toFun G (angleStrip n ρ) r M) {x : ComplexPhaseSpace n} (hx : x ∈ generatingSource G (angleStrip n ρ) r) : generatingInput S.toFun (conjPhase x) = conjPhase (generatingInput S.toFun x)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.output_conj {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} {M : ℝ} (S : AnalyticPhaseFunction n G ρ) (d : GeneratingData S.toFun G (angleStrip n ρ) r M) {x : ComplexPhaseSpace n} (hx : x ∈ generatingSource G (angleStrip n ρ) r) : generatingOutput S.toFun (conjPhase x) = conjPhase (generatingOutput S.toFun x)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.input_shift {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} {M : ℝ} (S : AnalyticPhaseFunction n G ρ) (d : GeneratingData S.toFun G (angleStrip n ρ) r M) {x : ComplexPhaseSpace n} (hx : x ∈ generatingSource G (angleStrip n ρ) r) (k : FourierIndex n) : generatingInput S.toFun (phaseShift k x) = phaseShift k (generatingInput S.toFun x)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.output_shift {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} {M : ℝ} (S : AnalyticPhaseFunction n G ρ) (d : GeneratingData S.toFun G (angleStrip n ρ) r M) {x : ComplexPhaseSpace n} (hx : x ∈ generatingSource G (angleStrip n ρ) r) (k : FourierIndex n) : generatingOutput S.toFun (phaseShift k x) = phaseShift k (generatingOutput S.toFun x)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.generatingInverse_conj {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} {M : ℝ} (S : AnalyticPhaseFunction n G ρ) (d : GeneratingData S.toFun G (angleStrip n ρ) r M) {y : ComplexPhaseSpace n} (hy : y ∈ generatingTarget G (angleStrip n ρ) r) : generatingInverse S.toFun G (angleStrip n ρ) r (conjPhase y) = conjPhase (generatingInverse S.toFun G (angleStrip n ρ) r y)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.generatingTransform_conj {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} {M : ℝ} (S : AnalyticPhaseFunction n G ρ) (d : GeneratingData S.toFun G (angleStrip n ρ) r M) {y : ComplexPhaseSpace n} (hy : y ∈ generatingTarget G (angleStrip n ρ) r) : generatingTransform S.toFun G (angleStrip n ρ) r (conjPhase y) = conjPhase (generatingTransform S.toFun G (angleStrip n ρ) r y)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.generatingInverse_shift {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} {M : ℝ} (S : AnalyticPhaseFunction n G ρ) (d : GeneratingData S.toFun G (angleStrip n ρ) r M) {y : ComplexPhaseSpace n} (hy : y ∈ generatingTarget G (angleStrip n ρ) r) (k : FourierIndex n) : generatingInverse S.toFun G (angleStrip n ρ) r (phaseShift k y) = phaseShift k (generatingInverse S.toFun G (angleStrip n ρ) r y)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.generatingTransform_shift {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} {M : ℝ} (S : AnalyticPhaseFunction n G ρ) (d : GeneratingData S.toFun G (angleStrip n ρ) r M) {y : ComplexPhaseSpace n} (hy : y ∈ generatingTarget G (angleStrip n ρ) r) (k : FourierIndex n) : generatingTransform S.toFun G (angleStrip n ρ) r (phaseShift k y) = phaseShift k (generatingTransform S.toFun G (angleStrip n ρ) r y)