One-variable contour shifts and exponential decay bounds for normalized Fourier integrals.

theorem KamProject.Arnold1963.integral_horizontal_shift {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (T a b : ℝ) (hf : DifferentiableOn ℂ f (Set.uIcc 0 T ×ℂ Set.uIcc a b)) (hperiod : ∀ y ∈ Set.uIcc a b, f (↑T + ↑y * Complex.I) = f (↑y * Complex.I)) : ∫ (x : ℝ) in 0..T, f (↑x + ↑a * Complex.I) = ∫ (x : ℝ) in 0..T, f (↑x + ↑b * Complex.I)

theorem KamProject.Arnold1963.integral_fourier_horizontal_shift (f : ℂ → ℂ) (k : ℤ) (y : ℝ) (hf : DifferentiableOn ℂ f (Set.uIcc 0 (2 * Real.pi) ×ℂ Set.uIcc 0 y)) (hperiod : ∀ t ∈ Set.uIcc 0 y, f (↑(2 * Real.pi) + ↑t * Complex.I) = f (↑t * Complex.I)) : ∫ (x : ℝ) in 0..2 * Real.pi, f ↑x * Complex.exp (-Complex.I * ↑k * ↑x) = ∫ (x : ℝ) in 0..2 * Real.pi, f (↑x + ↑y * Complex.I) * Complex.exp (-Complex.I * ↑k * (↑x + ↑y * Complex.I))

theorem KamProject.Arnold1963.norm_integral_fourier_le_on_shift (f : ℂ → ℂ) (k : ℤ) (y M : ℝ) (hf : DifferentiableOn ℂ f (Set.uIcc 0 (2 * Real.pi) ×ℂ Set.uIcc 0 y)) (hperiod : ∀ t ∈ Set.uIcc 0 y, f (↑(2 * Real.pi) + ↑t * Complex.I) = f (↑t * Complex.I)) (hbound : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), ‖f (↑x + ↑y * Complex.I)‖ ≤ M) : ‖∫ (x : ℝ) in 0..2 * Real.pi, f ↑x * Complex.exp (-Complex.I * ↑k * ↑x)‖ ≤ M * Real.exp (↑k * y) * (2 * Real.pi)

theorem KamProject.Arnold1963.norm_normalized_fourierIntegral_le (f : ℂ → ℂ) (k : ℤ) {ρ M : ℝ} (hρ : 0 ≤ ρ) (hf : DifferentiableOn ℂ f {z : ℂ | |z.im| ≤ ρ}) (hperiod : ∀ (z : ℂ), |z.im| ≤ ρ → f (z + ↑(2 * Real.pi)) = f z) (hbound : ∀ (z : ℂ), |z.im| ≤ ρ → ‖f z‖ ≤ M) : ‖(∫ (x : ℝ) in 0..2 * Real.pi, f ↑x * Complex.exp (-Complex.I * ↑k * ↑x)) / ↑(2 * Real.pi)‖ ≤ M * Real.exp (-|↑k| * ρ)