Skip to content
Permalink

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: mockingbirdnest/Principia
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: 982274ef38cb
Choose a base ref
...
head repository: mockingbirdnest/Principia
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: fc36d83bf6d8
Choose a head ref
  • 6 commits
  • 2 files changed
  • 1 contributor

Commits on Jan 22, 2019

  1. Proof of the missing case.

    pleroy committed Jan 22, 2019
    Copy the full SHA
    26c0790 View commit details

Commits on Jan 26, 2019

  1. Another round of review.

    pleroy committed Jan 26, 2019
    Copy the full SHA
    5424c7e View commit details
  2. Proof close to s0.

    pleroy committed Jan 26, 2019
    Copy the full SHA
    3e161ae View commit details

Commits on Jan 27, 2019

  1. Add a claim.

    pleroy committed Jan 27, 2019
    Copy the full SHA
    80db333 View commit details
  2. After egg's review.

    pleroy committed Jan 27, 2019
    Copy the full SHA
    75be5d0 View commit details
  3. Merge pull request #2068 from pleroy/Lemma2

    Proof of the damping condition close to s0
    pleroy authored Jan 27, 2019

    Verified

    This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
    Copy the full SHA
    fc36d83 View commit details
Showing with 46 additions and 14 deletions.
  1. BIN documentation/Geopotential.pdf
  2. +46 −14 documentation/Geopotential.tex
Binary file modified documentation/Geopotential.pdf
Binary file not shown.
60 changes: 46 additions & 14 deletions documentation/Geopotential.tex
Original file line number Diff line number Diff line change
@@ -381,7 +381,7 @@ \subsection*{Sigmoid}
\end{equation}

\begin{proposition}
The smallest value of $s_1>1.183s_0$ such that (\ref{eqnderiv}) holds for all $k>0$ and $n≥2$ is $s_1 = 3s_0$.
The smallest value of $s_1$ such that (\ref{eqnderiv}) holds for all $k>0$ and $n≥2$ is $s_1 = 3s_0$.
\begin{proof}
We start by writing:
\[
@@ -422,17 +422,20 @@ \subsection*{Sigmoid}
&\quad -3\pa{s_0+s_1}\pa{n+k-1} n \pa{n-1} r^2 \\
&\quad + 2 n \pa{n-1}\pa{n-2} r^3
\end{align*}
The following two lemmata establish properties of the roots of $d_{n k}\of{s_0, s_1; r}$:
\begin{lemma}[necessary condition]
If $1.183s_0<s_1<3s_0$ then there exist $k$ and $n$ such that $d_{n k}\of{s_0, s_1; r}$ has a zero in $\intopen{s_0} {s_1}$.
The following three lemmata establish properties of the roots of $d_{n k}\of{s_0, s_1; r}$:
\begin{lemma}[necessary condition, general case]
If $\frac{9}{7}s_0<s_1<3s_0$ then there exist $k$ and $n$ such that $d_{n k}\of{s_0, s_1; r}$ has a zero in $\intopen{s_0} {s_1}$.
\end{lemma}
\begin{lemma}[necessary condition, special case]
If $s_0<s_1<\pa{1+\frac{\sqrt{2}}{2}}s_0$ then there exist $k$ and $n$ such that $d_{n k}\of{s_0, s_1; r}$ has a zero in $\intopen{s_0} {s_1}$.
\end{lemma}
\begin{lemma}[sufficient condition]
If $s_1 = 3s_0$ then the positive roots of $d_{n k}\of{s_0, s_1; r}$ are greater than $s_1$.
\end{lemma}
These lemmata trivially constitute necessary and sufficient conditions, respectively, for the proposition.
\end{proof}
\end{proposition}
\begin{proof}[of necessary condition]
\begin{proof}[of necessary condition, general case]
In this proof we set $n=2$, which causes the term in $r^3$ of $d_{n k}\of{s_0, s_1; r}$ to vanish:
\begin{multline*}
d_{2,k}\of{s_0, s_1; r} = \pa{s_1-3s_0}s_1^2\pa{k+3}\pa{k+2}\pa{k+1} \\+ 12s_0 s_1\pa{k+2}\pa{k+1}r - 6\pa{s_0+s_1}\pa{k+1}r^2
@@ -453,8 +456,8 @@ \subsection*{Sigmoid}
\]
We will now define $k_1$ and $k_2$ such that the following claim holds:
\begin{claim}
For every $k \in \intopen{k_2}{k_1}\Intersection{\Naturals}$, $r_- \in \intopen{s_0}{s_1}$.
\end{claim}
For every $k \in \intopen{k_2}{k_1}\Intersection\intclop{2}{+\infty}\Intersection{\Naturals}$, $r_- \in \intopen{s_0}{s_1}$.
\begin{proof}
First, consider the inequality $r_-<s_1$. It can be rewritten as follows:
\begin{align*}
&6 s_0\pa{k+2} - 6\pa{s_0+s_1} < \sqrt{6\pa{k+2}\pa{k\pa{s_1^2-2 s_0 s_1 + 3s_0^2} + 3\pa{s_1-s_0}^2}}
@@ -487,10 +490,12 @@ \subsection*{Sigmoid}
\[
k_2 = \frac{-s_1\pa{-5s_1^2 + 15 s_0 s_1 - 12s_0^2} + \sqrt{\gD}}{2s_1^2\pa{3s_0-s_1}}
\]
\begin{claim}
$\intopen{k_2}{k_1}\Intersection{\Naturals}$ is nonempty when $s_1>1.183s_0$.
\end{proof}
\end{claim}
A necessary condition for the interval $\intopen{k_2}{k_1}$ to contain an integer is $k_1-k_2>1$. This inequality can be rewritten as follows:
\begin{claim}
$\intopen{k_2}{k_1}\Intersection\intclop{2}{+\infty}\Intersection{\Naturals}$ is nonempty when $s_1>\frac{9}{7}s_0 \approx 1.286s_0$.
\begin{proof}
For this set to be nonempty we must have $k_1>2$ which is equivalent to $s_1>\frac{9}{7}s_0$. Given $k_1>2$, a sufficient condition for the interval $\intopen{k_2}{k_1}$ to contain an integer greater than $1$ is $k_1-k_2>1$. This inequality can be rewritten as follows:
\begin{align*}
&2s_1^2\pa{5s_1-3s_0} + s_1\pa{-5s_1^2 + 15 s_0 s_1 - 12s_0^2} - 2s_1^2\pa{3s_0-s_1} - \sqrt{\gD} > 0 \\
\iff &s_1\pa{7s_1^2 + 3 s_0 s_1 - 12s_0^2} > \sqrt{\gD}
@@ -507,11 +512,38 @@ \subsection*{Sigmoid}
\hat\gq &= \frac{1}{3} \arctan\of{\frac{3 \sqrt{2517}}{41}} \\
\hat{s}_1 &= \frac{s_0}{6}\pa{-4+\sqrt{138}\sin\hat\gq + \sqrt{46}\cos\hat\gq} \approx 1.183s_0
\end{align*}
Thus, if $s_1 \in \intopen{\hat{s}_1}{3s_0}$ it is possible to find an integer $k$ such that the smallest root of $d_{2,k}\of{s_0, s_1; r}$ is in $\intopen{s_0} {s_1}$.
Noting that $\hat{s}_1<\frac{9}{7}s_0$, we conclude that, if $s_1 \in \intopen{\frac{9}{7}s_0}{3s_0}$ it is possible to find an integer $k≥2$ such that the smallest root of $d_{2,k}\of{s_0, s_1; r}$ is in $\intopen{s_0} {s_1}$.
\end{proof}
\end{claim}
\end{proof}

