Closed-ball neighborhoods, erosion, complex angle strips, and real slices. Radii are nonnegative. The neighborhood is a union of actual closed balls; its zero-radius value is the original set. Compactness hypotheses justify closedness when it is needed.

def KamProject.Arnold1963.closedBallNeighborhood {E : Type u_1} [MetricSpace E] (U : Set E) (r : NNReal) : Set E

The union of closed balls of a fixed radius centered at points of the set.

Equations

• KamProject.Arnold1963.closedBallNeighborhood U r = {x : E | ∃ y ∈ U, dist x y ≤ ↑r}

def KamProject.Arnold1963.erosion {E : Type u_1} [MetricSpace E] (U : Set E) (r : NNReal) : Set E

The points whose closed ball of the specified radius remains inside the set.

Equations

• KamProject.Arnold1963.erosion U r = {x : E | Metric.closedBall x ↑r ⊆ U}

@[simp]

theorem KamProject.Arnold1963.erosion_zero {E : Type u_1} [MetricSpace E] (U : Set E) : erosion U 0 = U

@[simp]

theorem KamProject.Arnold1963.closedBallNeighborhood_zero {E : Type u_1} [MetricSpace E] (U : Set E) : closedBallNeighborhood U 0 = U

theorem KamProject.Arnold1963.erosion_subset {E : Type u_1} [MetricSpace E] (U : Set E) (r : NNReal) : erosion U r ⊆ U

theorem KamProject.Arnold1963.subset_closedBallNeighborhood {E : Type u_1} [MetricSpace E] (U : Set E) (r : NNReal) : U ⊆ closedBallNeighborhood U r

theorem KamProject.Arnold1963.erosion_mono {E : Type u_1} [MetricSpace E] {U V : Set E} (hUV : U ⊆ V) (r : NNReal) : erosion U r ⊆ erosion V r

theorem KamProject.Arnold1963.erosion_antitone_radius {E : Type u_1} [MetricSpace E] (U : Set E) {r s : NNReal} (hrs : r ≤ s) : erosion U s ⊆ erosion U r

theorem KamProject.Arnold1963.erosion_inter {E : Type u_1} [MetricSpace E] (U V : Set E) (r : NNReal) : erosion (U ∩ V) r = erosion U r ∩ erosion V r

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

theorem KamProject.Arnold1963.closedBallNeighborhood_eq_cthickening_of_isCompact {E : Type u_1} [MetricSpace E] {U : Set E} (hU : IsCompact U) (r : NNReal) : closedBallNeighborhood U r = Metric.cthickening (↑r) U

theorem KamProject.Arnold1963.isClosed_closedBallNeighborhood_of_isCompact {E : Type u_1} [MetricSpace E] {U : Set E} (hU : IsCompact U) (r : NNReal) : IsClosed (closedBallNeighborhood U r)

theorem KamProject.Arnold1963.isCompact_closedBallNeighborhood {E : Type u_1} [MetricSpace E] {U : Set E} [ProperSpace E] (hU : IsCompact U) (r : NNReal) : IsCompact (closedBallNeighborhood U r)

theorem KamProject.Arnold1963.isClosed_closedBallNeighborhood {E : Type u_1} [MetricSpace E] {U : Set E} [ProperSpace E] (hU : IsClosed U) (r : NNReal) : IsClosed (closedBallNeighborhood U r)

def KamProject.Arnold1963.angleStrip (n : ℕ) (ρ : NNReal) : Set (ComplexSpace n)

The closed complex angle strip bounded in the supremum norm of imaginary coordinates.

Equations

• KamProject.Arnold1963.angleStrip n ρ = {q : KamProject.Arnold1963.ComplexSpace n | ‖KamProject.Arnold1963.imagPart q‖ ≤ ↑ρ}

def KamProject.Arnold1963.phaseDomain {n : ℕ} (G : Set (ComplexSpace n)) (ρ : NNReal) : Set (ComplexPhaseSpace n)

The product of an action domain and a closed complex angle strip.

Equations

• KamProject.Arnold1963.phaseDomain G ρ = G ×ˢ KamProject.Arnold1963.angleStrip n ρ

def KamProject.Arnold1963.realSlice {n : ℕ} (G : Set (ComplexSpace n)) : Set (RealSpace n)

The real actions whose complexifications belong to the complex domain.

Equations

• KamProject.Arnold1963.realSlice G = KamProject.Arnold1963.complexify ⁻¹' G

theorem KamProject.Arnold1963.isOpen_realSlice {n : ℕ} {G : Set (ComplexSpace n)} (hG : IsOpen G) : IsOpen (realSlice G)

theorem KamProject.Arnold1963.isClosed_realSlice {n : ℕ} {G : Set (ComplexSpace n)} (hG : IsClosed G) : IsClosed (realSlice G)

theorem KamProject.Arnold1963.isCompact_realSlice {n : ℕ} {G : Set (ComplexSpace n)} (hG : IsCompact G) : IsCompact (realSlice G)

def KamProject.Arnold1963.ConjInvariant {n : ℕ} (G : Set (ComplexSpace n)) : Prop

Closure of a complex action domain under coordinatewise conjugation.

Equations

• KamProject.Arnold1963.ConjInvariant G = ∀ p ∈ G, KamProject.Arnold1963.conjVec p ∈ G

theorem KamProject.Arnold1963.mem_angleStrip_iff {n : ℕ} (q : ComplexSpace n) (ρ : NNReal) : q ∈ angleStrip n ρ ↔ ∀ (j : Fin n), |(q j).im| ≤ ↑ρ

theorem KamProject.Arnold1963.complexify_mem_angleStrip {n : ℕ} (q : RealSpace n) (ρ : NNReal) : complexify q ∈ angleStrip n ρ

theorem KamProject.Arnold1963.angleStrip_mono {n : ℕ} {ρ σ : NNReal} (h : ρ ≤ σ) : angleStrip n ρ ⊆ angleStrip n σ