Documentation

LeanPool.JacobianDiffgeo.Surface.Bridges

Bridges: ContMDiff over ๐“˜(โ„‚) โ†” chart-local ContDiff/AnalyticAt #

Unit: surfaces-and-charts (docs/design/surfaces-and-charts.md ยง3.1; Forster ยง1).

On a Riemann surface X (ChartedSpace โ„‚ X + IsManifold ๐“˜(โ„‚) ฯ‰ X) these lemmas convert manifold smoothness/holomorphy into planar statements about the chart composites, eliminating ContDiffWithinAt-over-range I once and for all:

Maps into a complex Banach space (target = model space, no target chart) #

source
theorem RS.contMDiffAt_iff_contDiffAt_extChartAt_comp {X : Type u_1} [TopologicalSpace X] [ChartedSpace โ„‚ X] [IsManifold (modelWithCornersSelf โ„‚ โ„‚) โŠค X] {n : WithTop โ„•โˆž} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace โ„‚ F] {f : X โ†’ F} {x : X} :
ContMDiffAt (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ F) n f x โ†” ContDiffAt โ„‚ n (f โˆ˜ โ†‘(extChartAt (modelWithCornersSelf โ„‚ โ„‚) x).symm) (โ†‘(extChartAt (modelWithCornersSelf โ„‚ โ„‚) x) x)

C^n at x for f : X โ†’ F is exactly C^n of the chart composite (Banach-space target; requested by holomorphic-forms for (โ„‚ โ†’L[โ„‚] โ„‚)-valued maps).

source
theorem RS.contMDiffAt_iff_analyticAt_comp {X : Type u_1} [TopologicalSpace X] [ChartedSpace โ„‚ X] [IsManifold (modelWithCornersSelf โ„‚ โ„‚) โŠค X] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace โ„‚ F] [CompleteSpace F] {f : X โ†’ F} {x : X} :
ContMDiffAt (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ F) โŠค f x โ†” AnalyticAt โ„‚ (f โˆ˜ โ†‘(extChartAt (modelWithCornersSelf โ„‚ โ„‚) x).symm) (โ†‘(extChartAt (modelWithCornersSelf โ„‚ โ„‚) x) x)

Holomorphy at x for f : X โ†’ F is analyticity of the chart composite.

source
theorem RS.contMDiffAt_iff_analyticAt_comp_chartAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace โ„‚ X] [IsManifold (modelWithCornersSelf โ„‚ โ„‚) โŠค X] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace โ„‚ F] [CompleteSpace F] {f : X โ†’ F} {x : X} :
ContMDiffAt (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ F) โŠค f x โ†” AnalyticAt โ„‚ (f โˆ˜ โ†‘(chartAt โ„‚ x).symm) (โ†‘(chartAt โ„‚ x) x)

chartAt-spelled variant (the exact statement requested by holomorphic-forms).

Maps to โ„‚ (the frozen interface of the design) #

source
theorem RS.contMDiffAt_iff_contDiffAt_extChartAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace โ„‚ X] [IsManifold (modelWithCornersSelf โ„‚ โ„‚) โŠค X] {n : WithTop โ„•โˆž} {f : X โ†’ โ„‚} {x : X} :
ContMDiffAt (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) n f x โ†” ContDiffAt โ„‚ n (f โˆ˜ โ†‘(extChartAt (modelWithCornersSelf โ„‚ โ„‚) x).symm) (โ†‘(extChartAt (modelWithCornersSelf โ„‚ โ„‚) x) x)

C^n at x for f : X โ†’ โ„‚ is exactly C^n of the chart composite.

source
theorem RS.contMDiffAt_iff_analyticAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace โ„‚ X] [IsManifold (modelWithCornersSelf โ„‚ โ„‚) โŠค X] {f : X โ†’ โ„‚} {x : X} :
ContMDiffAt (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) โŠค f x โ†” AnalyticAt โ„‚ (f โˆ˜ โ†‘(extChartAt (modelWithCornersSelf โ„‚ โ„‚) x).symm) (โ†‘(extChartAt (modelWithCornersSelf โ„‚ โ„‚) x) x)

