TITLE: Proof Verification: $\binom{n}{k}$ is always a natural number if $0\leq k\leq n$ - Spivak's Calculus, Problem 2-3(b)
QUESTION [1 upvotes]: This is problem 3(b) from Spivak's Calculus 4th ed., Chapter 2:

Prove that $\binom{n}{k}$ is always a natural number if $0\leq k\leq n$

This is my proof:
If $n=0, \binom{0}{0}= \frac{0!}{0!}=1$
$\therefore \binom{0}{0} \in \Bbb N$, so the statement holds true for $n=0$.
Assuming that the statement holds true for $n=m$ such that $$\binom{m}{0},\binom{m}{1},\binom{m}{2},...,\binom{m}{m-1},\binom{m}{m} \in \Bbb N$$
Then for $n=m+1$, it follows that $\binom{m+1}{k}\in\Bbb N$ since $\binom{m+1}{k}=\binom{m}{k-1}+\binom{m}{k}$ and $\binom{m}{k-1}$ or $\binom{m}{k}\in \Bbb N$ by assumption.
$\therefore$ It has been proven that if the statement holds true for $n=m$ then it must hold true for $n=m+1 \Rightarrow$ By the principle of mathematical induction, the statement must hold true for all $0\leq k\leq n$ and $k,n\in \Bbb Z^{\geq}$. I'm posting this proof as it is different to the one Spivak provides and I'm not sure if it makes sense. Is it correct?

REPLY [2 votes]: In your proof the case of $ k =m +1$ has  to be addressed separately.
Otherwise it is a good proof.


TITLE: How to construct the combined transformation matrix that adjusts this rectangle.
QUESTION [0 upvotes]: Like what is shown above, dashed line constructed rectangle is the original one, and the solid constructed rectangle is the target we want to transform.
So we can see that points of the original one are (-1,0)(1,0)(-1,5)(1,5) and the points of target are (-5,2)(-5,3)(5,2)(5,3). Construct the combined transformation matrix that adjusts this rectangle.
The idea I use is to find the changes of scalling and translating Sx Sy Tx and Ty.
And then plug these number I find into these two and multiply them together.
Then I find
Sx = 5
Sy = 1/5
Tx = -4
Ty = 2 Such that

When I tried (-1,0) to test it, what I want to get is (-5,2) But I got

What is wrong with my process? I am not sure how to translate shape if the negative quadrant occurs?
Also, I tried to translate one corner of the original one to the origin. So that
Sx = 1
Sy = 1
Tx = 1
Ty = 0
And then I got

When I test (-1,0), it works. And then I don't know what should I do.

REPLY [0 votes]: The scaling is with respect to the origin. You need to translate the old rectangle so that its center is the origin, re-scale it, then translate it back.


text:
\begin{document}

