Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26
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 modulus of a holomorphic function on a closed polydisc is bounded by its supremum on the distinguished boundary

Statement

Let m1, let aCm, let r be a polyradius, and let f be continuous on the closed polydisc Δr(a) and holomorphic on Δr(a). Then

supΔr(a)f=supΓr(a)f,

and both suprema are attained. For m2 the bounding set Γr(a) is a proper subset of the topological boundary of Δr(a), so this is stronger than the bound by the topological boundary.

Facts & Assumptions

Given: f continuous on Δr(a) and holomorphic on Δr(a); Cm is read through Complex m-space and its real coordinate dictionary.

[L1]

If Ω is a bounded complex domain and g is continuous on Ω and holomorphic on Ω, then there is ζΩ with g(z)g(ζ) for every zΩ (Boundary maximum modulus principle on a bounded domain).

[L2]

Δr(a), Δr(a) and Γr(a) are defined coordinatewise by zkak<rk, rk and =rk; polydiscs are convex; and for m2 the distinguished boundary is a proper subset of the topological boundary (Balls, polydiscs and the distinguished boundary in Cm, A convex subset of Rm contains every line segment between two of its points).

[L3]

A holomorphic function of several variables is continuous and separately holomorphic (A holomorphic function of several variables is continuous and separately holomorphic), separate holomorphy being holomorphy of each slice on its open slice domain (Separately holomorphic functions).

[L4]

If a property holds at 0 and passes from p to p+1, it holds for every natural number (The principle of mathematical induction).

[L6]

A continuous map from a compact metric space is uniformly continuous (Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous).

[L7]

A complex domain is a nonempty, connected, open subset of C (A complex domain is a nonempty connected open subset of C).

[L8]

A set is open exactly when each of its points admits a ball inside it, a set is closed when its complement is open, and B(x,s)={y:d(x,y)<s} (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, Open ball, closed ball and sphere in a metric space).

[L9]

zw=zw and z+wz+w (Conjugation is an involutive real-field automorphism, zz=z2, and modulus is definite, multiplicative, and subadditive).

[L10]

Continuity of a map into Rn from a subset of a metric space is the usual εδ condition with the Euclidean norm (Vector-valued functions f:ARm, their limits and continuity, with the dictionary to the metric notions).

Proof

technique · direct
1.1

The sets Δr(a) and Γr(a) are closed and bounded by [L2] and [L9], hence compact and nonempty by [L5], so f attains a maximum on each by [L5] and both suprema are attained real numbers; write P=supΓr(a)f. By [L6] the function f is uniformly continuous on Δr(a).

givenL2L5L6L9
2.1

For a polyradius s with sk<rk for every k, put Ap:=sup{f(w):wΔs(a) and wkak=sk for every k<p} for 0pm; these are attained maxima by the argument of step 1.1 applied to the corresponding closed bounded sets, and Am=supΓs(a)f.

step 1.1L2L5
2.2

Let 0<t<1 and take s=tr. Every wΓtr(a) satisfies a+(wa)/tΓr(a) and (a+(wa)/t)w=(1/t1)wa by [L9], which tends to 0 as t1 uniformly in w because wa is bounded on Δr(a); so by the uniform continuity of step 1.1 and [L10], supΓtr(a)fP+ε once t is close enough to 1, for any prescribed ε>0.

step 1.1L9L10
3.1

Fix such an s and p<m, and let wΔs(a) have wkak=sk for k<p. Replacing the pth coordinate of w by any ξ with ξap<rp leaves the point in Δr(a), because the other coordinates satisfy wkaksk<rk; so by [L3] the slice g(ξ) is holomorphic on the disc D(ap,rp) and in particular continuous on the closed disc D(ap,sp), which is the closure of D(ap,sp) since every point of the circle is a limit of interior points along its radius and the closed disc is closed by [L8] and [L9].

step 2.1L2L3L8L9
4.1

The disc D(ap,sp) is a bounded complex domain by [L2], [L7] and [L8], being nonempty, open, convex hence connected, and bounded, and its topological boundary is the circle ξap=sp by step 3.1. So [L1] applied to the slice gives ξ on that circle with f(w)g(ξ), and the point obtained from w by putting ξ in the pth slot lies in Δs(a) with its first p+1 coordinates on their circles; hence f(w)Ap+1. Taking the supremum over such w gives ApAp+1.

step 2.1step 3.1L1L2L7L8
5.1

By [L4] the chain of step 4.1 gives A0Am, that is supΔs(a)fsupΓs(a)f for every polyradius s with sk<rk.

step 2.1step 4.1L4
6.1

Let zΔr(a) and ε>0. For t<1 the point a+t(za) lies in Δtr(a)Δtr(a) by [L2] and [L9], so steps 5.1 and 2.2 give f(a+t(za))supΓtr(a)fP+ε for t close enough to 1; letting t1 and using the continuity of f at z gives f(z)P+ε, hence f(z)P.

step 5.1step 2.2L2L9L10
7.1

Step 6.1 gives supΔr(a)fP, and the reverse inequality holds because Γr(a)Δr(a) by [L2]; so the two suprema are equal and attained by step 1.1. For m2 the set Γr(a) is by [L2] a proper subset of the topological boundary, so the bound is by a strictly smaller set than in the one-variable statement.

step 1.1step 6.1L2

Depends on

Used by

Dependency tree · two levels

89 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources