LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The flow of a bounded holomorphic field on a polydisc: existence in complex time, displacement bound, holomorphy, and the composition law

Statement

In this item, a complex-time solution on an open set $Ω \subseteq C$ is a holomorphic map $Y : Ω \to D$ satisfying $Y^{'} (τ) = F (Y (τ))$ . For a closed time disc, a solution means the restriction of such a map that is continuous on the closed disc.

Let $n \geq 1$ , let $D \subseteq C^{n}$ be open, let $F : D \to C^{n}$ be holomorphic in the sense of Complex phase domains, holomorphic maps on $C^{m}$ , and the complexified canonical form and bracket with $∥ F ∥ \leq M$ everywhere on $D$ for some $M > 0$ , let $Z_{0} \in D$ and let $s > 0$ satisfy $Δ_{s} (Z_{0}) \subseteq D$ (Complex phase domains, holomorphic maps on $C^{m}$ , and the complexified canonical form and bracket). Put

$t_{0} : = \frac{s}{8 n M}, D_{t_{0}} : = {t \in C : ∣ t ∣ \leq t_{0}} .$

Then there is a map $Φ : D_{t_{0}} \times B (Z_{0}, s / 4) \to D$ that is the restriction of a jointly holomorphic map on ${∣ t ∣ < 3 t_{0} / 2} \times B (Z_{0}, s / 4)$ , such that:

Solution. For every $Z \in B (Z_{0}, s / 4)$ , $t \mapsto Φ (t, Z)$ solves $Y^{'} = F (Y)$ with $Y (0) = Z$ for $∣ t ∣ < 3 t_{0} / 2$ . It is the unique holomorphic solution on $∣ t ∣ < t_{0}$ among solutions with values in $B (Z, s / 2)$ . On $D_{t_{0}}$ it satisfies $∥ Φ (t, Z) - Z ∥ \leq M ∣ t ∣ \leq s / (8 n)$ .
Holomorphy. $Φ$ is holomorphic on the open set ${∣ t ∣ < t_{0}} \times B (Z_{0}, s / 4)$ in the sense of Complex phase domains, holomorphic maps on $C^{m}$ , and the complexified canonical form and bracket, and $Φ (0, Z) = Z$ .
Composition and inverse. Repeating the construction with each initial point as a center gives a family of compatible local maps; in this clause $Φ (t, Z)$ denotes the map in the chart centered at $Z$ . If the two sides are defined by branches on the same connected open continuation of a solution, then $Φ (s_{2}, Φ (s_{1}, Z)) = Φ (s_{1} + s_{2}, Z)$ . In particular, along the reverse continuation of the same local solution, $Φ (- s_{1}, Φ (s_{1}, Z)) = Z$ whenever both sides are defined.

Facts & Assumptions

Given: The open $D \subseteq C^{n}$ , the holomorphic $F$ with $∥ F ∥ \leq M$ on $D$ , the point $Z_{0}$ , the radius $s$ with $Δ_{s} (Z_{0}) \subseteq D$ , and $t_{0} = s / (8 n M)$ .

[L1]

Scalar Cauchy estimates on polydiscs (Iterated Cauchy formula, power-series expansion and Cauchy estimates for functions continuous and separately holomorphic on a polydisc): if a scalar holomorphic $g$ is bounded by $A$ on the distinguished boundary of a polydisc of radius $r$ about $W$ , then $∣ \partial_{z_{k}} g (W) ∣ \leq A / r$ . Applying this to each component $F_{i}$ gives $∣ \partial_{z_{k}} F_{i} (W) ∣ \leq 4 M / s$ whenever $Δ_{s / 4} (W) \subseteq D$ . Thus the Euclidean norm of the $k$ -th column of $D F (W)$ is at most $4 \sqrt{n} M / s$ . For $v \in C^{n}$ , $∥ D F (W) v ∥ \leq (4 \sqrt{n} M / s) \sum_{k} ∣ v_{k} ∣ \leq (4 n M / s) ∥ v ∥$ , using $(\sum_{k} ∣ v_{k} ∣)^{2} \leq n \sum_{k} ∣ v_{k} ∣^{2}$ . This supplies the claimed vector-valued Lipschitz constant without applying a scalar estimate directly to a vector-valued map.

[L2]

Calculus of holomorphic maps (Calculus of holomorphic maps: chain rule, Wirtinger derivatives, coefficient extraction in one variable, and locally uniform limits): compositions of holomorphic maps are holomorphic with the chain rule; a locally uniform limit of holomorphic maps is holomorphic.

[L3]

Parameter integrals (A jointly continuous finite-interval parameter integral of holomorphic functions is holomorphic): a jointly continuous scalar $φ : [0, 1] \times Ω \to C$ whose slices are holomorphic in the complex parameter has a holomorphic integral, with differentiation under the integral when the parameter derivative is jointly continuous. For a $C^{n}$ -valued integrand, apply this scalar result to each of its $n$ components; the resulting integral is holomorphic componentwise.

[L4]

Completeness and componentwise uniform limits. A uniformly Cauchy sequence of maps into $C^{n} ≅ R^{2 n}$ has a pointwise limit: at each argument its $2 n$ real coordinates are Cauchy and converge by The reals are complete, and assembling these limits gives a vector limit. A uniform tail bound in Euclidean norm passes to that limit by continuity of the norm, so convergence is uniform. Each component of a uniform limit of continuous $C^{n}$ -valued maps is continuous by A uniform limit of continuous complex-valued functions is continuous; finitely many continuous components give a continuous vector map, since $∥ v ∥ \leq \sqrt{n} \max_{i} ∣ v_{i} ∣$ . Likewise a locally uniform limit of holomorphic scalar functions is holomorphic by Locally uniform limits of holomorphic functions are holomorphic and their derivatives converge locally uniformly. For a finite vector of componentwise holomorphic functions, collect their scalar derivatives into one complex-linear map; the Euclidean norm of the vector of finitely many $o (∥ v ∥)$ remainders is again $o (∥ v ∥)$ , so the vector map is holomorphic in the total-derivative sense.

[L5]

Integrals of continuous $C^{n}$ -valued functions satisfy $∥ \int_{0}^{1} φ d σ ∥ \leq \int_{0}^{1} ∥ φ ∥ d σ$ ; the complex segment integral $\int_{0}^{t} ψ (τ) d τ = t \int_{0}^{1} ψ (σ t) d σ$ is thereby controlled (For $a \leq b$ and $f : [a, b] \to R^{m}$ integrable when $a < b$ , $∥ \int_{a}^{b} f ∥_{2} \leq \int_{a}^{b} ∥ f ∥_{2}$ ; for $a < b$ , $∥ f ∥_{2}$ is integrable, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral).

[L6]

Polydisc and ball geometry: $B (W, r) \subseteq Δ_{r} (W)$ and $Δ_{r} (W) \subseteq B (W, r \sqrt{n})$ for every radius $r$ ; balls are convex and compact balls are compact (Complex phase domains, holomorphic maps on $C^{m}$ , and the complexified canonical form and bracket, Open ball, closed ball and sphere in a metric space, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value, Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ , The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder).

[L7]

The vector-valued fundamental theorem of calculus gives $\int_{0}^{1} u^{'} (σ) d σ = u (1) - u (0)$ for a differentiable $u : [0, 1] \to R^{2 n}$ with integrable derivative; its bounded-derivative clause says that if $u$ is continuous and $∥ u^{'} (σ) ∥ \leq A$ on $(0, 1)$ , then $∥ u (1) - u (0) ∥ \leq A$ (If $f : [a, b] \to R^{m}$ is differentiable with integrable $f^{'}$ then $\int_{a}^{b} f^{'} = f (b) - f (a)$ ; and a bounded derivative makes $f$ Lipschitz, both clauses).

Proof

technique · constructive; Picard iteration with the contraction estimate on the polydisc $\Delta_{s/2}(Z_0)$, uniform Cauchy convergence, and slice-wise holomorphy of the limit

1.1givenL1L2L6L7

Lipschitz estimate. For every $W$ with $∥ W - Z_{0} ∥ \leq 3 s / 4$ , the polydisc $Δ_{s / 4} (W)$ is contained in $Δ_{s} (Z_{0}) \subseteq D$ : each coordinate satisfies $∣ ζ_{k} - Z_{0}_{k} ∣ \leq ∣ W_{k} - Z_{0}_{k} ∣ + ∣ ζ_{k} - W_{k} ∣ < 3 s / 4 + s / 4 = s$ . By [L1], the operator norm of $D F (W)$ is at most $Λ = 4 n M / s$ . For $W, W^{'} \in B (Z_{0}, 3 s / 4)$ the segment $u (t) = F (W^{'} + t (W - W^{'}))$ , $0 \leq t \leq 1$ , stays in the convex ball by [L6]; by the chain rule in [L2], its derivative is $D F (W^{'} + t (W - W^{'})) (W - W^{'})$ and has norm at most $Λ ∥ W - W^{'} ∥$ . Applying [L7] to this real-parameter curve gives $∥ F (W) - F (W^{'}) ∥ \leq Λ ∥ W - W^{'} ∥$ . Since $t_{0} = s / (8 n M)$ , $Λ = 1 / (2 t_{0})$ .

2.1givenstep 1.1L4L5L6algebra

The Picard map [construct]. Fix $Z \in B (Z_{0}, s / 4)$ and let $X_{Z}$ be the set of continuous $γ : D_{t_{0}} \to C^{n}$ with $γ (0) = Z$ and $∥ γ (t) - Z ∥ \leq s / 2$ for all $t \in D_{t_{0}}$ , equipped with the supremum distance. Define $T γ$ by $(T γ) (t) : = Z + t \int_{0}^{1} F (γ (σ t)) d σ$ . For $γ \in X_{Z}$ , the integrand is continuous; since $∥ Z - Z_{0} ∥ < s / 4$ and $∥ γ (σ t) - Z ∥ \leq s / 2$ , its values satisfy $∥ γ (σ t) - Z_{0} ∥ < 3 s / 4$ and lie in $D$ . Therefore $∥ (T γ) (t) - Z ∥ \leq ∣ t ∣ M \leq t_{0} M = s / (8 n) \leq s / 2$ : $T$ maps $X_{Z}$ to itself. Moreover, by step 1.1 and [L5], for $γ_{1}, γ_{2} \in X_{Z}$ , $∥ (T γ_{1}) (t) - (T γ_{2}) (t) ∥ \leq ∣ t ∣ \int_{0}^{1} Λ ∥ γ_{1} (σ t) - γ_{2} (σ t) ∥ d σ \leq t_{0} Λ ∥ γ_{1} - γ_{2} ∥_{\infty} = \frac{1}{2} ∥ γ_{1} - γ_{2} ∥_{\infty} .$ The same construction on $D_{t_{*}}$ with $t_{*} : = 3 t_{0} / 2$ also works: $t_{*} Λ = 3 / 4 < 1$ and $t_{*} M = 3 s / (16 n) < s / 2$ , so the iterates have summable successive differences bounded by a geometric sequence with ratio $3 / 4$ and remain in $X_{Z}$ . The coordinatewise completeness argument of [L4] gives their limit. Repeating steps 3.1--5.1 with this radius yields a solution holomorphic on $∣ t ∣ < t_{*}$ , so the solution on $D_{t_{0}}$ extends through its boundary.

3.1givenstep 2.1L1L2L3L4

Iterates. For each initial value $Z$ , put $γ_{0} (t, Z) : = Z$ and $γ_{m + 1} (\cdot, Z) : = T (γ_{m} (\cdot, Z))$ ; all $γ_{m} (\cdot, Z)$ lie in $X_{Z}$ by step 2.1, and $∥ γ_{m + 1} (\cdot, Z) - γ_{m} (\cdot, Z) ∥_{\infty} \leq 2^{- m} ∥ γ_{1} (\cdot, Z) - γ_{0} (\cdot, Z) ∥_{\infty} \leq 2^{- m} t_{0} M$ . Joint continuity in $(t, Z)$ follows by induction: $γ_{0} (t, Z) = Z$ is continuous, and if $γ_{m}$ is jointly continuous then $(σ, t, Z) \mapsto F (γ_{m} (σ t, Z))$ is continuous; on each compact parameter neighborhood its $σ$ -integral is continuous by uniform continuity. Each $γ_{m}$ is also holomorphic on $D_{t_{0}}$ in the variable $t$ : $γ_{0}$ is constant; if $γ_{m}$ is holomorphic then $t \mapsto γ_{m} (σ t)$ and its composition with $F$ are holomorphic for each $σ$ by [L2]. The parameter integral in the definition of $T$ is holomorphic componentwise by [L3], so every component of $T γ_{m}$ is holomorphic in $t$ ; the finite-dimensional assembly described in [L4] makes the vector map holomorphic. For fixed $t$ , the same induction shows that each component of $γ_{m} (t, \cdot)$ is holomorphic in each coordinate of $Z$ : apply [L3] separately to each output component and each input coordinate. Thus the iterates are continuous and separately holomorphic in the variables needed below.

4.1givenstep 3.1L1L2L4

Uniform convergence. By step 3.1, $(γ_{m})$ is uniformly Cauchy on $D_{t_{0}} \times B (Z_{0}, s / 4)$ : $∥ γ_{m^{'}} - γ_{m} ∥_{\infty} \leq 2^{- m + 1} t_{0} M$ for $m^{'} \geq m$ . By the coordinatewise completeness argument in [L4], it converges uniformly to a map $Φ$ ; the componentwise continuity argument in [L4] makes $Φ$ continuous. It satisfies $∥ Φ (t, Z) - Z ∥ \leq s / 2$ , indeed $\leq M ∣ t ∣ \leq s / (8 n)$ , and $Φ (0, Z) = Z$ . For fixed $Z$ , each component of $t \mapsto Φ (t, Z)$ is a locally uniform limit of holomorphic functions, so it is holomorphic by [L4]; the same applies to each output component with $t$ fixed and one complex coordinate of $Z$ varying. At any point of the open product choose a polydisc contained in it. Each scalar component is continuous and separately holomorphic there, so Iterated Cauchy formula, power-series expansion and Cauchy estimates for functions continuous and separately holomorphic on a polydisc makes that component holomorphic in the total-derivative sense; the finite-dimensional assembly in [L4] then makes $Φ$ a holomorphic $C^{n}$ -valued map.

5.1givenstep 4.1L2L3L5L7

Fixed point and differential equation. $T$ is Lipschitz with constant $1 / 2$ on $X_{Z}$ by step 2.1, so $T Φ = \lim_{m} T γ_{m} = \lim_{m} γ_{m + 1} = Φ$ uniformly. Put $G (t) : = F (Φ (t, Z))$ , which is holomorphic with continuous derivative on $∣ t ∣ < t_{0}$ by step 4.1 and [L2]. The fixed-point identity is $Φ (t, Z) = Z + t \int_{0}^{1} G (σ t) d σ$ . By the derivative formula in [L3], applied componentwise, $\frac{d}{d t} Φ (t, Z) = \int_{0}^{1} G (σ t) d σ + t \int_{0}^{1} σ G^{'} (σ t) d σ = \int_{0}^{1} \frac{d}{d σ} (σ G (σ t)) d σ = G (t) = F (Φ (t, Z)),$ where the penultimate equality is [L7] applied to the $R^{2 n}$ -valued curve $σ \mapsto σ G (σ t)$ . The fixed-point identity also gives $Φ (0, Z) = Z$ and, by [L5], $∥ Φ (t, Z) - Z ∥ \leq M ∣ t ∣ \leq s / (8 n)$ . This proves clause 1 except uniqueness, and clause 2.

6.1givenstep 2.1step 5.1L6discharge-construct∎

Uniqueness and composition. Two solutions in the prescribed curve ball obey the contraction inequality of step 2.1 and coincide. More generally, two local solutions through any point agree on a sufficiently small time disc by that same argument centred at the point; the set of times of agreement is both relatively open and closed in a connected common continuation, hence they agree there. For fixed $s_{1}$ , the curves $t \mapsto Φ (s_{1} + t, Z)$ and $t \mapsto Φ (t, Φ (s_{1}, Z))$ have the same initial value and derivative $F$ wherever both are defined. Local uniqueness, followed by this continuation argument, proves the qualified composition rule and, with $t = - s_{1}$ , the inverse rule. This proves all three clauses.

Remarks

The lemma is local by design: the time radius $t_{0} = s / (8 n M)$ shrinks with the size of the field and with the complex margin, and the initial-data ball is $B (Z_{0}, s / 4)$ . Applying it at each point gives compatible local solution maps. Continued branches are used on specified connected time domains; the local construction does not select a single-valued global maximal flow.
Clause 1's uniqueness is asserted among solutions with values in the ball $B (Z, s / 2)$ , which is what the contraction proof gives; no global uniqueness of complex-time solutions outside that ball is claimed.

The flow of a bounded holomorphic field on a polydisc: existence in complex time, displacement bound, holomorphy, and the composition law

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources