Proof of Functions and Function-Valued Operators Given by Integrals over Subintervals

Under the axiom of dependent choice, $([a,b],\mathcal{B}_{[a,b]},\lambda_{[a,b]})$ is a measure space (Measurable Functions and the Lebesgue Integral: Standing Notation (vii)).

Integrals over $[a,t]$ as integrals over $[a,b]$. Let $t\in[a,b]$ and $f\in\mathcal{L}^{1}([a,b])$. As $[a,t]\in\mathcal{B}_{[a,b]}$ (Integrals over Subintervals of a Closed Interval: Notation (iii)), Integrals over Measurable Subsets (vi), applied to $\mu=\lambda_{[a,b]}$ and $A=[a,t]$, shows that $f$ is integrable on $[a,t]$. Since $\lambda_{[a,t]}$ is the restriction of $\lambda_{[a,b]}$ to $[a,t]$ (Integrals over Subintervals of a Closed Interval: Notation (iii)), this means $f|_{[a,t]}\in\mathcal{L}^{1}(\lambda_{[a,t]})$ (Integrals of Functions over a Measurable Subset (iii)), and the integral of $f$ over $[a,t]$ with respect to $\lambda_{[a,b]}$ is $\int f|_{[a,t]}\,d\lambda_{[a,t]}=\int_{[a,t]}f\,d\lambda$ (Integrals of Functions over a Measurable Subset (iv)). By Integrals over Measurable Subsets (ii), the function $f\mathbf{1}_{[a,t]}$, which equals $f$ on $[a,t]$ and $0$ on $[a,b]\setminus[a,t]$ (Indicator Function of a Subset (i)), lies in $\mathcal{L}^{1}([a,b])$, and

$$\int_{[a,t]}f\,d\lambda=\int f\mathbf{1}_{[a,t]}\,d\lambda_{[a,b]}.\tag{1}$$

Thus $f|_{[a,t]}\in\mathcal{L}^{1}(\lambda_{[a,t]})$ and $f\mathbf{1}_{[a,t]}\in\mathcal{L}^{1}([a,b])$, so both sides of (1) are defined. Let $g\in\mathcal{L}^{1}([a,b];\mathbb{R}^{n})$, and let $g^{t}:[a,b]\to\mathbb{R}^{n}$ be the function with $g^{t}(r)=g(r)$ for $r\le t$ and $g^{t}(r)=0$ for $r>t$ (Maps Defined by Cases (i)). As the origin of $\mathbb{R}^{n}$ has all components $0$ (Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (v)), the components of $g^{t}$ are $(g^{t})_{k}=g_{k}\mathbf{1}_{[a,t]}$ for $k\in[n]$. Since $g_{k}\in\mathcal{L}^{1}([a,b])$ (Integrable Vector- and Matrix-Valued Functions and Their Integrals (i)), the scalar case gives $g_{k}|_{[a,t]}\in\mathcal{L}^{1}(\lambda_{[a,t]})$ and $g_{k}\mathbf{1}_{[a,t]}\in\mathcal{L}^{1}([a,b])$. The restriction $g|_{[a,t]}$ is measurable (Measurable Maps: Generators, Composition, Continuous Maps, Restrictions, and Criteria for Real- and [0,∞]-Valued Maps (viii)) and has the components $g_{k}|_{[a,t]}$, and every component of $g^{t}$ is measurable, so $g^{t}$ is measurable (Vector- and Matrix-Valued Measurable Maps: Components, Entries and Continuous Images (i)); hence $g|_{[a,t]}\in\mathcal{L}^{1}(\lambda_{[a,t]};\mathbb{R}^{n})$ and $g^{t}\in\mathcal{L}^{1}([a,b];\mathbb{R}^{n})$ (Integrable Vector- and Matrix-Valued Functions and Their Integrals (i)). By Integrable Vector- and Matrix-Valued Functions and Their Integrals (ii), taken in both measure spaces, and (1), the $k$-th component of $\int g^{t}\,d\lambda_{[a,b]}$ is

$$\int g_{k}\mathbf{1}_{[a,t]}\,d\lambda_{[a,b]}=\int g_{k}|_{[a,t]}\,d\lambda_{[a,t]},$$

the $k$-th component of $\int g|_{[a,t]}\,d\lambda_{[a,t]}=\int_{[a,t]}g\,d\lambda$; hence (Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iii))

$$\int_{[a,t]}g\,d\lambda=\int g^{t}\,d\lambda_{[a,b]}.\tag{2}$$

Thus $g|_{[a,t]}\in\mathcal{L}^{1}(\lambda_{[a,t]};\mathbb{R}^{n})$ and $g^{t}\in\mathcal{L}^{1}([a,b];\mathbb{R}^{n})$, so both sides of (2) are defined.

A predicative description. Let $I:\mathcal{L}^{1}([a,b])\to\mathbb{R}$ and $J:\mathcal{L}^{1}([a,b];\mathbb{R}^{n})\to\mathbb{R}^{n}$ be the integrals with respect to $\lambda_{[a,b]}$ (Integrable Functions and Their Lebesgue Integral (iii) and Integrable Vector- and Matrix-Valued Functions and Their Integrals (ii)). With $[a,b]$, the order of $\mathbb{R}$, the origin $0$ of $\mathbb{R}^{n}$, $\mathcal{L}^{1}([a,b];\mathbb{R}^{n})$ and $J$ as parameters, let $\theta(y,g,t)$ be the formula

$$\exists h\,\Bigl(h\in\mathcal{L}^{1}([a,b];\mathbb{R}^{n})\wedge\forall r\,\bigl(r\in[a,b]\Rightarrow\bigl((r\le t\Rightarrow(r,g(r))\in h)\wedge(t<r\Rightarrow(r,0)\in h)\bigr)\bigr)\wedge(h,y)\in J\Bigr),$$

predicative under the guard "$g\in\mathcal{L}^{1}([a,b];\mathbb{R}^{n})$ and $t\in[a,b]$". Under this guard, the only $h$ satisfying the first two conjuncts is $g^{t}$, which lies in $\mathcal{L}^{1}([a,b];\mathbb{R}^{n})$; so, by (2), $\theta(y,g,t)$ holds exactly for $y=J(g^{t})=\int_{[a,t]}g\,d\lambda$. The same formula with $\mathcal{L}^{1}([a,b])$, $I$ and $0\in\mathbb{R}$ in place of $\mathcal{L}^{1}([a,b];\mathbb{R}^{n})$, $J$ and the origin holds, for $f\in\mathcal{L}^{1}([a,b])$ and $t\in[a,b]$, exactly for $y=I(f\mathbf{1}_{[a,t]})=\int_{[a,t]}f\,d\lambda$, by (1). By Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (ii), $\int_{[a,t]}f\,d\lambda$ and $\int_{[a,t]}g\,d\lambda$ may therefore be written in expressions as defined set symbols in $f,t$ and in $g,t$, used properly for $f\in\mathcal{L}^{1}([a,b])$, $g\in\mathcal{L}^{1}([a,b];\mathbb{R}^{n})$ and $t\in[a,b]$, with values in $\mathbb{R}$ and in $\mathbb{R}^{n}$.

Proof of (i) and (ii). The expressions $\int_{[a,t]}f\,d\lambda\in\mathbb{R}$ and $\int_{[a,t]}g\,d\lambda\in\mathbb{R}^{n}$ in $t\in[a,b]$ give exactly one such function $X$ each, by Maps and Relations Given by Formulas (i).

Proof of (iii). By Maps and Relations Given by Formulas (ii) there is a function $\Phi:\mathcal{L}^{1}([a,b];\mathbb{R}^{n})\times[a,b]\to\mathbb{R}^{n}$ with $\Phi(g,t)=\int_{[a,t]}g\,d\lambda$, and by Projection, Evaluation and Currying Maps (iii) there is exactly one function $\mathcal{J}:\mathcal{L}^{1}([a,b];\mathbb{R}^{n})\to(\mathbb{R}^{n})^{[a,b]}$ with $\mathcal{J}(g)(t)=\Phi(g,t)$ for all $g$ and $t$.

Proof of (iv). For $z\in(\mathbb{R}^{n})^{[a,b]}$ and $r\in[a,b]$ we have $(r,z(r))\in[a,b]\times\mathbb{R}^{n}$, so $F(r,z(r))\in\mathbb{R}^{n}$, and Maps and Relations Given by Formulas (ii) gives a function $G:(\mathbb{R}^{n})^{[a,b]}\times[a,b]\to\mathbb{R}^{n}$ with $G(z,r)=F(r,z(r))$. By Maps Formed Pointwise: Constant Maps, Pairs of Values, Maps Applied to Values, and Families of Maps (iv) there is exactly one function $\Theta:(\mathbb{R}^{n})^{[a,b]}\to(\mathbb{R}^{n})^{[a,b]}$ with $\Theta(z)(r)=G(z,r)$ for all $z$ and $r$.

Proof of (v). By Maps Formed Pointwise: Constant Maps, Pairs of Values, Maps Applied to Values, and Families of Maps (iv) there is a function $H:[a,b]\to(\mathbb{R}^{n})^{[a,b]}$ with $H(t)=h(t,\cdot)$ for every $t\in[a,b]$, and $\int_{[a,t]}h(t,s)\,ds=\int_{[a,t]}H(t)\,d\lambda$ by Integrals over Subintervals of a Closed Interval: Notation (iii). As $H(t)\in\mathcal{L}^{1}([a,b];\mathbb{R}^{n})$ for every $t\in[a,b]$ by hypothesis, the expression $\int_{[a,t]}H(t)\,d\lambda\in\mathbb{R}^{n}$ in $t\in[a,b]$ gives exactly one such function $Y$, by Maps and Relations Given by Formulas (i).