16.10. Dbar.DbarOpenDisk🔗

Jacobians.Dbar.DbarOpenDisk — source

diff_partialSum

Power-series partial sums (centred at c) are entire — they are polynomials.

theorem diff_partialSum (p : FormalMultilinearSeries ℂ ℂ ℂ) (n : ℕ) (c : ℂ) :
    Differentiable ℂ (fun y => p.partialSum n (y - c))

exists_holo_approx

Runge/Taylor approximation on a closed subdisk. A function holomorphic on ball c R' is, on any closed subdisk closedBall c r (r < R'), uniformly approximated to within ε by an *entire* function (a Taylor partial sum).

theorem exists_holo_approx (φ : ℂ → ℂ) (c : ℂ) (R' : ℝ)
    (hφ : DifferentiableOn ℂ φ (ball c R')) (r : ℝ) (hr0 : 0 ≤ r) (hrR : r < R')
    (ε : ℝ) (hε : 0 < ε) :
    ∃ P : ℂ → ℂ, Differentiable ℂ P ∧ ∀ z ∈ closedBall c r, ‖φ z - P z‖ ≤ ε

contDiff_cutoff_mul

Cutoff × open-disk-smooth datum is globally smooth. If g is smooth on the open set U, ψ is globally smooth, and tsupport ψ ⊆ U, then ψ·g is globally smooth (it is ψ·g on U and 0 off tsupport ψ).

theorem contDiff_cutoff_mul {g ψ : ℂ → ℂ} {U : Set ℂ} (hU : IsOpen U)
    (hg : ContDiffOn ℝ (⊤ : ℕ∞) g U) (hψ : ContDiff ℝ (⊤ : ℕ∞) ψ)
    (hsupp : tsupport ψ ⊆ U) :
    ContDiff ℝ (⊤ : ℕ∞) (fun x => ψ x * g x)

dbar_sub

∂̄ is subtractive at a point where both functions are real-differentiable.

theorem dbar_sub {f h : ℂ → ℂ} {z : ℂ} (hf : DifferentiableAt ℝ f z) (hh : DifferentiableAt ℝ h z) :
    DbarDisk.dbar (fun x => f x - h x) z = DbarDisk.dbar f z - DbarDisk.dbar h z

dbar_add

∂̄ is additive at a point where both functions are real-differentiable.

theorem dbar_add {f h : ℂ → ℂ} {z : ℂ} (hf : DifferentiableAt ℝ f z) (hh : DifferentiableAt ℝ h z) :
    DbarDisk.dbar (fun x => f x + h x) z = DbarDisk.dbar f z + DbarDisk.dbar h z

entire_contDiffR

An entire function is ℝ-smooth (holomorphic ⟹ ℝ-analytic ⟹ C^∞).

theorem entire_contDiffR {P : ℂ → ℂ} (hP : Differentiable ℂ P) : ContDiff ℝ (⊤ : ℕ∞) P

holo_contDiffOnR

A holomorphic function on an open set is ℝ-smooth there.

theorem holo_contDiffOnR {f : ℂ → ℂ} {s : Set ℂ} (hs : IsOpen s) (hf : DifferentiableOn ℂ f s) :
    ContDiffOn ℝ (⊤ : ℕ∞) f s

rho

The exhaustion radii ρₙ = R(1 − 2⁻⁽ⁿ⁺¹⁾) ↑ R.

noncomputable def rho (R : ℝ) (n : ℕ) : ℝ

rho_props

The exhaustion radii are positive, strictly increasing, bounded by R, and tend to R.

theorem rho_props {R : ℝ} (hR : 0 < R) :
    (∀ n, 0 < rho R n) ∧ StrictMono (rho R) ∧ (∀ n, rho R n < R) ∧
      Tendsto (rho R) atTop (nhds R)

solve_on_ball

The per-ball solve. With the open-disk datum g, solve ∂̄u = g on ball c a for radii 0 < a < b < R: cut off g by a bump (= 1 on closedBall c a, supported in closedBall c b ⊆ ball c R) so χ·g is globally smooth with compact support, then apply Forster 13.1.

theorem solve_on_ball (c : ℂ) {R : ℝ} {g : ℂ → ℂ} (hg : ContDiffOn ℝ (⊤ : ℕ∞) g (ball c R))
    {a b : ℝ} (ha : 0 < a) (hab : a < b) (hbR : b < R) :
    ∃ u : ℂ → ℂ, ContDiff ℝ (⊤ : ℕ∞) u ∧ ∀ z ∈ ball c a, DbarDisk.dbar u z = g z

dbar_solvable_open_disk

Forster 13.2 — ∂̄-solvability on an open disk. For g smooth on the *open* ball ball c R, there is u smooth on ball c R with ∂̄u = g there. Unlike DbarDiskCohomology.dbar_solvable_ball, the datum need not be globally smooth — this is the version required by genuine disk-acyclicity (Forster 13.4 / Leray 12.8).

theorem dbar_solvable_open_disk (c : ℂ) {R : ℝ} (hR : 0 < R) {g : ℂ → ℂ}
    (hg : ContDiffOn ℝ (⊤ : ℕ∞) g (ball c R)) :
    ∃ u : ℂ → ℂ, ContDiffOn ℝ (⊤ : ℕ∞) u (ball c R) ∧
      ∀ z ∈ ball c R, DbarDisk.dbar u z = g z