\title{High-dimensional $\mathcal Z$-stable AH algebras}
\author{Aaron Tikuisis}
\address{Institute of Mathematics\\
University of Aberdeen\\
Aberdeen, UK AB24 3UE}
\urladdr{http://homepages.abdn.ac.uk/a.tikuisis/}
\email{a.tikuisis@abdn.ac.uk}

\begin{abstract}
It is shown that a $C^*$-algebra of the form $C(X,U)$, where $U$ is a UHF algebra, is not an inductive limit of subhomogeneous $C^*$-algebras of topological dimension less than that of $X$.
This is in sharp contrast to dimension-reduction phenomenon in (i) simple inductive limits of such algebras, where classification implies low-dimensional approximations, and (ii) when dimension is measured using decomposition rank, as the author and Winter proved that $\dr(C(X,U)) \leq 2$.
\end{abstract}

\thanks{The author is supported by an NSERC PDF}

\subjclass[2010]{46L35, 46L05, (46L80, 47L40, 46L85)}

\keywords{Nuclear $\mathrm C^*$-algebras; decomposition rank; nuclear dimension; UHF algebra; $\mathcal Z$-stability; Jiang-Su algebra; approximately homogeneous $C^*$-algebras}

\maketitle

\section{Introduction}

Consider $C^*$-algebras that take the form of a direct sum of algebras of continuous functions from a topological space to a matrix algebra; call this class $\mathcal C$.
Now consider the class A$\mathcal C$ of algebras that are inductive limits of algebras in $\mathcal C$.
Such algebras, including AF, AI, A$\mathbb T$, and (some) AH algebras, have arisen naturally, for instance, as crossed products of the Cantor set or the circle by minimal homeomorphisms.
However, the present purpose of considering this class of $C^*$-algebras is as a test case for phenomena among the broader, less-understood class of finite nuclear $C^*$-algebras.

A mixture of classification and other arguments has shown that there is a dichotomy amongst the simple $C^*$-algebras in A$\mathcal C$, dividing them into algebras of low and high topological dimension.
Classification arguments, on the one hand, show that for a simple algebra in A$\mathcal C$, if it is an inductive limit of building blocks (in $\mathcal C$) with bounded topological dimension (or even ``slow dimension growth''), or if it is $\mathcal Z$-stable, then it is an inductive limit of algebras in $\mathcal C$ with topological dimension at most three \cite{ElliottGongLi:AHclassification,Gong:SimpleReduction,Lin:LocalAH}.
(Note that one can show, without classification, that slow dimension growth implies $\mathcal Z$-stability; see \cite{Toms:rigidity,Toms:stability,Winter:pure}, so $\mathcal Z$-stability should be viewed as the weakest of these hypotheses.)
By a general $\mathcal Z$-stability theorem of Winter \cite{Winter:pure}, it follows that this is also the case for simple algebras in A$\mathcal C$ with finite nuclear dimension (or decomposition rank).
Villadsen first produced examples of simple algebras in A$\mathcal C$ that don't have bounded-dimension building blocks \cite{Villadsen:Perforation}; these examples, and their high-dimensional properties, were further analyzed by Toms and Winter \cite{TomsWinter:V1}.

The aforementioned dimension reductions (going from bounded dimension/slow dimension/$\mathcal Z$-stability to dimension at most three) owes itself to (i) simplicity and (ii) dimension-reducing effects of tensoring with $\mathcal Z$.
Villadsen's high-dimensional algebras show that simplicity alone does not produce dimension reduction.
Moreover, the author and Winter showed that dimension-reduction, in terms of decomposition rank (and therefore also nuclear dimension), does occur even for nonsimple, $\mathcal Z$-stable algebras in A$\mathcal C$: if $A \in \text{A}\mathcal C$ then $\dr(A \otimes \mathcal Z) \leq 2$ \cite{TW:Zdr}.
This result has recently been extended, by the author and others, to algebras $A$ that are inductive limits of subhomogeneous algebras \cite{ENSTW}.

The main result here is that certain non-simple $\mathcal Z$-stable algebras in A$\mathcal C$ (namely, algebras of the form $C(X,U)$ where $U$ is a UHF algebra) cannot be approximated by low-dimensional algebras in $\mathcal C$--or even from the significantly larger class of subhomogeneous $C^*$-algebras.
This result clarifies the role played by simplicity in classification results such as \cite{ElliottGongLi:AHclassification,Gong:SimpleReduction,Lin:LocalAH}.
It also provides the first example of a $\mathcal Z$-stable approximately subhomogeneous algebra $A$ which cannot be approximated by subhomogeneous algebras with bounded decomposition rank; it is expected (and largely entailed by classification conjectures) that this phenomenon cannot occur in the simple case.

In \cite{BBSTWW}, the author and others showed that many simple $\mathcal Z$-stable $C^*$-algebras have decomposition rank $1$, including a number of approximately subhomogeneous algebras that cannot be approximated by subhomogeneous algebras with decomposition rank less than $2$.
This and the present article give complementary accounts of the same phenomenon: that decomposition rank does not produce the same $K$-theoretic restrictions as subhomogeneous dimension.

In \cite{KirchbergRordam:pi3}, Kirchberg and R\o rdam devised a way to show that for any commutative $C^*$-algebra $C$, $C \otimes 1_{\mathcal O_2}$ can be approximated within $C \otimes \mathcal O_2$ by commutative $C^*$-algebras with one-dimensional spectrum.
They use this result to show that a large swathe of strongly purely infinite, non-simple algebras are approximated by algebras in $\mathcal C$ with one-dimensional spectrum; the result also plays a crucial role in the dimension-reduction result of \cite{TW:Zdr}.
Kirchberg and R\o rdam's result rests mainly on the fact that $\mathcal O_2$ has trivial $K$-theory, which is closely tied to the existence of an $\mathcal O_2$-relativized retract $D^2 \to S^1$; that is, a solution to
\[
\xymatrix{
C(S^{1}) \ar@{-->}[r]^-{\exists} \ar[rd]_-{\id \otimes 1_{A}} & C(D^2,\mathcal O_2) \ar[d]^{f \mapsto f|_{S^{1}}} \\
& C(S^{1},\mathcal O_2),
}\]
It is not difficult to adapt their argument (as we do in Section \ref{sec:4}) to show that if $A$ is a $C^*$-algebra for which we can solve
\begin{equation}
\label{eq:RelRetract}
\xymatrix{
C(S^{n-1}) \ar@{-->}[r]^-{\exists} \ar[rd]_-{\id \otimes 1_{A}} & C(D^n,A) \ar[d]^{f \mapsto f|_{S^{n-1}}} \\
& C(S^{n-1},A),
} \end{equation}
then for any $n$-dimensional space $X$, $C(X) \otimes 1_A$ can be approximated in $C(X,A)$ by commutative $C^*$-algebras with $(n-1)$-dimensional spectrum.
Our main result arises by showing that the converse is true: if $C(X) \otimes 1_A$ can be approximated in $C(X,A)$ by $(n-1)$-dimensional commutative (or even subhomogeneous) algebras then there is an $A$-relativized retract of $D^n$ onto $S^{n-1}$, as in \eqref{eq:RelRetract}.

Let us introduce our notation precisely before clearly stating the main result.
For a $C^*$-algebra $A$, a $C^*$-subalgebra $B$, and a class $\mathcal S$ of $C^*$-algebras, we say that $B$ is \textbf{locally approximated} in $A$ by $C^*$-algebras in $\mathcal S$ if the following holds: for every finite subset $\mathcal F$ of $B$ and every $\e > 0$, there exists a $C^*$-subalgebra $C$ of $A$ such that $C \in \mathcal S$ and $\mathcal F \subset_\e C$.
Note that if $A$ is an inductive limit of algebras in $\mathcal S$ (or an inductive limit of inductive limits of algebras in $\mathcal S$, etc.) then it is locally approximated by algebras in $\mathcal S$.

The \textbf{topological dimension} of a commutative $C^*$-algebra $C(X)$ means, naturally, the dimension of $X$.
More generally, if $A$ is subhomogeneous, then the value of its decomposition rank and nuclear dimension coincide, and also agrees with a value obtained from the primitive ideal space \cite{Winter:drSH} (see also \cite[Corollary 3.18]{ENSTW} for an alternate proof); we continue to use the term topological dimension to refer to this value.

In the sequel, we identify $C(X)$ with the subalgebra $C(X, \mathbb C1_A)$ of $C(X,A)$.

\begin{thm}
\label{thm:MainThm}
Let $A$ be a unital $C^*$-algebra and let $n\in\N$.
The following are equivalent.
\begin{enumerate}[(i)]
\item
\label{MainThm1}
For every $n$-dimensional compact Hausdorff space $X$, $C(X)$ is approximated in $C(X,A)$ by commutative $C^*$-algebras of topological dimension at most $n-1$;
\item
\label{MainThm2}
For every $n$-dimensional compact Hausdorff space $X$, $C(X)$ is approximated in $C(X,A)$ by subhomogeneous $C^*$-algebras of topological dimension at most $n-1$;
\item
\label{MainThm3}
There exists a $*$-homomorphism $\phi:C(S^{n-1}) \to C(D^n,A)$ such that the diagram
\[
\xymatrix{
C(S^{n-1}) \ar[r]^\phi \ar[dr]_{\iota} & C(D^n,A) \ar[d]_{r} \\
& C(S^{n-1},A),
}
\]
commutes, where $\iota$ denotes the inclusion map and $r:C(D^n,A) \to C(S^{n-1},A)$ denotes the restriction map.
\end{enumerate}
If $A \cong A \otimes A$ (using any tensor norm), then these are also equivalent to statement (i) with the words ``$n$-dimensional'' removed; that is, that for any Hausdorff space $X$, $C(X)$ is approximated in $C(X,A)$ by commutative $C^*$-algebras of topological dimension at most $n-1$.
\end{thm}

Well-known topological arguments can be used to reformulate (\ref{MainThm3}) as: the inclusion map $C_0(\R^{n-1}) \to C_0(\R^{n-1},A)$ is nullhomotopic.
By an easy $K$-theoretic obstruction to (\ref{MainThm3}), we obtain:

\begin{cor}
\label{cor:MainCor}
Neither $C(D^n,U)$ (where $U$ is UHF) nor $C(D^n,\mathcal Z)$ are locally approximated by subhomogeneous algebras of topological dimension less than $n$.
\end{cor}

The remainder of the article is devoted to proving Theorem \ref{thm:MainThm}.
In Section \ref{sec:2}, we derive from (\ref{MainThm2}) a covering-dimension-related condition, that $C(X,A)$ contains arbitrarily fine, \textit{commuting} $n$-colourable partitions of unity, in the sense of \cite[Proposition 3.2 (iv)]{TW:Zdr} (this in particular implies (\ref{MainThm1})).
A significant part of this argument is handling the subhomogeneous case, which is aided by \cite[Theorem 2.15]{ENSTW}, which allows us to work with quotients of noncommutative cell complexes in place of arbitrary subhomogeneous approximants.
In Section \ref{sec:3}, we use the commuting partitions of unity from Section \ref{sec:2} to obtain the $A$-relativized retract of $D^n$ onto $S^{n-1}$ (i.e.\ condition (\ref{MainThm3}); the main part of this argument is showing that (\ref{MainThm3}) holds approximately.
Finally, Section \ref{sec:4} shows that (\ref{MainThm3}) implies (\ref{MainThm1}), which is essentially a reproduction of Kirchberg and R\o rdam's argument in the proof of \cite[Proposition 3.5]{KirchbergRordam:pi3}.

For elements $a$ and $b$ of a $C^*$-algebra $A$, and a real number $\e > 0$, we will use the notation $a \approx_\e b$ to mean $\|a-b\|<\e$.
If $A$ is a $C^*$-algebra and $a \in A$, then $\mathrm{sp}(a)$ denotes the spectrum of $a$.
For a compact topological space $X$, $CX$ denotes the cone
\begin{equation}
\label{eq:Cone} CX:= X \times [0,1]/(X \times \{1\}).
\end{equation}

\subsection{Acknowledgements}
The author would like to thank Luis Santiago for discussions that prompted this research, and Ilijas Farah for helpful feedback on an earlier preprint.

\section{Simplicial complexes}
\label{sec:SimpComplex}

In this section we review some basic notions and results about simplicial complexes for use in the sequel.
For a more thorough treatment, see \cite[VIII.5]{Dugundji}.
Let $V$ be a finite set.
Recall that an (abstract, finite) simplicial complex on the vertex set $V$ is a subset $N$ of the power set of $V$, containing all singletons, and closed under taking subsets.
If $N$ is a simplicial complex, each set in $N$ is called a face or a simplex of $N$.
If $N$ is a simplicial complex with vertex set $V$, we use $|N|$ to denote its geometric realization.
Concretely, this can be realized as the subset of $[0,1]^V$ consisting of all $(\lambda_v)_{v\in V}$ such that:
\begin{enumerate}
\item $\sum_v \lambda_v = 1$; and
\item For any $v_1,\dots,v_k \in V$, if $\{v_1,\dots,v_k\} \not\in N$ then
\[ \lambda_{v_1} \cdots \lambda_{v_k} = 0. \]
\end{enumerate}
For a vertex $v_0 \in V$, $\mathrm{Star}(v_0)$ denotes the star around $v_0$, that is, the open subset of $|N|$ made up of the union of the interiors of the realization of faces containing $v_0$.
With the above description of the geometric realization, $\mathrm{Star}(v)$ is precisely all $(\lambda_v)_{v\in V} \in |N|$ such that $\lambda_{v_0} \neq 0$.

We say that $N$ has dimension at most $n$ if every face of $N$ contains at most $n+1$ vertices.
This is the same as saying that the covering dimension of $|N|$ is at most $n$.

Let $N,N'$ be simplicial complexes with vertex sets $V,V'$ respectively.
A morphism from $N$ to $N'$ is a map $\alpha:V \to V'$ which takes each set in $N$ to a set in $N'$.
A morphism from $N$ to $N'$ induces a continuous map $\hat\alpha:|N|$ to $|N'|$ which takes the realization of a simplex $\sigma \in N$ to the realization of $\alpha(\sigma)$, namely
\[ \hat\alpha((\lambda_v)_{v\in V}) = (\mu_{v'})_{v' \in V'} \]
where $\mu_{v'} = \sum_{v \in \alpha^{-1}(v)} \lambda_v$.
In particular, $\hat\alpha(\mathrm{Star}(v))=\mathrm{Star}(\alpha(v))$ for every $v\in V$.

The following result follows almost immediately from the above description of the geometric realization of a simplicial complex.

\begin{prop}
\label{prop:SimpComplexCstar}
Let $N$ be a simplicial complex with vertex set $V$.
Then $C(|N|)$ can be canonically identified with the universal $C^*$-algebra with generator set $\{e_v \mid v \in V\}$ and the following relations:
\begin{enumerate}
\item Each $e_v$ is a positive contraction;
\item The $e_v$s commute;
\item For each $v_1,\dots,v_k \in V$, if $\{v_1,\dots,v_k\} \not\in N$ then
\[ e_{v_1}\dots e_{v_k} = 0; \quad \text{and} \]
\item $\sum_{v \in V} e_v = 1$.
\end{enumerate}
With this identification, for each vertex $v\in V$, we have
\[ \mathrm{Star}(v) = e_v{-1}((0,1]). \]
\end{prop}

Given a commuting finite partition of unity $(f_i)_{i \in I}$ in a $C^*$-algebra $A$ (that is, a finite set of commuting positive elements that sum to $1_A$), we define the \textbf{nerve} of $(f_i)_{i\in I}$ to be the following simplicial complex $N((f_i)_{i\in i})$ with vertex set $I$:
\[ N((f_i)_{i\in I}) := \Big\{\,\{i_1,\dots,i_k\} \subseteq I \mid f_{i_1}\dots f_{i_k} \neq 0\Big\}. \]
By Proposition \ref{prop:SimpComplexCstar}, we obtain a canonical map $C(|N((f_i)_{i\in I})|) \to C^*(\{f_i \mid i \in I\})$, sending $e_i$ to $f_i$.

\section{Subhomogeneous approximations and covering dimension}
\label{sec:2}

In this section, we prove that conditions (\ref{MainThm1}) and (\ref{MainThm2}) of Theorem \ref{thm:MainThm} are equivalent, and are equivalent to another, somewhat technical, covering-dimension-related condition.

We begin with a technical lemma, that will allow us to turn approximations in noncommutative cell complexes (defined in \cite{ENSTW}) into commutative approximations.

\begin{lemma}
\label{lem:CommGluing}
Let $X$ be a compact metric spaces, let $A_0$ be a unital $C^*$-algebra, and let $\phi:A_0 \to C(X,M_k)$ be a $*$-homomorphism for some $k\in\N$.
Define $A$ by the pullback diagram
\[
\begin{array}{rcl}
A & \labelledrightarrow{\rho} & C(CX,M_k) \\
{\scriptstyle \lambda} \downarrow && \downarrow {\scriptstyle f \mapsto f|_{X \times \{0\}}} \\
A_0 & \labelledrightarrow{\phi} & C(X,M_k).
\end{array}
\]
Let $f_1,\dots,f_m \in A_+$ and let $\e > 0$.
Suppose that $B_0$ is a commutative $C^*$-subalgebra of $A_0$, $1_{A_0} \in B_0$, and $g_0,\dots,g_m \in (B_0)_+$ are such that
\[ \mathrm{sp}(\pi(g_i)) \subset [\min \mathrm{sp}(\pi(\lambda(f_i))) - \e, \max \mathrm{sp}(\pi(\lambda(f_i)))+\e] \]
for all representations $\pi$ of $A_0$ and all $i=1,\dots,m$.
There exists a commutative unital $C^*$-subalgebra $B$ of $A$ and $h_1,\dots,h_m \in B$ such that $\lambda(h_i) = g_i$ and
\begin{equation}
\label{eq:CommGluingCrucialRTP}
\mathrm{sp}(\pi(h_i)) \subset [\min \mathrm{sp}(\pi(f_i)) - 2\e, \max \mathrm{sp}(\pi(f_i))+2\e]
\end{equation}
for all representations $\pi$ of $A$ and all $i=1,\dots,m$.
Moreover, the dimension of the spectrum of $B$ is at most the maximum of the dimension of $CX$ and the dimension of the spectrum of $B_0$.
\end{lemma}

\begin{proof}
Fix $\eta > 0$ such that
\[ \rho(f_i)(x,t) \approx_\e \rho(f_i)(x,s) \]
for all $s,t \in [0,\eta]$.
Define $\theta:C(X \times [0,\eta],B_0) \to C(X \times [0,\eta],M_k)$ by
\[ \theta(c)(x,t) = \phi(c(x,t))(x), \]
and set $D$ to be the image of $\theta$.
Evidently, $D$ is commutative.
Due to the way $\theta$ is defined, each irreducible representation of $D$ factors through a point evaluation at some unique point in $X \times [0,\eta]$, and this provides a finite-to-one continuous map from the spectrum of $D$ to $X \times [0,\eta]$.
It follows by \cite[Theorem 1.12.4]{Engelking:DimTheory} that the topological dimension of $D$ is at most the dimension of $X \times [0,\eta]$ (which is the same as the dimension of $CX$).
Set
\begin{align*}
B := &\{(c,d,b) \in C(CX|_{[\eta,1]}) \oplus D \oplus B_0 \\
&\quad \mid
c(x,\eta) = d(x,\eta)\text{ for all }x\in X\text{ and }
\phi(b)=d|_{X \times \{0\}}\}.
\end{align*}
$B$ is evidently commutative, and it embeds into $A$ in a pretty straightforward way: by sending $(c,d,b)$ to $(e,b) \in C(CX,M_k) \oplus A_0$ where
\[ e|_{CX|_{[\eta,1]}} = c \quad \text{and}\quad e|_{CX|_{[0,\eta]}} = d. \]

The spectrum of $B$ is given by gluing together $CX|_{[\eta,1]}$, the spectrum of $D$, and the spectrum of $B_0$.
Hence, the spectrum of $B$ has dimension at most
\begin{align*}
\max\{\dim(CX), \dim(\text{spectrum of }B_0)\}.
\end{align*}

For $i=1,\dots,m$, define $d_i \in C(X \times [0,\eta],B_0)$ by
\[ d_i(x,t) = \frac t\eta \|\rho(f_i)(x,t)\| 1_{B_0} + (1-\frac t\eta)g_i, \]
for all $(x,t) \in X \times [0,\eta]$.
Note that
\begin{align*}
\theta(d_i)(x,\eta) &= \|\rho(f_i)(x,\eta)\|,\quad\text{for all }x\in X, \\
\theta(d_i)(x,0) &= g_i,\quad\text{for all }x \in X,
\end{align*}
and that $\theta(d_i)(x,t)$ is a convex combination of $\|\rho(f_i)(x,t)\|1_{M_k}$ and $\phi(g_i)(x)$ for all $(x,t) \in X \times [0,\eta]$.
Define $c_i:CX|_{[\eta,1]} \to M_k$ by
\[ c_i(x) := \|\rho(f_i)(x)\| \]
Then evidently, $h_i:=(c_i,\theta(d_i),g_i) \in B$ and it is not hard to see that \eqref{eq:CommGluingCrucialRTP} holds.
\end{proof}

Let $X$ be a compact metric space and let $A$ be a $C^*$-algebra.
Let $\mathcal U$ be an open cover of $X$.
Following \cite[Proposition 3.2 (iv)]{TW:Zdr}, an \textbf{$(n+1)$-colourable partition of unity subordinate to $\mathcal U$} means positive elements $b_j^{(i)} \in C(X,A)$ for $i=0,\dots,n, j=1,\dots,r$, such that:
\begin{enumerate}
\item for each $i$, the elements $b_1^{(i)},\dots,b_r^{(i)}$ are pairwise orthogonal,
\item for each $i,j$, the support of $b_j^{(i)}$ is contained in some open set in the given cover $\mathcal{U}$, and
\item $\sum_{i,j} b_j^{(i)} = 1$.
\end{enumerate}

\begin{prop}
\label{prop:CoveringTFAE}
Let $X$ be a compact metric space, let $n \in \N$, and let $A$ be a unital $C^*$-algebra.
The following are equivalent:
\begin{enumerate}[(a)]
\item
\label{CoveringTFAEa}
$C(X)$ is approximated in $C(X,A)$ by subhomogeneous algebras of topological dimension at most $n$;
\item
\label{CoveringTFAEb}
$C(X)$ is approximated in $C(X,A)$ by abelian $C^*$-algebras whose spectrum has dimension at most $n$;
\item
\label{CoveringTFAEc}
For every open cover $\mathcal U$ of $X$, there exists a \textbf{commuting} $(n+1)$-colourable partition of unity subordinate to $\mathcal U$.
\end{enumerate}
\end{prop}

\begin{remark}
In \cite[Proposition 3.2]{TW:Zdr}, it is shown that the existence of $(n+1)$-colourable approximate partitions of unity in $C(X,A)$ is equivalent to $\mathrm{dr} (C(X) \subset C(X,A)) \leq n$.
Condition (\ref{CoveringTFAEc}) is a notable strengthening, in that the partition of unity is asked to be commuting.
(Note that the difference between approximate and exact commuting partitions of unity is moot, since any commuting approximate partition of unity can be turned into a commuting exact partition of unity by functional calculus.)
Corollary \ref{cor:MainCor} and \cite[Theorem 4.1]{TW:Zdr} shows that in many cases,
(\ref{CoveringTFAEc}) is not equivalent to the weaker condition of non-commuting approximate partitions of unity.
\end{remark}

\begin{proof}
(\ref{CoveringTFAEa}) $\Rightarrow$ (\ref{CoveringTFAEb}):
Let $\mathcal F = \{a_1,\dots,a_m\} \subset C(X)$ be a finite set and let $\e > 0$.
Without loss of generality, $\mathcal F$ consists of positive elements.
By \cite[Theorem 2.15]{ENSTW}, every subhomogeneous algebra is approximated by images of noncommutative cell complexes (defined in \cite[Definition 2.1]{ENSTW}) of the same topological dimension.
Therefore, this result and (\ref{CoveringTFAEa}) provide the existence of a noncommutative cell complex $B$ of dimension at most $n-1$, a $*$-homomorphism $\phi:B \to C(X,A)$, and elements $b_1,\dots,b_m \in B$ be such that $a_i \approx_{\e/2} \phi(b_i)$ for $i=1,\dots,m$.
By an inductive argument with Lemma \ref{lem:CommGluing} as the inductive step, there exists a commutative $C^*$-subalgebra $C$ of $B$, whose spectrum has dimension at most $n-1$, and $c_1,\dots,c_m \in C_+$ such that, for every representation $\pi$ of $B$,
\begin{equation}
\label{eq:CoveringTFAEspContain}
\mathrm{sp}(\pi(c_i)) \subseteq [\min \mathrm{sp}(\pi(b_i))-\e/2, \max\mathrm{sp}(\pi(b_i))+\e/2].
 \end{equation}
For each $x\in X$, $\phi(b_i)(x) \approx_{\e/2} a_i(x) \in \mathbb C$, so that
\[  \mathrm{sp}(\phi(b_i)(x)) \subseteq (a_i(x)-\e/2, a_i(x)+\e/2). \]
Using this and \eqref{eq:CoveringTFAEspContain} with $\pi=\phi(\cdot)(x)$, this yields that
\[ \mathrm{sp}(\phi(c_i)(x)) \subseteq (a_i(x)-\e, a_i(x)+\e), \]
and thus, $\phi(c_i) \approx_\e a_i$.

Hence, $C$ and $c_1,\dots,c_m$ witness that (\ref{CoveringTFAEb}) holds.

(\ref{CoveringTFAEb}) $\Rightarrow$ (\ref{CoveringTFAEc}):
Let $\mathcal F$ be a finite partition of unity such that, for each $f \in \mathcal F$, there exists $U_f \in \mathcal{U}$ such that $\mathrm{supp}\, f \subset U_f$.
Use (\ref{CoveringTFAEb}) to obtain a space $Y$ of dimension at most $n$ and a $*$-homomorphism $\phi:C(Y) \to C(X,A)$ such that $\mathcal F \subset_\e \phi(C(Y))$ (for some sufficiently small $\e$ to be defined).
For each $f \in \mathcal F$, let $g_f \in C(Y)$ be such that $f \approx_\e \phi(g_f)$.
By functional calculus, we may assume that $\mathrm{supp}\, \phi(g_f) \subset U_f$.
Note that $1 \approx_{|\mathcal F|\e} \sum_{f \in \mathcal F} \phi(g_f)$.

Set $Y' := \{y \in Y : \sum_{f \in \mathcal F} g_f(y) \geq 1-2|\mathcal F|\e\}$.
It follows that $\ker \phi = C_0(Z)$ for some open set $Z$ such that $Z \cap Y' = \emptyset$.

Since $Y$ has dimension at most $n$, let $(a_j^{(i)})$ be an $(n+1)$-colourable family of positive elements, that is subordinate to $\{g_f^{-1}((0,\infty)): f \in \mathcal F\}$, such that
\[ \sum_{i,j} a_j^{(i)}|_{Y'} = 1_{Y'}. \]
Set
\[ b_j^{(i)} := \phi(a_j^{(i)}). \]
This is $(n+1)$-colourable since $(a_j^{(i)})$ is.
It is subordinate to $\mathcal U$, since if the support of $a_j^{(i)}$ is contained in $g_f^{-1}((0,\infty))$ then the support of $b_j^{(i)}$ is contained in $U_f$.
Finally, $1-\sum_{i,j} a_j^{(i)} \in C_0(Y \setminus Y') \subseteq C_0(Z)$, and so $\sum_{i,j} b_j^{(i)} = 1$.

(\ref{CoveringTFAEc}) $\Rightarrow$ (\ref{CoveringTFAEa}):
This is clear, since the universal $C^*$-algebra generated by a commuting, $(n+1)$-colourable partition of unity $(b_j^{(i)})_{i=0,\dots,n-1,j=1,\dots,r}$ is $C(Z)$ where $Z$ is the geometric realization of an $n$-dimensional simplicial complex, see Proposition \ref{prop:SimpComplexCstar}.
\end{proof}

\section{Disk-to-sphere retracts}
\label{sec:3}

In this section, we show that low-dimensional, commutative approximations of $C(D^n)$ inside $C(D^n,A)$ implies condition (\ref{MainThm3}) of Theorem \ref{thm:MainThm}.
Condition (\ref{MainThm3}) can be viewed as the existence of noncommutative retracts $D^n \to S^{n-1}$, when $D^n$ is enriched by the space $A$.
We first show that we can (point-norm) approximately satisfy condition (\ref{MainThm3}), which is the more difficult step, and then we use a semiprojectivity argument (in the category of commutative $C^*$-algebras) to obtain condition (\ref{MainThm3}) exactly.

Given an open cover $\mathcal U$ of a topological space $X$, we define the $n$-nerve of $\mathcal U$ to be the following simplicial complex on the vertex set $\mathcal U$:
\[ N_n(\mathcal U) := \big\{\, \{U_1,\dots,U_k\} \subseteq \mathcal U \mid k \leq n\text{ and } U_1 \cap \cdots \cap U_k \neq \emptyset\big\}. \]
(That is, it is the $(n-1)$-dimensional skeleton of the nerve of $\mathcal U$.)

\begin{lemma}
\label{lem:SnNerve}
Let $\mathcal U$ be an open cover of $S^{n-1}$.
Then there exists an open cover $\mathcal V$ of $D^n$ and a continuous map $\alpha:|N_n(\mathcal V)| \to S^{n-1}$ such that, for each $V \in \mathcal V$, if $V \cap S^{n-1} \neq \emptyset$ then
\begin{enumerate}
\item there exists $U \in \mathcal U$ such that $V \cap S^{n-1} \subseteq U$; and
\item $\alpha(\mathrm{Star}(V)) = V \cap S^{n-1}$.
\end{enumerate}
\end{lemma}

\begin{proof}
Let $N$ be a simplicial complex with vertex set $X$ such that $|N| \cong S^{n-1}$, such that upon identifying these spaces, each star in $N$ is contained in some set in $\mathcal U$.

View $D^n$ as $CS^{n-1}$ (as in \eqref{eq:Cone}), so that the boundary $S^{n-1}$ is identified with $S^{n-1} \times \{0\}$.
Let $\pi:S^{n-1} \times [0,1] \to D^{n}$ be the quotient map.
For $x \in X$, set
\[ V_0(x) := \pi(\mathrm{Star}(x) \times [0,1/2)), \quad V_1(x) := \pi(\mathrm{Star}(x) \times (0,1)). \]
Then define
\[ \mathcal V := \{V_i(x) \mid i=0,1, x\in X\} \cup \{\pi(S^{n-1} \times (1/2,1])\}, \]
an open cover of $D^n$.

Note that $V_0(x) \cap \pi(S^{n-1} \times (1/2,1]) = \emptyset$, so that if $\{W_1,\dots,W_k\} \in N_{n}(\mathcal V)$ then either:
\begin{enumerate}[(a)]
\item Each $W_j$ is of the form $V_i(x)$ for some $i=0,1$ and $x\in X$; or
\item Some $W_j$ is equal to $\pi(S^{n-1} \times (1/2,1])$ and for every other $j$, $W_j$ is of the form $V_1(x)$ for some $x \in X$.
\end{enumerate}
Let $N'$ be the subcomplex of $N_n(\mathcal V)$ consisting of simplices $\{W_1,\dots,W_k\}$ of the first type; then the map $V_i(x) \to x$ induces a simplicial map $N' \to N$, and thereby a continuous map
\[ |N'| \to |N|=S^{n-1}. \]
We set $\alpha|_{|N'|}$ to be this map.
Then, since $|N_{n}(\mathcal V)|$ is $(n-1)$-dimensional, we may extend this map to all of $|N_{n}(\mathcal V)|$.

For $V \in \mathcal V$, if $V\cap S^{n-1} \neq \emptyset$ then $V= V_0(W)$ for some $W \in \mathcal W$.
In this case, $\mathrm{Star}(V)$ is contained entirely in $|N'|$, so that its image is precisely $W=V \cap S^{n-1}$, so that (ii) holds.
By our choice of $\mathcal W$, (i) also holds.
\end{proof}

The following proposition, making use of the covering dimension result in the previous section, establishes that Theorem \ref{thm:MainThm} (\ref{MainThm1}) implies an approximate version of Theorem \ref{thm:MainThm} (\ref{MainThm3}).

\begin{prop}
\label{prop:ApproxRetract}
Let $A$ be a unital $C^*$-algebra and let $n \in \N$.
If $C(D^n)$ is approximated in $C(D^n,A)$ by commutative $C^*$-algebras whose spectrum has dimension at most $(n-1)$, then the following holds.
For any finite set $\mathcal F \subset C(S^{n-1})$ and any $\e > 0$, there exists a $*$-homomorphism $\phi:C(S^{n-1}) \to C(D^n,A)$ such that
\[ a \approx_\e \phi(a)|_{S^{n-1}} \]
for all $a\in\mathcal F$;
\end{prop}

\begin{proof}
Let $\mathcal F \subset C(S^{n-1})$ and $\e > 0$ be given.
Let $\mathcal U_0$ be an open cover of $S^{n-1}$ such that for every $a \in \mathcal F$, $U \in \mathcal U_0$ and $x,y \in U$, $\|a(x)-a(y)\| < \e$.
There exists an open cover $\mathcal U$ of $S^{n-1}$ such that, for every $k$ and every $V_1,\dots,V_k \in \mathcal U$, if $V_1 \cap \cdots \cap V_k \neq \emptyset$ then there exists $U \in \mathcal U_0$ such that
\[ V_1 \cup \cdots \cup V_k \subseteq U. \]
(This can be done by taking a barycentric refinement of $\mathcal U_0$, see eg.\ \cite[VIII.3]{Dugundji}; alternatively, it is not hard to do by putting a metric on $S^{n-1}$.)

Let $\mathcal V$ be an open cover of $D^n$ and $\alpha:|N_n(\mathcal V)| \to S^{n-1}$ be a continuous map as provided by Lemma \ref{lem:SnNerve}.
By the hypothesis and Proposition \ref{prop:CoveringTFAE}, let $(b^{(i)}_j)_{i=0,\dots,n;\ j=1,\dots,r}$ be an $n$-colourable commuting partition of unity subordinate to $\mathcal V$.
For each $i,j$, let $V^{(i)}_j \in \mathcal V$ be a set containing the support of $b^{(i)}_j$.

As described in Section \ref{sec:SimpComplex}, let $N$ be the nerve of $(b^{(i)}_j)$ (with $\{(i,j)\mid i=0,\dots,n, j=1,\dots,r\}$ as the set of vertices) and let $\psi:C(|N|) \to C^*(\{b^{(i)}_j\})$ be the canonical $*$-homomorphism.
If $\{b^{(i_1)}_{j_1},\dots,b^{(i_k)}_{j_k}\}$ is a simplex in $N$ then evidently $k \leq n$ (by $n$-colourability), and
\[ V^{i_1}_{j_1} \cap \cdots \cap V^{i_k}_{j_k} \neq \emptyset. \]
Thus, $(i,j) \mapsto V^{(i)}_j$ induces a simplicial map from $N$ to $N_{n}(\mathcal V)$, and thereby a continuous map $\beta:|N| \to |N_{n}(\mathcal V)|$.

Define $\phi:C(S^{n-1}) \to C(D^{n},A)$ to be the following composition
\[ C(S^{n-1}) \labelledrightarrow{f \mapsto f \circ \alpha} C(|N_{n}(\mathcal V)|) \labelledrightarrow{f \mapsto f \circ \beta} C(|N|) \labelledrightarrow{\psi} C^*(\{b^{(i)}_j\}) \subseteq C(D^{n},A). \]
Let us now show that $\|a-\phi(a)|_{S^{n-1}}\| \leq \e$ for $a \in \mathcal F$, by showing that $\|a(x)-\phi(a)(x)\| \leq \e$ for every $x \in S^{n-1}$.

Therefore, fix $x \in S^{n-1}$ and $a \in \mathcal F$.
Let the kernel of $\ev_x \circ \phi$ be $C_0(S^{n-1} \setminus Y)$, where $Y \subseteq S^{n-1}$ is closed; thus, $\ev_x \circ \phi$ can be viewed as a representation of $C(Y)$.
Using the fact that $a(x) \in \C$ and $\phi$ is unital, we see that $\|a(x)-\phi(a)(x)\| \leq \sup_{y \in Y} \|a(x)-a(y)\|$.
We shall show that $Y$ is a subset of some open set in $\mathcal U'$, so that we may conclude that $\|a(x)-\phi(a)(x)\| \leq \e$.

Let the kernel of $\ev_x \circ \psi$ be $C_0(|N| \setminus Z)$, so that $Y \subseteq \alpha(\beta(Z))$ (by the definition of $\phi$).
Set $T:= \{(i,j) \mid b^{(i)}_j(x) \neq 0\}$.
By the definition of $\psi$, we can see that $Z$ is contained in the union of stars about vertices $(i,j)\in T$.
The definition of $\beta$ then ensures that $\beta(Z)$ is contained in the union of stars about vertices $V^{(i)}_j$, where $(i,j) \in T$.
By Lemma \ref{lem:SnNerve} (ii), $\alpha(\mathrm{Star}(V^{(i)}_j)) = V^{(i)}_j \cap S^{n-1}$ in $S^{n-1}$, so that
\begin{equation}
\label{eq:ApproxRetractYsub}
 Y \subseteq \alpha(\beta(Z)) \subseteq \bigcup_{(i,j) \in T} V^{(i)}_j \cap S^{n-1}.
\end{equation}

By definition of $T$, and since the support of $b^{(i)}_j$ is contained in $V^{(i)}_j$, we have
\[ x \in \bigcap_{(i,j) \in T} V^{(i)}_j \cap S^{n-1}. \]
By Lemma \ref{lem:SnNerve} (i), $V^{(i)}_j \cap S^{n-1}$ is a subset of some $U^{(i)}_j \in \mathcal U$.
By our choice of $\mathcal U$, this implies that there exists $U \in \mathcal U_0$ such that
\[ \bigcup_{(i,j) \in T} V^{(i)}_j \cap S^{n-1} \subseteq U. \]
Combined with \eqref{eq:ApproxRetractYsub}, we find that $Y \subseteq U$, as required.
\end{proof}

Our next task is to turn the approximate version of Theorem \ref{thm:MainThm} (\ref{MainThm3}) into an exact version, thus completing the proof of Theorem \ref{thm:MainThm} (\ref{MainThm1}) $\Rightarrow$ (\ref{MainThm3}).
This will use a fact about ANRs, namely that nearby maps into an ANR are homotopic \cite[Theorem IV.1.1]{Hu:RetractBook}, applied to the ANR $S^{n-1}$.
We state (and use) this result in the language of commutative $C^*$-algebras.

\begin{lemma} \cite[Theorem IV.1.1]{Hu:RetractBook}
\label{lem:SnHomotopy}
Let $n \in \N$.
There is a finite set $\mathcal F \subset C(S^{n-1})$ and $\e > 0$ such that the following holds:
If $A$ is a commutative $C^*$-algebra and $\phi_0,\phi_1:C(S^{n-1}) \to A$ are $*$-homomorphisms which satisfy
\[ \phi_0(a) \approx_\e \phi_1(a) \]
for all $a\in \mathcal F$, then $\phi_0$ and $\phi_1$ are homotopic, i.e.\ there is a $*$-homomorphism $\phi:C(S^{n-1}) \to C([0,1],A)$ such that
\[ \phi_i = \ev_i \circ \phi \]
for $i=0,1$.
\end{lemma}

\begin{proof}[Proof of Theorem \ref{thm:MainThm} (\ref{MainThm1}) $\Rightarrow$ (\ref{MainThm3})]
Suppose that (\ref{MainThm1}) holds, and thereby so does the conclusion of Proposition \ref{prop:ApproxRetract}.
Let $\mathcal F \subset C(S^{n-1})$ and $\e>0$ be given by Lemma \ref{lem:SnHomotopy}.
Use the conclusion of Proposition \ref{prop:ApproxRetract} to get a $*$-homomorphism
\[ \phi_0:C(S^{n-1}) \to C(D^{n},A) \]
such that $\phi_0(a)|_{S^{n-1}} \approx_\e a$ for all $a\in \mathcal F$.
Note that
\[ B:=C^*(C(S^{n-1}) \cup \phi_0(C(S^{n-1}))|_{S^{n-1}}) \]
is a commutative subalgebra of $C(S^{n-1},A)$.
Therefore by Lemma \ref{lem:SnHomotopy}, there exists $\psi:C(S^{n-1}) \to C([0,1],B)$ such that
\begin{equation}
\label{eq:DimRetractHomotope}
 \ev_0 \circ \psi = \phi_0|_{S^{n-1}}
\end{equation}
and $\ev_1 \circ \psi$ is equal to the trivial inclusion $C(S^{n-1}) \subseteq B$.

$D^{n}$ is homeomorphic to $(D^{n} \cup [0,1] \times S^{n-1})/\sim$, where $\sim$ identifies each point of $\partial D^{n} \cong S^{n-1}$ with the corresponding point of $\{0\} \times S^{n-1}$.
This provides an identification of $C(D^n,A)$ with a subalgebra $C$ of
\[ C(D^n,A) \oplus C([0,1] \times S^{n-1},A), \]
and we see that \eqref{eq:DimRetractHomotope} ensures that the image of the map $\phi_0 \oplus \psi:C(S^{n-1}) \to C(D^{n},A) \oplus C([0,1] \times S^{n-1},A)$ is contained in $C$.
Thus, we may view $\phi_0 \oplus \psi$ as a map $\phi:C(S^{n-1}) \to C(D^n,A)$.
Then for $a \in C(S^{n-1})$,
\[ \phi(a)|_{S^{n-1}} = \psi(a)|_{\{1\} \times S^{n-1}} = a, \]
as required.
\end{proof}

\section{Kirchberg and R\o rdam's argument}
\label{sec:4}

\begin{proof}[Proof of Theorem \ref{thm:MainThm} (\ref{MainThm3}) $\Rightarrow$ (\ref{MainThm1}).]
This is essentially contained in the proof of \cite[Proposition 3.5]{KirchbergRordam:pi3}.

Assume that (\ref{MainThm3}) holds.
Let us first assume that $X$ is a CW complex.
Given a finite subset $\mathcal F$ of $C(X)$ and $\e>0$, let us take a CW decomposition of $X$ so that each $a\in \mathcal F$ varies by at most $\e$ on each cell.
We may view this decomposition as a canonical surjection
\[ \alpha:\coprod_{k=1}^r D_k \to X, \]
where each $D_k$ is homeomorphic to a disc of dimension at most $n$,
and the restriction of $\alpha$ to $\bigcup D_k^{\circ}$ is one-to-one.
Composition with $\alpha$ provides an injective $*$-homomorphism $C(X) \to C(\coprod_{k=1}^r D_k)$; we will identify $C(X)$ with its image under this map.
For each $k$, define $Y_k \subseteq D_k$ and $\phi_k:C(Y_k) \to C(D_k,A)$ as follows:
If $D_k$ has dimension $n$, set $Y_k:= \partial D_k$ and let $\phi_k$ be as given by (\ref{MainThm3}).
Otherwise, set $Y_k := D_k$ and let $\phi_k:C(D_k) \to C(D_k,A)$ be the inclusion.

Note that in both cases, we have $\partial D_k \subseteq \partial Y_k$ and $\phi_k(a)|_{\partial D_k} = a|_{\partial D_k}$ for all $a \in C(D_k)$.
Set $\hat\phi = \bigoplus \phi_k:C(\coprod_{k=1}^r Y_k) \to C(\bigcup_{k=1}^r D_k)$, and set $Y = \alpha(\coprod Y_k)$.
Identify $C(Y)$ with a subalgebra of $C(\coprod_k Y_k)$ via $\alpha$.
Since $\hat\phi(a)|_{\bigcup \partial D_k} = a|_{\bigcup \partial D_k}$, we see that for $a \in C(Y)$,
\[ \hat\phi(a) \in C(X,A). \]
Hence, $\phi:= \hat\phi|_{C(Y)}$ is a map from $C(Y)$ to $C(X,A)$.
For $x \in X$, the kernel of $\ev_x \circ \phi$ is $C_0(Y \setminus K)$ where
\[ K \subseteq \bigcup \{\alpha(D_k) \mid x \in \alpha(D_k)\}. \]
Since each $a \in \mathcal F$ varies by at most $\e$ on each $\alpha(D_k)$, we see that
\[ \phi(a|_Y)(x) \approx_\e a(x). \]
In particular, $\mathcal F$ is approximated by the image of $C(Y)$, thus concluding the proof in the case that $X=D^n$.

Now, any other $n$-dimensional compact Hausdorff space $X$ is an inverse limit of CW complexes of dimension at most $n$, so that $\mathcal F$ can be approximated (up to $\e/2$), inside $C(X)$, by an algebra $C$ isomorphic to $C(Z)$ for some $n$-dimensional CW complex $Z$.
Hence, we may approximate $\mathcal F$ (up to $\e$) inside $C \otimes A \subseteq C(X) \otimes A$ by a commutative algebra of topological dimension at most $n-1$.
\end{proof}

\begin{proof}[Proof of the last sentence of Theorem \ref{thm:MainThm}]
The above argument, and induction, shows that if Theorem \ref{thm:MainThm} (\ref{MainThm3}) holds, then for any $m \geq n$, the inclusion $C(D^m) \to C(D^m,A^{\otimes m})$ can be approximately factorized as
\[ C(D^m) \labelledrightarrow{\psi} C(\Gamma) \labelledrightarrow{\phi} C(D^m,A^{\otimes (m-n+1)}), \]
where $\Gamma$ has dimension at most $n-1$ and $\psi\phi(f)|_{S^{m-1}} = f|_{S^{m-1}}$.
We may identify $A^{m-n+1}$ with $A$, so that for any $m \in \N$, the inclusion $C(D^m) \to C(D^m,A^{\otimes m})$ can be approximately factorized as
\[ C(D^m) \labelledrightarrow{\psi} C(\Gamma) \labelledrightarrow{\phi} C(D^m,A^{\otimes (m-n+1)}), \]
where $\Gamma$ has dimension at most $n-1$ and $\psi\phi(f)|_{S^{m-1}} = f|_{S^{m-1}}$ (this factorization is trivial if $m \leq n-1$).
Then, a patching-together argument as in the above proof shows that (\ref{MainThm1}) holds with the words ``$n$-dimensional'' removed, when $X$ is a CW complex.
Approximating arbitrary $X$ by CW complexes, again as in the above argument, yields (\ref{MainThm1}) with the words ``$n$-dimensional'' removed, in general.
\end{proof}

\newcommand{\cstar}{$\mathrm C^*$}

config: arxiv


TITLE: Why does hot water gets cooler on stirring instead it should have gotten hotter
QUESTION [0 upvotes]: When we keep on stirring hot water vigorously it starts getting cooler. But we are increasing the random kinetic energy of the molecules of water. Heat is as it is the energy of RANDOM motion of atoms. So when we are stirring the water vigorously it should get hotter and hotter because the increase in energy of molecules of water. But the opposite happens..Why is this so? Has it something to do Mpemba effect

REPLY [2 votes]: Getting cooler is the key phrase in you question.  If you vigorously stir cold water you might get it to warm up if it was well insulated - duplicating  Joule's clasic Mechanical equivalent of heat experiment.  But if you stir a cup of hot coffee or a pot of hot water the far more significant effect effect it that the stirring accelerates cooling.
Stirring allows hot liquid to reach the surface much faster than unassisted convection.  At the surface this hot water evaporates cooling the remaining water as a result.

REPLY [1 votes]: Moving water convects heat better than static water. Take the reference frame of the water being static and the air moving. In this case, new cooler air is always sweeping in to take heat away. If the air is static, hot air remains at the interface and will not accept heat as well as cooler air. The same argument can be made for the moving water.
Edit: The motion you are providing by stirring in minimal compared to the microscopic motion of the water.


text:
theory NegInfinityUni
  imports UniAtoms NegInfinity QE
begin

fun allZero' :: "real * real * real \<Rightarrow> atomUni fmUni" where
  "allZero' (a,b,c) = AndUni(AndUni(AtomUni(EqUni(0,0,a))) (AtomUni(EqUni(0,0,b)))) (AtomUni(EqUni(0,0,c)))"

lemma convert_allZero :
  assumes "convert_poly var p (xs'@x#xs) = Some p'"
  assumes "length xs' = var"
  shows "eval (allZero p var) (xs'@x#xs) = evalUni (allZero' p') x"
proof(cases p')
  case (fields a b c)
  then show ?thesis proof(cases "MPoly_Type.degree p var = 0")
    case True
    then show ?thesis
      using assms fields
      by(simp add:eval_list_conj isovar_greater_degree)
  next
    case False
    then have nonzero : "MPoly_Type.degree p var \<noteq> 0" by auto
    then show ?thesis
    proof(cases "MPoly_Type.degree p var = 1")
      case True
      then show ?thesis
        using assms fields
        apply(simp add:eval_list_conj isovar_greater_degree)
        by (metis)
    next
      case False
      then have degree2 : "MPoly_Type.degree p var = 2" using degree_convert_eq[OF assms(1)] nonzero by auto
      then show ?thesis
        using assms
        apply(simp add:eval_list_conj isovar_greater_degree)
        using insertion_isovarspars_free list_update_code(2)
        apply auto
        by (metis One_nat_def Suc_1 less_2_cases less_Suc_eq numeral_3_eq_3)
    qed
  qed
qed

fun alternateNegInfinity' :: "real * real * real \<Rightarrow> atomUni fmUni" where
  "alternateNegInfinity' (a,b,c) =
OrUni(AtomUni(LessUni(0,0,a)))(
AndUni(AtomUni(EqUni(0,0,a))) (
  OrUni(AtomUni(LessUni(0,0,-b)))(
  AndUni(AtomUni(EqUni(0,0,b)))(
    AtomUni(LessUni(0,0,c))
  ))
))
"

lemma convert_alternateNegInfinity :
  assumes "convert_poly var p (xs'@x#xs) = Some X"
  assumes "length xs' = var"
  shows "eval (alternateNegInfinity p var) (xs'@x#xs) = evalUni (alternateNegInfinity' X) x"
proof(cases X)
  case (fields a b c)
  then show ?thesis proof(cases "MPoly_Type.degree p var = 0")
    case True
    then show ?thesis
      using assms
      apply (simp add: isovar_greater_degree)
      apply auto
      apply (metis aEval.simps(2) eval.simps(1) eval_and eval_false eval_or  mult_one_left)
      by (metis aEval.simps(2) eval.simps(1) eval_or  mult_one_left)
  next
    case False
    then have nonzero : "MPoly_Type.degree p var \<noteq> 0" by auto
    then show ?thesis
    proof(cases "MPoly_Type.degree p var = 1")
      case True
      have letbind: "eval
     (let a_n = isolate_variable_sparse p var (Suc 0)
      in or (fm.Atom (Less (Const (- 1) * a_n)))
          (and (fm.Atom (Eq a_n))
            (let a_n = isolate_variable_sparse p var 0
             in or (fm.Atom (Less (Const 1 * a_n))) (and (fm.Atom (Eq a_n)) FalseF))))
     (xs'@x#xs) =
    eval
     (or (fm.Atom (Less (Const (- 1) * (isolate_variable_sparse p var (Suc 0)))))
          (and (fm.Atom (Eq (isolate_variable_sparse p var (Suc 0))))
            (or (fm.Atom (Less (Const 1 * (isolate_variable_sparse p var 0)))) (and (fm.Atom (Eq (isolate_variable_sparse p var 0))) FalseF))))
     (xs'@x#xs)"
        by meson
      show ?thesis
        using assms True unfolding fields
        by (simp add: isovar_greater_degree letbind eval_or eval_and insertion_mult insertion_const)
    next
      case False
      then have degree2 : "MPoly_Type.degree p var = 2" using degree_convert_eq[OF assms(1)] nonzero by auto
      have "[0..<3] = [0,1,2]"
        by (simp add: upt_rec)
      then have unfold : " (foldl
       (\<lambda>F i. let a_n = isolate_variable_sparse p var i
               in or (fm.Atom (Less ((if i mod 2 = 0 then Const 1 else Const (- 1)) * a_n)))
                   (and (fm.Atom (Eq a_n)) F))
       FalseF [0..<3]) =
     (let a_n = isolate_variable_sparse p var 2
               in or (fm.Atom (Less ((Const 1) * a_n)))
                   (and (fm.Atom (Eq a_n))
       (let a_n = isolate_variable_sparse p var (Suc 0)
      in or (fm.Atom (Less (Const (- 1) * a_n)))
          (and (fm.Atom (Eq a_n))
            (let a_n = isolate_variable_sparse p var 0
             in or (fm.Atom (Less (Const 1 * a_n))) (and (fm.Atom (Eq a_n)) FalseF))))))"
        by auto
      have letbind : "eval
     (foldl
       (\<lambda>F i. let a_n = isolate_variable_sparse p var i
               in or (fm.Atom (Less ((if i mod 2 = 0 then Const 1 else Const (- 1)) * a_n)))
                   (and (fm.Atom (Eq a_n)) F))
       FalseF [0..<3]) (xs'@x#xs) =
      eval

(or (fm.Atom (Less ( Const 1 * (isolate_variable_sparse p var 2))))
                   (and (fm.Atom (Eq (isolate_variable_sparse p var 2)))
(or (fm.Atom (Less (Const (- 1) * (isolate_variable_sparse p var (Suc 0)))))
          (and (fm.Atom (Eq (isolate_variable_sparse p var (Suc 0))))
            (or (fm.Atom (Less (Const 1 * (isolate_variable_sparse p var 0)))) (and (fm.Atom (Eq (isolate_variable_sparse p var 0))) FalseF))))))
(xs'@x#xs)" apply (simp add:unfold) by metis
      show ?thesis
        using degree2 assms unfolding fields by (simp add: isovar_greater_degree eval_or eval_and letbind insertion_mult insertion_const)
    qed
  qed
qed

fun substNegInfinityUni :: "atomUni \<Rightarrow> atomUni fmUni" where
  "substNegInfinityUni (EqUni p) = allZero' p " |
  "substNegInfinityUni (LessUni p) = alternateNegInfinity' p"|
  "substNegInfinityUni (LeqUni p) = OrUni (alternateNegInfinity' p) (allZero' p)"|
  "substNegInfinityUni (NeqUni p) = negUni (allZero' p)"

lemma convert_substNegInfinity :
  assumes "convert_atom var A (xs'@x#xs) = Some(A')"
  assumes "length xs' = var"
  shows "eval (substNegInfinity var A) (xs'@x#xs) = evalUni (substNegInfinityUni A') x"
  using assms
proof(cases A)
  case (Less p)
  have "\<exists>X. convert_poly var p (xs' @ x # xs) = Some X" using assms Less apply(cases "MPoly_Type.degree p var < 3") by (simp_all)
  then obtain X where X_def: "convert_poly var p (xs' @ x # xs) = Some X" by auto
  then have A' : "A' = LessUni X" using assms Less apply(cases "MPoly_Type.degree p var < 3") by (simp_all)
  show ?thesis unfolding Less substNegInfinity.simps
    unfolding convert_alternateNegInfinity[OF X_def assms(2)] A'
    apply(cases X) by simp
next
  case (Eq p)
  then show ?thesis using assms convert_allZero by auto
next
  case (Leq p)
  define p' where "p' = (case convert_poly var p (xs'@x#xs) of Some p' \<Rightarrow> p')"
  have A'_simp :  "A' = LeqUni p'"
    using assms Leq
    using p'_def by auto
  have allZ : "eval (allZero p var) (xs'@x#xs) = evalUni (allZero' p') x" using convert_allZero
    using Leq assms p'_def by auto
  have altNeg : "eval (alternateNegInfinity p var) (xs'@x#xs) = evalUni (alternateNegInfinity' p') x" using convert_alternateNegInfinity
    using Leq assms p'_def by auto
  show ?thesis
    unfolding Leq substNegInfinity.simps eval_Or A'_simp substNegInfinityUni.simps evalUni.simps
    using allZ altNeg by auto
next
  case (Neq p)
  then show ?thesis using assms convert_allZero convert_neg by auto
qed

lemma change_eval_eq:
  fixes x y:: "real"
  assumes "((aEvalUni (EqUni(a,b,c)) x \<noteq> aEvalUni (EqUni(a,b,c)) y) \<and> x < y)"
  shows "(\<exists>w. x \<le> w \<and> w \<le> y \<and> a*w^2 + b*w + c = 0)"
  using assms by auto
lemma change_eval_lt:
  fixes x y:: "real"
  assumes "((aEvalUni (LessUni (a,b,c)) x \<noteq> aEvalUni (LessUni (a,b,c)) y) \<and> x < y)"
  shows "(\<exists>w. x \<le> w \<and> w \<le> y \<and> a*w^2 + b*w + c = 0)"
proof -
  let ?p = "[:c, b, a:]"
  have "sign ?p x \<noteq> sign ?p y"
    using assms unfolding sign_def
    apply (simp add: distrib_left mult.commute mult.left_commute power2_eq_square)
    by linarith
  then have "(\<exists>w \<in> (root_list ?p). x \<le> w \<and> w \<le> y)" using changes_sign
      assms by auto
  then obtain w where w_prop: "w \<in> (root_list ?p) \<and> x \<le> w \<and> w \<le> y" by auto
  then have "a*w^2 + b*w + c = 0" unfolding root_list_def
    using add.commute distrib_right mult.assoc mult.commute power2_eq_square
    using quadratic_poly_eval by force
  then show ?thesis using w_prop by auto
qed

lemma no_change_eval_lt:
  fixes x y:: "real"
  assumes "x < y"
  assumes "\<not>(\<exists>w. x \<le> w \<and> w \<le> y \<and> a*w^2 + b*w + c = 0)"
  shows "((aEvalUni (LessUni (a,b,c)) x = aEvalUni (LessUni (a,b,c)) y))"
  using change_eval_lt
  using assms(1) assms(2) by blast

lemma change_eval_neq:
  fixes x y:: "real"
  assumes "((aEvalUni (NeqUni (a,b,c)) x \<noteq> aEvalUni (NeqUni (a,b,c)) y) \<and> x < y)"
  shows "(\<exists>w. x \<le> w \<and> w \<le> y \<and> a*w^2 + b*w + c = 0)"
  using assms by auto

lemma change_eval_leq:
  fixes x y:: "real"
  assumes "((aEvalUni (LeqUni (a,b,c)) x \<noteq> aEvalUni (LeqUni (a,b,c)) y) \<and> x < y)"
  shows "(\<exists>w. x \<le> w \<and> w \<le> y \<and> a*w^2 + b*w + c = 0)"
proof -
  let ?p = "[:c, b, a:]"
  have "sign ?p x \<noteq> sign ?p y"
    using assms unfolding sign_def
    apply (simp add: distrib_left mult.commute mult.left_commute power2_eq_square)
    by linarith
  then have "(\<exists>w \<in> (root_list ?p). x \<le> w \<and> w \<le> y)" using changes_sign
      assms by auto
  then obtain w where w_prop: "w \<in> (root_list ?p) \<and> x \<le> w \<and> w \<le> y" by auto
  then have "a*w^2 + b*w + c = 0" unfolding root_list_def
    using add.commute distrib_right mult.assoc mult.commute power2_eq_square
    using quadratic_poly_eval by force
  then show ?thesis using w_prop by auto
qed

lemma change_eval:
  fixes x y:: "real"
  fixes At:: "atomUni"
  assumes xlt: "x < y"
  assumes noteq: "((aEvalUni At) x \<noteq> aEvalUni (At) y)"
  assumes "getPoly At = (a, b, c)"
  shows "(\<exists>w. x \<le> w \<and> w \<le> y \<and> a*w^2 + b*w + c = 0)"
proof -
  have four_types: "At = (EqUni (a,b,c)) \<or> At = (LessUni (a,b,c)) \<or> At = (LeqUni (a,b,c)) \<or> At = (NeqUni (a,b,c))"
    using getPoly.elims assms(3) by force
  have eq_h: "At = (EqUni (a,b,c)) \<longrightarrow> (\<exists>w. x \<le> w \<and> w \<le> y \<and> a*w^2 + b*w + c = 0)"
    using assms(1) assms(2) change_eval_eq
    by blast
  have less_h: "At = (LessUni(a,b,c)) \<longrightarrow> (\<exists>w. x \<le> w \<and> w \<le> y \<and> a*w^2 + b*w + c = 0)"
    using change_eval_lt assms
    by blast
  have leq_h: "At = (LeqUni(a,b,c)) \<longrightarrow> (\<exists>w. x \<le> w \<and> w \<le> y \<and> a*w^2 + b*w + c = 0)"
    using change_eval_leq assms
    by blast
  have neq_h: "At = (NeqUni(a,b,c)) \<longrightarrow> (\<exists>w. x \<le> w \<and> w \<le> y \<and> a*w^2 + b*w + c = 0)"
    using change_eval_neq assms
    by blast
  show ?thesis
    using four_types eq_h less_h leq_h neq_h
    by blast
qed

lemma no_change_eval:
  fixes x y:: "real"
  assumes "getPoly At = (a, b, c)"
  assumes "x < y"
  assumes "\<not>(\<exists>w. x \<le> w \<and> w \<le> y \<and> a*w^2 + b*w + c = 0)"
  shows  "((aEvalUni At) x = aEvalUni (At) y \<and> x < y)"
  using change_eval
  using assms(1) assms(2) assms(3) by blast

lemma same_eval'' :
  assumes "getPoly At = (a, b, c)"
  assumes nonz: "a \<noteq> 0 \<or> b \<noteq> 0 \<or> c \<noteq> 0"
  shows "\<exists>x. \<forall>y<x. (aEvalUni At y = aEvalUni At x)"
proof -
  let ?p = "[:c, b, a:]"
  have poly_eval: "\<forall>y. poly ?p y = a*y^2 + b*y + c"
    by (simp add: distrib_left power2_eq_square)
  have "?p \<noteq> 0" using nonz by auto
  then have "finite {y. poly ?p y = 0}"
    using poly_roots_finite
    by blast
  then have "finite {y. c + (a * y\<^sup>2 + b * y) = 0} \<Longrightarrow>
    \<forall>y. y * (b + y * a) = a * y\<^sup>2 + b * y \<Longrightarrow>
    finite {y. a * y\<^sup>2 + b * y + c = 0}"
  proof -
    assume a1: "finite {y. c + (a * y\<^sup>2 + b * y) = 0}"
    have "\<forall>x0. c + (a * x0\<^sup>2 + b * x0) = a * x0\<^sup>2 + b * x0 + c"
      by simp
    then show ?thesis
      using a1 by presburger
  qed
  then have finset: "finite {y. a*y^2 + b*y + c = 0}"
    using poly_eval
    by (metis \<open>finite {y. poly [:c, b, a:] y = 0}\<close> poly_roots_set_same)
  then have "\<exists>x. (\<forall>y. a*y^2 + b*y + c = 0 \<longrightarrow> x < y)"
  proof -
    let ?l = "sorted_list_of_set {y. a*y^2 + b*y + c = 0}"
    have "\<exists>x. x < ?l ! 0"
      using infzeros nonz by blast
    then obtain x where x_prop: "x < ?l! 0" by auto
    then have "\<forall> y. List.member ?l y \<longrightarrow> x < y"
    proof clarsimp
      fix y
      assume "List.member ?l y"
      then have "\<exists>n. n < length ?l \<and> ?l ! n = y"
        by (meson in_set_conv_nth in_set_member)
      then obtain n where n_prop: "n < length ?l \<and> ?l ! n = y"
        by auto
      have h: "\<forall>n < length ?l. ?l ! n \<ge> ?l !0" using sorted_iff_nth_mono
        using sorted_sorted_list_of_set by blast
      then have h: "y \<ge> ?l ! 0" using n_prop by auto
      then show "x < y" using x_prop by auto
    qed
    then show ?thesis
      using finset set_sorted_list_of_set in_set_member
      by (metis (mono_tags, lifting) mem_Collect_eq)
  qed
  then obtain x where x_prop: "(\<forall>y. a*y^2 + b*y + c = 0 \<longrightarrow> x < y)" by auto
  then have same_as: "\<forall>y<x. (aEvalUni At y = aEvalUni At x)"
    using no_change_eval change_eval assms
  proof -
    have f1: "\<forall>x0. (x0 < x) = (\<not> 0 \<le> x0 + - 1 * x)"
      by auto
    have f2: "(0 \<le> - 1 * x + v0_0) = (x + - 1 * v0_0 \<le> 0)"
      by auto
    have f3: "v0_0 + - 1 * x = - 1 * x + v0_0"
      by auto
    have f4: "\<forall>x0 x1 x2 x3. (x3::real) * x0\<^sup>2 + x2 * x0 + x1 = x1 + x3 * x0\<^sup>2 + x2 * x0"
      by auto
    have f5: "\<forall>x3 x4 x5. (aEvalUni x3 x5 \<noteq> aEvalUni x3 x4) = ((\<not> aEvalUni x3 x5) = aEvalUni x3 x4)"
      by fastforce
    have f6: "\<forall>x0 x1 x2 x3 x4 x5. (x5 < x4 \<and> (\<not> aEvalUni x3 x5) = aEvalUni x3 x4 \<and> getPoly x3 = (x2, x1, x0) \<longrightarrow> (\<exists>v6\<ge>x5. v6 \<le> x4 \<and> x0 + x2 * v6\<^sup>2 + x1 * v6 = 0)) = ((\<not> x5 < x4 \<or> (\<not> aEvalUni x3 x5) \<noteq> aEvalUni x3 x4 \<or> getPoly x3 \<noteq> (x2, x1, x0)) \<or> (\<exists>v6\<ge>x5. v6 \<le> x4 \<and> x0 + x2 * v6\<^sup>2 + x1 * v6 = 0))"
      by fastforce
    have f7: "\<forall>x0 x5. ((x0::real) \<le> x5) = (x0 + - 1 * x5 \<le> 0)"
      by auto
    have f8: "\<forall>x0 x6. ((x6::real) \<le> x0) = (0 \<le> x0 + - 1 * x6)"
      by auto
    have "\<forall>x4 x5. ((x5::real) < x4) = (\<not> x4 + - 1 * x5 \<le> 0)"
      by auto
    then have "(\<forall>r ra a rb rc rd. r < ra \<and> aEvalUni a r \<noteq> aEvalUni a ra \<and> getPoly a = (rb, rc, rd) \<longrightarrow> (\<exists>re\<ge>r. re \<le> ra \<and> rb * re\<^sup>2 + rc * re + rd = 0)) = (\<forall>r ra a rb rc rd. (ra + - 1 * r \<le> 0 \<or> (\<not> aEvalUni a r) \<noteq> aEvalUni a ra \<or> getPoly a \<noteq> (rb, rc, rd)) \<or> (\<exists>re. 0 \<le> re + - 1 * r \<and> re + - 1 * ra \<le> 0 \<and> rd + rb * re\<^sup>2 + rc * re = 0))"
      using f8 f7 f6 f5 f4 by presburger
    then have f9: "\<forall>r ra a rb rc rd. (ra + - 1 * r \<le> 0 \<or> (\<not> aEvalUni a r) \<noteq> aEvalUni a ra \<or> getPoly a \<noteq> (rb, rc, rd)) \<or> (\<exists>re. 0 \<le> re + - 1 * r \<and> re + - 1 * ra \<le> 0 \<and> rd + rb * re\<^sup>2 + rc * re = 0)"
      by (meson change_eval)
    obtain rr :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where
      "\<forall>x0 x1 x2 x4 x5. (\<exists>v6. 0 \<le> v6 + - 1 * x5 \<and> v6 + - 1 * x4 \<le> 0 \<and> x0 + x2 * v6\<^sup>2 + x1 * v6 = 0) = (0 \<le> rr x0 x1 x2 x4 x5 + - 1 * x5 \<and> rr x0 x1 x2 x4 x5 + - 1 * x4 \<le> 0 \<and> x0 + x2 * (rr x0 x1 x2 x4 x5)\<^sup>2 + x1 * rr x0 x1 x2 x4 x5 = 0)"
      by moura
    then have f10: "\<forall>r ra a rb rc rd. ra + - 1 * r \<le> 0 \<or> aEvalUni a r = aEvalUni a ra \<or> getPoly a \<noteq> (rb, rc, rd) \<or> r + - 1 * rr rd rc rb ra r \<le> 0 \<and> 0 \<le> ra + - 1 * rr rd rc rb ra r \<and> rd + rb * (rr rd rc rb ra r)\<^sup>2 + rc * rr rd rc rb ra r = 0"
      using f9 by simp
    have f11: "(rr c b a x v0_0 + - 1 * x \<le> 0) = (0 \<le> x + - 1 * rr c b a x v0_0)"
      by force
    have "\<forall>x0. (x < x0) = (\<not> x0 + - 1 * x \<le> 0)"
      by auto
    then have f12: "\<forall>r. c + a * r\<^sup>2 + b * r \<noteq> 0 \<or> \<not> r + - 1 * x \<le> 0"
      using x_prop by auto
    obtain rra :: real where
      "(\<exists>v0. \<not> 0 \<le> v0 + - 1 * x \<and> aEvalUni At v0 \<noteq> aEvalUni At x) = (\<not> 0 \<le> rra + - 1 * x \<and> aEvalUni At rra \<noteq> aEvalUni At x)"
      by moura
    then show ?thesis
      using f12 f11 f10 f3 f2 f1
    proof -
      have f1: "\<forall>x0. (x0 < x) = (\<not> 0 \<le> x0 + - 1 * x)"
        by auto
      have f2: "(0 \<le> v0_0a + - 1 * x) = (x + - 1 * v0_0a \<le> 0)"
        by auto
      have f3: "(rr c b a x v0_0a + - 1 * x \<le> 0) = (0 \<le> x + - 1 * rr c b a x v0_0a)"
        by auto
      obtain rrb :: real where
        "(\<exists>v0. \<not> 0 \<le> v0 + - 1 * x \<and> aEvalUni At v0 \<noteq> aEvalUni At x) = (\<not> 0 \<le> rrb + - 1 * x \<and> aEvalUni At rrb \<noteq> aEvalUni At x)"
        by blast
      then show ?thesis
        using f3 f2 f1 assms(1) f10 f12
        by smt
    qed
  qed
  then show ?thesis by auto
qed

lemma inequality_case : "(\<exists>(x::real). \<forall>(y::real)<x. (a::real) * y\<^sup>2 + (b::real) * y + (c::real) < 0) =
    (a < 0 \<or> a = 0 \<and> (0 < b \<or> b = 0 \<and> c < 0))"
proof-
  let ?At = "(LessUni (a, b, c))"
  have firsth : "\<And>x. (\<forall>y<x. a * y\<^sup>2 + b * y + c < 0 \<Longrightarrow> a\<le>0)"
  proof -
    fix x
    assume lt: "\<forall>y<x. a * y\<^sup>2 + b * y + c < 0"
    have "\<exists>w. \<forall>y < w. y^2 > (-b/a)*y - c/a"  using ysq_dom_y_plus_coeff[where b = "-b/a", where c = "-c/a"]
      by auto
    then have gtdomhelp: "a > 0 \<Longrightarrow> \<exists>w. \<forall>y < w. a*y^2 > a*((-b/a)*y - c/a)"
      by auto
    have "\<forall>y. (a > 0 \<longrightarrow> a*((-b/a)*y - c/a) = -b*y - c)"
      by (simp add: right_diff_distrib')
    then have gtdom: "a > 0 \<Longrightarrow> \<exists>w.\<forall>y < w. a*y^2 > -b*y - c"
      using gtdomhelp
      by simp
    then have " a > 0 \<Longrightarrow> False"
    proof -
      assume "a > 0"
      then have "\<exists>w.\<forall>y < w. a*y^2 > -b*y - c" using gtdom by auto
      then obtain w where w_prop: "\<forall>y < w. a*y^2 + b*y + c > 0"
        by fastforce
      let ?mn = "min w x - 1"
      have gtz: "a*?mn^2 + b*?mn + c > 0" using w_prop
        by auto
      have ltz: "a*?mn^2 + b*?mn + c < 0" using lt by auto
      then show "False" using gtz ltz by auto
    qed
    then show "a \<le> 0"
      by fastforce
  qed
  have bleq0 : "\<And>x. (\<forall>y<x. b * y + c < 0 \<Longrightarrow> b\<ge>0)"
  proof -
    fix x
    assume lt: "\<forall>y<x. b * y + c < 0"
    have gtdom: "b < 0 \<Longrightarrow> \<exists>w.\<forall>y < w. b*y > - c"
      by (metis mult.commute neg_less_divide_eq)
    then have "b < 0 \<Longrightarrow> False"
    proof -
      assume "b < 0"
      then have "\<exists>w.\<forall>y < w. b*y > - c" using gtdom by auto
      then obtain w where w_prop: "\<forall>y < w .b*y + c > 0"
        by fastforce
      let ?mn = "min w x - 1"
      have gtz: "b*?mn + c > 0" using w_prop
        by auto
      have ltz: "b*?mn + c < 0" using lt by auto
      then show "False" using gtz ltz by auto
    qed
    then show "b \<ge> 0"
      by fastforce
  qed
  have secondh: "\<And>x. (\<forall>y<x. a * y\<^sup>2 + b * y + c < 0 \<Longrightarrow> \<not> a < 0 \<Longrightarrow> \<not> 0 < b \<Longrightarrow> b = 0)"
    using firsth bleq0
    by (metis add.commute add.right_neutral less_eq_real_def mult_zero_class.mult_zero_left)
  have thirdh : "\<And>x. \<forall>y<x. a * y\<^sup>2 + b * y + c < 0 \<Longrightarrow> \<not> a < 0 \<Longrightarrow> \<not> 0 < b \<Longrightarrow> c < 0"
    using firsth secondh add.commute add.right_neutral infzeros mult_zero_class.mult_zero_left not_numeral_le_zero order_refl
    by (metis less_eq_real_def)
  have fourthh : "a < 0 \<Longrightarrow> \<exists>x. \<forall>y<x. a * y\<^sup>2 + b * y + c < 0"
  proof -
    assume aleq: "a < 0"
    have "\<exists>(w::real). \<forall>(y::real). (y < w \<longrightarrow> y^2 > (-b/a)*y + (-c/a))"
      using ysq_dom_y_plus_coeff[where b = "-b/a", where c = "-c/a"]
      by blast
    then have hyp:"\<exists>(w::real). \<forall>(y::real). (y < w \<longrightarrow> a*y^2 \<le> a*(-b/a)*y + a*(-c/a))"
      by (metis (no_types, opaque_lifting) \<open>a < 0\<close> distrib_left less_eq_real_def linorder_not_le mult.assoc mult_less_cancel_left)
    have "\<forall>y. a*(-b/a)*y + a*(-c/a) = -b*y -c"
      using \<open>a < 0\<close> by auto
    then have "\<exists>(w::real). \<forall>(y::real). (y < w \<longrightarrow> a*y^2 \<le> -b*y - c)"
      using hyp by auto
    then have "\<exists>(w::real). \<forall>(y::real). (y < w \<longrightarrow> a*y^2 + b*y + c \<le> 0)"
      by (metis add.commute add_uminus_conv_diff le_diff_eq mult_minus_left real_add_le_0_iff)
    then obtain w where w_prop: "\<forall>(y::real). (y < w \<longrightarrow> a*y^2 + b*y + c \<le> 0)" by auto
    have "\<exists>x. \<forall>y < x. aEvalUni ?At x = aEvalUni ?At y" using same_eval''
    proof -
      have f1: "\<forall>x0 x1. ((x0::real) < x1) = (\<not> 0 \<le> x0 + - 1 * x1)"
        by linarith
      have "a \<noteq> 0"
        using \<open>a < 0\<close> by force
      then obtain rr :: "atomUni \<Rightarrow> real" where
        "\<forall>r. 0 \<le> r + - 1 * rr (LessUni (a, b, c)) \<or> aEvalUni (LessUni (a, b, c)) r = aEvalUni (LessUni (a, b, c)) (rr (LessUni (a, b, c)))"
        using f1 by (metis getPoly.simps(4) same_eval'')
      then show ?thesis
        using f1 by meson
    qed
    then obtain x where x_prop: "\<forall>y < x. aEvalUni ?At x = aEvalUni ?At y" by auto
    let ?mn = "min x w - 1"
    have "\<forall>y < ?mn.  aEvalUni ?At y = True \<or> aEvalUni ?At y = False"
      using x_prop by auto
    have "\<forall> y < ?mn. aEvalUni ?At y = False \<longrightarrow> a*y^2 + b*y + c \<ge> 0"
      by auto
    then have "\<And>y. \<forall>y<w. a * y\<^sup>2 + b * y + c \<le> 0 \<Longrightarrow>
         y < min x w - 1 \<Longrightarrow>
         \<not> a * y\<^sup>2 + b * y + c < 0 \<Longrightarrow>
         a * y\<^sup>2 + b * y + c = 0"
    proof -
      fix y :: real
      assume a1: "y < min x w - 1"
      assume a2: "\<not> a * y\<^sup>2 + b * y + c < 0"
      assume a3: "\<forall>y<w. a * y\<^sup>2 + b * y + c \<le> 0"
      have "y < w"
        using a1 by linarith
      then show "a * y\<^sup>2 + b * y + c = 0"
        using a3 a2 less_eq_real_def by blast
    qed
    then have "\<forall> y < ?mn. aEvalUni ?At y = False \<longrightarrow> a*y^2 + b*y + c = 0"
      using w_prop by auto
    then have "\<forall> y < ?mn. aEvalUni ?At y = False \<Longrightarrow> False" using infzeros aleq
      by (metis power_zero_numeral zero_less_power2)
    then have "\<forall> y < ?mn. aEvalUni ?At y = True"
    proof -
      { fix rr :: real
        have "\<forall>r ra. (ra::real) < r \<or> \<not> ra < r + - 1"
          by linarith
        then have "\<not> rr < min x w - 1 \<or> aEvalUni (LessUni (a, b, c)) rr"
          by (metis (no_types) \<open>\<forall>y<min x w - 1. aEvalUni (LessUni (a, b, c)) y = False \<Longrightarrow> False\<close> ab_group_add_class.ab_diff_conv_add_uminus less_eq_real_def min_less_iff_disj not_le x_prop) }
      then show ?thesis
        by blast
    qed
    then show ?thesis by auto
  qed
  have fifthh : "b > 0 \<Longrightarrow> \<exists>x. \<forall>y<x. b * y + c < 0"
  proof-
    assume bh : "b > 0"
    show "\<exists>x. \<forall>y<x. b * y + c < 0"
      apply(rule exI[where x="-c/b"])
      apply auto
      using bh
      by (simp add: mult.commute pos_less_minus_divide_eq)
  qed
  show ?thesis
    apply(auto)
    using firsth apply simp
    using secondh apply simp
    using thirdh apply simp
    using fourthh apply simp
    using fifthh by simp
qed

lemma inequality_case_geq : "(\<exists>(x::real). \<forall>(y::real)<x. (a::real) * y\<^sup>2 + (b::real) * y + (c::real) > 0) =
    (a > 0 \<or> a = 0 \<and> (0 > b \<or> b = 0 \<and> c > 0))"
proof -
  have s1: "\<forall>y. - 1 * a * y\<^sup>2 + - 1 * b * y + - 1 * c < 0 \<longleftrightarrow>  a * y\<^sup>2 +  b * y +  c > 0"
    by auto
  have s2: "(- 1 * a < 0 \<or> - 1 * a = 0 \<and> (0 < - 1 * b \<or> - 1 * b = 0 \<and> - 1 * c < 0)) \<longleftrightarrow>
   (a > 0 \<or> a = 0 \<and> (0 > b \<or>  b = 0 \<and> c > 0))  "
    by auto
  have "(\<exists>x. \<forall>y<x. - 1 * a * y\<^sup>2 + - 1 * b * y + - 1 * c < 0) =
  (- 1 * a < 0 \<or> - 1 * a = 0 \<and> (0 < - 1 * b \<or> - 1 * b = 0 \<and> - 1 * c < 0))"
    using inequality_case[where a = "-1*a", where b = "-1*b", where c= "-1*c"]
    by auto
  then show ?thesis
    using s1 s2 by auto
qed

lemma infinity_evalUni_LessUni : "(\<exists>x. \<forall>y<x. aEvalUni (LessUni p) y) = (evalUni (substNegInfinityUni (LessUni p)) x)"
proof(cases p)
  case (fields a b c)
  show ?thesis
    unfolding fields  apply simp
    using inequality_case[of a b c] .
qed

lemma infinity_evalUni_EqUni : "(\<exists>x. \<forall>y<x. aEvalUni (EqUni p) y) = (evalUni (substNegInfinityUni (EqUni p)) x)"
proof(cases p)
  case (fields a b c)
  show ?thesis
    using infzeros[of _ a b c] by(auto simp add: fields)
qed

lemma infinity_evalUni_NeqUni : "(\<exists>x. \<forall>y<x. aEvalUni (NeqUni p) y) = (evalUni (substNegInfinityUni (NeqUni p)) x)"
proof(cases p)
  case (fields a b c)
  show ?thesis
    unfolding fields  apply simp
    using inequality_case[of a b c]
    using inequality_case_geq[of a b c]
    by (metis less_numeral_extra(3) linorder_neqE_linordered_idom mult_eq_0_iff)

qed

lemma infinity_evalUni_LeqUni : "(\<exists>x. \<forall>y<x. aEvalUni (LeqUni p) y) = (evalUni (substNegInfinityUni (LeqUni p)) x)"
proof(cases p)
  case (fields a b c)
  show ?thesis
    unfolding fields  apply simp
  proof -
    have h1: "((\<exists>x. \<forall>y<x. a * y\<^sup>2 + b * y + c < 0) \<or> (\<exists>x. \<forall>y<x. a * y\<^sup>2 + b * y + c = 0)) \<longrightarrow> (\<exists>x. \<forall>y<x. a * y\<^sup>2 + b * y + c \<le> 0)"
      using less_eq_real_def
      by auto
    have h2: "(\<exists>x. \<forall>y<x. a * y\<^sup>2 + b * y + c \<le> 0) \<Longrightarrow> ((\<exists>x. \<forall>y<x. a * y\<^sup>2 + b * y + c < 0) \<or> (\<exists>x. \<forall>y<x. a * y\<^sup>2 + b * y + c = 0))"
    proof -
      assume a1: "(\<exists>x. \<forall>y<x. a * y\<^sup>2 + b * y + c \<le> 0)"
      have "\<not>(\<exists>x. \<forall>y<x. a * y\<^sup>2 + b * y + c = 0) \<Longrightarrow> (\<exists>x. \<forall>y<x. a * y\<^sup>2 + b * y + c < 0) "
      proof -
        assume a2: "\<not>(\<exists>x. \<forall>y<x. a * y\<^sup>2 + b * y + c = 0)"
        then have "a \<noteq> 0 \<or> b \<noteq> 0 \<or> c \<noteq> 0" by auto
        then have "(a < 0 \<or> a = 0 \<and> (0 < b \<or> b = 0 \<and> c < 0))"
        proof -
          have x1: "a > 0 \<Longrightarrow> False"
          proof -
            assume "a > 0"
            then have "(\<exists>(x::real). \<forall>(y::real)<x. (a::real) * y\<^sup>2 + (b::real) * y + (c::real) > 0)" using inequality_case_geq
              by auto
            then  show ?thesis
              using a1
              by (meson a2 linorder_not_le min_less_iff_conj)
          qed
          then have x2: "a = 0 \<and> 0 > b \<Longrightarrow> False"
          proof -
            assume "a = 0 \<and> 0 > b"
            then have "(\<exists>(x::real). \<forall>(y::real)<x. (a::real) * y\<^sup>2 + (b::real) * y + (c::real) > 0)" using inequality_case_geq
              by blast
            then show ?thesis
              using a1
              by (meson a2 linorder_not_le min_less_iff_conj)
          qed
          then have x3: "a = 0 \<and> b = 0 \<and> c > 0 \<Longrightarrow> False "
            using a1 a2 by auto
          show ?thesis using x1 x2 x3
            by (meson \<open>a \<noteq> 0 \<or> b \<noteq> 0 \<or> c \<noteq> 0\<close> linorder_neqE_linordered_idom)
        qed
        then show "(\<exists>x. \<forall>y<x. a * y\<^sup>2 + b * y + c < 0)" using inequality_case
          by auto
      qed
      then show ?thesis
        by auto
    qed
    have "(\<exists>x. \<forall>y<x. a * y\<^sup>2 + b * y + c \<le> 0) = (\<exists>x. \<forall>y<x. a * y\<^sup>2 + b * y + c < 0) \<or> (\<exists>x. \<forall>y<x. a * y\<^sup>2 + b * y + c = 0)"
      using h1 h2 by auto
    then show "(\<exists>x. \<forall>y<x. a * y\<^sup>2 + b * y + c \<le> 0) =
    (a < 0 \<or> a = 0 \<and> (0 < b \<or> b = 0 \<and> c < 0) \<or> a = 0 \<and> b = 0 \<and> c = 0)"
      using inequality_case[of a b c] infzeros[of _ a b c] by auto
  qed
qed

text "This is the vertical translation for substNegInfinityUni where we represent the virtual
substution of negative infinity in the univariate case"
lemma infinity_evalUni :
  shows "(\<exists>x. \<forall>y<x. aEvalUni At y) = (evalUni (substNegInfinityUni At) x)"
proof(cases At)
  case (LessUni p)
  then show ?thesis using infinity_evalUni_LessUni by auto
next
  case (EqUni p)
  then show ?thesis using infinity_evalUni_EqUni by auto
next
  case (LeqUni p)
  then show ?thesis using infinity_evalUni_LeqUni by auto
next
  case (NeqUni p)
  then show ?thesis using infinity_evalUni_NeqUni by auto
qed

end

subset_name: curated


TITLE: A sequence modified from the Catalan recurrence and $2$-adic valuations
QUESTION [3 upvotes]: Earlier, I posted this MO question to which Max Alekseyev found counter-examples. I realized that there was some error in my computational programming with Maple. Oh, well $\dots$ I have scaled down the problem.
Recall: Let $\nu_2(x)$ denote the $2$-adic valuation of $x$ and $s(x)$ stand for the number of $1$’s in the $2$-ary (binary) expansion of $x$.
Consider the sequence $w_0=1$ and $w_{n+1}=\sum_{i=0}^nw_i^2w_{n-i}^2$.

QUESTION. Is the following true?
If $C_n=\frac1{n+1}\binom{2n}n$, then $\nu_2(w_n)=(C_n\mod2)+2s(n+1)-3$.
Equivalently,
$$\nu_2(w_n)=\begin{cases} 2s(n+1)-2 \qquad\text{if $n=2^k-1$} \\ 2s(n+1)-3 \qquad\text{otherwise}. \end{cases}$$

REPLY [2 votes]: This is still not true. The smallest counterexample is given by $n=30$ with $\nu_2(w_{30}) = 10$ and $2s(31)-3=7$. This can be easily verified by computing $w_n$ modulo $2^{11}$.