text:
\section{Introduction}
\label{sec:introduction}
Adaptive gradient methods such as \adagrad/~\citep{duchi2011adaptive}, \rmsprop/~\citep{tieleman2012lecture}, \adadelta/~\citep{zeiler2012adadelta}, \adam/~\citep{kingma2014adam}, and \amsgrad/~\citep{reddi2019convergence} are popular optimizers for training deep neural networks~\citep{goodfellow2016deep}.
These methods scale well and exhibit good performance across problems, making them the default choice for many machine learning applications. Theoretically, these methods are usually studied in the non-smooth, online convex optimization setting~\citep{duchi2011adaptive, reddi2019convergence} with recent extensions to the strongly-convex~\citep{mukkamala2017variants, wang2019sadam,xie2019linear} and non-convex settings~\citep{li2018convergence, ward2018adagrad,zhou2018convergence,chen2018convergence,wu2019global, defossez2020convergence,staib2019escaping}.
Further, an online-to-batch reduction gives guarantees similar to stochastic gradient descent (SGD) in the offline setting~\citep{cesa2004generalization, hazan2014beyond, levy2018online}.

While constant step-size \adagrad/ has been shown to be ``universal'' as it converges with any step-size in the stochastic smooth and non-smooth settings~\citep{levy2018online},
its empirical performance is often disappointing when training deep models~\citep{kingma2014adam}.
Improving the empirical performance was indeed the main motivation behind \adam/ and other methods~\citep{tieleman2012lecture, zeiler2012adadelta} that followed \adagrad/. However, there are several discrepancies between the theory and application of these methods. Although the theory advocates for using decreasing step-sizes for \adam/, \amsgrad/ and its variants~\citep{kingma2014adam, reddi2019convergence}, a constant step-size is typically used in practice. Similarly, the standard analyses of these methods requires a decreasing momentum parameter~\citep{reddi2019convergence}, which is also fixed in practice. Consequently, there are no theoretical results corroborating the adaptivity to the step-size for the \adam/ variants used in practice.

Furthermore, adaptive gradient methods are typically used to train highly expressive, over-parameterized models~\citep{zhang2016understanding, liang2018just} capable of \emph{interpolating} the data.
However, the standard theoretical analyses do not take advantage of these additional structural properties.
A recent line of work~\citep{schmidt2013fast, jain2017accelerating, ma2018power, cevher2018linear, vaswani2019fast, vaswani2019painless,wu2019global, liu2020accelerating, loizou2020stochastic} focuses on the convergence of SGD in this interpolation setting.
For a finite-sum of loss functions, interpolation implies that all the functions in the sum are minimized at the same solution.
Under this additional assumption, these works show that constant step-size SGD converges at a faster rate for both convex and non-convex smooth functions.

\subsection{Background and Contributions}
\label{sec:contributions}
As a first step to reconcile the theory and practice of adaptive gradient methods, we focus on their convergence in a simplistic setting - minimizing smooth, convex loss functions using models capable of interpolating the data. We study two practical methods - constant step-size \adagrad/, and \amsgrad/ with a constant step-size and constant momentum. In particular, we make the contributions below.

\textbf{Constant step-size \adagrad/.} For smooth, convex functions,~\citet{levy2018online} prove that constant step-size \adagrad/ adapts to the smoothness and gradient noise, resulting in an $\bigO(\nicefrac{1}{T} + \nicefrac{\zeta}{\m!\sqrt{T}})$ convergence rate, where $T$ is the number of iterations and $\zeta^2$ is a global bound on the variance in the stochastic gradients. This convergence rate matches that of SGD under the same setting~\citep{moulines2011non}.

\textit{Contribution.} In~\cref{sec:adagrad-constant}, we show that constant step-size \adagrad/ also adapts to the degree of interpolation and prove an $\bigO(\nicefrac{1}{T} + \nicefrac{\sigma}{\m!\sqrt{T}})$ rate, where $\sigma$ is the extent to which interpolation is violated. Similarly to the result of ~\citet{levy2018online}, this holds for any bounded constant step-size.

\textbf{\amsgrad/ with constant step-size and momentum.}
Unlike \adagrad/, the preconditioner for \amsgrad/ does not have nice structural properties~\cite{defossez2020convergence},
making it difficult to prove strong guarantees.
To analyze the convergence of \amsgrad/,
we make the simplifying assumption that its corresponding preconditioner remains bounded.

