Chart bridge for local multiplicity

• RS.inChartAt F x : ℂ → ℂ — the map F : X → Y read in the standard charts at x and F x, recentered to vanish at chartAt ℂ x x. This is the germ whose analyticOrderAt defines the local multiplicity (CC4).
• RS.LMCompat.contMDiffAt_iff_analyticAt_inChartAt — CC7 holomorphy bridge (ContMDiffAt … ω ↔ ContinuousAt ∧ AnalyticAt of the chart representative). Local copy; the canonical version is owned by surfaces-and-charts (request filed).
• RS.eventuallyConst_inChartAt(_iff) — local constancy transports through the charts.
• RS.mem_contDiffGroupoid_iff_analytic — contDiffGroupoid ω 𝓘(ℂ) membership is analyticity of both directions on source/target.
• RS.analyticAt_transition — maximal-atlas transitions are analytic with deriv ≠ 0.
• RS.trans_mem_maximalAtlas — the maximal atlas is stable under ≫ₕ with a groupoid element.
• RS.map_nhdsNE — an OpenPartialHomeomorph maps 𝓝[≠] x to 𝓝[≠] (e x) on its source.

noncomputable def RS.inChartAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (F : X → Y) (x : X) : ℂ → ℂ

F read in the standard charts at x and F x, recentered to vanish at chartAt ℂ x x. Junk (from the charts' junk values) away from the chart sources; only its germ matters.

Equations

• RS.inChartAt F x z = ↑(chartAt ℂ (F x)) (F (↑(chartAt ℂ x).symm z)) - ↑(chartAt ℂ (F x)) (F x)

@[simp]

theorem RS.inChartAt_apply_chart {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (F : X → Y) (x : X) : inChartAt F x (↑(chartAt ℂ x) x) = 0

theorem RS.analyticAt_inChartAt_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {x : X} : AnalyticAt ℂ (inChartAt F x) (↑(chartAt ℂ x) x) ↔ AnalyticAt ℂ (↑(chartAt ℂ (F x)) ∘ F ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x)

Recentering does not matter for analyticity of the chart representative.

theorem RS.LMCompat.contMDiffAt_iff_analyticAt_inChartAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {x : X} : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F x ↔ ContinuousAt F x ∧ AnalyticAt ℂ (inChartAt F x) (↑(chartAt ℂ x) x)

CC7 holomorphy bridge (temporary local copy; canonical version owned by surfaces-and-charts — see docs/requests/surfaces-and-charts.md).

theorem RS.eventuallyConst_nhds_iff {α : Type u_3} {β : Type u_4} [TopologicalSpace α] {f : α → β} {x : α} : Filter.EventuallyConst f (nhds x) ↔ ∀ᶠ (y : α) in nhds x, f y = f x

EventuallyConst at a neighborhood filter pins the constant to the value at the point.

theorem RS.eventuallyConst_inChartAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {x : X} (h : Filter.EventuallyConst F (nhds x)) : Filter.EventuallyConst (inChartAt F x) (nhds (↑(chartAt ℂ x) x))

theorem RS.eventuallyConst_inChartAt_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {x : X} (hFc : ContinuousAt F x) : Filter.EventuallyConst (inChartAt F x) (nhds (↑(chartAt ℂ x) x)) ↔ Filter.EventuallyConst F (nhds x)

theorem RS.mem_contDiffGroupoid_iff_analytic {Φ : OpenPartialHomeomorph ℂ ℂ} : Φ ∈ contDiffGroupoid ⊤ (modelWithCornersSelf ℂ ℂ) ↔ AnalyticOnNhd ℂ (↑Φ) Φ.source ∧ AnalyticOnNhd ℂ (↑Φ.symm) Φ.target

contDiffGroupoid ω 𝓘(ℂ) membership is analyticity of both directions.

theorem RS.analyticAt_transition_fun {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {e e' : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {x : X} (hx : x ∈ e.source) (hx' : x ∈ e'.source) : AnalyticAt ℂ (↑e' ∘ ↑e.symm) (↑e x)

Transitions between maximal-atlas charts are analytic (one direction).

theorem RS.analyticAt_transition {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {e e' : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {x : X} (hx : x ∈ e.source) (hx' : x ∈ e'.source) : AnalyticAt ℂ (↑e' ∘ ↑e.symm) (↑e x) ∧ deriv (↑e' ∘ ↑e.symm) (↑e x) ≠ 0

Transitions between maximal-atlas charts are analytic with nonvanishing derivative.

theorem RS.trans_mem_maximalAtlas {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {Φ : OpenPartialHomeomorph ℂ ℂ} (hΦ : Φ ∈ contDiffGroupoid ⊤ (modelWithCornersSelf ℂ ℂ)) : e.trans Φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X

Trans with a groupoid element stays in the maximal atlas (upstreamable helper).

theorem RS.map_nhdsNE {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] (e : OpenPartialHomeomorph α β) {x : α} (hx : x ∈ e.source) : Filter.map (↑e) (nhdsWithin x {x}ᶜ) = nhdsWithin (↑e x) {↑e x}ᶜ

An OpenPartialHomeomorph maps punctured neighborhoods of source points to punctured neighborhoods.