text:
\subsection{Experiments}

To investigate the robustness and scalability of our methodology, we conducted a series of numerical experiments based on a collection of test cases from MATPOWER \citep{Zimmerman2011a} (which includes a number of test cases from \citep{josz2016}) and Power Grid Lib \citep{Pglib} with as many as $n= 70,\!000$ power buses; we have also included a synthetic case of the continental USA from the Electric Grid Test Case Repository \citep{Birchfield:2018} with $n= 82,\!000$ power buses. We excluded cases that are infeasible and cases with generator cost functions that are neither quadratic nor linear. For each test case, we set up a CLP formulation of the SDR and solved it using five different CLP solvers: MOSEK 8.1 \citep{mosek}, SeDuMi 1.3 \citep{Sturm1999}, SDPT3 4.0 \citep{sdpt3}, SCS 1.2.7 \citep{ocpb:16}, and CDCS 1.1 \citep{CDCS}. MOSEK, SeDuMi, and SDPT3 are interior-point methods whereas SCS and CDCS are first-order methods based on the alternating direction method of multipliers (ADMM).

To compare our methodology to an approach based on a modeling tool, we used SDPOPF \citep{Molzahn2013} from ``MATPOWER Extras'' to set up and solve an SDR of each case. SDPOPF uses YALMIP \citep{Lofberg2004} to set up the problem which is then solved numerically using one of several possible solvers: we used MOSEK in order to facilitate a fair comparison. Finally, to compare our approach to a nonlinear optimization approach, we used MATPOWER to set up and solve each case  with three different interior-point methods for nonlinear optimization: MIPS \citep{WMSZ+:07} from MATPOWER 6.1, IPOPT 3.12.9 \citep{Wachter2006} with PARDISO 6.0 \citep{Kourounis:2018}, and KNITRO 10.3.1 \citep{byrd2006}. These are all called via MATPOWER using its default initialization---the default is sometimes referred to as ``flat start'' since all voltages are set to 1 p.u. and the active power generation is set to the midpoint of its bounds. When successful, these solvers return a locally optimal solution that provides an upper bound on the optimal value in contrast to the SDR that provides a lower bound.

\subsection{Setup}
Using the implementation described in section \ref{implementation}, we processed the problem data before setting up the SDRs. Specifically, we truncated generator bounds larger than 50 times the base MVA.
We remark that SDPOPF enforces a minimum transmission line resistance of $10^{-4}$; in the experiments, we do not enforce a minimum resistance in our SDR.

All experiments but those involving KNITRO were conducted on an HPC node with two Intel XeonE5-2650v4 processors (a total of 24 cores) and 240 GB memory. All experiments with KNITRO were conducted on different hardware (2.5 GHz Intel Core i5 CPU, 8 GB of memory) because of license restrictions. As a result, the KNITRO computation times that we report cannot be compared directly to those reported for the other solvers. All MATLAB-based solvers were used with MATLAB R2017b, and MOSEK was called through its Python interface in Python 3.6.3.  Finally, we modified the default solver options as follows: for SeDuMi, we raised the maximum number of iterations from 150 to 250; for SCS and CDCS, we limited the number of iterations to 20,000; for CDCS, we disabled ``chordalize'' and used the ``primal" solver since this allowed us to solve the most cases; for SCS, we used the direct solver; for SDPT3 we used a value of 400 for ``smallblockdim'' and changed the maximum number of iterations from 100 to 250.

\subsection{Robustness}
We start with an investigation of robustness. Table \ref{tab:status} contains a summary of return statuses for the different solvers for a total of 159 test cases. The column labeled ``success" refers to return values that indicate successful termination with an optimal or near optimal (global or local) solution. The ``failure'' column refers to return values that indicate some kind of error.
\begin{table}
	\centering

	\caption{Summary of return statuses by solver.}
	\label{tab:status}
	\input{files/returnTabular.txt}
\end{table}

We remark that SDPOPF ignores phase angle constraints and fails in 31 cases because of a MATPOWER error; the solver is never called in these cases.

The results in Table \ref{tab:status} clearly demonstrate that the SDRs can be solved reliably using MOSEK: all cases were solved to optimality with MOSEK's default tolerances. In contrast, the nonlinear solvers IPOPT and KNITRO only succeed in roughly 85\% of the cases while MIPS succeeds in approximately 75\% of the cases.
Note also that although CDCS solves all but one case, the accuracy and speed is poor compared to MOSEK as we show later in this section.
Both SeDuMi and SCS succeed in less than 50\% of the cases.

\subsection{Accuracy}
We now compare the solutions returned by the five CLP solvers. Since the solvers have different tolerances (\ie, stopping criteria), we will compare the solvers based on the so-called ``DIMACS error measures" described in \citep{Mittelmann2003}. Roughly speaking, these are five relative error measures quantifying the primal residual norm, primal cone violation, dual residual norm, dual cone violation, and duality gap.
Fig.~\ref{fig:dimacsbox} summarizes the results in a box plot of the DIMACS measures for each solver (the smaller the error, the better).

\begin{figure*}

	\subfloat[MOSEK]{
		\includegraphics[trim={{\myLeftTrim} {\myBotTrim} {\myRightTrim} {\myTopTrim}},clip=true,width=.48\linewidth]{figs/mosek_box.pdf}
		\label{fig:dimacsbox:mosek}
		}\hfill
	\subfloat[CDCS]{
		\includegraphics[trim={{\myLeftTrim} {\myBotTrim} {\myRightTrim} {\myTopTrim}},clip=true,width=.48\linewidth]{figs/cdcs_box.pdf}
		\label{fig:dimacsbox:cdcs}
		} \\[-1em]
	\subfloat[SeDuMi]{
		\includegraphics[trim={{\myLeftTrim} {\myBotTrim} {\myRightTrim} {\myTopTrim}},clip=true,width=.48\linewidth]{figs/sedumi_box.pdf}
		\label{fig:dimacsbox:sedumi}
		}\hfill
	\subfloat[SCS]{
		\includegraphics[trim={{\myLeftTrim} {\myBotTrim} {\myRightTrim} {\myTopTrim}},clip=true,width=.48\linewidth]{figs/scs_box.pdf}
		\label{fig:dimacsbox:scs}
		}\\[-1em]
	\subfloat[SDPT3]{
		\includegraphics[trim={{\myLeftTrim} {\myBotTrim} {\myRightTrim} {\myTopTrim}},clip=true,width=.48\linewidth]{figs/sdpt3_box.pdf}
		\label{fig:dimacsbox:sdpt3}
	}
	\caption{Box plots of logarithm of DIMACS errors. The red markers correspond to cases where the solver did not succeed. We note that in order to accommodate a logarithmic axis, we have replaced errors below $10^{-16}$ by this value.}
	\label{fig:dimacsbox}
\end{figure*}

MOSEK, shown in Fig.~\ref{fig:dimacsbox:mosek}, generally performs well with DIMACS errors below $10^{-7}$ in all cases.
The SeDuMi errors, shown in Fig.~\ref{fig:dimacsbox:sedumi}, reveal that SeDuMi returns a high-accuracy solution whenever it succeeds; the same is true for SDPT3, shown in Fig.~\ref{fig:dimacsbox:sdpt3}. This suggests that the default tolerances may be too strict for all but the small cases.
Both CDCS and SCS generally return solutions with larger errors, as shown in Fig.~\ref{fig:dimacsbox:cdcs} and \ref{fig:dimacsbox:scs}. This is to be expected since they are both first-order methods. While CDCS is relatively robust, it often terminates with sizable dual residuals which are indicative of low-accuracy solutions.

\subsection{Optimality Gap}
Next we investigate the objective values provided by the solvers. We limit our attention to MOSEK and the nonlinear solvers IPOPT, MIPS, and KNITRO. The nonlinear solvers provide an upper bound when they terminate at a feasible point. We define the best upper bound as
\begin{equation}
    \overline{f} = \min(f_{\text{IPOPT}},f_{\text{KNITRO}},f_{\text{MIPS}}),
\end{equation}
\ie, the minimum of the objective values provided by the three solvers (if a solver does not succeed, we define its objective value to be $\infty$).
Similarly, the SDR (MOSEK) provides a lower bound which we denote by $ \underline{f} = f_{\text{MOSEK}}$. The optimality gap may then be defined as
\begin{equation}
	\mathrm{gap} = \frac{\overline{f} - \underline{f}}{\overline{f}} \cdot 100\%.
\end{equation}
The gap is equal to $0$ if $ \underline{f} = \overline{f} $, implying that we have a globally optimal solution. On the other hand, if the gap is large, $ \overline{f} $ may be a poor local minimum and/or the SDR provides a weak lower bound $\underline{f}$.

We have made four tables listing objective values and optimality gap for all cases with more than 300 buses based on their origin:
table \ref{tab:cases_matpower} contains cases from the MATPOWER library;
table \ref{tab:cases_pglib} contains cases from PGLIB in typical operating conditions;
table \ref{tab:cases_pglib_sad} contains cases from PGLIB with small phase angle difference constraints;
table \ref{tab:cases_pglib_api} contains cases from PGLIB with binding thermal limit constraints.
The cases are sorted by the number of buses in ascending order. Note that the optimality gap is undefined if none of the nonlinear solvers succeed.
The optimality gap is close to zero in many cases and below 1\% in all but a handful of cases.

\subsection{Scalability}
We end this section by comparing the time required by each solver to solve the test cases. Fig.~\ref{fig:timescat} shows the time used by the SDP solvers compared to the number of buses in the case. To make a fair comparison, we report computation times without preprocessing, \ie, only the time required by the actual solver is recorded (we briefly discuss some considerations related to preprocessing in Section \ref{sec:discussion}).
\begin{figure}
	\centering
	\includegraphics[width=0.9\columnwidth]{figs/timescatter.pdf}
	\caption{Scatter plot of the time used by the SDP solvers against the number of buses for successful cases. Note that SDPOPF solves an equivalent but different SDR.}
	\label{fig:timescat}
\end{figure}

MOSEK is generally the fastest.

The difference between MOSEK and SDPOPF (which also uses MOSEK, but based on the problem formulation compiled by YALMIP) highlights that the formulation of the SDR may have a significant impact on the computation time as well as robustness.
The striking difference between MOSEK and CDCS, both in terms of computation time and accuracy, makes it hard to justify the use of first-order methods for highly sparse problems like these.

In addition to cost function value and optimality gap, tables \ref{tab:cases_matpower}--\ref{tab:cases_pglib_api} list the computation times (excluding preprocessing) for MOSEK and the three solvers IPOPT, KNITRO, and MIPS.

MOSEK solves the SDR of all but one case with less than 25,000 buses in less than 10 minutes; the only exception is the case 4661\_sdet from PGLIB (all three operating conditions). Solving this problem takes MOSEK around 80 minutes. The longer computation time required to solve this case compared to other cases with a similar number of buses can in part be explain by looking at the chordal embedding of the network graph. The largest clique is of size 242 which is similar to the case with 82,000 buses (238) and around three times the size of all other cases with less than 25,000 buses. The case with 25,000 power buses is solved in approximately an hour by MOSEK, and the largest cases with 70,000 and 82,000 buses are solved in around seven hours. The nonlinear solvers are typically 5-20 times faster than MOSEK (they solve a different problem!), but they sometimes fail. The RTE cases from PGLIB appear to be particularly difficult for the nonlinear solvers: in some cases, none of the nonlinear solvers succeed, and the computation times are occasionally large compared to the general trend.

\input{files/table_matpower.tex}
\input{files/table_pglib.tex}
\input{files/table_pglib_sad.tex}
\input{files/table_pglib_api.tex}

\iffalse
In Table \ref{tab:smallcases}, we see the results for the small-scale cases.
All cases are solved in less than 3 seconds by MOSEK and the optimality gap is generally small.
All cases except two (with binding thermal limits) are solved by IPOPT and the time used is generally less than MOSEK.

In Table \ref{tab:mediumcases}, we see the results for the medium-scale cases.
All cases are solved by MOSEK in less than 2 minutes.
IPOPT fails for cases from all libraries but it is fast for the cases that it does solve using less than 10 seconds for most cases; there are some (rte) cases where IPOPT uses more time than MOSEK.
The optimality gap is small (less than 1\%) for all cases except a few.

In Table \ref{tab:largecases}, we see the results for the large-scale cases.
Again MOSEK solves all cases and the time used is roughly 10 minutes for the largest case (scaling the cases the maximum time use by MOSEK was 3.5 minutes).
IPOPT solves around half the cases and the time used varies from very fast (less than 5 seconds) to immensely slow (more than 10 hours in the extreme).
The optimality gap is less than $ 1.5\% $ for all solved cases.
\fi


TITLE: Finding all entire functions satisfying $\text{Re}(g(z))+2\text{Re}(z)=\text{Im}(g(z))$
QUESTION [2 upvotes]: I have been asked to...

Find all entire functions $g$ such that $\forall z\in\mathbb{C}$ we have $\text{Re}(g(z))+2\text{Re}(z)=\text{Im}(g(z))$ satisfied.

Now, since $g$ is entire, it has to satisfy the Cauchy-Riemann equations on all of $\mathbb{C}$. Also, writing $g(z)=u(x,y)+iv(x,y)$, with $x\equiv \text{Re}(z)$ and $y\equiv \text{Im}(z)$, for some real functions $u$ and $v$, we find that
\begin{align}
u(x,y) + 2x = v(x,y),
\end{align}
and thus that
\begin{align}
\frac{\partial v}{\partial x} = \frac{\partial}{\partial x}\bigg[ u(x,y) +2x \bigg] = \frac{\partial u}{\partial x} + 2.
\end{align}
Applying the Cauchy-Riemann equations, we find
\begin{align}
\frac{\partial v}{\partial x} =-\frac{\partial u}{\partial y} &= \frac{\partial u}{\partial x} + 2  \\
\Rightarrow \frac{\partial u}{\partial x} + \frac{\partial u}{\partial y} &= -2.
\end{align}
This, however, doesnt really seem to help a lot. I am unsure how to proceed. Any hints would be appreciated!

REPLY [2 votes]: Using $\text{Im}(w) = -\text{Re}(iw)$, your condition is equivalent to
$$
    \text{Re}(g(z))+2\text{Re}(z) = \text{Re}(ig(z))
$$
or
$$
   \text{Re}\bigl(g(z) + 2z + ig(z)\bigr) = 0 \, .
$$
A holomorphic function in a domain is uniquely determined by its real part
up to a constant, this can easily be seen by applying the Cauchy-Riemann
equations to $h(z) := g(z) + 2z + ig(z)$.
Therefore
$$
    g(z) + 2z + ig(z) = iC \quad \text{for some } C \in \mathbb R \, .
$$
Solving this for $g$ gives
$$
   g(z) = (-1+i)z + \frac12 (1+i)C
$$
or
$$
   g(z) = (-1+i)z + (1+i)D \quad\text{for some } D \in \mathbb R \, .
$$

REPLY [1 votes]: Differentiating your first line with respect to y gives:
$${\partial u\over\partial y}={\partial v\over\partial y}={\partial u\over\partial x}$$.
The last equation follows from the Cauchy-Riemann equations. Should be easy now by combining with your result.


TITLE: Discrete derivative condition for martingale?
QUESTION [1 upvotes]: For a simple symmetric random walk $S_n$, the process $f(S_n)$ is a martingale if and only if
$$D^2 f = f(x+1) - 2f(x) + f(x-1) = 0.$$
Where this condition comes from I have no idea. I have never seen this anywhere and cannot find it anywhere. That being said, I need to find a condition for some function $f(n, S_n)$ using this fact and then prove that $Y_n = \rho ^ {-n} e^{S_n}$ is a martingale where
$$\rho = \frac{e + e^{-1}}{2}.$$
Now, I have been looking at this problem for days and have no idea how to do it. I think we can write $f(n,S_n)$ as
$$f(n, S_n) = g(n)f(S_n).$$ Then we have that $g(n) D^2 f = 0$, so $g(n)$ can be anything at all. Obviously this is not true.
I truly have no idea. Any help is appreciated.

REPLY [2 votes]: The $D^2f = 0$ condition can be rewritten as $f(x) = \frac 12 (f(x+1)+f(x-1))$.  We compute \begin{align*}
\mathbb{E}[f(S_{n+1})|S_n] = \mathbb{E}[f(S_n + X_n) | S_n] = \frac 12 f(S_n + 1) + \frac 12 f(S_n-1),
\end{align*}
so we can see that the martingale condition $\mathbb{E}[f(S_{n+1})|S_n] = f(S_n)$ is equivalent to the $D^2f=0$ condition.
Do you see how to apply a similar method to find a condition for $f(n,S_n)$ to be a martingale?


TITLE: Is there a (introductory) differential equations books from the infinitesimal perspective?
QUESTION [6 upvotes]: I am aware that there are books treating calculus solely from the infinitesimal perpective.  Are there books doing the same for ordinary/partial differential equations?  I would be interested in introductory to advanced books - if such books exist.

REPLY [1 votes]: Keisler's Foundations of Infinitesimal Calculus has a chapter (chapter 14) on differential equations, at http://www.math.wisc.edu/~keisler/foundations.html


TITLE: Formal definition of limits (operator?)
QUESTION [0 upvotes]: I am still quite new to high level maths and I am interested in how the limit is actually defined. Could it be an operation, like this: $$\lim_{x\to \infty} : f\to\mathbb{R}^{n-1}\ , \ \textrm{with}\ f:\mathbb{R}^n\to\mathbb{R}^m\ \textrm{and}\ x\in\mathbb{R},\ n,m\in\mathbb{N}$$
Thanks in advance for the help :)

REPLY [0 votes]: You can put: $$\lim_{{\bf x}\to \infty}:\{f: \Bbb R^n \to \Bbb R^m \mid \exists\,\lim_{{\bf x}\to +\infty}f({\bf x})   \} \to \Bbb R^m \\ f \mapsto \left(\lim_{{\bf x}\to \infty}\right)(f):= \lim_{{\bf x}\to\infty}f({\bf x}),$$ where $\lim_{{\bf x}\to\infty}f({\bf x}) = L$ if: $$\forall\,\epsilon > 0,~\exists\, M > 0\,:\, \|{\bf x}\| > M \implies \|f({\bf x})-L\|<\epsilon.$$
Writing $f$ as the domain of $\lim_{{\bf x}\to \infty}$ is not good - $f$ is the object that you want to apply $\lim_{{\bf x}\to \infty}$ on, not its domain.


TITLE: The $\mathbb{N}_0 \to \mathbb{N}_0$ function that returns $n$ consecutive integers, skips $m$ consecutive integers, returns $n$... ad infinitum?
QUESTION [1 upvotes]: What is the $\mathbb{N}_0 \to \mathbb{N}_0$ function which returns $n$ consecutive integers, skips $m$ consecutive integers, returns $n$ consecutive integers again, and so on, repeating, ad infinitum?
Motivation: I was studying multiplication series and got curious when I found examples of this pattern. I found one such case when looking at the even multiples of $6$, e.g $\sum_{i=0}^\infty 6\cdot 2i$. The number on the $10$s place in the answer increment with $n=5$ and $m=1$.
$$
\begin{array}
\text{x} & \text{f(x)}\\
\hline
0 & 0 \\
1 & 1 \\
2 & 2 \\
3 & 3 \\
4 & 4 \\
5 & 6 \\
6 & 7 \\
7 & 8 \\
8 & 9 \\
9 & 10 \\
10 & 12 \\
\end{array}
$$

REPLY [1 votes]: If you're looking for a formula for such a function, it is not hard to see that one is given by
$$f_{n,m}(x) := x + m \lfloor x/n \rfloor,$$
where $\lfloor\cdot\rfloor$ is the floor function (for $x\ge 0$, $\lfloor x/n \rfloor$ is the same as integer division in many programming languages).  The factor $\lfloor x/n \rfloor$ counts which "bracket" the input $x$ falls into (in your example the numbers 0–4 fall into the 0th bracket, the numbers 5–9 fall into the 1st, etc.).


TITLE: Impossibility of making an "If and only if statement" stronger?
QUESTION [2 upvotes]: Is it impossible to prove a stronger version of an "if an only if" result?
It seems to me that the answer would be "no" because to strengthen "$A$ iff $B$" I would need to either weaken $A$ or $B$. Suppose I weaken $A$ (so $A$ no longer holds but some condition implied by $A$ holds). Then $B$ cannot hold since $A$ is necessary for $B$ (i.e. $B\implies A$, so $\text{not } A\implies\text{not }B$).
So basically, if there is an "if and only if" result, in order to improve upon it would both $A$ and $B$ need to be weakened?
Thanks