\begin{proof}[of necessary condition, special case]
In this proof we set $n=2$ and $k=1$.
\begin{claim}
If $s_1<2s_0$, then for every $k \in \intopen{k_2}{k_1}\Intersection{\Positives}$, $r_- \in \intopen{s_0}{s_1}$.
\begin{proof}
The inequality $r_-<s_1$ can be rewritten as in the previous proof, with the caveat that since the condition $k≥2$ does not hold anymore, we have to require $s_1<2s_0$ for the quantity $s_0\pa{k+2}-\pa{s_0+s_1}$ to be positive. This is acceptable since we are looking for a proof when $s_1$ is close to $s_0$. The inequality $s_0<r_-$ is unaffected by any condition on $k$ so the definition of $k_2$ remains valid.
\end{proof}
\end{claim}
\begin{claim}
$1 \in \intopen{k_2}{k_1}$ when $s_1<\pa{1+\frac{\sqrt{2}}{2}}s_0 \approx 1.707s_0$.
\begin{proof}
The inequality $1<k_1$ can be rewritten:
\[
1 < \frac{5s_1-3s_0}{3s_0-s_1} \iff s_0 > s_1 \qquad\text{which is trivially true.}
\]
The inequality $s_0<r_-$ can be rewritten as in the previous proof and becomes, substituting $k$:
\begin{align*}
&k^2 s_1^2\pa{3s_0-s_1} + k s_1\pa{-5s_1^2 + 15 s_0 s_1 - 12s_0^2} + 6\pa{s_0-s_1}^3 > 0 \\
\iff &s_1\pa{-6s_1^2 + 18 s_0 s_1 - 12 s_0^2} + 6\pa{s_0-s_1}^3 > 0 \\
\iff &-2s_1^3 + 6 s_0 s_1^2 - 5 s_0^2 s_1 + s_0^3 > 0 \\
\iff &\pa{s_1 - s_0}\pa{-2 s_1^2 + 4 s_0 s_1 - s_0^2} > 0
\end{align*}
The quadratic term in the above condition is positive between its roots, and its only root greater than $s_0$ is $\pa{1+\frac{\sqrt{2}}{2}}s_0$. Thus, if $s_1 \in \intopen{s_0}{\pa{1+\frac{\sqrt{2}}{2}}s_0}$ the smallest root of $d_{2,1}\of{s_0, s_1; r}$ is in $\intopen{s_0} {s_1}$.
\end{proof}
\begin{remark}
It is possible that $\intopen{k_2}{k_1}$ contains an integer value even if $k_1-k_2<1$, in which case more values $s_1 \in \intopen{s_0}{\hat{s}_1}$ could be excluded.
\end{remark}
\end{claim}
\end{proof}

\begin{proof}[of sufficient condition]
With the choice $s_1=3s_0$ the constant term of the polynomial $d_{n k}\of{s_0, s_1; r}$ vanishes and $r=0$ is a trivial root. We are left with the equation:
\[