Coordinate induction extends the contour-shift identity to unit-cube integrals.

def KamProject.Arnold1963.complexShift {n : ℕ} (y x : RealSpace n) : ComplexSpace n

A real coordinate vector shifted in the imaginary direction by another real vector.

Equations

• KamProject.Arnold1963.complexShift y x j = ↑(x j) + ↑(y j) * Complex.I

@[simp]

theorem KamProject.Arnold1963.complexShift_zero {n : ℕ} (x : RealSpace n) : complexShift 0 x = complexify x

@[simp]

theorem KamProject.Arnold1963.complexShift_cons {n : ℕ} (y : RealSpace (n + 1)) (x : ℝ) (t : RealSpace n) : complexShift y (Fin.cons x t) = Fin.cons (↑x + ↑(y 0) * Complex.I) (complexShift (Fin.tail y) t)

theorem KamProject.Arnold1963.complexShift_mem_strip {n : ℕ} {r : NNReal} (y x : RealSpace n) (hy : ∀ (j : Fin n), |y j| ≤ ↑r) : complexShift y x ∈ angleStrip n r

theorem KamProject.Arnold1963.continuous_shift_slice {n : ℕ} {r : NNReal} {f : ComplexSpace n → ℂ} (hf : ContinuousOn f (angleStrip n r)) (y : RealSpace n) (hy : ∀ (j : Fin n), |y j| ≤ ↑r) : Continuous fun (x : RealSpace n) => f (complexShift y x)

theorem KamProject.Arnold1963.integral_cons_horizontal_shift {n : ℕ} {r : NNReal} {f : ComplexSpace (n + 1) → ℂ} (hf : AnalyticOnNhd ℂ f (angleStrip (n + 1) r)) (hp : ∀ q ∈ angleStrip (n + 1) r, ∀ (j : Fin (n + 1)), f (Function.update q j (q j + 1)) = f q) {q : ComplexSpace n} (hq : q ∈ angleStrip n r) {y : ℝ} (hy : |y| ≤ ↑r) : ∫ (x : ℝ), f (Fin.cons (↑x + ↑y * Complex.I) q) ∂unitIntervalMeasure = ∫ (x : ℝ), f (Fin.cons (↑x) q) ∂unitIntervalMeasure

theorem KamProject.Arnold1963.unitCubeIntegral_shift_eq {n : ℕ} {r : NNReal} {f : ComplexSpace n → ℂ} (hf : AnalyticOnNhd ℂ f (angleStrip n r)) (hp : ∀ q ∈ angleStrip n r, ∀ (j : Fin n), f (Function.update q j (q j + 1)) = f q) (y : RealSpace n) (hy : ∀ (j : Fin n), |y j| ≤ ↑r) : (unitCubeIntegral fun (x : RealSpace n) => f (complexShift y x)) = unitCubeIntegral fun (x : RealSpace n) => f (complexify x)