REPLY [0 votes]: In practice, the way to "strenghten" an equivalence is often the following: Suppose we proved
$$
A \iff B.
$$
Now it's often the case that this equivalence is a 'corollary' of a more general result that we later discover. I.e. there are statements $A^-, B^-$ for which we can prove
$$
A^- \iff B^-
$$
and for which we (usually for trivial reasons) have
$$
A \wedge B^-  \implies B \text{ and } B \wedge A^- \implies A.
$$
In this case the proof of $A^- \iff B^-$ can be viewed as a strengthening of the previous result that $A \iff B$.
The way this usually goes is that $A,B$ are 'global' statements and $A^-, B^-$ are 'localized' version of this. (This came up recently in a discussion about strong cardinals but I don't think that going into details will be very helpful to this thread.)


TITLE: An exercise in Treves related to Cauchy-Riemann operator
QUESTION [1 upvotes]: This is part of the exercise 5.10 from the book "basic linear partial differential equations" by  Treves:
" Let $P(z)$ be a polynomial in one variable, with complex coefficients. Describe all solutions in $\mathbb{R^2}$ of the partial differential equation
  $P(\frac{\partial}{\partial \bar{z}})h=0$. "
I tried a lot of methods end up being messed up. For example, it is natural to write $h=u+iv$ and $P(z)=R(z)+iT(z)$, where u,v are real valued functions and R, T are polynomials with real coefficients. Therefore we have
$R(\frac{\partial}{\partial \bar{z}})u-T(\frac{\partial}{\partial \bar{z}})v=0$
, and $T(\frac{\partial}{\partial \bar{z}})u+R(\frac{\partial}{\partial \bar{z}})v=0$. But unfortunately, I got stuck here.  I also tried using change of variables, but I found it was impossible to derive the desired form. I also carefully read the textbook, but I didn't get any hint. Actually, I don't feel good in doing this question, because I don't have much background in solving specific ODEs.
Could anyone give me some help? I would really appreciate it.

REPLY [1 votes]: I'll try to take a stab at this.  Analogously to the situation with ODEs, suppose $P(z)$ is a polynomial with distinct roots $r_1, \dots, r_n$.  Then
$$e^{r_1 \bar{z}}, \dots, e^{r_n \bar{z}}$$
should each be solutions to the equation $P(\frac{\partial}{\partial \bar{z}})h=0$.  Indeed, they would make up a fundamental solution set, and the general solution should be:
$$h(z,\bar{z}) = h_1(z)e^{r_1 \bar{z}} + \cdots+ h_n(z)e^{r_1 \bar{z}},$$
where $h_1, \dots, h_n$ are entire functions.
If we have roots of $P(z)$ with multiplicity, I suppose we must modify our fundamental solutions in the usual way by multiplying by powers of $\bar{z}$.


TITLE: Multiplicity of the intersection of a Rational curve in a quadric with a tangent plane
QUESTION [1 upvotes]: Consider a rational map $u : \mathbb{CP}^1 \to \mathbb{CP}^4$ of degree~$d$, such that the image lies in a fixed 3-dimensional quadric $Q^3$. In other words, its image is a rational curve in $Q^3 \subset \mathbb{CP}^4$. Now consider a point $p$ on this curve and look at a linear hypersurface $T_p \subset \mathbb{CP}^4$ which is tangent to the quadric $Q$ at $p$. It is also tangent to the curve defined by the parametrization $u$ and therefore the rational curve intersects $T_p$ at $p$ with multiplicity at least 2. If the multiplicity is more than 2, is there an arbitrary small perturbation of this curve to a rational curve of the same degree inside the quadric that will intersect $T_p$ with multilicity exactly 2?

REPLY [2 votes]: If I understand the question correctly, the answer is yes (if $d$ is at least $2$), by irreducibility of the stable maps space + semicontinuity + existence of a nodal rational curve satisfying what you want. For the nodal rational curve, just take a conic through $p$ and some lines intersecting the conic at a single point away from $p$.
I don't know what the best approach to irreducibility of the moduli space of genus $0$ stable maps to $Q^3$ is. It's equivalent to the irreducibility of the moduli space of genus $0$ stable maps to $\mathbb{CP}^3$, which is well-known, but I don't know a reference. Alternatively, you can just cite "Rational curves on hypersurfaces of low degree", Harris-Roth-Starr, which proves something significantly more general.


TITLE: Using the Weierstrass M-test, show that the series converges uniformly on the given domain
QUESTION [5 upvotes]: $\sum_{k \geq 0} \frac{z^k}{z^k+1}$ on the domain $\overline{D}[0, r]$, where $0 \leq r < 1$
I'm honestly not sure how to do this.  My text mentions the Weierstrass M-test but the example they gave after stating it uses a completely different method (looks like a repeat of a previous example) and looks nothing like the M-test.

REPLY [4 votes]: From the notation and complex analysis tag I would guess we should assume $z\in \mathbb C,|z|\le r.$ For $k>0,$ we can then say $|1+z^k|\ge 1-|z^k| = 1-|z|^k \ge 1- |z| \ge 1-r.$ Thus
$$\left |\frac{z^k}{1+z^k}\right | = \frac{|z^k|}{|1+z^k|} \le \frac{r^k}{1-r}.$$
Since $\sum_{k=1}^{\infty} r^k/(1-r) < 1/(1-r)^2,$ we have uniform convergence in $|z|\le r$ by Weierstrass M.


TITLE: Formalize answer to $\lim_{n \to\infty}\sqrt[n]{\{\sqrt{2}\}\{2\sqrt{2}\}\{3\sqrt{2}\}\cdots\{n\sqrt{2}\} }$
QUESTION [2 upvotes]: I was trying to understand the accepted answer here this answer Calculate $\lim_{n \to\infty}\sqrt[n]{\{\sqrt{2}\}\{2\sqrt{2}\}\{3\sqrt{2}\}\cdots\ \{n\sqrt{2}\} }$ , in particular the statement of the accepted answer:
Since $\{ n\sqrt{2} \}$ is equidistributed modulo $1$, the limit could be rewritten as the limit of the expected value of the geometric average of $n$ uniform random variables.
I find the statement intuitive, but do not understand how it can be formalized, hence this separate question.
Note 1: I am aware that the problem can be solved using Weyl's theorem as here: limit of arithmetic mean of $|\sin n|$, $n\in\mathbb{N}$ , but this I am not sure directly justifies the reported statement (even if it provides a solution to the problem).
OLDER VERSION OF THE QUESTION:
Since the statement involves random variables I thought to use https://en.wikipedia.org/wiki/Ergodic_theory .
The only way I see here to introduce a measure space is to define $\Omega$ as the unit interval $[0,1]$ with the Lesbesgue measure. Than define $T :\Omega \rightarrow \Omega : x \rightarrow \{ x+\sqrt{2} \} $, with brackets indicating fractional part. We have to check that the transformation is ergodic to apply Birkhoff's theorem but, even after doing that, what we can conclude ? Birkhoff's theorem would say that the relation:
$$\frac{1}{N} \sum_{k=0}^{N}f(\{ x+k\sqrt{2}\}) \rightarrow \int_0^1 f(y)dy$$
would hold for almost any $x \in  \Omega$. But to apply this to our problem we would need that the relation holds for $x=0$, that is a specific element, and I am not sure therefore that Birkhoff can be applied here. Further, Birkhoff would not justify the statement even if we introduced some probability concepts.
So I have these two questions:

can Birkhoff's theorem or some ergodic theory based on r.v. be used to formalize the accepted answer ?

if not, how can the reported statement be formalized? (maybe it is already formal enough but I do not see why)

REPLY [3 votes]: I’ll be rather vague in using the term nice function, and for simplicity we can assume the term means Riemann inegrable (or improper integrable).
Here I explain why the method, or rather interpretation,  described by @Varun Vejalla in his answer to the the problem here works, which is indeed a very clever reduction of the problem.
Suppose $\{x_n\}$ is an equicontinuous sequence in $(0,1)$. Then, by Weyl's equidistribution theorem, for any nice function $f$
\begin{align}
\frac1n\sum^n_{k=1}f(x_k)\xrightarrow{n\rightarrow\infty}\int^1_0f(t)\,dt\tag{1}\label{one}
\end{align}
The right has side being the expectation  of the random variable $f(U)$ where $U$ is uniformly distributed in $(0,1)$
Now, suppose $\phi:(0,1)\rightarrow(0,\infty)$ is a nice function such that $\log\circ \phi$ is also nice, then applying \eqref{one} to $f=\log\circ\phi$ yields
\begin{align}
\alpha_n&:=\sqrt[n]{\phi(x_1)\cdot\ldots \phi(x_n)}\\&=\exp\Big(\frac1n\sum^n_{k=1}\log\circ\phi(x_k)\Big)\xrightarrow{n\rightarrow\infty}\exp\Big(\int^1_0\log\circ\phi(t)\,du\Big)\tag{2}\label{two}
\end{align}
On the other hand, the expectation of $\Big(\phi(U_1)\cdot\ldots\phi(U_n)\Big)^{1/n}$ where $U_1,\ldots, U_n$ are i.i.d uniformly distributed random variables in $(0,1)$ is
\begin{align}
\beta_n:=\mathbb{E}\left[\Big(\phi(U_1)\cdot\ldots\phi(U_n)\Big)^{1/n}\right]=\Big(\int^1_0 \phi^{1/n}(t)\,dt\Big)^n\tag{3}\label{three}
\end{align}
If for example $\phi(t)=t^\alpha$ then \eqref{two} yields
$a_n\xrightarrow{n\rightarrow\infty}e^{-\alpha}$ while \eqref{three} yields
$\beta_n\xrightarrow{n\rightarrow\infty}\lim_n\Big(1+\tfrac{\alpha}{n}\Big)^{-n}=e^{-\alpha}$ (observe that the original problem has $\phi(t)=t$).
The question then is whether for all nice functions $\phi$
$$\lim_{n\rightarrow\infty}\Big(\int^1_0\phi^{1/n}(t)\,dt\Big)^n=\exp\Big(\int^1_0\log\circ\phi(t)\,dt\Big)$$
This is in fact the case for any measurable function $\phi\geq0$ such that  $\|\phi\|_p<\infty$ for some $0<p<\infty$.
That is the interpretation by Verun works, that is,  for the purposes the the problem at hand, the sequence $(x_n:n\in\mathbb{N})$ can be considered as an i.i.d sample from the uniform distribution $U$ in $(0,1)$ to justify the application of the law of large numbers. This however, is just an interpretation of the original problem in terms of probabilistic elements. There is nothing random about the sequence $(\{\sqrt{2}n\}:n\in\mathbb{N}\}$.


text:
\subsection{Classification of linear forms on $\Z_2^{g+1}$ under the action of $O(\Z_2^{g+1})$}\label{ssec:linform}

\bs
The family $\{\sigma(v_i), 0\leq i\leq g,h\}$ is a basis of $H_1(P_n;\Z_2)$. Hence there is a bijection between the special  $\Z_2-$coverings  $E_\psi$ and the  linear forms $\theta=\psi\circ \sigma$ on $\Z_2^{g+1}$ and
 the action $A_1^\sigma$ is determined by the action by right composition of $ O(\Z_2^{g+1})$ on the linear forms $\theta$ on $\Z_2^{g+1}.$

We consider the right action by composition of $O(\Z_2^{g+1})$ on  $\Z_2^{g+1}.$
If $\theta$ and $\theta'$, two linear forms on $\Z_2^{g+1}$, are  in the same orbit,  we will write $\theta\sim\theta'.$

Let us denote by $v=\Sigma_{i=0}^{i=g} v_i$. Any $T\in
O(\Z_2^{g+1})$ lets invariant $v^\perp=\{ x\in \Z_2^{g+1}\mid
0=<x,x>=\Sigma x_i=<v,x>\}$  then also $v^{\perp\perp}=\Z_2 v$ {\sl
i.e.} $T(v)=v$. This is the proof of the following  lemma which will
be useful in this paper.

\begin{lem}\label{lem:uti} Any $T\in O(\Z_2^{g+1})$ lets fixed $v=\Sigma_{i=0}^{i=g} v_i$.
\end{lem}

\qed

\begin{prop}\label{prop:mi} Under the action by right composition by elements of $O(\Z_2^{g+1})$,
a) the following two linear forms are fixed : $\theta_0\colon x\mapsto 0$ and $\theta_1\colon x=\Sigma_{i=0}^{i=g} x_iv_i\mapsto
\Sigma_{i=0}^{i=g} x_i$;

Apart from these two linear forms,

\noindent b) when $g=1$, the two linear forms $x_0v_0+x_1v_1\mapsto x_0$ and $x_0v_0+x_1v_1\mapsto x_1$ are equivalent;

\noindent c) when $g\geq 2$, $\theta\sim\theta'$ if and only if
$\Sigma_{i=0}^{i=g} \theta(v_i)=\Sigma_{i=0}^{i=g} \theta'(v_i)$.
\end{prop}

\bs

\proof

Let us denote by $m_i=\theta(v_i)$ and $m'_i=\theta'(v_i)$.

1) First we want  to show that if $\theta\sim\theta'$ then $\Sigma m_i=\Sigma m'_i$. If $\theta\sim\theta'$ there exists $T$  such that $\theta'=\theta\circ T$, we get $\Sigma m'_i=\theta'(v)=\theta\circ T(v)=\theta(v)=\Sigma m_i.$ because $T(v)=v.$

2) Choose any $a=\Sigma a_iv_i$ with $\Sigma a_i=0$, and define, for $x\in \Z_2^{g+1}$, $T_a(x)=x+<a,x>a$. Here we have the equality $<a,a>=\Sigma a_i^2=\Sigma a_i=0$, so $<T_a(x),T_a(y)>=<x,y>$ and $T_a\in O(\Z_2^{g+1})$.

Let $\theta$ be a linear form such that there exists at least one
pair $i,j$ such that  $m_i\neq m_j.$  Notice that the order of the
terms $0$ and $1$ is not important because the permutations are
elements of $O(\Z_2^{g+1})$ so  we can work with
$m=(0,1,m_2,\cdots,m_{g})$.  Let $a=(1, 1+\lambda, m_2,\cdots,m_g)$
with $\lambda=\Sigma_{i\geq 2}m_i$, we have $\Sigma a_i=0$ and
$\Sigma a_im_i=1$ hence $m'_i=\theta\circ
T_a(v_i)=\theta(v_i+a_ia)=m_i+a_i$ and $m'=(1,\lambda,0,\cdots,0).$

\qed

\bs By definition,  $\Sigma_{i=0}^{i=g} \theta(v_i)\psi\circ\sigma(v_i)=\Sigma_0^g
\psi(\overline v_i)+\Sigma_0^g\rho_i, $ hence we have the following
lemma (for the notation $\overline v_i$ see (\ref{nota:sigm}) :

\begin{lem}\label{lem:01} Let us distinguish $\psi_0\circ\sigma\colon x\mapsto 0$ and $\psi_1\circ\sigma\colon x=\Sigma x_iv_i\mapsto \Sigma x_i, $ (with $\psi_i(h)=1$).
\begin{itemize}
\item  $\Sigma_0^g \psi_0(\bar v_i)=\Sigma_0^g\rho_i;$
\item  $\Sigma_0^g \psi_1(\bar v_i)=g+1+ \Sigma_0^g\rho_i.$
\end{itemize}
\end{lem}

A  direct consequence of the above classification is the following theorem :

\begin{thm}\label{thm:1} Let us distinguish two  special $\Z_2-$coverings $ E_{\psi_0}$ and $ E_{\psi_1}$, characterized by the property : $\psi_0\circ\sigma\colon x\mapsto 0$ and $\psi_1\circ\sigma\colon x=\Sigma x_iv_i\mapsto \Sigma x_i.$

1) If $g=1$, under the action $A_1^\sigma$ on the space ${\cal E}$ of special  $\Z_2-$coverings, there are two fixed points
$ E_{\psi_0}$ and $ E_{\psi_1}$. The two other elements are in the same class.

2) If $g\geq 2$, there are also two fixed points
$ E_{\psi_0}$ and $ E_{\psi_1}$ and two other classes
\begin{itemize}
\item if $g$ is even, $ \{E_\psi\mid \Sigma_0^g (\psi(\overline v_i)+\rho_i)=1,\psi\neq\psi_1\},$
$\{E_\psi\mid \Sigma_0^g (\psi(\overline v_i)+\rho_i)=0,\psi\neq \psi_0\};$
\item if $g$ is odd, $ \{E_\psi\mid \Sigma_0^g (\psi(\overline v_i)+\rho_i)=1\},$
$\{E_\psi\mid \Sigma_0^g (\psi(\overline v_i)+\rho_i)=0,\psi\neq \psi_0,\psi_1\};$
\end{itemize}
\end{thm}

\qed

\bs

\subsection{Isotropy subgroups of $O(\Z_2^{g+1})$}\label{ssec:isosg}

\bs

From the proposition (\ref{prop:mi}), we know that, when $g>1$, the
set of linear form on $\Z_2^{g+1}$ is the union of four orbits under
the action of $O(\Z_2^{g+1})$, two of them are reduced to an element
$\{\theta_0\},\{\theta_1\}$ and the two others are $
orb_0=\{\theta\neq\theta_0,\theta_1\mid \Sigma_0^g\theta(v_i)=0\}$
and $ orb_1=\{\theta\neq\theta_0,\theta_1\mid
\Sigma_0^g\theta(v_i)=1\}.$ Moreover any $F\in O(\Z_2^{g+1})$ allways fixes
 $\theta_0$ and $\theta_1$ but possibly no other linear
form (for example: $F$ with matrix $\left(\begin{array}{cc} 0&1\\
1&0\end{array}\right)$ in the basis $(v_0,v_1)$).

\bs
\begin{thm}\label{thm:1234}
\begin{description}
\item[1)] The isotropy subgroups $Iso_{\theta_0}$ of $\theta_0$, and $Iso_{\theta_1}$ of $\theta_1$, are the whole
$O(\Z_2^{g+1})$.
\item[2)] Let us chose  a representative $\alpha_i\in {\rm  orb}_i, (i=0,1)$, for example such that $\alpha_0(v_0)=1;\alpha_0(v_1)=1;\alpha_0(v_j)=0$ for $j\neq 0;1$ and $\alpha_1(v_0)=1,\alpha_1(v_j)=0$ for $j\neq 0.$  For every $\theta\in {\rm orb}_i$ the isotropy subgroup $Iso_\theta$ is conjugate to the isotropic subgroup $Iso_{\alpha_i}$ and
$$Iso_{\alpha_1}=\{F\in O(\Z_2^{g+1})\mid F(v_0)=v_0\}\simeq O(\Z_2^{g});$$
$$Iso_{\alpha_0}=\{F\in O(\Z_2^{g+1})\mid F(v_0+v_1)=v_0+v_1\}.$$
\item[3)] The elements of $Iso_{\alpha_1}$ are products of \\
$\bullet$  permutations of the elements $v_i, 1\leq i\leq g$ and \\
$\bullet$ if $g\geq 4,$ the transvection $T_{v_1+v_2+v_3+v_4}\colon x\mapsto x+<x,v_1+v_2+v_3+v_4>(v_1+v_2+v_3+v_4).$
\item[4)] Here $g\geq 1$. Every element of $Iso_{\alpha_0}$ is a product of\\
$\bullet$ elements of $O(\Z_2^2)\times O(\Z_2^{g-1})$, and\\
$\bullet$ if $g\geq 3$, the transvection $T_{v_0+v_1+v_2+v_3}\colon x\mapsto x+<x,v_0+v_1+v_2+v_3>(v_0+v_1+v_2+v_3).$
\end{description}
\end{thm}
\bs

