The intrinsic dbar operator and IsDbarOn (Jacobian/Dbar/Operator.lean)

Unit: dbar-solvability (docs/design/dbar-solvability.md D6/D7, §4.7, §7.3-4).

SmoothC X is a hand-rolled subtype {f : X → ℂ // ContMDiff 𝓘(ℝ,ℂ) 𝓘(ℝ,ℂ) ∞ f} with our OWN AddCommGroup/Module ℂ instances (per design D6: mathlib's bundled ContMDiffMap ring/module instances only give a Module ℝ for our target model 𝓘(ℝ,ℂ), and layering a competing ℂ scalar action on mathlib's own type is exactly the restrictScalars diamond trap the blueprint warns about — a private subtype dodges it). Closure under the ring/module operations, and the chart-representative smoothness needed for dbar, are proved via the CC7 bridge contMDiffAt_real_iff_contDiffAt (Jacobian.Surface.RealSmooth) and the composition ContMDiffOn.comp with contMDiffOn_extChartAt_symm (mathlib), reduced to ContDiffOn ℝ via contMDiffOn_iff_contDiffOn — this avoids needing any project-local "chart invariance for real smoothness" lemma (extChartAt 𝓘(ℂ) x coincides with chartAt ℂ x definitionally, Compat bridge facts checked in-line).

The intrinsic dbar : SmoothC X →ₗ[ℂ] Form01 X is chart-local wirtingerDbar of the chart representative; IsDbarAt/IsDbarOn are the chart-free (evaluated-at-centers) local dbar-equation predicates (D7); exists_dbar_solution_chart_ball transports Forster 13.2 (SolveDisk.lean) through a chart.

SmoothC X: real-smooth ℂ-valued functions, with ℂ-linear structure

def RS.SmoothC (X : Type u_2) [TopologicalSpace X] [ChartedSpace ℂ X] : Type u_2

Real-smooth ℂ-valued functions on X, as a private subtype (D6).

Equations

• RS.SmoothC X = { f : X → ℂ // ContMDiff (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) f }

@[instance_reducible]

instance RS.SmoothC.instFunLikeComplex {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] : FunLike (SmoothC X) X ℂ

Equations

• RS.SmoothC.instFunLikeComplex = { coe := fun (f : RS.SmoothC X) => ↑f, coe_injective := ⋯ }

theorem RS.SmoothC.contMDiff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : SmoothC X) : ContMDiff (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) ↑⊤ ⇑f

theorem RS.SmoothC.contDiffOn_comp_chartAt_symm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : SmoothC X) (x : X) : ContDiffOn ℝ (↑⊤) (⇑f ∘ ↑(chartAt ℂ x).symm) (chartAt ℂ x).target

Compat (design §4.7): the chart representative of a SmoothC function is planar-smooth on the whole chart target (not just at the chart's own centre): compose the globally ContMDiff function with the (mathlib) chart-inverse smoothness contMDiffOn_extChartAt_symm, then reduce ContMDiff on planar sets to ContDiff via contMDiffOn_iff_contDiffOn.

theorem RS.SmoothC.contDiffAt_comp_chartAt_symm_self {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : SmoothC X) (x : X) : ContDiffAt ℝ (↑⊤) (⇑f ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x)

theorem RS.SmoothC.differentiableAt_comp_chartAt_symm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : SmoothC X) (x : X) {z : ℂ} (hz : z ∈ (chartAt ℂ x).target) : DifferentiableAt ℝ (⇑f ∘ ↑(chartAt ℂ x).symm) z

@[instance_reducible]

