A machine-checked solution to the Jacobians challenge

16.1. Keystones🔗

RealForms.dbarsource · report an issue

noncomputable def dbar (f : ℂ → ℂ) (z : ℂ) : ℂ

DbarOpenDisk.dbar_solvable_open_disksource · report an issue

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
  • CechDiskAcyclic