Coordinate second-derivative bounds and rectangular buffers in complex phase space.

@[reducible, inline]

abbrev KamProject.Arnold1963.phaseBasis {n : ℕ} : Fin n ⊕ Fin n → ComplexPhaseSpace n

The coordinate basis of phase space, with action coordinates preceding angle coordinates.

Equations

• KamProject.Arnold1963.phaseBasis = KamProject.Arnold1963.phaseDirection

theorem KamProject.Arnold1963.norm_phaseBasis {n : ℕ} (j : Fin n ⊕ Fin n) : ‖phaseBasis j‖ = 1

theorem KamProject.Arnold1963.norm_phaseBasis_add_le {n : ℕ} {i j : Fin n ⊕ Fin n} (h : i ≠ j) : ‖phaseBasis i + phaseBasis j‖ ≤ 1

theorem KamProject.Arnold1963.norm_phaseBasis_sub_le {n : ℕ} {i j : Fin n ⊕ Fin n} (h : i ≠ j) : ‖phaseBasis i - phaseBasis j‖ ≤ 1

theorem KamProject.Arnold1963.norm_second_phaseCoordinate_le {n : ℕ} {f : ComplexPhaseSpace n → ℂ} {U : Set (ComplexPhaseSpace n)} {r : NNReal} {M : ℝ} {x : ComplexPhaseSpace n} (hr : 0 < r) (hf : AnalyticOnNhd ℂ f U) (hM : NormBoundOn f U M) (hx : x ∈ erosion U r) (i j : Fin n ⊕ Fin n) : ‖((fderiv ℂ (fderiv ℂ f) x) (phaseBasis i)) (phaseBasis j)‖ ≤ 2 * M / ↑r ^ 2

theorem KamProject.Arnold1963.phaseDomain_buffer_of_neighborhood {n : ℕ} {S T : Set (ComplexSpace n)} {r σ τ : NNReal} (hrσ : r ≤ σ) (hτσ : τ ≤ σ - r) (hST : closedBallNeighborhood S r ⊆ T) : phaseDomain S τ ⊆ erosion (phaseDomain T σ) r