Joint analyticity and operator norm estimates for Hamiltonian gradients in the maximum norm.

theorem KamProject.Arnold1963.mem_erosion_of_dist_le {E : Type u_1} [MetricSpace E] {U : Set E} {r s : NNReal} {x y : E} (hx : x ∈ erosion U (r + s)) (hy : dist y x ≤ ↑s) : y ∈ erosion U r

theorem KamProject.Arnold1963.prod_mem_erosion {E : Type u_1} {F : Type u_2} [MetricSpace E] [MetricSpace F] {G : Set E} {U : Set F} {r : NNReal} {p : E} {q : F} (hp : p ∈ erosion G r) (hq : q ∈ erosion U r) : (p, q) ∈ erosion (G ×ˢ U) r

noncomputable def KamProject.Arnold1963.pGradientCLM (n : ℕ) : (ComplexPhaseSpace n →L[ℂ] ℂ) →L[ℂ] ComplexSpace n

Evaluation of a phase covector on all action-coordinate basis directions.

Equations

• KamProject.Arnold1963.pGradientCLM n = ContinuousLinearMap.pi fun (j : Fin n) => (ContinuousLinearMap.apply ℂ ℂ) (KamProject.Arnold1963.pDirection j)

noncomputable def KamProject.Arnold1963.qGradientCLM (n : ℕ) : (ComplexPhaseSpace n →L[ℂ] ℂ) →L[ℂ] ComplexSpace n

Evaluation of a phase covector on all angle-coordinate basis directions.

Equations

• KamProject.Arnold1963.qGradientCLM n = ContinuousLinearMap.pi fun (j : Fin n) => (ContinuousLinearMap.apply ℂ ℂ) (KamProject.Arnold1963.qDirection j)

theorem KamProject.Arnold1963.analyticAt_pGradient {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {x : ComplexPhaseSpace n} (hS : AnalyticAt ℂ S x) : AnalyticAt ℂ (pGradient S) x

theorem KamProject.Arnold1963.analyticAt_qGradient {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {x : ComplexPhaseSpace n} (hS : AnalyticAt ℂ S x) : AnalyticAt ℂ (qGradient S) x

theorem KamProject.Arnold1963.fderiv_pGradient_apply {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {x : ComplexPhaseSpace n} (hS : AnalyticAt ℂ S x) (v : ComplexPhaseSpace n) (j : Fin n) : (fderiv ℂ (pGradient S) x) v j = ((fderiv ℂ (fderiv ℂ S) x) v) (pDirection j)

theorem KamProject.Arnold1963.fderiv_qGradient_apply {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {x : ComplexPhaseSpace n} (hS : AnalyticAt ℂ S x) (v : ComplexPhaseSpace n) (j : Fin n) : (fderiv ℂ (qGradient S) x) v j = ((fderiv ℂ (fderiv ℂ S) x) v) (qDirection j)

theorem KamProject.Arnold1963.norm_fderiv_pGradient_le {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {U : Set (ComplexPhaseSpace n)} {r : NNReal} {M : ℝ} {x : ComplexPhaseSpace n} (hr : 0 < r) (hS : AnalyticOnNhd ℂ S U) (hM : NormBoundOn S U M) (hx : x ∈ erosion U (r + r)) : ‖fderiv ℂ (pGradient S) x‖ ≤ M / ↑r / ↑r

theorem KamProject.Arnold1963.norm_fderiv_qGradient_le {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {U : Set (ComplexPhaseSpace n)} {r : NNReal} {M : ℝ} {x : ComplexPhaseSpace n} (hr : 0 < r) (hS : AnalyticOnNhd ℂ S U) (hM : NormBoundOn S U M) (hx : x ∈ erosion U (r + r)) : ‖fderiv ℂ (qGradient S) x‖ ≤ M / ↑r / ↑r

theorem KamProject.Arnold1963.norm_qGradient_le_on_product {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {δ : NNReal} {M : ℝ} {P q : ComplexSpace n} (hδ : 0 < δ) (hS : AnalyticOnNhd ℂ S (G ×ˢ U)) (hM : NormBoundOn S (G ×ˢ U) M) (hP : P ∈ G) (hq : q ∈ erosion U δ) : ‖qGradient S (P, q)‖ ≤ M / ↑δ