instance RS.SmoothC.instAdd {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Add (SmoothC X)

Equations

• RS.SmoothC.instAdd = { add := fun (f g : RS.SmoothC X) => ⟨fun (x : X) => f x + g x, ⋯⟩ }

@[instance_reducible]

instance RS.SmoothC.instNeg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Neg (SmoothC X)

Equations

• RS.SmoothC.instNeg = { neg := fun (f : RS.SmoothC X) => ⟨fun (x : X) => -f x, ⋯⟩ }

@[instance_reducible]

instance RS.SmoothC.instSub {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Sub (SmoothC X)

Equations

• RS.SmoothC.instSub = { sub := fun (f g : RS.SmoothC X) => ⟨fun (x : X) => f x - g x, ⋯⟩ }

@[instance_reducible]

instance RS.SmoothC.instZero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Zero (SmoothC X)

Equations

• RS.SmoothC.instZero = { zero := ⟨fun (x : X) => 0, ⋯⟩ }

@[instance_reducible]

instance RS.SmoothC.instSMulComplex {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : SMul ℂ (SmoothC X)

Equations

• RS.SmoothC.instSMulComplex = { smul := fun (c : ℂ) (f : RS.SmoothC X) => ⟨fun (x : X) => c * f x, ⋯⟩ }

@[simp]

theorem RS.SmoothC.coe_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f g : SmoothC X) (x : X) : (f + g) x = f x + g x

@[simp]

theorem RS.SmoothC.coe_neg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : SmoothC X) (x : X) : (-f) x = -f x

@[simp]

theorem RS.SmoothC.coe_sub {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f g : SmoothC X) (x : X) : (f - g) x = f x - g x

@[simp]

theorem RS.SmoothC.coe_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (x : X) : 0 x = 0

@[simp]

theorem RS.SmoothC.coe_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (c : ℂ) (f : SmoothC X) (x : X) : (c • f) x = c * f x

theorem RS.SmoothC.ext' {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : SmoothC X} (h : ∀ (x : X), f x = g x) : f = g

@[instance_reducible]

instance RS.SmoothC.instAddCommGroup {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : AddCommGroup (SmoothC X)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance RS.SmoothC.instModuleComplex {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Module ℂ (SmoothC X)

Equations

• RS.SmoothC.instModuleComplex = { toSMul := RS.SmoothC.instSMulComplex, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

The intrinsic dbar

noncomputable def RS.dbarCoeffAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : SmoothC X) (x : X) : ℂ → ℂ

The raw coefficient family underlying dbar f: chart-local wirtingerDbar of the chart representative of f, junk-zero off the chart target.

Equations

• RS.dbarCoeffAt f x = (chartAt ℂ x).target.indicator fun (z : ℂ) => RS.wirtingerDbar (⇑f ∘ ↑(chartAt ℂ x).symm) z

noncomputable def RS.dbar {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : SmoothC X →ₗ[ℂ] Form01 X

The intrinsic dbar, chart-locally the planar Wirtinger operator.

Equations

• RS.dbar = { toFun := fun (f : RS.SmoothC X) => { coeffAt := RS.dbarCoeffAt f, coeffAt_zero_off := ⋯, contDiffOn_coeffAt := ⋯, compat := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem RS.coeffAt_dbar {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : SmoothC X) (x : X) {z : ℂ} (hz : z ∈ (chartAt ℂ x).target) : (dbar f).coeffAt x z = wirtingerDbar (⇑f ∘ ↑(chartAt ℂ x).symm) z

IsDbarAt / IsDbarOn (D7): chart-free local dbar-equations

def RS.IsDbarAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (u : X → ℂ) (η : Form01 X) (x : X) : Prop

u solves dbaru = η at x, evaluated in x's own preferred chart.

Equations

• RS.IsDbarAt u η x = (RS.wirtingerDbar (u ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x) = η.coeffAt x (↑(chartAt ℂ x) x))

def RS.IsDbarOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (u : X → ℂ) (η : Form01 X) (s : Set X) : Prop

u solves dbaru = η at every point of s.

Equations

• RS.IsDbarOn u η s = ∀ x ∈ s, RS.IsDbarAt u η x

theorem RS.isDbarOn_dbar {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : SmoothC X) : IsDbarOn (⇑f) (dbar f) Set.univ

theorem RS.eqOn_coeffAt_of_isDbarOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x₀ : X} {s : Set X} (hs : IsOpen s) (hsub : s ⊆ (chartAt ℂ x₀).source) {u : X → ℂ} {η : Form01 X} (hu : ContMDiffOn (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) u s) (h : ∀ x ∈ s, IsDbarAt u η x) : Set.EqOn (wirtingerDbar (u ∘ ↑(chartAt ℂ x₀).symm)) (η.coeffAt x₀) (↑(chartAt ℂ x₀) '' s)

The chart-transition transport of the local dbar-equation: IsDbarAt at every point of s (each evaluated in ITS OWN preferred chart) forces the coefficient equation for η to hold on the WHOLE image of s under any single chart x₀ whose source contains s, provided u is ContMDiff there (needed to actually invoke the (0,1) chain rule, not just junk-0 wirtingerDbar). This is the key lemma underlying dbar_eq_iff, contMDiffOn_omega_of_isDbarOn_zero, and exists_dbar_solution_chart_ball.

theorem RS.dbar_eq_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : SmoothC X} {η : Form01 X} : dbar f = η ↔ IsDbarOn (⇑f) η Set.univ

theorem RS.contMDiffOn_omega_of_isDbarOn_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {u : X → ℂ} {s : Set X} (hs : IsOpen s) (hu : ContMDiffOn (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) u s) (h : IsDbarOn u 0 s) : ContMDiffOn (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ u s

Deliverable (iv): a smooth dbar-closed function is holomorphic.

theorem RS.contMDiffOn_omega_sub_of_isDbarOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {u v : X → ℂ} {η : Form01 X} {s : Set X} (hs : IsOpen s) (hu : ContMDiffOn (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) u s) (hv : ContMDiffOn (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) v s) (h1 : IsDbarOn u η s) (h2 : IsDbarOn v η s) : ContMDiffOn (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (u - v) s

Deliverable (v): two smooth solutions of the same dbar-equation differ by a holomorphic function.

Chart-disk solvability

theorem RS.exists_dbar_solution_chart_ball {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x₀ : X} {r : ℝ} (hr : 0 < r) {V : Set X} (hVs : V ⊆ (chartAt ℂ x₀).source) (hVim : ↑(chartAt ℂ x₀) '' V = Metric.ball (↑(chartAt ℂ x₀) x₀) r) (η : Form01 X) : ∃ (u : X → ℂ), ContMDiffOn (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) u V ∧ IsDbarOn u η V

Deliverable (vi): Forster 13.2, transported through a chart — dbar is surjective from SmoothC-representatives onto Form01 data supported in a chart disk.