To prove this theorem, we first establish the following lemma :

\begin{lem}\label{lem:trans}
Let us denote by $H=\{x\in V\mid x\neq 0, x\neq e\}$ where $V=\oplus_{i=1}^{i=g}\Z_2v_i, e=v_1+\cdots+v_g.$ The action of $O(\Z_2^{g})$ on the subset $H_0=\{x\in H\mid <x,e>=0\}$ and on $H_1=\{x\in H\mid <x,e>=1\}$, is transitive.
\end{lem}

 {\sl Proof of the lemma.}

 First we remark that $O(\Z_2^{g})$ contains all the permutations of the elements $v_i, 1\leq i\leq g$ and all the transvections $T_u(x)=x+<x,u>u$ such that $<u,e>=0.$ These transvections verify $T_u^{-1}=T_u.$\\
$i)$ When $x$ is an element of $H_0$, it is possible to suppose (up to permutations) that $<x,v_1>=1$ and $<x,v_2>=0.$ For $u=x+v_1+v_2$, we have $<u,e>=0$ and $T_u(v_1+v_2)=x.$\\
$ii)$ When $x$ is an element of $H_1$,  it is possible to suppose (up to permutations) that $<x,v_1>=0.$  For $u=x+v_1$, we have $<u,e>=0$ and $T_u(v_1)=x.$

\qed

{\sl Proof of the part $3)$ of the theorem :}

Let $V=\oplus_{1\leq i\leq g}\Z_2v_i$, then $Iso_{\alpha_1}$ is naturally isomorphic to $O(V)$ (by restriction). If $g=0$ or $g=1$ then $O(V)=\{{\rm id}_V\}$ and the result is obvious.

Assume henceforth that $g\geq 2$ and that the result is true for $g-1$. The elements of $Iso_{\alpha_1}$ fixing $v_1$ are called of ``type $R$''. By induction hypothesis they are products of the described generators.

Let $\gamma\in O(V)$ and $e=v_1+\ldots+v_g$. By lemma (\ref{lem:uti}), $\gamma(e)=e$. Since $g\geq 2$, we have $v_1\neq e$, hence $\gamma(v_1)\neq\gamma(e)=e$, which means that $\gamma(v_1)$ has at least one coordinate equal to $0$. Therefore (up to permutations) we may assume $\gamma(v_1)\in V':=\oplus_{2\leq i\leq g}\Z_2v_i$.

First case: if $\gamma(v_1)\neq v_2+\ldots+v_g$ or if $\gamma(v_1)=v_2$, the lemma (\ref{lem:trans}) applied to $V'$ says that there exists $F$ of type $R$ such that $F^{-1}(\gamma(v_1))=v_2$, hence $F^{-1}\circ\gamma$ is the product of a permutation and of a type $R$.

Second case: if $\gamma(v_1)=v_2+\ldots+v_g$ and $g>2$ (which implies that $g$ is even and $>2$, hence $g\geq 4$), then $T^{-1}_{v_1+v_2+v_3+v_4}(\gamma(v_1))=v_1+v_5+\ldots+v_g\neq v_2+\ldots+v_g$, hence $T^{-1}_{v_1+v_2+v_3+v_4}\circ\gamma$ belongs to the first case above.

\bs

 {\sl Proof of the part $4)$ of the theorem:}

For $g=1$ it is evident.\\
Let us suppose that $g>1$. For $\gamma\in Iso_{\alpha_0} $ i.e. $\gamma(v_0+v_1)=v_0+v_1$, we write $\gamma(v_0)=x+y$ where $x\in V(v_0;v_1)$, the space generated by $\{v_0,v_1\},$ and $y\in V(v_2;\cdots;v_g)$ the space generated by $\{v_2,\cdots,v_g\}.$
The following computations show that $<y,y>=0$ and that $x=v_0$ or $x=v_1$ hence $<x,x>=1$ :
$$\begin{array}{rl} 1=&<\gamma(v_0),\gamma(v_0>=<x+y,x+y>=<x,x>+<y,y>; \\
0=&<\gamma(v_0),\gamma(v_1)>=<\gamma(v_0),\gamma(v_0)+v_0+v_1>\\
=&<\gamma(v_0),\gamma(v_0)>+
<x+y,v_0+v_1>=1+<x,v_0+v_1>.\end{array}
$$

First case: if $y=0.$ then $\gamma\in O(\Z_2^2)\times O(\Z_2^{g-1}).$

\bs

Second case: if $y\neq 0$ (which implies that $g\geq 3$) but $y\neq v_2+\cdots+v_g$, the lemma (\ref{lem:trans}) shows that there exists $F\in id_{\Z_2}\times O(\Z_2^{g-1})$ such that $F^{-1}(y)=v_2+v_3$ then
$$T_{v_0+\cdots+v_3}^{-1}(F^{-1}(\gamma(v_0)))=T_{v_0+\cdots+v_3}(x+v_2+v_3)=v_0+v_1+x,$$
so
$$T_{v_0+\cdots+v_3}^{-1}(F^{-1}(\gamma(v_0)))=\left\{\begin{array}{c} v_0\mbox{ if } x=v_1\\ v_1 \mbox{ if } x=v_0,\end{array}\right\},$$
{\sl i.e.}  we are now in the situation of the first case above.

\bs

Third case : if $y\neq 0$ (which implies that $g\geq 3$) but $y= v_2+\cdots+v_g$, then
$$T_{v_0+\cdots+v_3}^{-1}(\gamma(v_0))=T_{v_0+\cdots+v_3}(x+v_2+\cdots+v_g)=(v_0+v_1+x)+(v_4+\cdots+v_g)=x'+y'.$$
If $g=3$, then $y'=0$ and we are in the first case. If $g\geq 4$, ($y'\neq 0$ but $y'\neq v_2+\cdots+v_g$) we are in the second case.

\qed

config: arxiv


TITLE: Show that $\mu (E \setminus A)>0$ if $A$ is a nonmeasurable subset of $X$ and $A \subseteq E$, $E$ is measurable.
QUESTION [2 upvotes]: This question was asked here, but the question wasn't asking for an answer, just a clarification on the proof by contradiction they already had, so I'm reposting it to ask for help arriving at the answer.
Because the asker above said they proved it by contradiction, that is what I'm attempting. But I'm having issues wrapping my brain around the concept of set measurability. So let's give it a good college try with what I can understand.
For clarity, $\mu$ is an outer measure.
A is nonmeasurable, so $\exists B \subseteq X$ such that $\mu (B) \ne \mu (B \bigcap A) + (B \bigcap A^c)$.
E is measurable, so $\mu (B) = \mu (B \bigcap E) + (B \bigcap E^c)$.
This essentially means $\mu (B) \ge \mu (B \bigcap E) + (B \bigcap E^c)$ (Since monotonicity is alredy implied by the definition of outer measure).
So we can attempt a proof (or the start of one) by contradiction.
Assume $\mu (E \setminus A)=0$. So $E \setminus A$ is a null set.
So $\mu (B) \ge \mu (B \bigcap E) + (B \bigcap E^c)$. I assume I'm supposed to show a contradiction using that A is nonmeasurable. I'm unsure how.
Another way I think could work would be to use: $\mu (E \setminus A)= \mu (E \bigcap A^c) = 0$ and arrive at a contradiction given that A is nonmeasurable, but again, I'm unsure how.
I just need some direction from here. Thank you in advance for any advice.

REPLY [3 votes]: Measures induced by outer measures are complete, meaning that any subset of $X$ with outer measure zero is measurable. To see this, suppose that $S \subseteq X$ and $\mu(S) = 0$. Let $Y \subseteq X$ be any subset. By monotonicity, we have $\mu(Y \cap S) \leq \mu(S) = 0$, so $\mu(Y \cap S) = 0$. Also by monotonicity, we have $\mu(Y \cap S^c) \leq \mu(Y)$.
Therefore,
$$\mu(Y \cap S) + \mu(Y \cap S^c) = \mu(Y \cap S^c) \leq \mu(Y)$$
which shows that $S$ is measurable.
Now, let $E$ and $A$ be as in your problem. Suppose for a contradiction that $\mu(E \cap A^c) = 0$. Then by the above argument, $E \cap A^c$ is measurable. But $E$ is also measurable, so this means that $A = E \setminus (E \cap A^c)$ must be measurable. But this is a contradiction.
So, our assumption that $\mu(E \cap A^c) = 0$ is untenable; hence we must have $\mu(E \cap A^c) > 0$.


TITLE: trigonometric equation help sought
QUESTION [0 upvotes]: Let $\alpha_4, A_1, A_2, A_3$, and $B_1$ be non-zero real numbers. Consider the set of equations
$$
\begin{split}
\alpha_4\cos(3\omega\tau) &= A_1+A_2\cos(2\omega\tau)-A_3\sin(2\omega\tau)\\
\alpha_4\sin(3\omega\tau) &= B_1+A_3\cos(2\omega\tau)+A_2\sin(2\omega\tau)
\end{split}
$$
where $\tau,\omega\in\mathbb{R}^{+}$. I need to solve the above set of equations for $\omega\tau$. I've tried squaring both sides and then adding; but this hasn't helped! I've tried using trig identities; this hasn't helped either. Someone out there has to have an idea!

REPLY [1 votes]: if you write
$$\phi = \omega \tau$$
and
$$\theta = tan^{-1}\frac{A_3}{A_2}$$
and
$$\lambda = \sqrt{(A_2)^2+(A_3)^2}$$
and
$$
C=A_1 + iB_1
$$
then, multiplying the second equation by $i$ gives you (something like)
$$
\alpha_4 e^{3\phi i} = \lambda e^{i(\theta+2\phi)} +C
$$
these details may not be quite right - unfortunately i am rather busy right now, and my calculations are unreliable at the best of times, but this seems the most fruitful way to proceed with the simplification


text:
(*  Title:       BIT is 1.75 competitive on lists of length 2
    Author:      Max Haslbeck
*)
section "BIT is 1.75 competitive on lists of length 2"

theory BIT_2comp_on2
imports BIT Phase_Partitioning
begin

subsection "auxliary lemmas"

subsubsection "\<open>E_bernoulli3\<close>"

lemma E_bernoulli3: assumes "0<p"
    and "p<1"
    and "finite (set_pmf (bind_pmf (bernoulli_pmf p) f))"
    shows "E (bind_pmf (bernoulli_pmf p) f) = E(f True)*p + E(f False)*(1-p)" (is "?L = ?R")
proof -

  have T: "(\<Sum>a\<in>(\<Union>x. set_pmf (f x)). (a * pmf (f True) a))
            = E(f True)"
    unfolding E_def
    apply(subst integral_measure_pmf[of "bind_pmf (bernoulli_pmf p) f"])
      using assms apply(simp)
      using assms apply(simp add: set_pmf_bernoulli) apply blast
      using assms by(simp add: set_pmf_bernoulli mult_ac)
  have F: "(\<Sum>a\<in>(\<Union>x. set_pmf (f x)). (a * pmf (f False) a))
            = E(f False)"
    unfolding E_def
    apply(subst integral_measure_pmf[of "bind_pmf (bernoulli_pmf p) f"])
      using assms apply(simp)
      using assms apply(simp add: set_pmf_bernoulli) apply blast
      using assms by(simp add: set_pmf_bernoulli mult_ac)

  have "?L = (\<Sum>a\<in>(\<Union>x. set_pmf (f x)).
       a *
       (pmf (f True) a * p +
        pmf (f False) a * (1 - p)))"
  unfolding E_def
  apply(subst integral_measure_pmf[of "bind_pmf (bernoulli_pmf p) f"])
    using assms apply(simp)
    apply(simp)
    using assms apply(simp add: set_pmf_bernoulli )
    by(simp add: pmf_bind mult_ac)
  also have "\<dots> = (\<Sum>a\<in>(\<Union>x. set_pmf (f x)). (a * pmf (f True) a * p)
                                    + (a * pmf (f False) a * (1 - p)))"
    apply(rule sum.cong) apply(simp) by algebra
  also have "\<dots> = (\<Sum>a\<in>(\<Union>x. set_pmf (f x)). (a * pmf (f True) a * p))
                  + (\<Sum>a\<in>(\<Union>x. set_pmf (f x)). (a * pmf (f False) a * (1 - p)))"
    by (simp add: sum.distrib)
  also have "\<dots> = (\<Sum>a\<in>(\<Union>x. set_pmf (f x)). (a * pmf (f True) a)) * p
                  + (\<Sum>a\<in>(\<Union>x. set_pmf (f x)). (a * pmf (f False) a )) * (1 - p)"
    by (simp add: sum_distrib_right)
  also have "\<dots> = ?R" unfolding T F by simp
  finally show ?thesis .
