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:A→E 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. B∘f is continuous on γ∗ and B ⁣(∫γf(z) dz)=∫γ(B∘f)(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(γ) sup⁡z∈γ∗∥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:A→E, 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]

∫γf dz 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)∥≤∥B∥ ∥u∥ for all u,v∈A 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(γ)=∑k∫tk−1tk∣γ′(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.1L1L2algebra

B∘f 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.

1.2L1L2algebra

For every such tagged partition, ∥∑jf(γ(ξj))vk(j)(ξj)Δj∥≤(sup⁡γ∗∥f∥)∑j∣vk(j)(ξj)∣Δj.

2.1step 1.1L1L2

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

2.2step 1.2L1L3

Passing to the limit in [step 1.2] and using that the speed sums converge to the length, as in [L3], gives the estimate ∥∫γf dz∥≤L(γ)sup⁡γ∗∥f∥, which is claim 2.

3.1step 2.1step 2.2∎

The two claims of the statement are exactly [step 2.1] and [step 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