Reconstruction of the original analytic phase function and bounds for its Fourier remainder.

theorem KamProject.Arnold1963.angleScale_normalize {n : ℕ} (q : ComplexSpace n) : (angleScale n) (complexShift (fun (j : Fin n) => (q j).im / (2 * Real.pi)) fun (j : Fin n) => (q j).re / (2 * Real.pi)) = q

theorem KamProject.Arnold1963.imagPart_shift_zero {n : ℕ} (y t : RealSpace n) : imagPart ((angleScale n) (complexShift y 0)) = imagPart ((angleScale n) (complexShift y t))

theorem KamProject.Arnold1963.AnalyticPhaseFunction.hasSum_fourier_on_strip {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {p : ComplexSpace n} (hp : p ∈ G) {σ : NNReal} (hσρ : σ < ρ) {q : ComplexSpace n} (hq : q ∈ angleStrip n σ) : HasSum (fun (k : FourierIndex n) => f.fourierCoeff p k * fourierMonomial k q) (f.toFun (p, q))

theorem KamProject.Arnold1963.AnalyticPhaseFunction.tsum_fourierTerms_apply {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {p : ComplexSpace n} (hp : p ∈ G) {σ : NNReal} (hσρ : σ < ρ) (q : ↑(angleStrip n σ)) : (∑' (k : FourierIndex n), fourierTermOnStrip (f.fourierCoeff p) σ k) q = f.toFun (p, ↑q)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.norm_sub_fourierTruncation_le {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {p : ComplexSpace n} (hp : p ∈ G) (hn : 0 < n) {δ γ N : ℝ} {σ : NNReal} (hδ : 0 < δ) (hsmall : δ ≤ 1 / 12) (hγ : 0 ≤ γ) (hσ : ↑σ ≤ ↑ρ - (δ + γ)) {q : ComplexSpace n} (hq : q ∈ angleStrip n σ) : ‖f.toFun (p, q) - fourierTruncation (f.fourierCoeff p) N q‖ ≤ (2 * ↑n / Real.exp 1) ^ n * f.uniformNorm / δ ^ (n + 1) * Real.exp (-N * γ)

noncomputable def KamProject.Arnold1963.AnalyticPhaseFunction.fourierRemainder {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) (N : ℝ) (z : ComplexPhaseSpace n) : ℂ

The difference between a phase function and its finite Fourier truncation.

Equations

• f.fourierRemainder N z = f.toFun z - KamProject.Arnold1963.fourierTruncation (f.fourierCoeff z.1) N z.2

theorem KamProject.Arnold1963.AnalyticPhaseFunction.normBoundOn_fourierRemainder {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) (hn : 0 < n) {δ γ N : ℝ} {σ : NNReal} (hδ : 0 < δ) (hsmall : δ ≤ 1 / 12) (hγ : 0 ≤ γ) (hσ : ↑σ ≤ ↑ρ - (δ + γ)) : NormBoundOn (f.fourierRemainder N) (phaseDomain G σ) ((2 * ↑n / Real.exp 1) ^ n * f.uniformNorm / δ ^ (n + 1) * Real.exp (-N * γ))