Hartogs' theorem on separate analyticity

TheoremSub-mean-value inequality for the positive logarithm of a holomorphic function#✓fully proved

Let \(c \in \mathbb{C}\), \(R > 0\) and let \(f : \mathbb{C} \to \mathbb{C}\) be analytic at every point of the closed disc \(|z - c| \le R\). Then

\[\log^+ |f(c)| \le \frac{1}{2\pi} \int_0^{2\pi} \log^+ |f(c + R e^{i\theta})| \, d\theta,\]

where \(\log^+ t = \max(0, \log t)\).

theorem hartogs_posLog_norm_le_circleAverage {c : ℂ} {R : ℝ} {f : ℂ → ℂ}
    (hR : 0 < R) (hf : AnalyticOnNhd ℂ f (Metric.closedBall c R)) :
    Real.posLog ‖f c‖ ≤ Real.circleAverage (fun z ↦ Real.posLog ‖f z‖) c R
Used by 1
Used byHartogs' theorem on separate analyticity

TheoremOsgood's lemma at the origin#✓fully proved

Let \(E\) be a complex normed space and let \(f(z, w)\) be a complex-valued function of \(z \in E\) and \(w \in \mathbb{C}\) such that \(z \mapsto f(z, w)\) is complex differentiable on all of \(E\) for every \(w \in \mathbb{C}\) and \(w \mapsto f(z, w)\) is complex differentiable on all of \(\mathbb{C}\) for every \(z \in E\). If there is a real number \(M\) with \(|f(z, w)| \le M\) whenever \(\|z\| \le 1\) and \(|w| \le 1\), then \(f\), as a function on \(E \times \mathbb{C}\), is complex differentiable at \((0, 0)\).

theorem differentiableAt_uncurry_of_separately_differentiable_of_bounded
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
    {f : E → ℂ → ℂ} {M : ℝ}
    (hf₁ : ∀ w, Differentiable ℂ (fun z ↦ f z w))
    (hf₂ : ∀ z, Differentiable ℂ (f z))
    (hM : ∀ z ∈ closedBall 0 1, ∀ w ∈ closedBall 0 1, ‖f z w‖ ≤ M) :
    DifferentiableAt ℂ (Function.uncurry f) (0, 0)
Used by 1
Used byOsgood's lemma for functions bounded on open sets

TheoremOsgood's lemma for functions bounded on open sets#✓fully proved

Let \(E\) be a complex normed space and let \(f(z, w)\) be a complex-valued function of \(z \in E\) and \(w \in \mathbb{C}\) such that \(z \mapsto f(z, w)\) is complex differentiable on all of \(E\) for every \(w \in \mathbb{C}\) and \(w \mapsto f(z, w)\) is complex differentiable on all of \(\mathbb{C}\) for every \(z \in E\). Let \(U \subseteq E\) and \(V \subseteq \mathbb{C}\) be open sets and \(M\) a real number with \(|f(z, w)| \le M\) for all \(z \in U\) and \(w \in V\). Then \(f\), as a function on \(E \times \mathbb{C}\), is complex differentiable at every point \((z_0, w_0)\) with \(z_0 \in U\) and \(w_0 \in V\).

theorem differentiableAt_uncurry_of_separately_differentiable_of_locally_bounded
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
    {f : E → ℂ → ℂ} {U : Set E} {V : Set ℂ} {M : ℝ}
    (hU : IsOpen U) (hV : IsOpen V)
    (hf₁ : ∀ w, Differentiable ℂ (fun z ↦ f z w))
    (hf₂ : ∀ z, Differentiable ℂ (f z))
    (hM : ∀ z ∈ U, ∀ w ∈ V, ‖f z w‖ ≤ M)
    {z₀ : E} (hz₀ : z₀ ∈ U) {w₀ : ℂ} (hw₀ : w₀ ∈ V) :
    DifferentiableAt ℂ (Function.uncurry f) (z₀, w₀)
Uses 1 · Used by 2
Proof usesOsgood's lemma at the origin
Used byHolomorphic dependence of Cauchy coefficients on a parameter · Hartogs' theorem on separate analyticity

