The arctan-compression route (Cohn, Measure Theory, 2nd ed., Thm. 7.4.4; Rudin, Real and Complex Analysis, Thm. 2.24), which avoids any integrability hypothesis on \(u\). Replace \(u\) by the bounded measurable \(v=\arctan \circ u\), valued in \((-\pi /2,\pi /2)\) hence in \(L^1(\mu )\) since \(\mu \) is finite. Bounded continuous functions are dense in \(L^1\) (a finite measure on a metrizable Borel space is weakly regular), so pick continuous \(g_n\) with \(\mathrm{eLpNorm}(v-g_n)\, 1\, \mu \to 0\); \(L^1\)-convergence gives convergence in measure, hence an a.e.-convergent subsequence. Egorov’s theorem upgrades this to uniform convergence off a small measurable set, and inner regularity carves a compact \(K\) out of its complement with \(\mu (K^{\mathsf c}){\lt}\varepsilon \). On \(K\) the continuous \(g_n\) converge uniformly to \(v\), so \(v\) is continuous on \(K\); composing with \(\tan \) (continuous on \((-\pi /2,\pi /2)\), and \(\tan \circ \arctan =\mathrm{id}\)) recovers \(\mathrm{ContinuousOn}\, u\, K\).

Write \(s\cap t=\bigcap _{b:\mathrm{Bool}}\mathrm{cond}\, b\, s\, t\) and apply Mathlib’s countable intersection AnalyticSet.iInter over the two-element index \(\mathrm{Bool}\).

Write \(s\cup t=\bigcup _{b:\mathrm{Bool}}\mathrm{cond}\, b\, s\, t\) and apply the countable union AnalyticSet.iUnion over \(\mathrm{Bool}\).

Parametrise \(s=\mathrm{range}\, f\), \(t=\mathrm{range}\, g\) by continuous maps from Polish spaces (analyticSet_iff_exists_polishSpace_range); then \(s\times t\) is the range of the continuous product map \(f\times g\) from the product Polish space.

Choquet’s capacitability theorem (Kechris, Thm. 30.13; Srivastava, Thm. 4.3.1): for a finite Borel measure the compact capacity \(\mathrm{compactCap}\, \mu \, s=\sup \{ \mu K\mid K\text{ compact}, K\subseteq s\} \) agrees with \(\mu s\) on analytic sets, so an increasing union of compact subsets exhausts \(s\) up to a null set, giving \(s=^{\mu }B\) with \(B\) Borel; the s-finite case dominates \(\mu \) by a finite measure. This route needs no analytic complement (Suslin’s theorem does), which is exactly why it applies to a Borel projection. It underlies the a.e. singular tier (Theorem 18.23); the everywhere upgrade below replaces it by the Novikov projection theorem.

Given separators \(B^{(m)}\) for each refinement, assemble a separator for \(E\): at position \(j\) take \(\bigcup _m B^{(m)}_j\), at every other position \(n\) take \(\bigcap _m B^{(m)}_n\). These are measurable, contain \(E\) (using \(E_j\subseteq \bigcup _m G_m\) at \(j\)), and have empty intersection: a point in the intersection lies in some \(B^{(m_0)}_j\), hence in \(\bigcap _n B^{(m_0)}_n=\emptyset \), a contradiction.

