Analyticity characterization of holomorphic 1-forms (CC1, design §2.2)

Unit: holomorphic-forms (docs/design/holomorphic-forms.md). This file proves the CC1 statement "coeffIn is analytic iff the section is ω-smooth", using the canonical ContMDiffAt ↔ AnalyticAt bridge from the surfaces-and-charts unit (Jacobian.Surface.Bridges) instead of a local re-proof.

Main declarations:

• RS.analyticAt_trans — transitions between maximal-atlas charts are analytic.
• RS.deriv_trans_comp — chain rule for transition derivatives through a third chart.
• RS.tangentCoord_mfderiv_comp — scalar chain rule: the mfderiv-composite read in the canonical tangent coordinate is the planar deriv of the composite.
• RS.contMDiffAt_section_iff_analyticAt_coeffInFun — a covector section is C^ω at x iff its coefficient function in the preferred chart is analytic at chartAt ℂ x x.
• RS.Form1.ofSectionAnalytic — constructor for Form1 from a raw section with analytic preferred-chart coefficients.
• RS.Form1.analyticAt_coeffAt, RS.Form1.analyticOnNhd_coeffIn, RS.Form1.continuousOn_coeffIn — coefficients of holomorphic 1-forms are analytic on chart targets (any maximal-atlas chart).

Analyticity and derivatives of transition maps

theorem RS.analyticAt_trans {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {e e' : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {z : ℂ} (hzt : z ∈ e'.target) (hzs : ↑e'.symm z ∈ e.source) : AnalyticAt ℂ (↑e ∘ ↑e'.symm) z

The transition map between two maximal-atlas charts is analytic at every point of the image of the overlap.

theorem RS.deriv_trans_comp {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {e e' f : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (hf : f ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {z : ℂ} (hzt : z ∈ f.target) (hes : ↑f.symm z ∈ e.source) (he's : ↑f.symm z ∈ e'.source) : deriv (↑e ∘ ↑f.symm) z = deriv (↑e ∘ ↑e'.symm) (↑e' (↑f.symm z)) * deriv (↑e' ∘ ↑f.symm) z

Chain rule for transition derivatives: reading the transition from f to e through an intermediate chart e' multiplies the derivatives.

theorem RS.tangentCoord_mfderiv_comp {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {g : ℂ → X} {z : ℂ} (hf : MDiffAt f (g z)) (hg : MDiffAt g z) : tangentCoord ((mfderiv% f (g z)) ((mfderiv% g z) 1)) = deriv (f ∘ g) z

Scalar chain rule: the composite of mfderivs applied to the canonical tangent vector 1, read in the canonical coordinate, is the planar derivative of the composite.

The planar (ℂ →L[ℂ] ℂ)-valued analyticity reduction

theorem RS.analyticAt_clm_iff_apply_one {F : ℂ → ℂ →L[ℂ] ℂ} {z : ℂ} : AnalyticAt ℂ F z ↔ AnalyticAt ℂ (fun (w : ℂ) => (F w) 1) z

A ℂ →L[ℂ] ℂ-valued map is analytic iff its pointwise evaluation at 1 is (the fiber is one-dimensional; evaluation at 1 is a linear isometry equivalence).

theorem RS.inCoordinates_apply_one {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (σ : (x : X) → TangentSpace (modelWithCornersSelf ℂ ℂ) x →L[ℂ] Bundle.Trivial X ℂ x) (x : X) {z : ℂ} (hz : z ∈ (chartAt ℂ x).target) : (ContinuousLinearMap.inCoordinates ℂ (TangentSpace (modelWithCornersSelf ℂ ℂ)) ℂ (Bundle.Trivial X ℂ) x (↑(chartAt ℂ x).symm z) x (↑(chartAt ℂ x).symm z) (σ (↑(chartAt ℂ x).symm z))) 1 = coeffInFun (chartAt ℂ x) σ z

Defeq bridge: the hom-bundle trivialization representative of a covector section, evaluated at the canonical tangent vector 1, is the chart coefficient function.

The section characterization

theorem RS.contMDiffAt_section_iff_analyticAt_coeffInFun {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (σ : (x : X) → TangentSpace (modelWithCornersSelf ℂ ℂ) x →L[ℂ] Bundle.Trivial X ℂ x) (x : X) : ContMDiffAt (modelWithCornersSelf ℂ ℂ) ((modelWithCornersSelf ℂ ℂ).prod (modelWithCornersSelf ℂ (ℂ →L[ℂ] ℂ))) ⊤ (fun (p : X) => ⟨p, σ p⟩) x ↔ AnalyticAt ℂ (coeffInFun (chartAt ℂ x) σ) (↑(chartAt ℂ x) x)

Smoothness ↔ analytic coefficients (CC1): a covector section is C^ω at x iff its coefficient function in the preferred chart at x is analytic at the chart image of x.

def RS.Form1.ofSectionAnalytic {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (σ : (x : X) → TangentSpace (modelWithCornersSelf ℂ ℂ) x →L[ℂ] Bundle.Trivial X ℂ x) (h : ∀ (x : X), AnalyticAt ℂ (coeffInFun (chartAt ℂ x) σ) (↑(chartAt ℂ x) x)) : Form1 X

Build a holomorphic 1-form from a raw covector section whose preferred-chart coefficient functions are analytic.

Equations

• RS.Form1.ofSectionAnalytic σ h = { toFun := σ, contMDiff_toFun := ⋯ }

@[simp]

theorem RS.Form1.coe_ofSectionAnalytic {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (σ : (x : X) → TangentSpace (modelWithCornersSelf ℂ ℂ) x →L[ℂ] Bundle.Trivial X ℂ x) (h : ∀ (x : X), AnalyticAt ℂ (coeffInFun (chartAt ℂ x) σ) (↑(chartAt ℂ x) x)) : ⇑(ofSectionAnalytic σ h) = σ

Analyticity of the coefficients of a holomorphic 1-form

theorem RS.Form1.analyticAt_coeffAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (η : Form1 X) (x : X) : AnalyticAt ℂ (coeffIn (chartAt ℂ x) η) (↑(chartAt ℂ x) x)

The coefficient of a holomorphic 1-form in the preferred chart at x is analytic at the chart image of x.

theorem RS.Form1.analyticOnNhd_coeffIn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (η : Form1 X) {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) : AnalyticOnNhd ℂ (coeffIn e η) e.target

The coefficient of a holomorphic 1-form in any maximal-atlas chart is analytic on the whole chart target.

theorem RS.Form1.analyticAt_coeffIn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (η : Form1 X) {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {z : ℂ} (hz : z ∈ e.target) : AnalyticAt ℂ (coeffIn e η) z

The coefficient of a holomorphic 1-form in a maximal-atlas chart is analytic at each target point (pointwise form).

theorem RS.Form1.continuousOn_coeffIn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (η : Form1 X) {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) : ContinuousOn (coeffIn e η) e.target

Coefficients of holomorphic 1-forms are continuous on chart targets.