\textit{Contribution.} With this additional assumption,
we show that \amsgrad/ with a constant step-size and momentum converges to the minimizer
at a $\bigO(\nicefrac{1}{T})$ rate under interpolation (\cref{sec:amsgrad-constant}).
Unlike \adagrad/, this result requires a specific range of step-sizes that depend on the smoothness of the problem.
In general, constant step-size \amsgrad/ converges to a neighbourhood of the solution,
attaining an $\bigO(\nicefrac{1}{T} + \sigma^2)$ rate,
matching the rate of constant step-size SGD~\citep{schmidt2013fast, vaswani2019fast}.
For over-parameterized models,
$\sigma^2 \approx 0$ and this result provides some justification for the faster
($\bigO(\nicefrac{1}{T})$ vs. $\bigO(\nicefrac{1}{\m!\sqrt{T}})$)
convergence of the \amsgrad/ variants used in practice.

\textbf{Sensitivity of \adagrad/ and \amsgrad/.} Although \adagrad/ converges at the same asymptotic rate for any step-size, it is unclear how the choice of step-size affects its practical performance. On the other hand, our theoretical results for convex minimization indicate that \amsgrad/ is sensitive to the step-size, converging only for a specific range that depends on typically unknown problem-dependent constants.

\textit{Contribution.} In~\cref{sec:sensitivity}, we empirically demonstrate this sensitivity to the step-size for both methods. In particular, we show that even for a convex problem satisfying interpolation, such as logistic regression on linearly separable data, the choice of step-size has a big impact on the performance of both \adagrad/ and \amsgrad/, questioning their adaptivity.

\textbf{\adagrad/ and \amsgrad/ with an adaptive step-size.} To improve the robustness to the step-size, we use recent techniques~\citep{vaswani2019fast, loizou2020stochastic} that automatically determine the step-size for each iteration of SGD. These works use stochastic variants of the classical Armijo line-search~\citep{armijo1966minimization} and Polyak step-size~\citep{polyak1963gradient} and prove their convergence under interpolation.

\textit{Contribution.} In~\cref{sec:adaptive}, we modify these techniques for their use with adaptive gradient methods. In particular, we show that a variant of stochastic line-search (SLS) can be used to set the step-size in each iteration of \adagrad/. SLS enables \adagrad/ to adapt to the smoothness of the underlying function, while retaining its favourable convergence properties (\cref{sec:adagrad-adaptive}). Under the same bounded preconditioner assumption, we prove that \amsgrad/ used with a variant of SLS or stochastic Polyak step-size (SPS) can match the convergence rate of its constant step-size counterpart, but without requiring the knowledge of problem-dependent constants (\cref{sec:amsgrad-adaptive}). For the logistic regression example considered in~\cref{sec:sensitivity}, we observe that using SLS/SPS improves the convergence of both \adagrad/ and \amsgrad/, matching or out-performing the best constant step-size.

\textbf{Large-scale experiments.} To demonstrate the empirical advantage of SLS/SPS beyond convex minimization, we consider both convex and non-convex tasks, ranging from binary classification with a kernel mapping to multi-class classification with standard deep network architectures (\cref{sec:experiments}). We benchmark the performance of \adagrad/ and \amsgrad/ equipped with SLS, and compare against tuned \adam/ and recently proposed variants~\citep{luo2019adaptive, liu2019variance}. To disentangle the effects of the step-size and the adaptive preconditioner, we compare against SGD using SLS~\citep{vaswani2019painless} and SPS~\citep{loizou2020stochastic}. We find that both the step-size and the adaptive preconditioner contribute to good performance, with the SLS variants of \adagrad/ and \amsgrad/ consistently outperforming other methods. Furthermore, for the experiments with deep neural networks, these variants generalize better than SGD, demonstrating the effect of the step-size in the generalization performance~\citep{nar2018step}.


