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 . If is bounded and continuous, is holomorphic on , and satisfies then for every .
Facts & Assumptions
Given: The closed strip and a function satisfying the hypotheses. The exponential is entire, holomorphic compositions obey the chain rule, and the real exponential tends to 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 at ).
If is a bounded complex domain and is continuous on and holomorphic on , then attains its maximum on (Boundary maximum modulus principle on a bounded domain).
For real , (, , and ).
A segment that lies in a subset is a continuous path in , and a path-connected subset of a topological space is a connected subset (A finite concatenation of straight segments in is a continuous path, Every path-connected space is connected, and every path component lies inside a component, claim 2).
Proof
Fix and define . By [L2], . On the exponential factor is at most , and on it is , so both vertical boundary lines retain modulus at most .
Choose with . Since for , the horizontal sides at heights satisfy . For all sufficiently large , this is at most .
The rectangle 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 and [L3] makes connected; it is therefore a bounded complex domain. With as in step 2.1, all four boundary sides of have . The boundary maximum theorem [L1] therefore gives throughout .
Given , choose such a . Step 3.1 yields . Letting decrease to gives . This also covers both vertical boundary lines and the zero function.
Depends on
- Boundary maximum modulus principle on a bounded domain
- The complex exponential is entire and its complex derivative is itself
- $\exp(x+iy)=e^x(\cos y+i\sin y)$, $|\exp(x+iy)|=e^x$, and $e^{i\pi}+1=0$
- The chain rule for complex derivatives
- The exponential tends to $+\infty$ at $+\infty$ and to $0$ at $-\infty$
- A finite concatenation of straight segments in $\mathbb{R}^n$ is a continuous path
- Every path-connected space is connected, and every path component lies inside a component
Used by
- Hadamard three-lines theorem Theorem
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
- J. A. Tropp, Matrix Analysis, Claim 7.14 (standard reference, not scraped)