Banach-Mazur applied to a Hilbert space The Banach-Mazur theorem says that every separable Banach space is isometric to a subspace of $C^0([0;1],R)$, the space of continuous real valued functions on the interval $[0;1]$, with the sup norm.
If we apply this to $\ell^2(R)$, then we see that $C^0([0;1],R)$ has a subspace which is a Hilbert space for the sup norm. 
My question is can one write down explicitly such a subspace of $C^0([0;1],R)$?
I'm just curious, that's all.
 A: 
By "explicit", I was really asking for a sequence of continuous functions...

Ah, OK. Take a Peano curve $(f,g)$ from $[-1,1]$ to $[-1,1]^2$. Now define inductively $F_1=f$, $F_{k+1}=F_k\circ g$. Note that for any finite sequence of points $y_j\in[-1,1]$ ($j=1,\dots, n$), we can find $x\in[-1,1]$ such that $F_j(x)=y_j$ (induction: the last $n-1$ functions determine $g(x)$ after which $f(x)$ is free to choose). Now just define $H_1=F_1$, $H_{k+1}=F_{k+1}\sqrt{1-H_1^2-\dots-H_k^2}$. This is your sequence. 
It just remains to construct the Peano curve "explicitly". It is not going to be nice, so an elementary formula is out of question. However, you can take the Fourier series $\sum_{k} v_k\cos(2\pi A_k x)$, where $v_k$ is a sequence of vectors in $\mathbb R^2$ and $A_k$ is a sequence of integers, with properly chosen (explicit) $v_k$ and $A_k$ to get the image to contain the unit square. Now just truncate the values to $[-1,1]$ in the usual way. 
A: Let $\varphi$ be a continuous function from $[0,1]$ onto the closed unit ball $B$ of $\ell^2$ in the weak topology.  Then we define $J: \ell^2 \to C[0,1]$ by $(Jx)(t) = <\phi(t), x>$.  Now, how to construct $\varphi$?  
Consider convex compact subsets of $B$ of the form $K(a_1,\ldots,a_n) = \{x \in B: a_i/2^n \le x_i \le (a_i+1)/2^n \text{ for } i = 1 \ldots n\}$ for integers $a_i$, $-2^n \le a_i \le 2^n$.  Of course many of these are empty, and we disregard those.  We can consider the nonempty ones as forming a 
tree structure $T$ with vertices $v = (a_1, \ldots, a_n)$, and edges joining $(a_1, \ldots, a_n)$ to its children $(b_1, \ldots, b_{n+1})$ where for $1 \le i \le n$, $b_i$ is either $2 a_i$ or $2 a_i + 1$.  Thus $K(v) = \bigcup_w K(w)$ where $w$ runs over the children of $v$.  The root $r$ of the tree corresponds to $B$ itself (with $n=0$).
Recursively define closed subintervals $J(v)$ of $J(r) = [0,1]$ for $v \in T$ so that


*

*If $w$ is a child of $v$, $J(w) \subset \text{interior}(J(v))$ 

*If $w_1$ and $w_2$ are disjoint children of $v$, $J(w_1)$ and $J(w_2)$ are disjoint.

*If $v$ is at level $n$ in the tree, $J(v)$ has length at most $2^{-n}$.


Let $E_n$ be the union of $J(v)$ for all vertices $v$ at level $n$.
Define $\varphi_n: [0,1] \to B$ by selecting $x_v \in K(v)$ for each vertex $v$ at level $n$, and defining $\varphi_n(t) = \varphi_{n-1}(t)$ for $t \notin \text{interior}(E_n)$,
$\varphi_n(t) = x_v$ for $t \in J(v)$ where $v$ is a vertex at level $n$,
and interpolating linearly on the rest.  Note that if $m > n$ and $t \in J(v)$ where $v$ is a vertex at level $n$, $\varphi_m(t) \in K(v)$.  
Finally, define $\varphi(t) = \lim_{n \to \infty} \varphi_n(t)$. This, I claim, is 
a continuous surjective function from $[0,1]$ to $B$ with the weak topology.
A: If you want a reasonably explicit embedding of $\ell_2^n$ into $C[0,1]$ with distortion independent of $n$ (but not isometric) you can do the following.  Take the first $2^n$ terms of your favorite lacunary sequence of characters and form the Rademacher functions over them, divided by $2^n$--call them $x_1,\dots,x_n$. A  lacunary sequence of characters is equivalent to the unit vector basis of $\ell_!$ and hence $x_1,\dots,x_n$ is, by Khintchine's inequality, well equivalent to an orthonormal basis for $\ell_2^n$.
The better thing to do is to embed isometrically $\ell_2$ into $C(X)$, where $X$ is the unit ball of $\ell_2$ in its weak topology, in the way suggested by Robert Israel.  By Milutin's theorem, $C(X)$ is isomorphic (but, of course, not isometric) to $C[0,1]$.
A: This proof of Banach-Mazur seems quite constructive (well, as constructive as you can get in this business) -- this is from Banach Space Theory: the basis for linear and Nonlinear analysis.