TITLE: Probability that the final molecule removed from urn $ 1 $ is red
QUESTION [4 upvotes]: $ \textbf{Question:} $ (from Ross' $ \textit{A First Course in Probability}) $ Urn $ 1 $ initially has $ n $ red molecules and urn $ 2 $ has $ n $ blue molecules. Molecules are randomly removed from urn $ 1 $ in the following manner: After each removal from urn $ 1, $ a molecule is taken from urn $ 2 $ (if urn $ 2 $ has any molecules) and placed in urn $ 1. $ The process continues until all the molecules have been removed. (Thus, there are $ 2n $ removals in all.) What is the probability that the final molecule removed from urn $ 1 $ is red?
I have one question about a step in the solution that is confusing me so any help would be appreciated.
$ \textbf{Solution:} $ Focus attention on any particular red molecule, and let $ F $ be the event that this molecule is the ﬁnal one selected. Now, in order for $ F $ to occur, the molecule in question must still be in the urn after the ﬁrst $ n $ molecules have been removed (at which time urn $ 2 $ is empty).
My question is in the previous sentence why is it $ n $ but not $ 2n -1? $ In order for $ F $ to happen, doesn't that mean the selected molecule must still remain in urn $ 1 $ after $ 2n - 1 $ molecules have been removed?
$ \dots $ The proof continues and the desired probability is $ \displaystyle \left(1 - \frac{1}{n} \right)^n $

REPLY [0 votes]: I deem it would be of general interest
to develop this scheme in a step-by-step fashion for the more general case in which
$k$ extractions are made from an urn  containing $n$ red molecules at start ($1 \leqslant n$),
and inserting one blue molecule after each extraction.
We can then construct the $\left( {0,\; \ldots ,\;n} \right) \times \left( {0,\; \ldots ,\;n} \right)$  transition matrix, giving the probability of getting
$m(k)$ blue molecules at the $k$-th extraction, given that there are $m(k-1)$
blue molecules resulting from precedent extractions, which will clearly be:
$$
\overline {\mathbf{T}_{\,\mathbf{n}} }  = \;\left[ {\begin{array}{*{20}c}
   {m_{\,k - 1} \backslash m_{\,k} } &| &  0 & 1 & 2 &  \cdots  & {n - 1} & n  \\
\hline
   0 &| &  {0/n} & {n/n} & {} & {} & {} & {}  \\
   1 &| &  {} & {1/n} & {\left( {n - 1} \right)/n} & {} & {} & {}  \\
   2 &| &  {} & {} & {2/n} &  \ddots  & {} & {}  \\
    \vdots  &| &  {} & {} & {} &  \ddots  & {} & {}  \\
   {n - 1} &| &  {} & {} & {} & {} & {\left( {n - 1} \right)/n} & {1/n}  \\
   n &| &  {} & {} & {} & {} & {} & {n/n}  \\
 \end{array} } \right]
$$
where empty cells contain $0$, and
$\mathbf{T}_{\,\mathbf{n}}  = \overline {\overline {\mathbf{T}_{\,\mathbf{n}} } }  = \text{transpose}\left( {\overline {\mathbf{T}_{\,\mathbf{n}} } } \right)$
So, representing the probabilities of having $0,\; \ldots ,\;n$ blue molecules by the column vector $\mathbf{m}_{\,\mathbf{n}} \left( k \right)$, we can write:
$$
\mathbf{m}_{\,\mathbf{n}} \left( k \right) = \mathbf{T}_{\,\mathbf{n}} \;\mathbf{m}_{\,\mathbf{n}} \left( {k - 1} \right) = \mathbf{T}_{\,\mathbf{n}} ^{\,\mathbf{k}} \;\mathbf{m}_{\,\mathbf{n}} \left( 0 \right) = \mathbf{T}_{\,\mathbf{n}} ^{\,\mathbf{k}} \;\left[ {\begin{array}{*{20}c}
   1  \\
   0  \\
    \vdots   \\
   0  \\
 \end{array} } \right]
$$
The interesting fact is that the matrix $\mathbf{T}_{\,\mathbf{n}} $ diagonalizes nicely into:
$$
\mathbf{T}_{\,\mathbf{n}}  = \mathbf{C}_{\,\mathbf{n}} \;\left( {\left( {i/n} \right) \circ \mathbf{I}_{\,\mathbf{n}} } \right)\;\mathbf{C}_{\,\mathbf{n}} ^{\, - \,\mathbf{1}}  = \mathbf{C}_{\,\mathbf{n}} \;\left( {\left( {i/n} \right) \circ \mathbf{I}_{\,\mathbf{n}} } \right)\;\mathbf{C}_{\,\mathbf{n}}
$$
where the matrix in the centre indicates the diagonal matrix
$$
\left( {\left( {i/n} \right) \circ \mathbf{I}_{\,\mathbf{n}} } \right) = \left[ {i/n\;\delta _{\,i,\,j} } \right]_{\,\mathbf{n}}
$$
while the matrix $\mathbf{C}_{\,\mathbf{n}} $ represents
$$
\mathbf{C}_{\,\mathbf{n}}  = \mathbf{C}_{\,\mathbf{n}} ^{\, - \,\mathbf{1}}  = \left[ {\left( { - 1} \right)^{\,i} \left( \begin{gathered}
  n - j \\
  n - i \\
\end{gathered}  \right)} \right]_{\,\mathbf{n}}
$$
Therefore
$$
\begin{gathered}
  \mathbf{m}_{\,\mathbf{n}} \left( k \right) = \mathbf{T}_{\,\mathbf{n}} ^{\,\mathbf{k}} \;\mathbf{m}_{\,\mathbf{n}} \left( 0 \right) = \mathbf{C}_{\,\mathbf{n}} \;\left( {\left( {i/n} \right) \circ \mathbf{I}_{\,\mathbf{n}} } \right)^{\,\mathbf{k}} \;\mathbf{C}_{\,\mathbf{n}} ^{\, - \,\mathbf{1}} \;\mathbf{m}_{\,\mathbf{n}} \left( 0 \right) =  \hfill \\
   = \mathbf{C}_{\,\mathbf{n}} \;\left( {\left( {i/n} \right)^{\,k}  \circ \mathbf{I}_{\,\mathbf{n}} } \right)\;\mathbf{C}_{\,\mathbf{n}} \;\mathbf{m}_{\,\mathbf{n}} \left( 0 \right) =  \hfill \\
   = \left[ {\sum\limits_{0\, \leqslant \,l\, \leqslant \,n} {\left( { - 1} \right)^{\,i} \left( \begin{gathered}
  n - l \\
  n - i \\
\end{gathered}  \right)\left( {l/n} \right)^{\,k} \left( { - 1} \right)^{\,l} \left( \begin{gathered}
  n \\
  n - l \\
\end{gathered}  \right)} } \right]_{\,\mathbf{n}}  =  \hfill \\
   = \left[ {\sum\limits_{0\, \leqslant \,l\,\left( { \leqslant \,i} \right)} {\left( { - 1} \right)^{\,i - l} \left( \begin{gathered}
  n \\
  n - i \\
\end{gathered}  \right)\left( \begin{gathered}
  i \\
  l \\
\end{gathered}  \right)\left( {l/n} \right)^{\,k} } } \right]_{\,\mathbf{n}}  =  \hfill \\
   = \left[ {\frac{1}
{{n^{\,k} }}\left( \begin{gathered}
  n \\
  i \\
\end{gathered}  \right)\sum\limits_{0\, \leqslant \,l\,\left( { \leqslant \,i} \right)} {\left( { - 1} \right)^{\,i - l} \left( \begin{gathered}
  i \\
  l \\
\end{gathered}  \right)l^{\,k} } } \right]_{\,\mathbf{n}}  =  \hfill \\
   = \left[ {\frac{{i!}}
{{n^{\,k} }}\left( \begin{gathered}
  n \\
  i \\
\end{gathered}  \right)\left\{ \begin{gathered}
  k \\
  i \\
\end{gathered}  \right\}} \right]_{\,\mathbf{n}}  = \left[ {\frac{{n!}}
{{n^{\,k} \left( {n - i} \right)!}}\left\{ \begin{gathered}
  k \\
  i \\
\end{gathered}  \right\}} \right]_{\,\mathbf{n}}  \hfill \\
\end{gathered}
$$
Now, if after $k$ extractions with replacement, ending with $m_k$ blue molecules,
we extract (without replacement) all the $n$ balls from the urn and ask for the probability of the last to be red, that will be:
$$
\frac{{p(k,n)}}
{{p\left( {m_{\,k} } \right)}} = \frac{{\left( \begin{gathered}
  n - 1 \\
  m_{\,k}  \\
\end{gathered}  \right)}}
{{\left( \begin{gathered}
  n \\
  m_{\,k}  \\
\end{gathered}  \right)}} = \frac{{n - m_{\,k} }}
{n}\quad \left| \begin{gathered}
  \;0 \leqslant m_{\,k}  \leqslant n \hfill \\
  \;1 \leqslant n \hfill \\
\end{gathered}  \right.
$$
So, finally we arrive at:
$$
\begin{gathered}
  p(k,n) = \frac{1}
{{n^{\,k} }}\sum\limits_{0\, \leqslant \,l\,\left( { \leqslant \,n} \right)} {\left( {\frac{{n - l}}
{n}} \right)\frac{{n!}}
{{\left( {n - l} \right)!}}\left\{ \begin{gathered}
  k \\
  l \\
\end{gathered}  \right\}}  =  \hfill \\
   = \frac{1}
{{n^{\,k} }}\sum\limits_{0\, \leqslant \,l\,\left( { \leqslant \,n} \right)} {\left\{ \begin{gathered}
  k \\
  l \\
\end{gathered}  \right\}\left( {n - 1} \right)^{\,\underline {\,l\,} } }  = \left( {\frac{{n - 1}}
{n}} \right)^{\,k}  \hfill \\
\end{gathered}
$$
which confirms and generalize the formula already given.


text:
horizon := 0;;

let SUC_INJ_1 = thm `;
  now
    now [1]
      let m n be num;
      now [2]
        assume mk_num (IND_SUC (dest_num m)) =
               mk_num (IND_SUC (dest_num n)) [3];
        now [4]
          let p be num;
          NUM_REP (dest_num p) [5]
            by REWRITE_TAC[fst num_tydef; snd num_tydef] ;
          thus NUM_REP (IND_SUC (dest_num p))
            by MATCH_MP_TAC (CONJUNCT2 NUM_REP_RULES) from 5;
        end;
        !p. NUM_REP (IND_SUC (dest_num p)) [6] by GEN_TAC from 4;
        now [7]
          assume !p. dest_num (mk_num (IND_SUC (dest_num p))) =
                     IND_SUC (dest_num p) [8];
          mk_num (dest_num m) = mk_num (dest_num n) ==> m = n [9]
            by REWRITE_TAC[fst num_tydef];
          dest_num m = dest_num n ==> m = n [10]
            by DISCH_THEN(MP_TAC o AP_TERM (parse_term "mk_num")) from 9;
          thus dest_num (mk_num (IND_SUC (dest_num m))) =
               dest_num (mk_num (IND_SUC (dest_num n)))
               ==> m = n by ASM_REWRITE_TAC[IND_SUC_INJ],8 from 10;
        end;
        (!p. dest_num (mk_num (IND_SUC (dest_num p))) =
               IND_SUC (dest_num p))
          ==> dest_num (mk_num (IND_SUC (dest_num m))) =
              dest_num (mk_num (IND_SUC (dest_num n)))
          ==> m = n [11] by DISCH_TAC from 7;
        (!p. NUM_REP (IND_SUC (dest_num p)))
          ==> dest_num (mk_num (IND_SUC (dest_num m))) =
              dest_num (mk_num (IND_SUC (dest_num n)))
          ==> m = n [12] by REWRITE_TAC[fst num_tydef; snd num_tydef] from 11;
        dest_num (mk_num (IND_SUC (dest_num m))) =
          dest_num (mk_num (IND_SUC (dest_num n)))
          ==> m = n [13]
            by SUBGOAL_THEN (parse_term "!p. NUM_REP (IND_SUC (dest_num p))")
              MP_TAC from 6,12;
        thus m = n
          by POP_ASSUM(MP_TAC o AP_TERM (parse_term "dest_num")),3 from 13;
      end;
      mk_num (IND_SUC (dest_num m)) = mk_num (IND_SUC (dest_num n))
        ==> m = n [14] by DISCH_TAC from 2;
      now [15]
        assume m = n [16];
        thus mk_num (IND_SUC (dest_num m)) =
             mk_num (IND_SUC (dest_num n)) by ASM_REWRITE_TAC[],16;
      end;
      m = n
        ==> mk_num (IND_SUC (dest_num m)) =
            mk_num (IND_SUC (dest_num n)) [17] by DISCH_TAC from 15;
      mk_num (IND_SUC (dest_num m)) = mk_num (IND_SUC (dest_num n)) <=>
        m = n [18] by EQ_TAC from 14,17;
      thus SUC m = SUC n <=> m = n by REWRITE_TAC[SUC_DEF] from 18;
    end;
    thus !m n. SUC m = SUC n <=> m = n by REPEAT GEN_TAC from 1;
  end;
`;;

let SUC_INJ_2 = thm `;
  !m n. SUC m = SUC n <=> m = n [1]
  proof
    let m n be num;
    mk_num (IND_SUC (dest_num m)) = mk_num (IND_SUC (dest_num n))
    ==> m = n [2]
    proof
      assume mk_num (IND_SUC (dest_num m)) =
             mk_num (IND_SUC (dest_num n)) [3];
      !p. NUM_REP (IND_SUC (dest_num p)) [4]
      proof
        let p be num;
        NUM_REP (dest_num p) [5]
          by REWRITE_TAC[fst num_tydef; snd num_tydef];
      qed by MATCH_MP_TAC (CONJUNCT2 NUM_REP_RULES) from 5;
      (!p. dest_num (mk_num (IND_SUC (dest_num p))) =
           IND_SUC (dest_num p))
      ==> dest_num (mk_num (IND_SUC (dest_num m))) =
          dest_num (mk_num (IND_SUC (dest_num n)))
      ==> m = n [6]
      proof
        assume !p. dest_num (mk_num (IND_SUC (dest_num p))) =
                   IND_SUC (dest_num p) [7];
        mk_num (dest_num m) = mk_num (dest_num n) ==> m = n [8]
          by REWRITE_TAC[fst num_tydef];
        dest_num m = dest_num n ==> m = n [9]
          by DISCH_THEN(MP_TAC o AP_TERM (parse_term "mk_num")) from 8;
      qed by ASM_REWRITE_TAC[IND_SUC_INJ],* from 9;
      (!p. NUM_REP (IND_SUC (dest_num p)))
      ==> dest_num (mk_num (IND_SUC (dest_num m))) =
          dest_num (mk_num (IND_SUC (dest_num n)))
      ==> m = n [10] by REWRITE_TAC[fst num_tydef; snd num_tydef] from 6;
      dest_num (mk_num (IND_SUC (dest_num m))) =
      dest_num (mk_num (IND_SUC (dest_num n)))
      ==> m = n [11]
        by SUBGOAL_THEN (parse_term "!p. NUM_REP (IND_SUC (dest_num p))")
          MP_TAC
        from 4,10;
    qed by POP_ASSUM(MP_TAC o AP_TERM (parse_term "dest_num")),3 from 11;
    m = n
    ==> mk_num (IND_SUC (dest_num m)) = mk_num (IND_SUC (dest_num n)) [12]
    proof
      assume m = n [13];
    qed by ASM_REWRITE_TAC[],*;
    mk_num (IND_SUC (dest_num m)) = mk_num (IND_SUC (dest_num n)) <=>
    m = n [14] by EQ_TAC from 2,12;
  qed by REWRITE_TAC[SUC_DEF] from 14;`;;

let num_INDUCTION_ = thm `;
  now [1]
    let P be num->bool;
    let n be num;
    assume P _0;
    assume !n. P n ==> P (SUC n);
    now [2]
      let i be ind;
      assume NUM_REP i;
      assume P (mk_num i);
      NUM_REP i [3] by ASM_REWRITE_TAC[],*;
      thus NUM_REP (IND_SUC i)
        by MATCH_MP_TAC(CONJUNCT2 NUM_REP_RULES) from 3;
    end;
    now [4]
      let i be ind;
      assume NUM_REP i;
      assume P (mk_num i);
      NUM_REP i [5] by FIRST_ASSUM MATCH_ACCEPT_TAC,*;
      dest_num (mk_num i) = i [6] by REWRITE_TAC[GSYM(snd num_tydef)] from 5;
      i = dest_num (mk_num i) [7] by CONV_TAC SYM_CONV from 6;
      mk_num (IND_SUC i) = mk_num (IND_SUC (dest_num (mk_num i))) [8]
        by REPEAT AP_TERM_TAC from 7;
      mk_num (IND_SUC i) = SUC (mk_num i) [9] by REWRITE_TAC[SUC_DEF] from 8;
      P (mk_num i) [10] by FIRST_ASSUM MATCH_ACCEPT_TAC,*;
      P (SUC (mk_num i)) [11] by FIRST_ASSUM MATCH_MP_TAC,* from 10;
      thus P (mk_num (IND_SUC i))
        by SUBGOAL_THEN (parse_term "mk_num(IND_SUC i) = SUC(mk_num i)")
           SUBST1_TAC
        from 9,11;
    end;
    !i. NUM_REP i /\ P (mk_num i)
          ==> NUM_REP (IND_SUC i) /\ P (mk_num (IND_SUC i)) [12]
      by REPEAT STRIP_TAC from 2,4;
    (NUM_REP (dest_num n)
       ==> NUM_REP (dest_num n) /\ P (mk_num (dest_num n)))
      ==> P n [13] by REWRITE_TAC[fst num_tydef; snd num_tydef];
    (!a. NUM_REP a ==> NUM_REP a /\ P (mk_num a)) ==> P n [14]
      by DISCH_THEN(MP_TAC o SPEC (parse_term "dest_num n")) from 13;
    ((!i. NUM_REP i /\ P (mk_num i)
            ==> NUM_REP (IND_SUC i) /\ P (mk_num (IND_SUC i)))
       ==> (!a. NUM_REP a ==> NUM_REP a /\ P (mk_num a)))
      ==> P n [15]
      by W(C SUBGOAL_THEN (fun t -> REWRITE_TAC[t]) o funpow 2 lhand o snd)
      from 12,14;
    ((\i. NUM_REP i /\ P (mk_num i)) IND_0 /\
       (!i. (\i. NUM_REP i /\ P (mk_num i)) i
            ==> (\i. NUM_REP i /\ P (mk_num i)) (IND_SUC i))
       ==> (!a. NUM_REP a ==> (\i. NUM_REP i /\ P (mk_num i)) a))
      ==> P n [16] by ASM_REWRITE_TAC[GSYM ZERO_DEF; NUM_REP_RULES],* from 15;
    thus P n by MP_TAC (SPEC (parse_term
      "\\i. NUM_REP i /\\ P(mk_num i):bool") NUM_REP_INDUCT) from 16;
  end;
  thus !P. P(_0) /\ (!n. P(n) ==> P(SUC n)) ==> !n. P n
    by REPEAT STRIP_TAC from 1;
`;;

let num_RECURSION_STD = thm `;
  !e:Z f. ?fn. (fn 0 = e) /\ (!n. fn (SUC n) = f n (fn n))
  proof
    !e:Z f. ?fn. fn 0 = e /\ (!n. fn (SUC n) = f n (fn n)) [1]
    proof
      let e be Z;
      let f be num->Z->Z;
      (?fn. fn 0 = e /\ (!n. fn (SUC n) = (\z n. f n z) (fn n) n))
        ==> (?fn. fn 0 = e /\ (!n. fn (SUC n) = f n (fn n))) [2]
        by REWRITE_TAC[];
    qed by MP_TAC(ISPECL [(parse_term "e:Z");
      (parse_term "(\\z n. (f:num->Z->Z) n z)")] num_RECURSION) from 2;
  qed by REPEAT GEN_TAC from 1;
`;;

subset_name: curated


TITLE: Big Rudin Exercise 3.26 - Which integral is larger
QUESTION [15 upvotes]: This is exercise 3.26 in Rudin's Real & Complex Analysis:

If $f$ is a positive measurable function on $[0,1]$, which is larger,
  $$\int_0^1 f(x) \log f(x) \, dx$$
  or
  $$\int_0^1 f(s) \, ds \int_0^1 \log f(t) \, dt$$

I tried a bunch of functions and always got the first to be larger, which suggests that Hölder's inequality won't help here (at least not a direct application). I couldn't find an example that made the second larger. I'm stuck otherwise.
(This is self-study, not homework)
Clarification: The integral here is the Lebesgue integral. The only answer so far is only applicable to Riemann integrable functions.

REPLY [25 votes]: The function $x\mapsto x\log x$ is convex on $(0,\infty)$, as its second derivative is positive. Thus by Jensen's inequality,
$$\int_0^1 f(t)\log f(t) dt \geq \int_0^1 f(t) dt \log\left( \int_0^1 f(t) dt \right) .$$
The function $x\mapsto \log x$ is concave, so another application of Jensen's inequality yields
$$\log\left( \int_0^1 f(t) dt \right) \geq \int_0^1\log f(t) dt .$$
Combining these two inequalities proves the result.


TITLE: Why doesn't the explanation for the destructive interference in single slit diffraction also apply to constructive interference?
QUESTION [2 upvotes]: The explanation for the single slit diffraction pattern is that when a ray at the top and a ray at the center of the slit, at $\frac{b}{2}$ where $b$ is the slit width, marked by red in the left figure, has a path difference of $\frac{\lambda}{2}$, it destructs totally. This explanation can be shifted to a pair of rays below the first 2 and shows that all rays destruct, leading to a dark fringe.
In the right figure, the next dark fringe is created when the top ray and the ray at $\frac{b}{4}$ destructs since they have a path difference of $\frac{\lambda}{2}$, leading to the first quarter destructing the second quarter. Similarly, the third quarter destructs the fourth quarter, and a dark fringe is shown.
However, I don't understand how this principle is not applied to constructive interference. In the second figure, the top ray and the ray at $\frac{b}{2}$ should interfere constructively since they have a path difference of $\lambda$. When it is applied to all other rays below it shows that it would create a bright fringe??
Thanks for helping out.

REPLY [1 votes]: So, to understand this, you have to keep the big picture in mind. Remember, what's happening is that a plane wave is coming upon a barrier with a non-pointlike slit in it (so, a slit of a certain length).
For a "pointlike" slit (smaller than the wavelength), this is what happens; the slit acts as a source of a spherical wave:

Note that its the wave phenomena that's the "real thing", the rays are just imaginary lines perpendicular to the wavefronts.
For a wider slit, the behavior is more complicated, but, according to the Huygens–Fresnel principle, the situation can be described by treating every point along the slit as an emitter of such spherical waves ("wavelets"), that then interfere (superpose) with each other. The amplitude of the actual (resulting) wave at any point is a superposition of all these wavelets.

So, every point is emitting rays in every direction (within the half plane). Now, the assumption for the explanation you posted is that the screen (where you observe the diffraction pattern) is very far away, meaning the distance to it is much larger than the size of the slit .
That means that the rays originating from every part of the slit that are hitting the same point on the screen are nearly parallel (just how we treat rays of sunlight as nearly parallel). All of the rays in the picture below are meant to be the rays that hit the same point at the other end:

So here, you're just trying to figure out what's happening at a single point on the screen, by summing contributions from all of these rays. Remember, though, it's the value of the field along the ray that is making the contribution (think of each ray as being a slice through its corresponding wavelet; the contribution comes from what the amplitude of the wavelet happens to be at the other end, where it hits the screen).

This image does not depict some alternate setup, this is the same experiment, at the same time. It's just that now you're considering rays that all hit a different point on the screen. Again, you're summing contributions from all of them.
Note that the picture only shows some representative rays, but that there are infinitely many of them; there are rays in-between, not just the ones depicted here. (The contributions from the wavelets are, really, infinitesimal, and the sum is an integral.) All of them, together, add up to zero.

However, I don't understand how this principle is not applied to constructive interference. In the second figure, the top ray and the ray at $\frac{b}{2}$ should interfere constructively since they have a path difference of $\lambda$.

These particular examples were chosen so that all the rays combine to form a minimum. Yes, considering random pairs, some add up constructively, some cancel out, some produce an arbitrary value. However, you're interested in the total sum. Now, rather then working with the actual values, you can make use of the phase-difference in your reasoning. The idea is that you can always pick a pair that interferes destructively (so, zero net contribution), take it out of the total sum, then pick another such pair. So if every pair cancels out, then everything cancels out.
It's the same logic as here:

Note that you don't have to know the actual values if you know that, in this particular arrangement, all the addends 6 positions apart cancel.

REPLY [0 votes]: It works both. Around single hole you will observe rings

of interchanging positive and negative interference.


TITLE: Gluing two continuous map in a certain condition
QUESTION [1 upvotes]: Let $A \subset X$ ,  $f : A\times I \to Y$ , $g :X \times \{0\} \to Y$ be two continuous maps with the same image on $A \times \{0\}$, where $I = [0,1]$.
In this situation, can I construct a continuous map $h: A\times I \cup X \times \{0\} \to Y$ by gluing $f$ and $g$ ?
If $A$ is a closed subset, it is right.
In general case, however, I don't know for sure.
If not, please suggest a counterexample.
Thank you.

REPLY [1 votes]: Not in general, here is a sketch of a counterexample. Take $X=[0,1]$, $A=(0,1)$. Consider a continuous function on $A\times[0,1]$ that takes value $0$ on the complement of a small open subset containing the points $(1/n,1/n)$ and value $n$ at $(1/n,1/n)$, let this be $f$, and let $g$ be $0$ on $X$.