TheoremHolomorphic dependence of Cauchy coefficients on a parameter#✓fully proved

Let \(E\) be a finite-dimensional complex normed space, let \(z_0 \in E\), \(w_0 \in \mathbb{C}\), \(A > 0\), \(B > 0\) and \(M \in \mathbb{R}\), and let \(f(z, w)\) be a complex-valued function of \(z \in E\) and \(w \in \mathbb{C}\) such that \(z \mapsto f(z, w)\) is complex differentiable on all of \(E\) for every \(w\) and \(w \mapsto f(z, w)\) is complex differentiable on all of \(\mathbb{C}\) for every \(z\). Suppose \(|f(z, w)| \le M\) whenever \(\|z - z_0\| \le A\) and \(|w - w_0| \le B\). Then for every \(k \in \mathbb{N}\) the \(k\)-th Cauchy coefficient of \(f(z, \cdot)\) about \(w_0\) on the circle of radius \(B/2\),

\[a_k(z) = \frac{1}{2\pi i} \oint_{|w - w_0| = B/2} \frac{f(z, w)}{(w - w_0)^{k+1}} \, dw,\]

is a complex differentiable function of \(z\) on the open ball \(\|z - z_0\| < A/2\).

theorem differentiableOn_cauchyCoefficient_of_separately_differentiable_of_bounded
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E]
    {f : E → ℂ → ℂ} {z₀ : E} {w₀ : ℂ} {A B M : ℝ}
    (hA : 0 < A) (hB : 0 < B)
    (hf₁ : ∀ w, Differentiable ℂ (fun z ↦ f z w))
    (hf₂ : ∀ z, Differentiable ℂ (f z))
    (hM : ∀ z ∈ closedBall z₀ A, ∀ w ∈ closedBall w₀ B, ‖f z w‖ ≤ M)
    (k : ℕ) :
    DifferentiableOn ℂ
      (fun z ↦ (cauchyPowerSeries (f z) w₀ (B / 2) k) (fun _ ↦ 1))
      (ball z₀ (A / 2))
Uses 1 · Used by 1
Proof usesOsgood's lemma for functions bounded on open sets
Used byHartogs' theorem on separate analyticity

TheoremCauchy's estimate for Taylor coefficients#✓fully proved

Let \(f : \mathbb{C} \to \mathbb{C}\) be complex differentiable on all of \(\mathbb{C}\), let \(c \in \mathbb{C}\), \(R > 0\) and \(M \in \mathbb{R}\) with \(|f(z)| \le M\) for all \(z\) with \(|z - c| = R\). Then for every \(k \in \mathbb{N}\) the \(k\)-th coefficient of the Cauchy power series of \(f\) about \(c\) on the circle of radius \(R\),

\[a_k = \frac{1}{2\pi i} \oint_{|w - c| = R} \frac{f(w)}{(w - c)^{k+1}} \, dw,\]

satisfies \(|a_k| \le M R^{-k}\).

theorem norm_cauchyCoefficient_le
    {f : ℂ → ℂ} {c : ℂ} {R M : ℝ}
    (hR : 0 < R) (hf : Differentiable ℂ f)
    (hM : ∀ z ∈ sphere c R, ‖f z‖ ≤ M) (k : ℕ) :
    ‖(cauchyPowerSeries f c R).coeff k‖ ≤ M * R⁻¹ ^ k
Used by 1
Used byHartogs' theorem on separate analyticity

DefinitionIterated integral over a polydisc#✓fully proved

For \(n \in \mathbb{N}\), a function \(u : \mathbb{C}^n \to \mathbb{R}\), a centre \(c \in \mathbb{C}^n\) and a radius \(R \in \mathbb{R}\), the iterated polydisc integral \(I(u, c, R)\) is defined by recursion on \(n\). For \(n = 0\) it is \(u(c)\). For \(n = m + 1\), writing \(c = (c_0, c_1, \dots, c_m)\), it is

