Rectangular action and angle buffers for Cauchy estimates on eroded phase domains.

theorem KamProject.Arnold1963.mem_angleStrip_of_dist_le {n : ℕ} {ρ δ : NNReal} (hδρ : δ ≤ ρ) {q q' : ComplexSpace n} (hq : q ∈ angleStrip n (ρ - δ)) (hd : dist q' q ≤ ↑δ) : q' ∈ angleStrip n ρ

theorem KamProject.Arnold1963.phaseDomain_rectangular_buffer {n : ℕ} {G : Set (ComplexSpace n)} {ρ β δ : NNReal} (hδρ : δ ≤ ρ) {p q : ComplexSpace n} (hx : (p, q) ∈ phaseDomain (erosion G β) (ρ - δ)) : Metric.closedBall p ↑β ×ˢ Metric.closedBall q ↑δ ⊆ phaseDomain G ρ

theorem KamProject.Arnold1963.phaseDomain_shrink_subset_erosion {n : ℕ} (G : Set (ComplexSpace n)) {ρ r : NNReal} (hrρ : r ≤ ρ) : phaseDomain (erosion G r) (ρ - r) ⊆ erosion (phaseDomain G ρ) r

theorem KamProject.Arnold1963.AnalyticPhaseFunction.norm_vectorField_le_on_shrink {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} (f : AnalyticPhaseFunction n G ρ) (hr : 0 < r) (hrρ : r ≤ ρ) {x : ComplexPhaseSpace n} (hx : x ∈ phaseDomain (erosion G r) (ρ - r)) : ‖hamiltonianVectorField f.toFun x‖ ≤ f.uniformNorm / ↑r

theorem KamProject.Arnold1963.AnalyticPhaseFunction.norm_pGradient_le_rectangular {n : ℕ} {G : Set (ComplexSpace n)} {ρ β : NNReal} (f : AnalyticPhaseFunction n G ρ) (hβ : 0 < β) {p q : ComplexSpace n} (hp : p ∈ erosion G β) (hq : q ∈ angleStrip n ρ) : ‖pGradient f.toFun (p, q)‖ ≤ f.uniformNorm / ↑β

theorem KamProject.Arnold1963.AnalyticPhaseFunction.norm_qGradient_le_rectangular {n : ℕ} {G : Set (ComplexSpace n)} {ρ δ : NNReal} (f : AnalyticPhaseFunction n G ρ) (hδ : 0 < δ) (hδρ : δ ≤ ρ) {p q : ComplexSpace n} (hp : p ∈ G) (hq : q ∈ angleStrip n (ρ - δ)) : ‖qGradient f.toFun (p, q)‖ ≤ f.uniformNorm / ↑δ