\documentclass{beamer}
\usepackage[utf8]{inputenc}
%\usepackage{polski}
\newtheorem{twierdzenie}{Twierdzenie}
\newtheorem{definicja}{Definicja}
\usepackage{tikz}
\usepackage{pgfplots}
\usepackage{datapie}
\usetikzlibrary{patterns}
\usetikzlibrary{arrows}
\usetikzlibrary{positioning}
\usetikzlibrary{decorations.pathmorphing}
\usetikzlibrary{decorations.pathreplacing}
\usetikzlibrary{decorations.text}
\usetikzlibrary{decorations.footprints}
\usetikzlibrary{shapes.symbols}
\usetikzlibrary{shapes.arrows}
\pgfplotsset{compat=1.10}
\DeclareMathOperator{\Hol}{Hol}
\DeclareMathOperator{\LI}{LI}
\DeclareMathOperator{\sgn}{sgn}
\DeclareMathOperator{\ord}{ord}
\DeclareMathOperator{\Cl}{Cl}
\global\long\def\BC{\mathbb{C}}
\global\long\def\BNZ{\mathbb{N}_{0}}
\global\long\def\NPI{\mathbb{Z}\setminus\mathbb{N}}
\global\long\def\BN{\mathbb{N}}
\global\long\def\BZ{\mathbb{Z}}
\global\long\def\BQ{\mathbb{Q}}
\global\long\def\BR{\mathbb{R}}
\global\long\def\BM{\mathbb{M}}
\global\long\def\BP{\mathbb{P}}
\global\long\def\BE{\mathbb{E}}
\newcommand{\w}{\overline{w}}
\usepackage{ragged2e}
\newenvironment{tikzexample}[1]{\def\temp{#1}\centering}{\par\bigskip\temp\newpage}
\newcommand{\nextexample}{\par\vspace{24pt}}
\apptocmd{\frame}{}{\justifying}{}
\makeatletter
\newcommand{\cs}[1]{\texttt{\@backslashchar #1}}
\makeatother

% \usetheme{Frankfurt}
 \usetheme{Warsaw}
% \usetheme{Madrid}
% \usetheme{Bergen}
% \usetheme{Antibes}
% \usetheme{Montpellier}
% \usetheme{Berkeley}
% \usetheme{Ilmenau}
% \usetheme{Singapore}

% \usecolortheme{crane}

\AtBeginSection[] % Do nothing for \section*
{
\begin{frame}<beamer>
  \frametitle{Spis treści}
  \tableofcontents[currentsection]
\end{frame}
}
\begin{document}

\title{Shiroin package - function \textit{prove}}
\author{Grzegorz Adamski}
\date{\today}

\begin{frame}
  \maketitle  
\end{frame}
\begin{frame}{Jensen and weighted AM-GM inequalities}\begin{block}{Jensen inequality}
If $f:\BR^k\to \BR$ is a convex function, $v_1,...,v_n\in \BR^k$, $w_1,...,w_n>0$ and $w=\sum_{i=1}^n w_i$, then 
$$\frac{\sum_{i=1}^n w_i f(v_i)}{w}\ge f\left(\frac{\sum_{i=1}^n v_i}{w} \right).$$
\end{block}
If $f(w_1,w_2,...,w_n)=\prod_{i=1}^n x_i^{w_i}$ for some $x_1,...,x_n>0$, then we've got
$$\frac{\sum_{i=1}^n w_i x_i}{w}\ge \sqrt[w]{\prod_{i=1}^n x_i^{w_i}}. $$
This is called inequality of weighted arithmetic and geometric means (AM-GM inequality for short).
We will use an equivalent inequality
$$\sum_{i=1}^n w_i x_i\ge w\prod_{i=1}^n x_i^{w_i/w}. $$
\end{frame}
\begin{frame}{Example}
\begin{block}{}
Let $a,b>0$. Prove that
$$30a^2b^2+60ab^4\le 48a^3+56b^6.$$
\end{block}
\pause
We will use AM-GM inequality. Let $x_1=a^3$, $x_2=b^6$. We need to find such $w_1,w_2,w_3,w_4$, that
$$30a^2b^2\le w_1a^3+w_2b^6$$
$$60ab^4\le w_3 a^3+w_4 b^6$$
To fulfill assumptions of AM-GM, we need:
$w_1,w_2,w_3,w_4\ge 0$
$$w_1+w_2=30$$
$$w_3+w_4=60$$
$$(a^3)^{w_1/30}(b^6)^{w_2/30}=a^2b^2$$
$$(a^3)^{w_3/30}(b^6)^{w_4/30}=ab^4$$
We also need $w_1+w_3\le 48$ and $w_2+w_4\le 56$
\end{frame}
\begin{frame}{Example}
$$w_1,w_2,w_3,w_4\ge 0$$
$$w_1+w_2=30$$
$$w_3+w_4=60$$
$$3w_1=30\cdot 2$$
$$6w_2=30\cdot 2$$
$$3w_3=30\cdot 1$$
$$6w_4=30\cdot 4$$
$$w_1+w_3\le 48$$
$$w_2+w_4\le 56$$
All these equations and inequalities are linear, so $w_1,w_2,w_3,w_4$ can be found using linear programming (in this case they can be found directly from equations, but this is not true in general case).
\end{frame}
\begin{frame}{Problem}
\begin{block}{}
Prove that for all $x>0$ $$4x^2 \le 4x+x^3.$$
\end{block}
This inequality follows directly from AM-GM. But we can't use the same algorithm as in the previous problem.

Let's try to do this. We want to find $w_1,w_2\ge 0$ such that
$$4x^2\le w_1x+w_2x^3$$
$$w_1+w_2=4$$
$$1w_1+3w_2=4\cdot 2$$
$$w_1\le 4$$
$$w_2\le 1$$
From the equations we can find that $w_1=w_2=2$. But $w_2\le 1$, so there is no solution.
\end{frame}
\begin{frame}{Substitutions}
This problem can be solved by substituting $x$ by $2y$. This way the problem can be reformulated.
\begin{block}{}
Prove that for all $y>0$ $$16y^2 \le 8x+8x^3.$$
\end{block}
This problem can be solved using the main algorithm.
\end{frame}
\begin{frame}{Dealing with real coefficients in the proof}
\begin{block}{}
Prove that for all $x>0$ $$4x^2 \le 1+2x+3x^3+4x^4.$$
\end{block}
This time the biggest problem is not finding a solution, but finding one with nice coefficients.
For example, using weighted AM-GM  we can show that
$$4x^2\le 2x+2x^3$$
or 
$$4x^2\le 1+x+x^3+x^4.$$
but we can also find a less nice solution like
$$4x^2\le 0.657238842+0.342761158x+0.342761158x^3+0.657238842x^4.$$
\end{frame}
\begin{frame}{Dealing with real coefficients in the proof}
The simplest idea is to specify a goal function with random coefficients. Algorithm choose then (almost surely) an extreme point from the set of feasible solutions.
\end{frame}
\begin{frame}{Set of solutions}
\begin{center}
\begin{figure}
\includegraphics[scale=2]{solset2.png}

\caption{Set of solutions projected onto the plane $w_3w_4$. $w_1,w_2$ are defined as $w_1=2w_3+3w_4-4$, $w_2=8-3w_3-4w_4$}
\end{figure}
\end{center}
\end{frame}
\begin{frame}{Function \textit{prove} - algorithm}
\begin{enumerate}
    \item Find a proof with real coefficients.\label{itm:first}
    \item Check which inequalities have integer coefficients.
    \item Subtract them from original inequality and go back to \ref{itm:first} with the new inequality.
\end{enumerate}
The loop breaks when all coefficients are integer or when it has run fixed amount of times.
\end{frame}
\end{document}