Construct the unique small-displacement root of the generating equation from analyticity and uniform bounds.
theorem
KamProject.Arnold1963.generating_ball_buffer
{n : ℕ}
{G U : Set (ComplexSpace n)}
{r : NNReal}
{P Q : ComplexSpace n}
(hP : P ∈ erosion G (r + r))
(hQ : Q ∈ erosion U (r + r + r))
{q : ComplexSpace n}
(hq : q ∈ Metric.closedBall Q ↑r)
:
theorem
KamProject.Arnold1963.existsUnique_generating_root
{n : ℕ}
{S : ComplexPhaseSpace n → ℂ}
{G U : Set (ComplexSpace n)}
{r : NNReal}
{M : ℝ}
{P Q : ComplexSpace n}
(hr : 0 < r)
(hS : AnalyticOnNhd ℂ S (G ×ˢ U))
(hM : NormBoundOn S (G ×ˢ U) M)
(hsmall : M / ↑r / ↑r < 1)
(hP : P ∈ erosion G (r + r))
(hQ : Q ∈ erosion U (r + r + r))
:
theorem
KamProject.Arnold1963.generating_root_bounds
{n : ℕ}
{S : ComplexPhaseSpace n → ℂ}
{G U : Set (ComplexSpace n)}
{r : NNReal}
{M : ℝ}
{P Q : ComplexSpace n}
(hr : 0 < r)
(hS : AnalyticOnNhd ℂ S (G ×ˢ U))
(hM : NormBoundOn S (G ×ˢ U) M)
(hsmall : M / ↑r / ↑r ≤ 1)
(hP : P ∈ erosion G (r + r))
(hQ : Q ∈ erosion U (r + r + r))
{q : ComplexSpace n}
(hq : q ∈ Metric.closedBall Q ↑r)
(he : q + pGradient S (P, q) = Q)
:
theorem
KamProject.Arnold1963.generating_action_displacement_le
{n : ℕ}
{S : ComplexPhaseSpace n → ℂ}
{G U : Set (ComplexSpace n)}
{r : NNReal}
{M : ℝ}
{P Q : ComplexSpace n}
{δ : NNReal}
(hδ : 0 < δ)
(hS : AnalyticOnNhd ℂ S (G ×ˢ U))
(hM : NormBoundOn S (G ×ˢ U) M)
(hP : P ∈ G)
(hQ : Q ∈ erosion U (r + r + r + δ))
{q : ComplexSpace n}
(hq : q ∈ Metric.closedBall Q ↑r)
: