Complex-line analyticity and convergence of angle derivatives for a fixed action label.

def KamProject.Arnold1963.Iteration.InitialData.lineDomain {n : ℕ} {ρ₀ : NNReal} (q v : ComplexSpace n) : Set ℂ

Complex times for which the indicated affine angle line lies in the common open strip.

Equations

• KamProject.Arnold1963.Iteration.InitialData.lineDomain q v = {t : ℂ | ‖KamProject.Arnold1963.imagPart (q + t • v)‖ < ↑ρ₀ / 3}

theorem KamProject.Arnold1963.Iteration.InitialData.lineDomain_open {n : ℕ} {ρ₀ : NNReal} (q v : ComplexSpace n) : IsOpen (lineDomain q v)

theorem KamProject.Arnold1963.Iteration.InitialData.line_mem_limitPhase {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) {q v : ComplexSpace n} {t : ℂ} (ht : t ∈ lineDomain q v) : (p, q + t • v) ∈ limitPhase b h

theorem KamProject.Arnold1963.Iteration.InitialData.line_uniform {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) (q v : ComplexSpace n) : TendstoUniformlyOn (fun (s : ℕ) (t : ℂ) => cumulative b h s (p, q + t • v)) (fun (t : ℂ) => limitMap b h (p, q + t • v)) Filter.atTop (lineDomain q v)

theorem KamProject.Arnold1963.Iteration.InitialData.line_differentiable {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) (q v : ComplexSpace n) (s : ℕ) : DifferentiableOn ℂ (fun (t : ℂ) => cumulative b h s (p, q + t • v)) (lineDomain q v)

theorem KamProject.Arnold1963.Iteration.InitialData.limitMap_line_analytic {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) (q v : ComplexSpace n) : AnalyticOnNhd ℂ (fun (t : ℂ) => limitMap b h (p, q + t • v)) (lineDomain q v)

theorem KamProject.Arnold1963.Iteration.InitialData.line_derivative_uniform {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) (q v : ComplexSpace n) : TendstoLocallyUniformlyOn (fun (s : ℕ) => deriv fun (t : ℂ) => cumulative b h s (p, q + t • v)) (deriv fun (t : ℂ) => limitMap b h (p, q + t • v)) Filter.atTop (lineDomain q v)

theorem KamProject.Arnold1963.Iteration.InitialData.line_derivative_eq {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) {q v : ComplexSpace n} {t : ℂ} (ht : t ∈ lineDomain q v) (s : ℕ) : deriv (fun (t : ℂ) => cumulative b h s (p, q + t • v)) t = (fderiv ℂ (cumulative b h s) (p, q + t • v)) (0, v)