Exponential decay of actual Fourier coefficients, using contour shifts in each coordinate.

noncomputable def KamProject.Arnold1963.angleScale (n : ℕ) : ComplexSpace n →L[ℂ] ComplexSpace n

Complex linear scaling from unit-period coordinates to angles with period 2π.

Equations

• KamProject.Arnold1963.angleScale n = (2 * ↑Real.pi) • ContinuousLinearMap.id ℂ (KamProject.Arnold1963.ComplexSpace n)

@[simp]

theorem KamProject.Arnold1963.angleScale_apply {n : ℕ} (q : ComplexSpace n) (j : Fin n) : (angleScale n) q j = 2 * ↑Real.pi * q j

theorem KamProject.Arnold1963.scaledAngle_eq_angleScale {n : ℕ} (t : RealSpace n) : scaledAngle t = (angleScale n) (complexify t)

noncomputable def KamProject.Arnold1963.normalizedWidth (ρ : NNReal) : NNReal

The strip width after converting angles to unit-period coordinates.

Equations

• KamProject.Arnold1963.normalizedWidth ρ = ⟨↑ρ / (2 * Real.pi), ⋯⟩

theorem KamProject.Arnold1963.angleScale_mem_strip {n : ℕ} {ρ : NNReal} {q : ComplexSpace n} (hq : q ∈ angleStrip n (normalizedWidth ρ)) : (angleScale n) q ∈ angleStrip n ρ

noncomputable def KamProject.Arnold1963.unitFourierWeight {n : ℕ} (k : FourierIndex n) (q : ComplexSpace n) : ℂ

The negative-frequency exponential weight for normalized Fourier integration.

Equations

• KamProject.Arnold1963.unitFourierWeight k q = Complex.exp (-Complex.I * (2 * ↑Real.pi) * KamProject.Arnold1963.indexPairing k q)

theorem KamProject.Arnold1963.analyticAt_unitFourierWeight {n : ℕ} (k : FourierIndex n) (q : ComplexSpace n) : AnalyticAt ℂ (unitFourierWeight k) q

theorem KamProject.Arnold1963.indexPairing_update_one {n : ℕ} (k : FourierIndex n) (q : ComplexSpace n) (j : Fin n) : indexPairing k (Function.update q j (q j + 1)) = indexPairing k q + ↑(k j)

theorem KamProject.Arnold1963.unitFourierWeight_periodic {n : ℕ} (k : FourierIndex n) (q : ComplexSpace n) (j : Fin n) : unitFourierWeight k (Function.update q j (q j + 1)) = unitFourierWeight k q

theorem KamProject.Arnold1963.unitFourierWeight_real {n : ℕ} (k : FourierIndex n) (x : RealSpace n) : unitFourierWeight k (complexify x) = fourierMonomial (-k) (scaledAngle x)

theorem KamProject.Arnold1963.norm_unitFourierWeight_shift {n : ℕ} (k : FourierIndex n) (y x : RealSpace n) : ‖unitFourierWeight k (complexShift y x)‖ = Real.exp (2 * Real.pi * ∑ j : Fin n, ↑(k j) * y j)

theorem KamProject.Arnold1963.angleScale_update_one {n : ℕ} (q : ComplexSpace n) (j : Fin n) : (angleScale n) (Function.update q j (q j + 1)) = (angleScale n) q + angleShift (Pi.single j 1)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.fourierCoeff_eq_unitCubeIntegral {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {p : ComplexSpace n} (hp : p ∈ G) (k : FourierIndex n) : f.fourierCoeff p k = unitCubeIntegral fun (x : RealSpace n) => f.toFun (p, (angleScale n) (complexify x)) * unitFourierWeight k (complexify x)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.norm_fourierCoeff_le_exp {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {p : ComplexSpace n} (hp : p ∈ G) (k : FourierIndex n) : ‖f.fourierCoeff p k‖ ≤ f.uniformNorm * Real.exp (-(indexLength k * ↑ρ))