\[I(u, c, R) = \int_{|z - c_0| \le R} I\big(u(z, \cdot), (c_1, \dots, c_m), R\big) \, dz,\]

where \(u(z, \cdot)\) is the function \(y \mapsto u(z, y)\) on \(\mathbb{C}^m\) and \(dz\) is Lebesgue measure on \(\mathbb{C}\). Thus, for \(c = (c_0, \dots, c_{n-1})\) and \(D_j\) the closed disc \(|z - c_j| \le R\),

\[I(u, c, R) = \int_{D_0} \cdots \int_{D_{n-1}} u(z_0, \dots, z_{n-1}) \, dz_{n-1} \cdots dz_0.\]

Each integral is a Bochner integral, taken to be \(0\) when the integrand is not integrable.

noncomputable def hartogsPolydiscIntegral : {n : ℕ} →
    ((Fin n → ℂ) → ℝ) → (Fin n → ℂ) → ℝ → ℝ
  | 0, u, c, _ => u c
  | _n + 1, u, c, R =>
      ∫ z in closedBall (c 0) R,
        hartogsPolydiscIntegral (fun y ↦ u (Fin.cons z y)) (c ∘ Fin.succ) R
Used by 2
Used byHartogs' lemma for sub-mean-value functions · Sub-mean-value inequality on a polydisc

TheoremSub-mean-value inequality on a polydisc#✓fully proved

Let \(n \in \mathbb{N}\), let \(u : \mathbb{C}^n \to \mathbb{R}\) be continuous, let \(c \in \mathbb{C}^n\) and \(R > 0\). Write \(\overline{P}(c, R) = \{x \in \mathbb{C}^n : |x_j - c_j| \le R \text{ for all } j\}\) for the closed polydisc, and for \(x \in \mathbb{C}^n\) and \(w \in \mathbb{C}\) write \(x_{j \leftarrow w}\) for \(x\) with its \(j\)-th coordinate replaced by \(w\). Suppose that for every \(x \in \overline{P}(c, R)\), every coordinate \(j\) and every \(r\) with \(0 < r \le R\),

\[u(x) \le \frac{1}{2\pi} \int_0^{2\pi} u(x_{j \leftarrow x_j + r e^{i\theta}}) \, d\theta.\]

Then \((\pi R^2)^n \, u(c) \le I(u, c, R)\), where \(\pi R^2\) is the area of a disc of radius \(R\) and \(I(u, c, R)\) is the iterated polydisc integral of \(u\) about \(c\) with radius \(R\).

theorem hartogsPolydisc_submean
    {n : ℕ} {u : (Fin n → ℂ) → ℝ} (hu : Continuous u)
    {c : Fin n → ℂ} {R : ℝ} (hR : 0 < R)
    (hcircle : ∀ x ∈ closedBall c R, ∀ (i : Fin n) r, r ∈ Ioc 0 R →
      u x ≤ Real.circleAverage (fun z ↦ u (Function.update x i z)) (x i) r) :
    (volume (closedBall (0 : ℂ) R)).toReal ^ n * u c ≤
      hartogsPolydiscIntegral u c R
Uses 1 · Used by 1
Statement usesIterated integral over a polydisc
Used byHartogs' lemma for sub-mean-value functions

TheoremHartogs' lemma for sub-mean-value functions#✓fully proved

Let \(n \in \mathbb{N}\), \(c \in \mathbb{C}^n\), \(R > 0\) and \(C \ge 0\). For \(\rho \ge 0\) write \(\overline{P}(c, \rho) = \{x \in \mathbb{C}^n : |x_j - c_j| \le \rho \text{ for all } j\}\) for the closed polydisc, and for \(x \in \mathbb{C}^n\) and \(w \in \mathbb{C}\) write \(x_{j \leftarrow w}\) for \(x\) with its \(j\)-th coordinate replaced by \(w\). Let \((u_k)_{k \in \mathbb{N}}\) be real-valued functions on \(\mathbb{C}^n\) such that each \(u_k\) is continuous on \(\overline{P}(c, R)\), \(0 \le u_k(x) \le C\) for all \(k\) and all \(x \in \overline{P}(c, R)\), and \(u_k(x) \to 0\) as \(k \to \infty\) for every \(x \in \overline{P}(c, R)\). Suppose moreover that for every \(k\), every \(x \in \overline{P}(c, R)\), every coordinate \(j\) and every \(r > 0\) such that \(x_{j \leftarrow z} \in \overline{P}(c, R)\) for all \(z\) with \(|z - x_j| \le r\),