Holomorphy at x for f : X โ†’ โ„‚ is analyticity of the chart composite.

Maps between surfaces (two charts) #

source
theorem RS.contMDiffAt_iff_contDiffAt_writtenInExtChartAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace โ„‚ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace โ„‚ Y] {n : WithTop โ„•โˆž} {f : X โ†’ Y} {x : X} :
ContMDiffAt (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) n f x โ†” ContinuousAt f x โˆง ContDiffAt โ„‚ n (writtenInExtChartAt (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) x f) (โ†‘(extChartAt (modelWithCornersSelf โ„‚ โ„‚) x) x)

Two-chart version, f : X โ†’ Y. ContinuousAt cannot be dropped on the โ† side (the chart composite does not see f outside the chart sources).

source
theorem RS.contMDiffAt_iff_analyticAt_writtenInExtChartAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace โ„‚ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace โ„‚ Y] {f : X โ†’ Y} {x : X} :
ContMDiffAt (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) โŠค f x โ†” ContinuousAt f x โˆง AnalyticAt โ„‚ (writtenInExtChartAt (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) x f) (โ†‘(extChartAt (modelWithCornersSelf โ„‚ โ„‚) x) x)
source
theorem RS.analyticAt_sub_const_iff {g : โ„‚ โ†’ โ„‚} {z c : โ„‚} :
AnalyticAt โ„‚ (fun (w : โ„‚) => g w - c) z โ†” AnalyticAt โ„‚ g z

Subtracting a constant does not change analyticity (helper for the recentered bridge).

source
theorem RS.contMDiffAt_iff_analyticAt_inChartAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace โ„‚ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace โ„‚ Y] {f : X โ†’ Y} {x : X} :
ContMDiffAt (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) โŠค f x โ†” ContinuousAt f x โˆง AnalyticAt โ„‚ (fun (z : โ„‚) => โ†‘(chartAt โ„‚ (f x)) (f (โ†‘(chartAt โ„‚ x).symm z)) - โ†‘(chartAt โ„‚ (f x)) (f x)) (โ†‘(chartAt โ„‚ x) x)

Recentered two-chart bridge (the exact statement requested by local-multiplicity, matching mathlib's analyticOrderAt normal form).

Chart invariance: read holomorphy in any atlas chart #

source
theorem RS.contMDiffAt_iff_analyticAt_of_mem_source {X : Type u_1} [TopologicalSpace X] [ChartedSpace โ„‚ X] [IsManifold (modelWithCornersSelf โ„‚ โ„‚) โŠค X] {f : X โ†’ โ„‚} {x : X} {e : OpenPartialHomeomorph X โ„‚} (he : e โˆˆ atlas โ„‚ X) (hx : x โˆˆ e.source) :
ContMDiffAt (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) โŠค f x โ†” AnalyticAt โ„‚ (f โˆ˜ โ†‘e.symm) (โ†‘e x)

Analyticity may be read in ANY atlas chart whose source contains x (chart-invariance; the workhorse for CC3/CC4-style definitions and for coeffIn).

source
theorem RS.contMDiffOn_iff_analyticOnNhd_of_subset_source {X : Type u_1} [TopologicalSpace X] [ChartedSpace โ„‚ X] [IsManifold (modelWithCornersSelf โ„‚ โ„‚) โŠค X] {f : X โ†’ โ„‚} {s : Set X} {e : OpenPartialHomeomorph X โ„‚} (he : e โˆˆ atlas โ„‚ X) (hs : s โŠ† e.source) (hso : IsOpen s) :
ContMDiffOn (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) โŠค f s โ†” AnalyticOnNhd โ„‚ (f โˆ˜ โ†‘e.symm) (โ†‘e '' s)

Set version on an open subset of a chart source.