qed

subsubsection "types of configurations"

definition "type0 init x y = do {
                  (a::bool) \<leftarrow> (bernoulli_pmf 0.5);
                  (b::bool) \<leftarrow> (bernoulli_pmf 0.5);
                  return_pmf  ([x,y], ([a,b],init))
                }"

definition "type1 init x y = do {
                  (a::bool) \<leftarrow> (bernoulli_pmf 0.5);
                  (b::bool) \<leftarrow> (bernoulli_pmf 0.5);
                  return_pmf ( if ~[a,b]!(index init x)\<and>[a,b]!(index init y) then ([y,x], ([a,b],init))
                         else ([x,y], ([a,b],init)))
                }"

definition "type3 init x y = do {
                  (a::bool) \<leftarrow> (bernoulli_pmf 0.5);
                  (b::bool) \<leftarrow> (bernoulli_pmf 0.5);
                  return_pmf ( if [a,b]!(index init x)\<and>~[a,b]!(index init y) then ([x,y], ([a,b],init))
                         else ([y,x], ([a,b],init)))
                }"

definition "type4 init x y = do {
                  (a::bool) \<leftarrow> (bernoulli_pmf 0.5);
                  (b::bool) \<leftarrow> (bernoulli_pmf 0.5);
                  return_pmf ( if ~[a,b]!(index init y) then ([x,y], ([a,b],init))
                         else ([y,x], ([a,b],init)))
                }"

definition "BIT_inv s x i == (s = (type0 i x (hd (filter (\<lambda>y. y\<noteq>x) i) )))"

lemma BIT_inv2: "x\<noteq>y \<Longrightarrow> z\<in>{x,y} \<Longrightarrow> BIT_inv s z [x,y] = (s= type0 [x,y] z (other z x y))"
  unfolding BIT_inv_def by(auto simp add: other_def)

subsubsection "cost of BIT"

lemma costBIT_0x:
    assumes "x\<noteq>y" "x : {x0,y0}" "y\<in>{x0,y0}"
    shows
  "E (type0 [x0, y0] x y \<bind>
       (\<lambda>s. BIT_step s x \<bind>
            (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) x a))))) = 0"
using assms apply(auto)
  apply(simp_all add: type0_def BIT_step_def bind_assoc_pmf bind_return_pmf )
  apply(simp_all add: E_bernoulli3 t\<^sub>p_def)
  done

lemma costBIT_0y:
    assumes "x\<noteq>y" "x : {x0,y0}" "y\<in>{x0,y0}"
    shows
  "E (type0 [x0, y0] x y \<bind>
       (\<lambda>s. BIT_step s y \<bind>
            (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) y a))))) = 1"
using assms apply(auto)
  apply(simp_all add: type0_def BIT_step_def bind_assoc_pmf bind_return_pmf )
  apply(simp_all add: E_bernoulli3 t\<^sub>p_def)
  done

lemma costBIT_1x:
    assumes "x\<noteq>y" "x : {x0,y0}" "y\<in>{x0,y0}"
    shows
  "E (type1 [x0, y0] x y \<bind>
       (\<lambda>s. BIT_step s x \<bind>
            (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) x a))))) = 1/4"
using assms apply(auto)
  apply(simp_all add: type1_def BIT_step_def bind_assoc_pmf bind_return_pmf )
  apply(simp_all add: E_bernoulli3 t\<^sub>p_def)
  done

lemma costBIT_1y:
    assumes "x\<noteq>y" "x : {x0,y0}" "y\<in>{x0,y0}"
    shows
  "E (type1 [x0, y0] x y \<bind>
       (\<lambda>s. BIT_step s y \<bind>
            (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) y a))))) = 3/4"
using assms apply(auto)
  apply(simp_all add: type1_def BIT_step_def bind_assoc_pmf bind_return_pmf )
  apply(simp_all add: E_bernoulli3 t\<^sub>p_def)
  done

lemma costBIT_3x:
    assumes "x\<noteq>y" "x : {x0,y0}" "y\<in>{x0,y0}"
    shows
  "E (type3 [x0, y0] x y \<bind>
       (\<lambda>s. BIT_step s x \<bind>
            (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) x a))))) = 3/4"
using assms apply(auto)
  apply(simp_all add: type3_def BIT_step_def bind_assoc_pmf bind_return_pmf )
  apply(simp_all add: E_bernoulli3 t\<^sub>p_def)
  done

lemma costBIT_3y:
    assumes "x\<noteq>y" "x : {x0,y0}" "y\<in>{x0,y0}"
    shows
  "E (type3 [x0, y0] x y \<bind>
       (\<lambda>s. BIT_step s y \<bind>
            (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) y a))))) = 1/4"
using assms apply(auto)
  apply(simp_all add: type3_def BIT_step_def bind_assoc_pmf bind_return_pmf )
  apply(simp_all add: E_bernoulli3 t\<^sub>p_def)
  done

lemma costBIT_4x:
    assumes "x\<noteq>y" "x : {x0,y0}" "y\<in>{x0,y0}"
    shows
  "E (type4 [x0, y0] x y \<bind>
       (\<lambda>s. BIT_step s x \<bind>
            (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) x a))))) = 0.5"
using assms apply(auto)
  apply(simp_all add: type4_def BIT_step_def bind_assoc_pmf bind_return_pmf )
  apply(simp_all add: E_bernoulli3 t\<^sub>p_def)
  done

lemma costBIT_4y:
    assumes "x\<noteq>y" "x : {x0,y0}" "y\<in>{x0,y0}"
    shows
  "E (type4 [x0, y0] x y \<bind>
       (\<lambda>s. BIT_step s y \<bind>
            (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) y a))))) = 0.5"
using assms apply(auto)
  apply(simp_all add: type4_def BIT_step_def bind_assoc_pmf bind_return_pmf )
  apply(simp_all add: E_bernoulli3 t\<^sub>p_def)
  done

lemmas costBIT = costBIT_0x costBIT_0y costBIT_1x costBIT_1y costBIT_3x costBIT_3y costBIT_4x costBIT_4y

subsubsection "state transformation of BIT"

abbreviation "BIT_Step s x == (s \<bind> (\<lambda>s. BIT_step s x \<bind> (\<lambda>(a, is'). return_pmf (step (fst s) x a, is'))))"

lemma oneBIT_step0x:
    assumes "x\<noteq>y" "x : {x0,y0}" "y\<in>{x0,y0}"
    shows "BIT_Step (type0 [x0, y0] x y) x = type0 [x0, y0] x y"
  using assms
  apply(simp add: type0_def BIT_step_def bind_assoc_pmf bind_return_pmf step_def mtf2_def)
  apply(safe)
    apply(rule pmf_eqI) apply(simp add: pmf_bind swap_def type0_def)
    apply(rule pmf_eqI) apply(simp add: add.commute pmf_bind swap_def type0_def)
    done

lemma oneBIT_step0y:
    assumes "x\<noteq>y" "x : {x0,y0}" "y\<in>{x0,y0}"
    shows "BIT_Step (type0 [x0, y0] x y) y = type4 [x0, y0] x y"
  using assms
  apply(simp add: type0_def BIT_step_def bind_assoc_pmf bind_return_pmf step_def mtf2_def)
  apply(safe)
    apply(rule pmf_eqI) apply(simp add: add.commute pmf_bind swap_def type4_def)
    apply(rule pmf_eqI) apply(simp add: pmf_bind swap_def type4_def)
    done

lemma oneBIT_step1x:
    assumes "x\<noteq>y" "x : {x0,y0}" "y\<in>{x0,y0}"
    shows "BIT_Step (type1 [x0, y0] x y) x = type0 [x0, y0] x y"
  using assms
  apply(simp add: type1_def BIT_step_def bind_assoc_pmf bind_return_pmf step_def mtf2_def)
  apply(safe)
    apply(rule pmf_eqI) apply(simp add: pmf_bind swap_def type0_def)
    apply(rule pmf_eqI) apply(simp add: add.commute pmf_bind swap_def type0_def)
    done

lemma oneBIT_step1y:
    assumes "x\<noteq>y" "x : {x0,y0}" "y\<in>{x0,y0}"
    shows "BIT_Step (type1 [x0, y0] x y) y = type3 [x0, y0] x y"
  using assms
  apply(simp add: type1_def BIT_step_def bind_assoc_pmf bind_return_pmf step_def mtf2_def)
  apply(safe)
    apply(rule pmf_eqI) apply(simp add: add.commute pmf_bind swap_def type3_def)
    apply(rule pmf_eqI) apply(simp add: pmf_bind swap_def type3_def)
    done

lemma oneBIT_step3x:
    assumes "x\<noteq>y" "x:{x0,y0}" "y:{x0,y0}"
    shows "BIT_Step (type3 [x0, y0] x y) x = type1 [x0, y0] x y"
  using assms
  apply(simp add: type3_def BIT_step_def bind_assoc_pmf bind_return_pmf step_def mtf2_def)
  apply(safe)
    apply(rule pmf_eqI) apply(simp add: pmf_bind swap_def type1_def)
    apply(rule pmf_eqI) apply(simp add: add.commute pmf_bind swap_def type1_def)
    done

lemma oneBIT_step3y:
    assumes "x\<noteq>y" "x : {x0,y0}" "y\<in>{x0,y0}"
    shows "BIT_Step (type3 [x0, y0] x y) y = type0 [x0, y0] y x"
  using assms
  apply(simp add: type3_def BIT_step_def bind_assoc_pmf bind_return_pmf step_def mtf2_def)
  apply(safe)
    apply(rule pmf_eqI) apply(simp add: add.commute pmf_bind swap_def type0_def)
    apply(rule pmf_eqI) apply(simp add: pmf_bind swap_def type0_def)
    done

lemma oneBIT_step4x:
    assumes "x\<noteq>y" "x : {x0,y0}" "y\<in>{x0,y0}"
    shows "BIT_Step (type4 [x0, y0] x y) x =  type1 [x0, y0] x y"
  using assms
  apply(simp add: type4_def BIT_step_def bind_assoc_pmf bind_return_pmf step_def mtf2_def)
  apply(safe)
    apply(rule pmf_eqI) apply(simp add: pmf_bind swap_def type1_def)
    apply(rule pmf_eqI) apply(simp add: add.commute pmf_bind swap_def type1_def)
    done

lemma oneBIT_step4y:
    assumes "x\<noteq>y" "x : {x0,y0}" "y\<in>{x0,y0}"
    shows "BIT_Step (type4 [x0, y0] x y) y = type0 [x0, y0] y x"
  using assms
  apply(simp add: type4_def BIT_step_def bind_assoc_pmf bind_return_pmf step_def mtf2_def)
  apply(safe)
    apply(rule pmf_eqI) apply(simp add: add.commute pmf_bind swap_def type0_def)
    apply(rule pmf_eqI) apply(simp add: pmf_bind swap_def type0_def)
    done

lemmas oneBIT_step = oneBIT_step0x oneBIT_step0y oneBIT_step1x oneBIT_step1y oneBIT_step3x oneBIT_step3y oneBIT_step4x oneBIT_step4y

subsection "Analysis of the four phase forms"

subsubsection "yx"

lemma bit_yx: assumes "x \<noteq> y"
      and kas: "init \<in> {[x,y],[y,x]}"
      and "qs \<in> lang (Star(Times (Atom y) (Atom x))) "
   shows "T\<^sub>p_on_rand' BIT (type1 init x y) (qs@r) = 0.75 * length qs + T\<^sub>p_on_rand' BIT (type1 init x y) r
    \<and> config'_rand BIT (type1 init x y) qs  = (type1 init x y)"