\[u_k(x) \le \frac{1}{2\pi} \int_0^{2\pi} u_k(x_{j \leftarrow x_j + r e^{i\theta}}) \, d\theta.\]

Then for every \(\varepsilon > 0\) there is \(K\) such that \(u_k(x) \le \varepsilon\) for all \(k \ge K\) and all \(x \in \overline{P}(c, R/4)\).

MathlibExt.Analysis.Complex.HartogsWanted.hartogs_eventually_uniform_of_submean · 17 lines 
theorem hartogs_eventually_uniform_of_submean
    {n : ℕ} {u : ℕ → (Fin n → ℂ) → ℝ}
    {c : Fin n → ℂ} {R C : ℝ}
    (hR : 0 < R)
    (hu : ∀ k, ContinuousOn (u k) (closedBall c R))
    (hu0 : ∀ k x, x ∈ closedBall c R → 0 ≤ u k x)
    (hC : 0 ≤ C)
    (hub : ∀ k x, x ∈ closedBall c R → u k x ≤ C)
    (hlim : ∀ x ∈ closedBall c R,
      Tendsto (fun k ↦ u k x) atTop (nhds 0))
    (hcircle : ∀ k x, x ∈ closedBall c R → ∀ (i : Fin n) r, 0 < r →
      (∀ z ∈ closedBall (x i) r,
        Function.update x i z ∈ closedBall c R) →
      u k x ≤
        Real.circleAverage (fun z ↦ u k (Function.update x i z)) (x i) r)
    {ε : ℝ} (hε : 0 < ε) :
    ∀ᶠ k in atTop, ∀ x ∈ closedBall c (R / 4), u k x ≤ ε
Uses 2 · Used by 1
Proof usesIterated integral over a polydisc · Sub-mean-value inequality on a polydisc
Used byHartogs' theorem on separate analyticity

TheoremHartogs' theorem on separate analyticity#✓fully proved

Let \(n \in \mathbb{N}\) and let \(f : \mathbb{C}^n \to \mathbb{C}\) be such that for every point \(x \in \mathbb{C}^n\) and every coordinate \(i\), the function \(z \mapsto f(x_1, \dots, x_{i-1}, z, x_{i+1}, \dots, x_n)\) is complex differentiable on all of \(\mathbb{C}\). Then \(f\) is complex differentiable on all of \(\mathbb{C}^n\).

No continuity or boundedness of \(f\) is assumed.

Proof: induction on the number of variables. Baire category gives a polydisc where \(f\) is bounded, where Osgood's lemma makes it holomorphic; Hartogs' lemma on sub-mean-value functions then makes the Cauchy expansion in the last variable converge locally uniformly.

theorem hartogs_separate_analyticity
    {n : ℕ}
    {f : EuclideanSpace ℂ (Fin n) → ℂ}
    (hf : ∀ (x : EuclideanSpace ℂ (Fin n)) (i : Fin n),
      Differentiable ℂ (fun z : ℂ =>
        f (WithLp.toLp 2 (Function.update (WithLp.ofLp x) i z)))) :
    Differentiable ℂ f
Sources
  • Hartogs separate analyticity (Osgood–Hartogs); see Hörmander; Lean is scalar-valued entire separately holomorphic via Function.update slices implies jointly Differentiable ℂ, finite-dimensional ℂⁿ specialization.
Uses 5
Proof usesOsgood's lemma for functions bounded on open sets · Holomorphic dependence of Cauchy coefficients on a parameter · Hartogs' lemma for sub-mean-value functions · Sub-mean-value inequality for the positive logarithm of a holomorphic function · Cauchy's estimate for Taylor coefficients
9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.