Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22
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.

Contour integral commutes with bounded linear maps

Statement

Let A be a unital complex Banach algebra, let E be a complex Banach space, let B:AE be a bounded complex-linear map (A bounded linear operator between normed spaces), let γ be a piecewise C1 complex contour, and let f:γA be continuous. Then

  1. Bf is continuous on γ and B ⁣(γf(z)dz)=γ(Bf)(z)dz, the first integral being that of Banach algebra valued contour integral and the second computed in the Banach space E;
  2. γf(z)dz    L(γ)supzγf(z), where L(γ) is the length of γ.

Facts & Assumptions

Given: A unital complex Banach algebra A, a complex Banach space E, a bounded linear B:AE, a piecewise C1 contour γ:[a,b]C with trace γ and length L(γ), a C1 subdivision a=t0<<tm=b with derivative extensions vk on the closed pieces, and a continuous f:γA.

[L1]

γfdz is the limit, over tagged partitions refining the subdivision, of jf(γ(ξj))vk(j)(ξj)Δj, where the derivative extension belonging to the subinterval is used even when a tag is a corner; the chain version is the corresponding finite sum (Banach algebra valued contour integral).

[L2]

B is complex-linear and bounded, and its operator norm satisfies B(λu+μv)=λB(u)+μB(v) and B(u)Bu for all u,vA and scalars λ,μ (A bounded linear operator between normed spaces, The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[L3]

For a piecewise C1 path γ the length is the sum of the speed integrals over a C1 subdivision: L(γ)=ktk1tkγ(t)dt; on each such interval the speed is continuous, and the corresponding refined Riemann sums converge to this sum (A continuous piecewise-C1 path is rectifiable and its length is the sum of the speed integrals over its pieces).

Proof

technique · direct
1.1

Bf is continuous as a composition of continuous maps, and for every tagged partition refining the fixed subdivision, jB(f(γ(ξj)))vk(j)(ξj)Δj=B ⁣(jf(γ(ξj))vk(j)(ξj)Δj), because B is linear and the scalars vk(j)(ξj)Δj pull out of B.

L1L2algebra
1.2

For every such tagged partition, jf(γ(ξj))vk(j)(ξj)Δj(supγf)jvk(j)(ξj)Δj.

L1L2algebra
2.1

Passing to the limit in [step 1.1] using continuity of B and the convergence of the Riemann sums in [L1] gives B(γfdz)=γ(Bf)dz, which is claim 1.

step 1.1L1L2
2.2

Passing to the limit in [step 1.2] and using that the speed sums converge to the length, as in [L3], gives the estimate γfdzL(γ)supγf, which is claim 2.

step 1.2L1L3
3.1

The two claims of the statement are exactly [step 2.1] and [step 2.2].

step 2.1step 2.2

Depends on

Used by

Dependency tree · two levels

18 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