Extend the entries one coordinate at a time along the mixed-length intermediate family \(\mathrm{famMix}\), by an inner induction over the position \(j\le k+1\): decompose the \(j\)-th cylinder into the one-longer cylinders \(\bigcup _m\mathrm{cylinder}(\mathrm{update}\, \sigma '_j\, (k-j)\, m)\), and invoke the single-entry split (Lemma 18.7) to pick a coordinate value \(m_0\) preserving non-separatedness. At \(j=k+1\) the mixed family is exactly \(\mathrm{famE}\, f\, \sigma '\, (k+1)\).

Suppose not. Iterating one stage of the recursion (Lemma 18.8) from the trivial centres builds, by dependent choice, centres refining coordinate by coordinate; a stationarity argument (coordinate \(i\) of entry \(n\) freezes from stage \(n+i+1\) on) produces diagonal limit points \(\alpha _n\in \mathbb {N}\to \mathbb {N}\) such that every truncated family \(\bigl(f_n[\mathrm{cylinder}(\alpha _n,k-n)]\bigr)\) is non-separated, hence in particular nonempty. If all \(f_n(\alpha _n)\) coincided, that common value would lie in \(\bigcap _n\mathrm{range}\, f_n=\emptyset \); so two differ, and Hausdorff-separate them by open \(u\ni f_i(\alpha _i)\), \(v\ni f_j(\alpha _j)\). At a late enough stage the ultrametric cylinders around \(\alpha _i,\alpha _j\) shrink inside \(f_i^{-1}u\), \(f_j^{-1}v\), so \((u,v,\mathrm{univ},\dots )\) is a Borel separator of that truncated family — contradicting its non-separatedness.

If some \(A_{n_0}=\emptyset \), take \(B_{n_0}=\emptyset \) and \(B_n=\mathrm{univ}\) otherwise. Otherwise every \(A_n\) is a nonempty continuous image of Baire space, \(A_n=\mathrm{range}\, f_n\), and Theorem 18.9 applies verbatim.

Apply Theorem 18.10 to the analytic sets \((\bigcup _m S_m)\cap (S_n)^{\mathsf c}\) (analytic by Lemma 18.2), whose intersection over \(n\) is empty. The resulting Borel separators \(D'_n\) give measurable pieces \((\bigcup _m S_m)\setminus D'_n\subseteq S_n\) with the correct union; disjointifying (disjointed) produces the pairwise-disjoint family.

Replace \(A_1\) by a Borel Lusin separator \(A_1'\) from \(A_0\) (AnalyticSet.measurablySeparable). Let \(C_n=\{ x\mid V_n\text{ misses the section }(A_0)_x\} \); its complement is the analytic projection \(\pi _X(A_0\cap (X\times V_n))\) (Lemma 18.2), and the closed sections give the basis decomposition \(A_0^{\mathsf c}=\bigcup _n C_n\times V_n\). Feed the coanalytic family \(S_n=A_1'\cap (C_n\times V_n)\) — whose complements are analytic by Lemma 18.3 and Lemma 18.4 and whose union is the Borel \(A_1'\) — to the weak reduction principle (Theorem 18.11), then Lusin-separate each analytic projection \(\pi _X(D_n)\) from the analytic \((C_n)^{\mathsf c}\) to get the Borel \(B_n\).

The special case \(A_0=B^{\mathsf c}\), \(A_1=B\) of Saint Raymond’s theorem: closed sections of \(B^{\mathsf c}\) are exactly open sections of \(B\). Saint Raymond covers \(B\) by \(\bigcup _n B_n\times V_n\) while keeping it disjoint from \(B^{\mathsf c}\), forcing the reverse inclusion and hence equality.

Insert \(\emptyset \) into a countable topological basis to make it a nonempty countable set, then enumerate it as a range.

The complement \(B^{\mathsf c}\) has open sections, so Kunugui–Novikov (Theorem 18.13) writes it as \(\bigcup _n B_n\times V_n\) with the \(V_n\) from an enumerated basis (Lemma 18.14). Each Borel \(B_n\) is clopenable: there is a finer Polish topology making it clopen. Amalgamating these countably many refinements into a single Polish topology \(t'\) (PolishSpace.exists_polishSpace_forall_le) makes every \(B_n\) open, hence \(B^{\mathsf c}=\bigcup _n B_n\times V_n\) open and \(B\) closed in \(t'\times t_Y\).

Refine \(X\)’s topology to make \(B\) closed (Theorem 18.15; compact sections are in particular closed). The first projection \(X\times Y\to X\) is a proper map when \(Y\) is compact, hence closed, so \(\pi _X(B)\) is closed in the refined topology \(t'\), thus Borel for \(t'\). Since \(t'\le t_X\) with both Polish, the two Borel \(\sigma \)-algebras coincide (borel_eq_borel_of_le, Lusin–Souslin), so \(\pi _X(B)\) is Borel for the original topology.

For \(Y\) nonempty, fix a dense sequence \((u_n)\) in a compatible complete metric and send \(y\mapsto \bigl(\min (\mathrm{dist}(y,u_n),1)\bigr)_n\). This is continuous, and injective: if two points have equal coordinates then approximating each by the dense sequence forces their distance to \(0\). The empty case is vacuous.

Compactify the fibre: push \(B\) into \(X\times (\mathbb {N}\to [0,1])\) along \(\mathrm{id}\times e\) for a continuous injection \(e\) (Lemma 18.17), which is a measurable embedding by Lusin–Souslin, so the image is Borel with the same first projection. The pushed sections are \(e[\, \text{compact section}\, ]\), still compact hence closed in the compact cube, so the compact-fibre-space case (Theorem 18.16) gives the Borel projection.

By measurable_of_Iic it suffices that each sublevel \(\{ x\mid \mathrm{infDist}\, c\, (V x)\le r\} \) is Borel. This set is the first projection of the graph sliced with the closed ball, \(\{ (x,v)\mid v\in V x\} \cap (X\times \overline B(c,r))\): a point \(x\) is in the sublevel iff the closed subspace \(V x\) — which attains its distance to \(c\) — meets \(\overline B(c,r)\). Each section \(V x\cap \overline B(c,r)\) is a closed subspace intersected with a compact ball in the proper Euclidean space, hence compact, so the Novikov projection theorem (Theorem 18.18) makes the projection Borel.

Reduce to entrywise measurability (Matrix carries the Pi structure). Each entry is a projected-basis coordinate (orthProjMatrix_apply), which the polarisation identity starProjection_apply_coord writes as a fixed real combination of the three scalar distance maps \(x\mapsto \mathrm{infDist}\, c\, (V x)\) for \(c\) among the two basis vectors and their difference. Each is Measurable by Theorem 18.19, and Measurable arithmetic with measurable_pi_lambda assembles the full projector.

The same polarisation reduction, but the distance sublevels are obtained only up to a null set, from the universal measurability of the analytic projection (Theorem 18.5) rather than its honest Borel-ness. This is the route of Chapter 4; the everywhere converter (Theorem 18.20) replaces Theorem 18.5 by the Novikov projection theorem.

The sublevel filtration has a measurable graph built from the measurable data \(A,T\) and the everywhere gate, and the general converter (Theorem 18.20) turns that graph into the everywhere-measurable projector via the Novikov compact-section projection theorem.

Here the ultrametric-growth gate holds only a.e. (isUltrametricGrowth_lambdaBar, itself needing invertibility, ergodicity, and integrable log-norms), so the a.e. converter (Theorem 18.21) applies. The everywhere headline (Theorem 18.22) is strictly stronger: it drops every dynamical hypothesis in exchange for the pointwise gate.

Prokhorov’s theorem makes \(P(X)\) compact and the Lévy–Prokhorov metric makes it metrizable and second countable. A compact metrizable space is completely metrizable (isCompletelyMetrizableSpace_of_compactSpace: a compatible metric on a compact — hence complete — uniform space is complete), which upgrades the package to Polishness. A companion polishSpace_prod assembles the finite products.

The Billingsley mapping-theorem argument. Test against a bounded continuous \(g : Y \to \mathbb {R}\) via \(\int g\, \mathrm d(f_*\nu ) = \int (g\circ f)\, \mathrm d\nu \) and split the difference into a weak-convergence term (\(\nu _i \to \nu \) tested against \(g\circ \sigma \)) and a uniform term bounded by \(\| g\circ \sigma _i - g\circ \sigma \| _\infty \), which vanishes because postcomposition \(\tau \mapsto g\circ \tau : C(X,Y) \to (X \to ^b \mathbb {R})\) is continuous. The filter form is tendsto_probabilityMeasure_map_of_tendsto. Mathlib previously had only the fixed-map continuity ProbabilityMeasure.continuous_map.

Each of the five conjuncts is an equalizer of jointly continuous maps into a Hausdorff space: composition is jointly continuous (ContinuousMap.continuous_comp’), and the pushforward is jointly continuous (Theorem 18.25); a finite intersection of closed sets is closed.

A closed subset of a Polish space is analytic and analyticity is preserved by continuous images (here the coordinate projection \(\mathrm{Prod.fst}\)), giving the \(\Sigma ^1_1\) bound; that \(\mathrm{Params}\, X\) and \(C(X,X)\) are Polish is Theorem 18.24 and the uniform metric on \(C(X,X)\). The sealed set is by definition the complement, hence \(\Pi ^1_1\); the identity tuple satisfies \(\mathrm{SectionRel}\) with \(s = \mathrm{id}\).