proof -
  from assms have "qs \<in> star ({[y]} @@ {[x]})" by (simp)
  from this assms show ?thesis
  proof (induct qs rule: star_induct)
    case (append u v)
    then have uyx: "u = [y,x]" by auto

    have yy: "T\<^sub>p_on_rand' BIT (type1 init x y)  (v @ r)  = 0.75*length v + T\<^sub>p_on_rand' BIT (type1 init x y) r
            \<and> config'_rand BIT  (type1 init x y) v = (type1 init x y)"
        apply(rule append(3))
          apply(fact)+
          using append(2,6) by(simp_all)

    have s2: "config'_rand BIT  (type1 init x y) [y,x] = (type1 init x y)"
      using kas assms(1) by (auto simp add: oneBIT_step )

    have ta: "T\<^sub>p_on_rand' BIT (type1 init x y) u = 1.5"
      using kas assms(1)
        by(auto simp add: uyx oneBIT_step costBIT_1y costBIT_3x)

    have config: "config'_rand BIT  (type1 init x y) (u @ v)
          = type1 init x y" by (simp only: config'_rand_append s2 uyx yy)

    have "T\<^sub>p_on_rand' BIT (type1 init x y) (u @ (v @ r))
        = T\<^sub>p_on_rand' BIT (type1 init x y) u  + T\<^sub>p_on_rand' BIT ( config'_rand BIT (type1 init x y)  u) (v@r) "
          by (simp only: T_on_rand'_append)
    also have "\<dots> =  T\<^sub>p_on_rand' BIT  (type1 init x y) u + T\<^sub>p_on_rand' BIT (type1 init x y) (v@r) "
      unfolding uyx by(simp only: s2)
    also have "\<dots> = T\<^sub>p_on_rand' BIT (type1 init x y) u  + 0.75*length v + T\<^sub>p_on_rand' BIT (type1 init x y) r "
        by(simp only: yy)
    also have "\<dots> = 2*0.75 + 0.75*length v + T\<^sub>p_on_rand' BIT (type1 init x y) r " by(simp add: ta)
    also have "\<dots> = 0.75 * (2+length v) + T\<^sub>p_on_rand' BIT (type1 init x y) r"
      by (simp add: ring_distribs del: add_2_eq_Suc' add_2_eq_Suc)
    also have "\<dots> = 0.75 * length (u @ v) + T\<^sub>p_on_rand' BIT (type1 init x y) r"
      using uyx by simp
    finally show ?case using config by simp
  qed simp
qed

subsubsection "(yx)*yx"

lemma bit_yxyx: assumes "x \<noteq> y" and kas: "init \<in> {[x,y],[y,x]}" and
      "qs \<in> lang (seq[Times (Atom y) (Atom x), Star(Times (Atom y) (Atom x))])"
   shows "T\<^sub>p_on_rand' BIT (type0 init x y) (qs@r) = 0.75 * length qs + T\<^sub>p_on_rand' BIT (type1 init x y) r
    \<and> config'_rand BIT (type0 init x y) qs  = (type1 init x y)"
proof -
  obtain u v where uu: "u \<in> lang (Times (Atom y) (Atom x))"
              and vv: "v \<in> lang (seq[ Star(Times (Atom y) (Atom x))])"
              and qsuv: "qs = u @ v"
  using assms(3) by (auto simp: conc_def)

  from uu have uyx: "u = [y,x]" by(auto)

  from qsuv uyx have vqs: "length v = length qs - 2" by auto
  from qsuv uyx  have vqs2: "length v + 2 = length qs" by auto

  have s2: "config'_rand BIT  (type0 init x y) [y,x] = (type1 init x y)"
     using kas assms(1) by(auto simp add: oneBIT_step)

  have ta: "T\<^sub>p_on_rand' BIT (type0 init x y) u = 1.5"
    using kas assms(1) by (auto simp add: uyx oneBIT_step costBIT)

  have tat: "T\<^sub>p_on_rand' BIT (type1 init x y) (v @ r) =   0.75*length v + T\<^sub>p_on_rand' BIT (type1 init x y) r
            \<and> config'_rand BIT (type1 init x y) v = (type1 init x y)"
        apply(rule bit_yx)
      apply(fact)+
      using vv by(simp_all)

  have config: "config'_rand BIT (type0 init x y) (u @ v) = type1 init x y"
    by(simp only: config'_rand_append s2 uyx tat)

  have "T\<^sub>p_on_rand' BIT (type0 init x y) (u @ (v @ r))
        = T\<^sub>p_on_rand' BIT (type0 init x y) u + T\<^sub>p_on_rand' BIT (config'_rand BIT (type0 init x y) u) (v@r)" by (simp only: T_on_rand'_append)
also
  have "\<dots> =  T\<^sub>p_on_rand' BIT (type0 init x y) u + T\<^sub>p_on_rand' BIT (type1 init x y) (v@r)" by(simp only: uyx s2)
also
  have "\<dots> = T\<^sub>p_on_rand' BIT (type0 init x y) u + 0.75*length v + T\<^sub>p_on_rand' BIT (type1 init x y) r" by(simp only: tat)
also
  have "\<dots> = 2*0.75 + 0.75*length v + T\<^sub>p_on_rand' BIT (type1 init x y) r" by(simp add: ta)
also
  have "\<dots> = 0.75 * (2+length v) + T\<^sub>p_on_rand' BIT (type1 init x y) r" by (simp add: ring_distribs del: add_2_eq_Suc' add_2_eq_Suc)
also
  have "\<dots> = 0.75 * length (u @ v) + T\<^sub>p_on_rand' BIT (type1 init x y) r" using uyx by simp
finally
  show ?thesis using qsuv config by simp
qed

subsubsection \<open>\<open>x^+..\<close>\<close>

lemma BIT_x: assumes "x\<noteq>y"
       "init \<in> {[x,y],[y,x]}" "qs \<in> lang (Plus (Atom x) One)"
 shows "T\<^sub>p_on_rand' BIT (type0 init x y) (qs@r) = T\<^sub>p_on_rand' BIT (type0 init x y) r
    \<and> config'_rand BIT  (type0 init x y) qs = (type0 init x y)"
proof -
  have s: "config'_rand BIT (type0 init x y) qs = type0 init x y"
    using assms by (auto simp add: oneBIT_step)

  have t: "T\<^sub>p_on_rand' BIT (type0 init x y) qs = 0"
    using assms by (auto simp add: costBIT)

  show ?thesis using s t by(simp add: T_on_rand'_append)
qed

subsubsection "Phase Form A"

lemma BIT_a: assumes "x \<noteq> y"
    " init \<in> {[x,y],[y,x]}"
   "qs \<in> lang (seq [Plus (Atom x) One, Atom y, Atom y])"
  shows "config'_rand BIT (type0 init x y) qs = (type0 init y x)" (is ?C)
    and b: "T\<^sub>p_on_rand' BIT (type0 init x y) qs = 1.5" (is ?T)
proof -
  from assms(3) have alt: "qs = [x,y,y] \<or> qs = [y,y]" apply(simp) by fastforce
  show ?C
    using assms(1,2) alt by (auto simp add: oneBIT_step)
  show ?T
    using assms(1,2) alt by(auto simp add: oneBIT_step costBIT)
qed

lemma bit_a: assumes
    "x \<noteq> y" "{x, y} = {x0, y0}" "BIT_inv s x [x0, y0]"
    "set qs \<subseteq> {x, y}" "qs \<in> lang (seq [Plus (Atom x) One, Atom y, Atom y])"
 shows
    "T\<^sub>p_on_rand' BIT s qs  \<le> 1.75 * T\<^sub>p [x,y] qs (OPT2 qs [x,y])
      \<and>  BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0]
      \<and> T\<^sub>p_on_rand' BIT s qs = 1.5"
proof -
  from assms have f: "x0\<noteq>y0" by auto
  from assms(1,3) assms(2)[symmetric] have s: "s = type0 [x0,y0] x y"
    apply(simp add: BIT_inv2[OF f] other_def) by fast

  from assms(1,2) have kas: "[x,y] = [x0,y0] \<or> [x,y] = [y0,x0]" by auto

  from assms have lqs: "last qs = y" by fastforce
  from assms(1,2) kas have p: "T\<^sub>p_on_rand' BIT s qs = 1.5"
    unfolding s
    apply(safe)
      apply(rule BIT_a)
        apply(simp) apply(simp) using assms(5) apply(simp)
      apply(rule BIT_a)
        apply(simp) apply(simp) using assms(5) apply(simp)
  done
  with OPT2_A[OF assms(1,5)] have BIT: "T\<^sub>p_on_rand' BIT s qs \<le> 1.75 * T\<^sub>p [x, y] qs (OPT2 qs [x, y])" by auto

  from assms(1,2) kas have "config'_rand BIT s qs = type0 [x0, y0] y x"
    unfolding s
    apply(safe)
      apply(rule BIT_a)
        apply(simp) apply(simp) using assms(5) apply(simp)
      apply(rule BIT_a)
        apply(simp) apply(simp) using assms(5) apply(simp)
  done

  then have "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0]"
    apply(simp)
    using assms(1) kas f lqs by(auto simp add: BIT_inv2 other_def)

  then show ?thesis using BIT s p by simp
qed

lemma bit_a'': " a \<noteq> b \<Longrightarrow>
         {a, b} = {x, y} \<Longrightarrow>
         BIT_inv s a [x, y] \<Longrightarrow>
         set qs \<subseteq> {a, b} \<Longrightarrow>
         qs \<in> lang (seq [question (Atom a), Atom b, Atom b]) \<Longrightarrow>
         BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' BIT s qs = 1.5"
using bit_a[of a b x y] by blast

subsubsection "Phase Form B"

lemma BIT_b: assumes A: "x \<noteq> y"
       "init \<in> {[x,y],[y,x]}"
    "v \<in> lang (seq [Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x)), Atom y, Atom y])"
    shows "T\<^sub>p_on_rand' BIT (type0 init x y) v = 0.75 * length v - 0.5" (is ?T)
     and "config'_rand BIT  (type0 init x y) v = (type0 init y x)" (is ?C)
proof -
  have lenvmod: "length v mod 2 = 0"
  proof -
    from assms(3) have "v \<in> ({[y]} @@ {[x]}) @@ star({[y]} @@ {[x]}) @@ {[y]} @@ {[y]}" by(simp add: conc_assoc)
    then obtain p q r where pqr: "v=p@q@r" and "p\<in>({[y]} @@ {[x]})"
              and q: "q \<in> star ({[y]} @@ {[x]})" and "r \<in>{[y]} @@ {[y]}" by (metis concE)
    then have "p = [y,x]" "r=[y,y]" by auto
    with pqr have a: "length v = 4+length q" by auto

    from q have b: "length q mod 2 = 0"
    apply(induct q rule: star_induct) by (auto)
    from a b show "length v mod 2 = 0" by auto
  qed

  from assms(3) have "v \<in> lang (seq[Times (Atom y) (Atom x), Star(Times (Atom y) (Atom x))])
                          @@ lang (seq[Atom y, Atom y])" by (auto simp: conc_def)
  then obtain a b where aa: "a \<in> lang (seq[Times (Atom y) (Atom x), Star(Times (Atom y) (Atom x))])"
                      and "b \<in> lang (seq[Atom y, Atom y])"
                      and vab: "v = a @ b"
                      by(erule concE)
  then have bb: "b=[y,y]" by auto
  from vab bb have lenv: "length v = length a + 2" by auto

  from bit_yxyx[OF assms(1,2) aa] have stars: "T\<^sub>p_on_rand' BIT (type0 init x y) (a @ b)  = 0.75 * length a + T\<^sub>p_on_rand' BIT (type1 init x y) b"
                             and s2: "config'_rand BIT (type0 init x y) a = type1 init x y"  by fast+

  have t: "T\<^sub>p_on_rand' BIT (type1 init x y) b = 1"
    using assms(1,2) by (auto simp add: oneBIT_step  costBIT bb)

  have s: "config'_rand BIT  (type1 init x y) [y, y] = type0 init y x"
    using assms(1,2) by (auto simp add: oneBIT_step)

  have config: "config'_rand BIT (type0 init x y) (a @ b) = type0 init y x"
    by (simp only: config'_rand_append s2 vab bb s)

  have calc: "3 * Suc (Suc (length a)) / 4 - 1 / 2 = 3 * (2+length a) / 4 - 1 / 2" by simp

  from t stars have "T\<^sub>p_on_rand' BIT (type0 init x y) (a @ b) = 0.75 * length a + 1" by auto
  then show "T\<^sub>p_on_rand' BIT  (type0 init x y) v = 0.75 * length v - 0.5"
    unfolding lenv by(simp add: vab ring_distribs del: add_2_eq_Suc')
  from config vab show ?C by simp
qed

lemma bit_b''1: assumes
    "x \<noteq> y" "{x, y} = {x0, y0}" "BIT_inv s x [x0, y0]"
    "set qs \<subseteq> {x, y}"
    "qs \<in> lang (seq[Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom y, Atom y])"
 shows "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0] \<and>
          T\<^sub>p_on_rand' BIT s qs  = 0.75 * length qs - 0.5"
proof -
  from assms have f: "x0\<noteq>y0" by auto
  from assms(1,3) assms(2)[symmetric] have s: "s = type0 [x0,y0] x y"
    apply(simp add: BIT_inv2[OF f] other_def) by fast

  from assms(1,2) have kas: "[x,y] = [x0,y0] \<or> [x,y] = [y0,x0]" by auto

  from assms(5) have lqs: "last qs = y" by fastforce
  from assms(1,2) kas have BIT: "T\<^sub>p_on_rand' BIT s qs = 0.75 * length qs - 0.5"
    unfolding s
    apply(safe)
      apply(rule BIT_b)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
      apply(rule BIT_b)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
  done

  from assms(1,2) kas have "config'_rand BIT s qs = type0 [x0, y0] y x"
    unfolding s
    apply(safe)
      apply(rule BIT_b)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
      apply(rule BIT_b)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
  done

  then have config: "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0]"
    apply(simp)
    using assms(1) kas lqs by(auto simp add: BIT_inv2 other_def)

  show ?thesis using BIT config by simp
qed

lemma BIT_b2: assumes A: "x \<noteq> y"
       "init \<in> {[x,y],[y,x]}"
    "v \<in> lang (seq [Atom x, Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x)), Atom y, Atom y])"
    shows "T\<^sub>p_on_rand' BIT (type0 init x y) v = 0.75 * (length v - 1) - 0.5" (is ?T)
     and "config'_rand BIT  (type0 init x y) v = (type0 init y x)" (is ?C)
proof -
  from assms(3) obtain w where  vw: "v = [x]@w" and
          w: "w \<in> lang (seq [Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x)), Atom y, Atom y])"
          by(auto)
  have c1: "config'_rand BIT (type0 init x y) [x] = type0 init x y"
      using assms by(auto simp add: oneBIT_step)
  have t1: "T\<^sub>p_on_rand' BIT (type0 init x y) [x] = 0"
      using assms by(auto simp add: costBIT)
  show "T\<^sub>p_on_rand' BIT (type0 init x y) v
      = 0.75 * (length v - 1) - 0.5"
      unfolding vw apply(simp only: T_on_rand'_append c1 BIT_b[OF assms(1,2) w] t1)
        by (simp)
  show "config'_rand BIT (type0 init x y) v = (type0 init y x)"
    unfolding vw by(simp only: config'_rand_append c1 BIT_b[OF assms(1,2) w])
qed

lemma bit_b''2: assumes
    "x \<noteq> y" "{x, y} = {x0, y0}" "BIT_inv s x [x0, y0]"
    "set qs \<subseteq> {x, y}"
    "qs \<in> lang (seq[Atom x, Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom y, Atom y])"
 shows "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0] \<and>
          T\<^sub>p_on_rand' BIT s qs  = 0.75 * (length qs - 1) - 0.5"
proof -
  from assms have f: "x0\<noteq>y0" by auto
  from assms(1,3) assms(2)[symmetric] have s: "s = type0 [x0,y0] x y"
    apply(simp add: BIT_inv2[OF f] other_def) by fast

  from assms(1,2) have kas: "[x,y] = [x0,y0] \<or> [x,y] = [y0,x0]" by auto

  from assms(5) have lqs: "last qs = y" by fastforce
  from assms(1,2) kas have BIT: "T\<^sub>p_on_rand' BIT s qs = 0.75 * (length qs-1) - 0.5"
    unfolding s
    apply(safe)
      apply(rule BIT_b2)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
      apply(rule BIT_b2)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
  done

  from assms(1,2) kas have "config'_rand BIT s qs = type0 [x0, y0] y x"
    unfolding s
    apply(safe)
      apply(rule BIT_b2)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
      apply(rule BIT_b2)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
  done

  then have config: "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0]"
    apply(simp)
    using assms(1) kas lqs by(auto simp add: BIT_inv2 other_def)

  show ?thesis using BIT config by simp
qed

lemma bit_b: assumes "x \<noteq> y"
      "init \<in> {[x,y],[y,x]}"
   "qs \<in> lang (seq[Plus (Atom x) One, Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom y, Atom y])"
 shows  "T\<^sub>p_on_rand' BIT (type0 init x y) qs \<le> 1.75 * T\<^sub>p [x,y] qs (OPT2 qs [x,y])"
  and "config'_rand BIT (type0 init x y) qs = type0 init y x"
proof -
  obtain u v where uu: "u \<in> lang (Plus (Atom x) One)"
        and vv: "v \<in> lang (seq[Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x)), Atom y, Atom y])"
        and qsuv: "qs = u @ v"
        using assms
        by (auto simp: conc_def)
  have lenv: "length v mod 2 = 0 \<and> last v = y \<and> v\<noteq>[]"
  proof -
    from vv have "v \<in> ({[y]} @@ {[x]}) @@ star({[y]} @@ {[x]}) @@ {[y]} @@ {[y]}" by simp
    then obtain p q r where pqr: "v=p@q@r" and "p\<in>({[y]} @@ {[x]})"
              and q: "q \<in> star ({[y]} @@ {[x]})" and "r \<in>{[y]} @@ {[y]}" by (metis concE)
    then have rr: "p = [y,x]" "r=[y,y]" by auto
    with pqr have a: "length v = 4+length q" by auto

    have "last v = last r" using pqr rr by auto
    then have c: "last v = y" using rr by auto

    from q have b: "length q mod 2 = 0"
    apply(induct q rule: star_induct) by (auto)
    from a b c show ?thesis by auto
  qed

  from vv have "v \<in> lang (seq[Times (Atom y) (Atom x), Star(Times (Atom y) (Atom x))])
                          @@ lang (seq[Atom y, Atom y])" by (auto simp: conc_def)
  then obtain a b where aa: "a \<in> lang (seq[Times (Atom y) (Atom x), Star(Times (Atom y) (Atom x))])"
                    and "b \<in> lang (seq[Atom y, Atom y])"
                    and vab: "v = a @ b"
                      by(erule concE)

  from BIT_x[OF assms(1,2) uu] have u_t: "T\<^sub>p_on_rand' BIT (type0 init x y) (u @ v)  = T\<^sub>p_on_rand' BIT (type0 init x y) v"
      and u_c: "config'_rand BIT (type0 init x y) u = type0 init x y" by auto
  from BIT_b[OF assms(1,2) vv] have b_t: "T\<^sub>p_on_rand' BIT (type0 init x y) v  = 0.75 * length v - 0.5"
      and  b_c: "config'_rand BIT (type0 init x y) v = (type0 init y x)" by auto

  have BIT: "T\<^sub>p_on_rand' BIT (type0 init x y) qs  = 0.75 * length v - 0.5"
    by(simp add: qsuv u_t b_t)

  (* OPT *)

  from uu have uuu: "u=[] \<or> u=[x]" by auto
  have OPT: "T\<^sub>p [x,y] qs (OPT2 qs [x,y]) = (length v) div 2" apply(rule OPT2_B) by(fact)+

  from lenv have "v \<noteq> []"  "last v = y" by auto
  then have 1:  "last qs = y" using last_appendR qsuv by simp
  then have 2: "other (last qs) x y = x" unfolding other_def by simp

  show "T\<^sub>p_on_rand' BIT (type0 init x y) qs \<le> 1.75 * T\<^sub>p [x,y] qs (OPT2 qs [x,y])"
    using BIT OPT lenv by auto

  (* config *)

  show "config'_rand BIT (type0 init x y) qs = type0 init y x"
    by (auto simp add: config'_rand_append qsuv u_c b_c)
qed

lemma bit_b'': assumes
    "x \<noteq> y" "{x, y} = {x0, y0}" "BIT_inv s x [x0, y0]"
    "set qs \<subseteq> {x, y}"
    "qs \<in> lang (seq[Plus (Atom x) One, Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom y, Atom y])"
 shows
    "T\<^sub>p_on_rand' BIT s qs  \<le> 1.75 * T\<^sub>p [x,y] qs (OPT2 qs [x,y])
      \<and>  BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0]"
proof -
  from assms have f: "x0\<noteq>y0" by auto
  from assms(1,3) assms(2)[symmetric] have s: "s = type0 [x0,y0] x y"
    apply(simp add: BIT_inv2[OF f] other_def) by fast

  from assms(1,2) have kas: "[x,y] = [x0,y0] \<or> [x,y] = [y0,x0]" by auto

  from assms(5) have lqs: "last qs = y" by fastforce
  from assms(1,2) kas have BIT: "T\<^sub>p_on_rand' BIT s qs \<le> 1.75 * T\<^sub>p [x, y] qs (OPT2 qs [x, y])"
    unfolding s
    apply(safe)
      apply(rule bit_b)
        apply(simp) apply(simp) using assms(5) apply(simp)
      apply(rule bit_b)
        apply(simp) apply(simp) using assms(5) apply(simp)
  done

  from assms(1,2) kas have "config'_rand BIT s qs = type0 [x0, y0] y x"
    unfolding s
    apply(safe)
      apply(rule bit_b)
        apply(simp) apply(simp) using assms(5) apply(simp)
      apply(rule bit_b)
        apply(simp) apply(simp) using assms(5) apply(simp)
  done

  then have "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0]"
    apply(simp)
    using assms(1) kas lqs by(auto simp add: BIT_inv2 other_def)

  then show ?thesis using BIT s by simp
qed

lemma bit_b''': " a \<noteq> b \<Longrightarrow>
         {a, b} = {x, y} \<Longrightarrow>
         BIT_inv s a [x, y] \<Longrightarrow>
         set qs \<subseteq> {a, b} \<Longrightarrow>
         qs \<in> lang (seq[Plus (Atom x) One, Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom y, Atom y]) \<Longrightarrow>
         BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' BIT s qs = 1.5"
using bit_a[of a b x y] oops

subsubsection "Phase Form C"

lemma BIT_c: assumes "x \<noteq> y"
       "init \<in> {[x,y],[y,x]}"
    "v \<in> lang (seq [Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x)), Atom x])"
    shows "T\<^sub>p_on_rand' BIT (type0 init x y) v = 0.75 * length v - 0.5"
      and "config'_rand BIT  (type0 init x y) v = (type0 init x y)" (is ?C)
proof -
  have A: "x\<noteq>y"  using assms by auto

  from assms(3) have "v \<in> lang (seq[Times (Atom y) (Atom x), Star(Times (Atom y) (Atom x))])
                          @@ lang (seq[Atom x])" by (auto simp: conc_def)
  then obtain a b where aa: "a \<in> lang (seq[Times (Atom y) (Atom x), Star(Times (Atom y) (Atom x))])"
                      and "b \<in> lang (seq[Atom x])"
                      and vab: "v = a @ b"
                      by(erule concE)
  then have bb: "b=[x]" by auto
  from aa have lena: "length a > 0" by auto
  from vab bb have lenv: "length v = length a + 1" by auto

  from bit_yxyx assms(1,2) aa have stars: "T\<^sub>p_on_rand' BIT (type0 init x y) (a @ b)  = 0.75 * length a + T\<^sub>p_on_rand' BIT (type1 init x y) b"
                             and s2: "config'_rand BIT (type0 init x y) a = type1 init x y"  by fast+

  have t: "T\<^sub>p_on_rand' BIT (type1 init x y) b = 1/4"
    using assms(1,2) by (auto simp add: bb costBIT)

  have s: "config'_rand BIT  (type1 init x y) b = type0 init x y"
    using assms(1,2) by (auto simp add: bb oneBIT_step1x )

  have config: "config'_rand BIT  (type0 init x y) (a @ b) = type0 init x y"
    by (simp only: config'_rand_append s2 vab s)

  have calc: "3 * Suc (Suc (length a)) / 4 - 1 / 2 = 3 * (2+length a) / 4 - 1 / 2" by simp

  from t stars have "T\<^sub>p_on_rand' BIT (type0 init x y) (a @ b) = 0.75 * length a + 1/4" by auto
  then show "T\<^sub>p_on_rand' BIT  (type0 init x y) v = 0.75 * length v - 0.5" unfolding lenv
    by(simp add: vab ring_distribs del: add_2_eq_Suc')
  from config vab show ?C by simp
qed

lemma bit_c''1: assumes
    "x \<noteq> y" "{x, y} = {x0, y0}" "BIT_inv s x [x0, y0]"
    "set qs \<subseteq> {x, y}"
    "qs \<in> lang (seq[Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom x])"
 shows "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0] \<and>
          T\<^sub>p_on_rand' BIT s qs  = 0.75 * length qs - 0.5"
proof -
  from assms have f: "x0\<noteq>y0" by auto
  from assms(1,3) assms(2)[symmetric] have s: "s = type0 [x0,y0] x y"
    apply(simp add: BIT_inv2[OF f] other_def) by fast

  from assms(1,2) have kas: "[x,y] = [x0,y0] \<or> [x,y] = [y0,x0]" by auto

  from assms(5) have lqs: "last qs = x" by fastforce
  from assms(1,2) kas have BIT: "T\<^sub>p_on_rand' BIT s qs = 0.75 * length qs - 0.5"
    unfolding s
    apply(safe)
      apply(rule BIT_c)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
      apply(rule BIT_c)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
  done

  from assms(1,2) kas have "config'_rand BIT s qs = type0 [x0, y0] x y"
    unfolding s
    apply(safe)
      apply(rule BIT_c)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
      apply(rule BIT_c)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
  done

  then have config: "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0]"
    apply(simp)
    using assms(1) kas lqs by(auto simp add: BIT_inv2 other_def)

  show ?thesis using BIT config by simp
qed

lemma bit_c: assumes "x \<noteq> y"
      "init \<in> {[x,y],[y,x]}"
   "qs \<in> lang (seq[Plus (Atom x) One, Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom x])"
 shows  "T\<^sub>p_on_rand' BIT (type0 init x y) qs \<le> 1.75 * T\<^sub>p [x,y] qs (OPT2 qs [x,y])"
  and "config'_rand BIT (type0 init x y) qs = type0 init x y"
proof -
  obtain u v where uu: "u \<in> lang (Plus (Atom x) One)"
        and vv: "v \<in> lang (seq[Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x)), Atom x])"
        and qsuv: "qs = u @ v"
        using assms
        by (auto simp: conc_def)
  have lenv: "length v mod 2 = 1 \<and> length v \<ge> 3 \<and> last v = x"
  proof -
    from vv have "v \<in> ({[y]} @@ {[x]}) @@ star({[y]} @@ {[x]}) @@ {[x]}" by auto
    then obtain p q r where pqr: "v=p@q@r" and "p\<in>({[y]} @@ {[x]})"
              and q: "q \<in> star ({[y]} @@ {[x]})" and "r \<in> {[x]}" by (metis concE)
    then have rr: "p = [y,x]"  "r=[x]" by auto
    with pqr have a: "length v = 3+length q" by auto

    have "last v = last r" using pqr rr by auto
    then have c: "last v = x" using rr by auto

    from q have b: "length q mod 2 = 0"
    apply(induct q rule: star_induct) by (auto)
    from a b c show "length v mod 2 = 1 \<and> length v \<ge> 3 \<and> last v = x" by auto
  qed

  from vv have "v \<in> lang (seq[Times (Atom y) (Atom x), Star(Times (Atom y) (Atom x))])
                          @@ lang (seq[Atom x])" by (auto simp: conc_def)
  then obtain a b where aa: "a \<in> lang (seq[Times (Atom y) (Atom x), Star(Times (Atom y) (Atom x))])"
                      and "b \<in> lang (seq[Atom x])"
                      and vab: "v = a @ b"
                      by(erule concE)

  from BIT_x[OF assms(1,2) uu] have u_t: "T\<^sub>p_on_rand' BIT (type0 init x y)  (u @ v)  = T\<^sub>p_on_rand' BIT (type0 init x y) v"
      and u_c: "config'_rand BIT (type0 init x y) u = type0 init x y" by auto
  from BIT_c[OF assms(1,2) vv] have b_t: "T\<^sub>p_on_rand' BIT (type0 init x y) v  = 0.75 * length v - 0.5"
      and  b_c: "config'_rand BIT (type0 init x y) v = (type0 init x y)" by auto

  have BIT: "T\<^sub>p_on_rand' BIT (type0 init x y) qs  = 0.75 * length v - 0.5"
    by(simp add: qsuv u_t b_t)

  (* OPT *)

  from uu have uuu: "u=[] \<or> u=[x]" by auto
  from vv have vvv: "v \<in> lang (seq
          [Atom y, Atom x,
           Star (Times (Atom y) (Atom x)),
           Atom x])" by(auto simp: conc_def)
  have OPT: "T\<^sub>p [x,y] qs (OPT2 qs [x,y]) = (length v) div 2" apply(rule OPT2_C) by(fact)+

  from lenv have "v \<noteq> []"  "last v = x" by auto
  then have 1:  "last qs = x" using last_appendR qsuv by simp
  then have 2: "other (last qs) x y = y" unfolding other_def by simp

  have vgt3: "length v \<ge> 3" using lenv by simp
  have "T\<^sub>p_on_rand' BIT (type0 init x y) qs  = 0.75 * length v - 0.5" using BIT by simp
also
  have "\<dots> \<le> 1.75 * (length v - 1)/2"
  proof -
    have "10 + 6 * length v \<le> 7 * Suc (length v)
        \<longleftrightarrow> 10 + 6 * length v \<le> 7 * length v + 7" by auto
    also have "\<dots> \<longleftrightarrow> 3 \<le> length v" by auto
    also have "\<dots> \<longleftrightarrow> True" using vgt3 by auto
    finally have A: " 6 * length v - 4 \<le> 7 * (length v - 1)" by simp
    show ?thesis apply(simp) using A by linarith
  qed
also
  have "\<dots> = 1.75 * (length v div 2)"
  proof -
    from div_mult_mod_eq have "length v = length v div 2 * 2 + length v mod 2" by auto
    with lenv have "length v = length v div 2 * 2 + 1" by auto
    then have "(length v - 1) / 2 = length v div 2" by simp
    then show ?thesis by simp
  qed
also
  have "\<dots> = 1.75 * T\<^sub>p [x, y] qs (OPT2 qs [x, y])" using OPT by auto
finally
  show "T\<^sub>p_on_rand' BIT (type0 init x y) qs \<le> 1.75 * T\<^sub>p [x,y] qs (OPT2 qs [x,y])"
    using BIT OPT lenv   1 2  by auto

  (* config *)

  show "config'_rand BIT  (type0 init x y) qs  = type0 init x y"
    by (auto simp add: config'_rand_append qsuv u_c b_c)
qed

lemma bit_c'': assumes
    "x \<noteq> y" "{x, y} = {x0, y0}" "BIT_inv s x [x0, y0]"
    "set qs \<subseteq> {x, y}"
    "qs \<in> lang (seq[Plus (Atom x) One, Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom x])"
 shows
    "T\<^sub>p_on_rand' BIT s qs  \<le> 1.75 * T\<^sub>p [x,y] qs (OPT2 qs [x,y])
      \<and>  BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0]"
proof -
  from assms have f: "x0\<noteq>y0" by auto
  from assms(1,3) assms(2)[symmetric] have s: "s = type0 [x0,y0] x y"
    apply(simp add: BIT_inv2[OF f] other_def) by fast

  from assms(1,2) have kas: "[x,y] = [x0,y0] \<or> [x,y] = [y0,x0]" by auto

  from assms have lqs: "last qs = x" by fastforce
  from assms(1,2) kas have BIT: "T\<^sub>p_on_rand' BIT s qs \<le> 1.75 * T\<^sub>p [x, y] qs (OPT2 qs [x, y])"
    unfolding s
    apply(safe)
      apply(rule bit_c )
        apply(simp) apply(simp) using assms(5) apply(simp)
      apply(rule bit_c)
        apply(simp) apply(simp) using assms(5) apply(simp)
  done

  from assms(1,2) kas have "config'_rand BIT s qs = type0 [x0, y0] x y"
    unfolding s
    apply(safe)
      apply(rule bit_c)
        apply(simp) apply(simp) using assms(5) apply(simp)
      apply(rule bit_c)
        apply(simp) apply(simp) using assms(5) apply(simp)
  done

  then have "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0]"
    apply(simp)
    using assms(1) kas f lqs by(auto simp add: BIT_inv2 other_def)

  then show ?thesis using BIT s by simp
qed

lemma BIT_c2: assumes A: "x \<noteq> y"
       "init \<in> {[x,y],[y,x]}"
    "v \<in> lang (seq [Atom x, Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x)), Atom x])"
    shows "T\<^sub>p_on_rand' BIT (type0 init x y) v = 0.75 * (length v - 1) - 0.5" (is ?T)
     and "config'_rand BIT  (type0 init x y) v = (type0 init x y)" (is ?C)
proof -
  from assms(3) obtain w where  vw: "v = [x]@w" and
          w: "w \<in> lang (seq [Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x)), Atom x])"
          by(auto)
  have c1: "config'_rand BIT (type0 init x y) [x] = type0 init x y"
      using assms by(auto simp add: oneBIT_step)
  have t1: "T\<^sub>p_on_rand' BIT (type0 init x y) [x] = 0"
      using assms by(auto simp add: costBIT)
  show "T\<^sub>p_on_rand' BIT (type0 init x y) v
      = 0.75 * (length v - 1) - 0.5"
      unfolding vw apply(simp only: T_on_rand'_append c1 BIT_c[OF assms(1,2) w] t1)
        by (simp)
  show "config'_rand BIT (type0 init x y) v = (type0 init x y)"
    unfolding vw by(simp only: config'_rand_append c1 BIT_c[OF assms(1,2) w])
qed

lemma bit_c''2: assumes
    "x \<noteq> y" "{x, y} = {x0, y0}" "BIT_inv s x [x0, y0]"
    "set qs \<subseteq> {x, y}"
    "qs \<in> lang (seq[Atom x, Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom x])"
 shows "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0] \<and>
          T\<^sub>p_on_rand' BIT s qs  = 0.75 * (length qs - 1) - 0.5"
proof -
  from assms have f: "x0\<noteq>y0" by auto
  from assms(1,3) assms(2)[symmetric] have s: "s = type0 [x0,y0] x y"
    apply(simp add: BIT_inv2[OF f] other_def) by fast

  from assms(1,2) have kas: "[x,y] = [x0,y0] \<or> [x,y] = [y0,x0]" by auto

  from assms(5) have lqs: "last qs = x" by fastforce
  from assms(1,2) kas have BIT: "T\<^sub>p_on_rand' BIT s qs = 0.75 * (length qs-1) - 0.5"
    unfolding s
    apply(safe)
      apply(rule BIT_c2)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
      apply(rule BIT_c2)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
  done

  from assms(1,2) kas have "config'_rand BIT s qs = type0 [x0, y0] x y"
    unfolding s
    apply(safe)
      apply(rule BIT_c2)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
      apply(rule BIT_c2)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
  done

  then have config: "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0]"
    apply(simp)
    using assms(1) kas lqs by(auto simp add: BIT_inv2 other_def)

  show ?thesis using BIT config by simp
qed

subsubsection "Phase Form D"

lemma bit_d: assumes
    "x \<noteq> y" "{x, y} = {x0, y0}" "BIT_inv s x [x0, y0]"
    "set qs \<subseteq> {x, y}" "qs \<in> lang (seq [Atom x, Atom x])"
  shows "T\<^sub>p_on_rand' BIT s qs \<le> 175 / 10\<^sup>2 * real (T\<^sub>p [x, y] qs (OPT2 qs [x, y])) \<and>
    BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0] \<and>
     T\<^sub>p_on_rand' BIT s qs = 0"
proof -
  from assms have qs: "qs = [x,x]" by auto
  then have OPT: "T\<^sub>p [x, y] qs (OPT2 qs [x, y]) = 0" by (simp add: t\<^sub>p_def step_def)

  from assms have f: "x0\<noteq>y0" by auto
  from assms(1,3) assms(2)[symmetric] have s: "s = type0 [x0,y0] x y"
    apply(simp add: BIT_inv2[OF f] other_def) by fast

  from assms(1,2) have kas: "[x,y] = [x0,y0] \<or> [x,y] = [y0,x0]" by auto

  have BIT: "T\<^sub>p_on_rand' BIT (type0 [x0,y0] x y) qs = 0"
    using kas assms(1,2) by (auto simp add: qs oneBIT_step costBIT)

  have lqs: "last qs = x" "last qs \<in> {x0,y0}" using assms(2,4) qs by auto

  have inv: "config'_rand BIT s qs = type0 [x0, y0] x y"
    using kas assms(1,2) by (auto simp add: qs s  oneBIT_step0x)

  then have "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0]"
    apply(simp)
    using assms(1) kas f lqs by(auto simp add: BIT_inv2 other_def)

  then show ?thesis using BIT s by(auto)
qed

lemma bit_d': assumes
    "x \<noteq> y" "{x, y} = {x0, y0}" "BIT_inv s x [x0, y0]"
    "set qs \<subseteq> {x, y}" "qs \<in> lang (seq [Atom x, Atom x])"
  shows "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0] \<and>
     T\<^sub>p_on_rand' BIT s qs = 0"
using bit_d[OF assms] by blast

subsection "Phase Partitioning"

lemma BIT_inv_initial: assumes "(x::nat) \<noteq> y"
    shows "BIT_inv (map_pmf (Pair [x, y]) (fst BIT [x, y])) x [x, y]"
using assms(1) apply(simp add: BIT_inv2 BIT_init_def type0_def)
      apply(simp add: map_pmf_def other_def bind_return_pmf bind_assoc_pmf)
      using bind_commute_pmf by fast

lemma D'': assumes "qs \<in> Lxx a b"
    "a \<noteq> b" "{a, b} = {x, y}" "BIT_inv s a [x, y]"
    "set qs \<subseteq> {a, b}"
 shows "T\<^sub>p_on_rand' BIT s qs \<le> 175 / 10\<^sup>2 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and>
    BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y]"
 apply(rule LxxE[OF assms(1)])
  using bit_d[OF assms(2-5)] apply(simp)
  apply(rule bit_b''[OF assms(2-5)]) apply(simp)
  apply(rule bit_c''[OF assms(2-5)]) apply(simp)
  using bit_a[OF assms(2-5)] apply(simp)
  done

theorem BIT_175comp_on_2:
    assumes "(x::nat) \<noteq> y" "set \<sigma> \<subseteq> {x,y}"
     shows "T\<^sub>p_on_rand BIT [x,y] \<sigma>  \<le> 1.75 * real (T\<^sub>p_opt [x,y] \<sigma>) + 1.75"
proof (rule Phase_partitioning_general[where P=BIT_inv], goal_cases)
  case 4
  show "BIT_inv (map_pmf (Pair [x, y]) (fst BIT [x, y])) x [x, y]"
   by (rule BIT_inv_initial[OF assms(1)])
next
  case (5 a b qs s)
  then show ?case by(rule D'')
qed (simp_all add: assms)

end

subset_name: curated


text:
{\bf Problem.} If $x = 101$ and $x^3y - 2x^2y + xy = 101000$, what is the value of $y$?
{\bf Level.} Level 2
{\bf Type.} Intermediate Algebra
{\bf Solution.} Note that the left hand side of the second equation can be factored: $(x^2 - 2x + 1)xy = (x - 1)^2xy = 101000$. We are given that $x = 101$, so we have $(101- 1)^2(101)y = 1010000y = 101000$. It follows that $y = \boxed{\frac{1}{10}}$.

set_name: MATH