Coverage of eroded domains via continuous induction along a segment, allowing nonconvex compact domains and proving the required boundary behavior from local inverses.
theorem
KamProject.Arnold1963.mem_interior_of_local_inverse
{n : ℕ}
{A g : ComplexSpace n → ComplexSpace n}
{G Ω : Set (ComplexSpace n)}
{p : ComplexSpace n}
(hA : ContinuousAt A p)
(hg : Set.MapsTo g Ω G)
(hl : ∀ᶠ (x : ComplexSpace n) in nhds p, g (A x) = x)
(hp : A p ∈ interior Ω)
:
theorem
KamProject.Arnold1963.mem_erosion_of_image_buffer
{n : ℕ}
{A : ComplexSpace n → ComplexSpace n}
{G Ω : Set (ComplexSpace n)}
{C r : NNReal}
(hG : IsClosed G)
(hC : 0 < C)
(hA : AnalyticOnNhd ℂ A G)
(hd : ∀ p ∈ G, ‖fderiv ℂ A p‖ ≤ ↑C)
(hback : ∀ p ∈ G, A p ∈ interior Ω → p ∈ interior G)
{p : ComplexSpace n}
(hp : p ∈ G)
(hy : A p ∈ erosion Ω (C * r))
: