The differential of a holomorphic function (CC1, design §2.4)

Unit: holomorphic-forms (docs/design/holomorphic-forms.md). RS.mdifferential f hf is the holomorphic 1-form df of a holomorphic function f : X → ℂ; in every maximal-atlas chart its coefficient is the planar derivative of the chart composite (RS.coeffIn_mdifferential : coeffIn e (df) = deriv (f ∘ e.symm) on e.target).

Also provides RS.Form1.smulFun (multiplication of a form by a holomorphic function, used by canonical-forms) with its coefficient formula.

Holomorphic 1-forms only — no meromorphic machinery here (meromorphic 1-forms are later f • η pairs in canonical-forms/meromorphic-trace).

noncomputable def RS.mdifferentialSection {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : X → ℂ) (x : X) : TangentSpace (modelWithCornersSelf ℂ ℂ) x →L[ℂ] Bundle.Trivial X ℂ x

The underlying covector section of the differential: x ↦ d f_x, crossing the TangentSpace ↦ Bundle.Trivial defeq in the codomain.

Equations

• RS.mdifferentialSection f x = mfderiv% f x

theorem RS.coeffInFun_mdifferentialSection {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {z : ℂ} (hz : z ∈ e.target) (hf : MDiffAt f (↑e.symm z)) : coeffInFun e (mdifferentialSection f) z = deriv (f ∘ ↑e.symm) z

The raw chart coefficient of the differential section is the derivative of the chart composite.

noncomputable def RS.mdifferential {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : X → ℂ) (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) : Form1 X

The differential of a holomorphic function, as a holomorphic 1-form.

Equations

• RS.mdifferential f hf = RS.Form1.ofSectionAnalytic (RS.mdifferentialSection f) ⋯

theorem RS.coeffIn_mdifferential {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {f : X → ℂ} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) : Set.EqOn (coeffIn e (mdifferential f hf)) (deriv (f ∘ ↑e.symm)) e.target

Chart-coefficient formula for the differential: coeffIn e (df) = deriv (f ∘ e.symm) on e.target (CC1's d-rule).

theorem RS.coeffAt_mdifferential {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : X → ℂ) (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (x : X) : coeffAt x (mdifferential f hf) = deriv (f ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x)

Preferred-chart coefficient of the differential.

ℂ-linearity of the differential

The smoothness proofs of the combined functions are taken as hypotheses (no smooth-algebra instances needed; the value of mdifferential does not depend on the proof argument).

@[simp]

theorem RS.mdifferential_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f g : X → ℂ} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hg : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ g) (hfg : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (f + g)) : mdifferential (f + g) hfg = mdifferential f hf + mdifferential g hg

@[simp]

theorem RS.mdifferential_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (c : ℂ) {f : X → ℂ} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hcf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (c • f)) : mdifferential (c • f) hcf = c • mdifferential f hf

@[simp]

theorem RS.mdifferential_const {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (c : ℂ) : mdifferential (fun (x : X) => c) ⋯ = 0

Multiplication of a form by a holomorphic function

noncomputable def RS.Form1.smulFun {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : X → ℂ) (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (η : Form1 X) : Form1 X

Multiply a holomorphic 1-form by a holomorphic function (used by canonical-forms to build h • η).

Equations

• RS.Form1.smulFun f hf η = { toFun := f • ⇑η, contMDiff_toFun := ⋯ }

@[simp]

theorem RS.coeffIn_smulFun {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (e : OpenPartialHomeomorph X ℂ) (f : X → ℂ) (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (η : Form1 X) (z : ℂ) : coeffIn e (Form1.smulFun f hf η) z = f (↑e.symm z) * coeffIn e η z

@[simp]

theorem RS.coeffAt_smulFun {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (x : X) (f : X → ℂ) (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (η : Form1 X) : coeffAt x (Form1.smulFun f hf η) = f x * coeffAt x η