Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-24
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.

Maximum principle on a closed strip for bounded holomorphic functions

Statement

A bounded function continuous on the closed strip, holomorphic inside, and of modulus at most one on both boundary lines has modulus at most one throughout the strip.

Precisely, let S={zC:0Rez1}. If g:SC is bounded and continuous, is holomorphic on 0<Rez<1, and satisfies g(iy)1,g(1+iy)1(yR), then g(z)1 for every zS.

Facts & Assumptions

Given: The closed strip S and a function g satisfying the hypotheses. The exponential is entire, holomorphic compositions obey the chain rule, and the real exponential tends to 0 at (The complex exponential is entire and its complex derivative is itself, The chain rule for complex derivatives, The exponential tends to + at + and to 0 at ).

[L1]

If Ω is a bounded complex domain and f is continuous on Ω and holomorphic on Ω, then f attains its maximum on Ω (Boundary maximum modulus principle on a bounded domain).

[L3]

A segment t(1t)v0+tv1 that lies in a subset A is a continuous path in A, and a path-connected subset of a topological space is a connected subset (A finite concatenation of straight segments in Rn is a continuous path, Every path-connected space is connected, and every path component lies inside a component, claim 2).

Proof

technique · direct
1.1

Fix ε>0 and define gε(z):=g(z)exp(ε(z21)). By [L2], gε(x+iy)=g(x+iy)exp(ε(x2y21)). On x=0 the exponential factor is at most 1, and on x=1 it is exp(εy2)1, so both vertical boundary lines retain modulus at most 1.

L2givenalgebra
2.1

Choose C0 with gC. Since x210 for 0x1, the horizontal sides at heights y=±T satisfy gε(x±iT)Cexp(εT2). For all sufficiently large T, this is at most 1.

step 1.1givenchoose
3.1

The rectangle RT:={z:0<Rez<1, Imz<T} is bounded, open and nonempty, and each coordinate of a segment between two of its points stays between that coordinate's endpoints, so the segment stays in RT and [L3] makes RT connected; it is therefore a bounded complex domain. With T as in step 2.1, all four boundary sides of RT have gε1. The boundary maximum theorem [L1] therefore gives gε1 throughout RT.

step 2.1L1L3
4.1

Given zS, choose such a T>Imz. Step 3.1 yields g(z)exp(εRe(z21)). Letting ε decrease to 0 gives g(z)1. This also covers both vertical boundary lines and the zero function.

step 3.1givenalgebra

Depends on

Used by

Dependency tree · two levels

42 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