HolomorphicRegularity.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Mahler.locally_bounded_fderiv line 16

Source documentation

The complex Schwarz estimate gives a local bound on the full derivative, from first-order holomorphicity alone.

lemma locally_bounded_fderiv {f : E → ℂ} {U : Set E} {x : E}
    (hU : IsOpen U) (hx : x ∈ U) (hf : DifferentiableOn ℂ f U) :
    ∃ r > 0, ∃ C ≥ 0, ball x r ⊆ U ∧
      ∀ y ∈ ball x r, ‖fderiv ℂ f y‖ ≤ C := by
…

lemma OAI.Mahler.differentiable_cauchy_parameter line 49

Source documentation

Differentiability of a Cauchy integral in an ambient finite-dimensional complex parameter. The derivative bound is obtained locally by Schwarz.

lemma differentiable_cauchy_parameter {f : E → ℂ} {U : Set E} {x v : E}
    {R C r : ℝ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U)
    (hR : 0 < R) (hr : 0 < r) (hv : r * ‖v‖ < R / 2)
    (hsub : ball x R ⊆ U)
    (hb : ∀ y ∈ ball x R, ‖fderiv ℂ f y‖ ≤ C) :
    DifferentiableAt ℂ
      (fun y => ∮ z in C(0, r), (1 / z ^ 2) • f (y + z • v)) x := by
…

theorem OAI.Mahler.differentiableAt_fderiv_apply_of_open line 117

Source documentation

A directional component of the ambient first derivative is holomorphic. Only first-order holomorphicity on the open domain is assumed.

theorem differentiableAt_fderiv_apply_of_open {f : E → ℂ} {U : Set E} {x v : E}
    (hU : IsOpen U) (hx : x ∈ U) (hf : DifferentiableOn ℂ f U) :
    DifferentiableAt ℂ (fun y => fderiv ℂ f y v) x := by
…

theorem OAI.Mahler.contDiffOn_nat_of_differentiableOn_open line 163
Source documentation
Holomorphic functions on open finite-dimensional complex domains are C^k for every finite k. Smoothness is derived, not added to the hypotheses.
```
theorem contDiffOn_nat_of_differentiableOn_open {U : Set E} (hU : IsOpen U)
    (k : ℕ) {f : E → ℂ} (hf : DifferentiableOn ℂ f U) :
    ContDiffOn ℂ k f U := by
…
```