Adapted charts (Forster Thm 2.1)

• RS.AdaptedChartsAt F x k — a pair of centered maximal-atlas charts with round-ball targets in which F reads exactly as z ↦ z ^ k.
• RS.exists_adaptedChartsAt — THE atom: a holomorphic nonconstant germ admits adapted charts with k = multiplicity F x, and the source can be shrunk into any given neighborhood.
• Derived API: eqOn_symm, image_source (F maps the chart source ONTO the target chart source), contMDiffOn_e/e'(_symm), and multiplicity_eq (adapted charts pin down the multiplicity).

structure RS.AdaptedChartsAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (F : X → Y) (x : X) (k : ℕ) : Type (max u_1 u_2)

Adapted chart pair at x exhibiting F as z ↦ z ^ k (Forster Thm 2.1). Both charts belong to the analytic maximal atlases (so all holomorphy transports), both are centered, targets are round balls, and F is exactly (· ^ k) in these coordinates.

• e : OpenPartialHomeomorph X ℂ

  The source chart, centred at the point.

• e' : OpenPartialHomeomorph Y ℂ

  The target chart, centred at the image point.

• mem_maximalAtlas : self.e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X
• mem_maximalAtlas' : self.e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ Y
• radius : ℝ

  The radius of the source disc on which the normal form holds.

• radius_pos : 0 < self.radius
• mem_source : x ∈ self.e.source
• mem_source' : F x ∈ self.e'.source
• map_eq_zero : ↑self.e x = 0
• map_eq_zero' : ↑self.e' (F x) = 0
• target_eq : self.e.target = Metric.ball 0 self.radius
• target_eq' : self.e'.target = Metric.ball 0 (self.radius ^ k)
• mapsTo : Set.MapsTo F self.e.source self.e'.source
• eqOn_pow (z : X) : z ∈ self.e.source → ↑self.e' (F z) = ↑self.e z ^ k

theorem RS.AdaptedChartsAt.eqOn_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {x : X} {k : ℕ} (A : AdaptedChartsAt F x k) (z : X) : z ∈ A.e.source → F z = ↑A.e'.symm (↑A.e z ^ k)

theorem RS.AdaptedChartsAt.image_source {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {x : X} {k : ℕ} (hk : k ≠ 0) (A : AdaptedChartsAt F x k) : F '' A.e.source = A.e'.source

F maps the adapted source onto the adapted target source (uses image_pow_ball).

theorem RS.AdaptedChartsAt.contMDiffOn_e {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {x : X} {k : ℕ} (A : AdaptedChartsAt F x k) : ContMDiffOn (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (↑A.e) A.e.source

theorem RS.AdaptedChartsAt.contMDiffOn_e_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {x : X} {k : ℕ} (A : AdaptedChartsAt F x k) : ContMDiffOn (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (↑A.e.symm) A.e.target

theorem RS.AdaptedChartsAt.contMDiffOn_e' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {x : X} {k : ℕ} (A : AdaptedChartsAt F x k) : ContMDiffOn (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (↑A.e') A.e'.source

theorem RS.AdaptedChartsAt.contMDiffOn_e'_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {x : X} {k : ℕ} (A : AdaptedChartsAt F x k) : ContMDiffOn (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (↑A.e'.symm) A.e'.target

theorem RS.AdaptedChartsAt.multiplicity_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {x : X} {k : ℕ} [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] (_hk : k ≠ 0) (hF : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F x) (A : AdaptedChartsAt F x k) : multiplicity F x = k

Adapted charts pin down the multiplicity: if F reads as z ^ k in adapted charts, then k IS the local multiplicity. (The hypothesis hk is kept for interface stability; it is not needed for this direction.)

theorem RS.exists_adaptedChartsAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} {x : X} (hF : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F x) (hnc : ¬Filter.EventuallyConst F (nhds x)) {U : Set X} (hU : U ∈ nhds x) : ∃ (A : AdaptedChartsAt F x (multiplicity F x)), A.e.source ⊆ U

Existence of adapted charts (Forster Thm 2.1), with source shrinkable into any given neighborhood. Here k = multiplicity F x ≥ 1.