LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Average convergence for a continuous Banach-valued function

Statement

Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )) for the Lebesgue-measure interfaces. Let $X$ be a real or complex Banach space, let $a < b$ and let $f : [a, b] \to X$ be continuous. Then $f$ is Bochner integrable, and for $t \in [a, b)$ and $h > 0$ with $t + h \leq b$ one has $∥ \frac{1}{h} \int_{t}^{t + h} f (s) d s - f (t) ∥ \leq \sup_{s \in [t, t + h]} ∥ f (s) - f (t) ∥ \to 0$ as $h ↓ 0$ ; analogously $\frac{1}{h} \int_{t - h}^{t} f \to f (t)$ as $h ↓ 0$ for $t \in (a, b]$ . The same one-sided limits hold for vector-valued curves that are merely continuous at $t$ provided they are Bochner integrable on some neighbourhood of $t$ .

Facts & Assumptions

Given: Countable Choice; A real or complex Banach space $X$ , real numbers $a < b$ , and a continuous $f : [a, b] \to X$ .

[F1]

$f$ is Bochner integrable when there are integrable $X$ -valued simple functions $s_{n}$ with $\int_{a}^{b} ∥ f - s_{n} ∥ d s \to 0$ , and then $\int_{a}^{b} f d s = \lim_{n} \int_{a}^{b} s_{n} d s$ ; integrals over subintervals are defined through the indicators $1_{[t, t + h]}$ , and constant functions have the expected integrals (Bochner-integrable function, Linearity of the Bochner integral).

[F2]

The Bochner integral is linear: for Bochner integrable $u, v$ and scalars $α, β$ the function $α u + β v$ is Bochner integrable with $\int (α u + β v) = α \int u + β \int v$ (Linearity of the Bochner integral).

[F3]

Norm inequality: $∥ \int_{E} u d s ∥ \leq \int_{E} ∥ u ∥ d s$ for every Bochner integrable $u$ and measurable $E$ (Bochner integral norm inequality).

[F4]

Continuity of $f$ at a point $t$ means: for every $η > 0$ there is $δ > 0$ with $∣ s - t ∣ < δ$ , $s \in [a, b]$ , implying $∥ f (s) - f (t) ∥ < η$ (Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form).

[F5]

The interval $[a, b]$ is a compact metric space (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line), and a continuous map from a compact metric space to a metric space is uniformly continuous (Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous): for every $η > 0$ there is $δ > 0$ such that $∥ f (s) - f (u) ∥ < η$ whenever $s, u \in [a, b]$ and $∣ s - u ∣ < δ$ .

Proof

technique · direct, using explicit uniform step approximation, then linearity and the integral norm inequality

1.1F5

By [F5], $f$ is uniformly continuous on $[a, b]$ . Its oscillation over pairs at distance at most $ℓ$ therefore tends to zero as $ℓ ↓ 0$ .

2.1F1step 1.1

For each $n \in N$ , set $ℓ_{n} = (b - a) / (n + 1)$ , $x_{k} = a + k ℓ_{n}$ for $0 \leq k \leq n + 1$ , and $s_{n} = \sum_{k < n + 1} f (x_{k}) 1_{[x_{k}, x_{k + 1})}$ , with the last interval including $b$ . These are integrable simple functions and converge uniformly, hence pointwise, to $f$ .

3.1F1step 1.1step 2.1

The norm error is at most the oscillation from step 1.1, so $\int_{a}^{b} ∥ f - s_{n} ∥ \leq (b - a) \sup_{∣ s - u ∣ \leq ℓ_{n}} ∥ f (s) - f (u) ∥ \to 0$ . Together with the pointwise simple approximation, [F1] proves Bochner integrability of $f$ .

4.1F1F2step 3.1

For $t \in [a, b)$ and $0 < h \leq b - t$ , linearity gives $h^{- 1} \int_{t}^{t + h} f - f (t) = h^{- 1} \int_{t}^{t + h} (f (s) - f (t)) d s$ , since the constant function has integral $h f (t)$ .

5.1F3step 4.1

By the norm inequality, the norm of this difference is at most $h^{- 1} \int_{t}^{t + h} ∥ f (s) - f (t) ∥ d s \leq \sup_{s \in [t, t + h]} ∥ f (s) - f (t) ∥$ .

6.1F4step 5.1

Continuity at $t$ makes the last supremum tend to zero as $h ↓ 0$ : given $η > 0$ , take $h$ below a continuity radius for $f$ at $t$ . Hence the forward averages converge to $f (t)$ .

7.1F2F3F4step 3.1step 6.1

For $t \in (a, b]$ and $0 < h \leq t - a$ , the same linearity and norm estimates give $∥ h^{- 1} \int_{t - h}^{t} f - f (t) ∥ \leq \sup_{s \in [t - h, t]} ∥ f (s) - f (t) ∥ \to 0$ . This proves the backward form directly.

8.1F2F3F4step 6.1step 7.1∎

If instead $f$ is only continuous at $t$ and Bochner integrable on a neighbourhood of $t$ , the forward and backward estimates above still apply: local integrability supplies the integrals and continuity at $t$ makes their norm errors vanish. Thus the stated general one-sided limits also hold.

Depends on

Used by

Dependency tree · two levels

49 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

Gerald Teschl, Partial Differential Equations: From Classical to Modern (2026 author manuscript; complete 392-page archived text) (standard reference, not scraped)
Mathew A. Johnson, Math 951 Lecture Notes, Chapter 6: Introduction to Semigroup Methods, University of Kansas (complete 37-page chapter) (standard reference, not scraped)