TITLE: Sum of alternating binomial-coefficient-type series
QUESTION [1 upvotes]: Let $D,n\in \mathbb N$ with $0<D<n$, and $y>0$ is a real number.
Question: Is there a closed-form for the following alternating sequence
\begin{equation}
\sum_{k=0}^D (-y)^k {n\choose k}?
\end{equation}
This question is related to a similar question where $y=1$.
Motivation: These kind of expressions arrive in numerical schemes that I am working on.
First attempt: I tried to repeat some of the techniques from $y=1$ case. For instance, using the complex integral argument, we have
\begin{align}
\sum_{k=0}^D (-y)^k {n\choose k} &= \sum_{k=0}^D (-y)^k \oint_{0<|z|<1} \frac{(1+z)^n}{z^{k+1}}\frac{dz}{2\pi i} = \oint_{0<|z|<1} \frac{(1+z)^n}{z} \sum_{k=0}^D \left(-\frac{y}{z}\right)^k \frac{dz}{2\pi i} \\
&= \oint_{0<|z|<1} \frac{(1+z)^n}{z} \left[\frac{z+y(-y/z)^D}{z+y}\right] \frac{dz}{2\pi i} \\
&= \oint_{0<|z|<1} \frac{(1+z)^n}{z+y} \frac{dz}{2\pi i} + y(-y)^D \oint_{0<|z|<1} \frac{(1+z)^n}{z^{D+1}(z+y)} \frac{dz}{2\pi i}.
\end{align}
I don't know much about complex integrals and so don't know how to complete this argument. Any ideas?
Or are their any other techniques that will work here? Any ideas/hints are appreciated.

REPLY [2 votes]: We show the difference between the variant with general $y$ and $y=1$. We use the coefficient of operator $[z^n]$ to denote the coefficient of $z^n$ in a series. This way we can write for instance
\begin{align*}
[z^k](1+z)^n=\binom{n}{k}=\oint_{0<|z|<1} \frac{(1+z)^n}{z^{k+1}}\frac{dz}{2\pi i} \tag{1}
\end{align*}

We obtain
  \begin{align*}
\color{blue}{\sum_{k=0}^D(-y)^k\binom{n}{k}}
&=\sum_{k=0}^D[z^k](1-yz)^n\tag{2}\\
&=[z^0](1-yz)^n\sum_{k=0}^Dz^{-k}\tag{3}\\
&=[z^0](1-yz)^n\frac{z^{-(D+1)}-1}{z^{-1}-1}\\
&=[z^{-1}](1-yz)^n\frac{z^{-(D+1)}-1}{1-z}\\
&=\left([z^D]-[z^{-1}]\right)\frac{(1-yz)^n}{1-z}\tag{4}\\
&\,\,\color{blue}{=[z^D]\frac{(1-yz)^n}{1-z}}\tag{5}
\end{align*}
We see in (5) that in case $y=1$ we get
  \begin{align*}
[z^D]\left.\frac{(1-yz)^n}{1-z}\right|_{y=1}=[z^D](1-z)^{n-1}=(-1)^D\binom{n-1}{D}
\end{align*}
  but there is no way to make similar simplifications with general $y$.

Comment:

In (2) we apply the coefficient of operator according to (1).
In (3) we use the rule $[z^{p-q}]A(z)=[z^p]z^qA(z)$.
In (4) we note $\frac{(1-yz)^n}{1-z}=(1-yz)^n\sum_{j=0}^\infty z^j$ is a power series in $z$ so that the residue $[z^{-1}]$ is zero.


TITLE: Doubts: All ideals of $M_n(R)$ are of the form $M_n(I)$, where $I$ is an ideal of $R$.
QUESTION [1 upvotes]: I know the result is true, however, if we are to consider $E_{ij} = \left\{\begin{pmatrix} 0 & 0 & ... & 0\\
. & . & ...& . \\
0 & 0 & r_{ij} & 0 \\
. & . & ...& . \\ \end{pmatrix} : r_{ij}\in R  \right\}$.
$E_{ij}$ is an ideal of $M_n(R)$ but doesn't appear to be of the type $M_n(I)$.
Can someone please explain what I am doing wrong here?

REPLY [0 votes]: Your set is not closed by multiplication on the right.
You can multiply a nonzero element like that by a matrix with a 1 in the $j,1$ position and zeros elsewhere, and that is not in your set.


TITLE: Calculus II series
QUESTION [7 upvotes]: I'm trying to find convergence or divergence of $$\sum_{n=1}^\infty\frac{\cos(\log n)}{n}\text{.}$$I've tried to use the squeeze theorem, however, my professor said that $\log(n)$ grows too slowly for the numerator to be assumed to be zero. I don't see a solution with nth term, limit comparison or direct comparison. Any suggestions would be great.

REPLY [6 votes]: The series does not converge because it oscillates too much. Let $$S_m = \sum_{n=1}^m \frac{\cos \ln n}{n}$$ be the sequence of partial sums. Then for arbitrary $N > 0$, we can find $m_1, m_2$ with $|S_{m_1} - S_{m_2}| > 1$, so the partial sums continue oscillating by a constant amount no matter how far out you go.
(In real analysis terms, $(S_m)$ does not converge because it is not Cauchy.)
To prove this, given any $N>0$, choose $k$ such that $e^{(k-\frac13)\pi} > N$ and consider the sum
$$\sum_{n = \exp((k-\frac13)\pi}^{\exp((k+\frac13)\pi)} \frac{\cos \ln n}{n}.$$
On this interval, we have $(k - \frac13)\pi \le \ln n \le (k + \frac13)\pi$ and therefore either $\cos \ln n \ge \frac12$ or $\cos \ln n < -\frac12$ according to whether $k$ is even or odd. The two cases are symmetric, so let's assume $k$ is even.
In that case, each term of the sum is at least $\frac{1}{2n}$, and we have $$\sum_{n=a}^b \frac{1}{2n} \approx \frac12 \left(\ln b - \ln a\right)$$ with an error that goes to $0$ as we choose large enough $a, b$. (We know this from an asymptotic estimate of the harmonic numbers (Wikipedia) or from a comparison to the integral of $\frac{1}{2x}$ between $a$ and $b$.)
In this case, $a = \exp((k-\frac13)\pi)$ and $b = \exp((k+\frac13)\pi)$, so $\frac12(\ln b - \ln a) = \frac\pi3$. If $k$ is chosen so that our estimates are precise enough (and we can choose $k$ to be as large as we want) then
$$\sum_{n = \exp((k-\frac13)\pi}^{\exp((k+\frac13)\pi)} \frac{\cos \ln n}{n} > \frac\pi3 - 0.001 > 1.$$


TITLE: Second order linear homogeneous ODE with variable coefficients
QUESTION [1 upvotes]: We have a second order linear homogeneous ODE with variable coefficients of the form:
$$y''(x)+ \frac{b(x)}{a(x)}y'(x)+\frac{c(x)}{a(x)} y(x)=0.$$

For $y=c_1\eta(x)+c_2\eta'(x)$, find $a(x)$, $b(x)$ and $c(x)$.
Use the result when $y = \log x$.
Check the result obtained.

I'm having trouble with the first part, mainly it seems like such a general form of an ODE that not much can be done. I was thinking of getting a system of three equations and solving that, two of them being immediate:
$$a(x)\eta''(x)+b(x)\eta'(x)+c(x)\eta(x)=0$$
$$a(x)\eta'''(x)+b(x)\eta''(x)+c(x)\eta'(x)=0$$
I don't know where a third linearly independent equation could come from. Also, are $c_1$ and $c_2$ important enough that I should work with them?
Thanks.

REPLY [2 votes]: The phrasing of the question is singularly vague; if this is indeed the exact way the question was put to you, I cannot blame you the least for not knowing how to proceed.
I interpret the first bullet as follows:

Assume that there exists a function $\eta(x)$ such that every solution to the above ODE can be written as a linear combination of $\eta(x)$ and $\eta'(x)$, i.e. $y(x) = c_1 \eta(x) + c_2 \eta'(x)$ is a solution to the ODE for every choice of $c_{1,2}$.

Call $q(x) = \frac{b(x)}{a(x)}$ and $r(x) = \frac{c(x)}{a(x)}$. Then, by substituting $\eta(x)$ resp. $\eta'(x)$ in the original ODE, you obtain expressions for $q(x)$ and $r(x)$ in terms of $\eta$ and its derivatives.
To obtain the third equation you're looking for, an idea would be to take the derivative of the entire ODE, and use the fact that $\eta'(x)$ solves the original ODE. After some cancellations, this yields
\begin{equation}
 r'(x) \eta(x) + q'(x) \eta'(x) = 0. \tag{1}
\end{equation}
The first two expressions obtained enable you to write
\begin{align}
 q(x) &= \frac{\eta(x) \eta'''(x) - \eta'(x) \eta''(x)}{\eta'(x)^2-\eta(x) \eta''(x)},\tag{2}\\
r(x) &= \frac{\eta''(x)^2 - \eta'(x) \eta'''(x)}{\eta'(x)^2-\eta(x) \eta''(x)}. \tag{3}
\end{align}
Note that $q(x) \eta'(x) + r(x) \eta(x) = -\eta''(x)$. Taking the derivative of this equation, and using the fact that $\eta'(x)$ solves the original ODE, you end up with $(1)$. In other words: there are only two independent equations, so you can only solve for $q(x)$ and $r(x)$, and not for $a,b,c$.
Note that an obvious choice for $a,b,c$ based on $(2)$ and $(3)$ would be
\begin{align}
a(x) &= \eta'(x)^2-\eta(x) \eta''(x),\\
b(x) &= \eta(x) \eta'''(x) - \eta'(x) \eta''(x),\\
c(x) &= \eta''(x)^2 - \eta'(x) \eta'''(x),
\end{align}
but as you can see, this choice is not uniquely determined: you could multiply these choices of $a,b,c$ with an arbitrary function of $x$ and still satisfy $(2)$ and $(3)$.
For the rest: I sincerely hope you inadvertently made a typo, and that it should read

For $\eta(x) = \log(x)$, apply the above results.


text:
section \<open>Exception-Aware Relational Framework\<close>
theory Run
imports "HOL-Imperative_HOL.Imperative_HOL"
begin

  text \<open>
    With Imperative HOL comes a relational framework.
    However, this can only be used if exception freeness is already assumed.
    This results in some proof duplication, because exception freeness and
    correctness need to be shown separately.

    In this theory, we develop a relational framework that is aware of
    exceptions, and makes it possible to show correctness and exception
    freeness in one run.
\<close>

  text \<open>
    There are two types of states:
    \begin{enumerate}
      \item A normal (Some) state contains the current heap.
      \item An exception state is None
    \end{enumerate}
    The two states exactly correspond to the option monad in Imperative HOL.
\<close>

type_synonym state = "Heap.heap option"

primrec is_exn where
  "is_exn (Some _) = False" |
  "is_exn None = True"

primrec the_state where
  "the_state (Some h) = h"

\<comment> \<open>The exception-aware, relational semantics\<close>

inductive run :: "'a Heap \<Rightarrow> state \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool" where
  push_exn: "is_exn \<sigma> \<Longrightarrow> run c \<sigma> \<sigma> r " |
  new_exn:  "\<lbrakk>\<not> is_exn \<sigma>; execute c (the_state \<sigma>) = None\<rbrakk>
    \<Longrightarrow> run c \<sigma> None r" |
  regular:  "\<lbrakk>\<not> is_exn \<sigma>; execute c (the_state \<sigma>) = Some (r, h')\<rbrakk>
    \<Longrightarrow> run c \<sigma> (Some h') r"

subsubsection "Link with \<open>effect\<close> and \<open>success\<close>"

lemma run_effectE:
  assumes "run c \<sigma> \<sigma>' r"
  assumes "\<not>is_exn \<sigma>'"
  obtains h h' where
    "\<sigma>=Some h" "\<sigma>' = Some h'"
    "effect c h h' r"
  using assms
  unfolding effect_def
  apply (cases \<sigma>)
  by (auto simp add: run.simps)

lemma run_effectI:
  assumes  "run c (Some h) (Some h') r"
  shows  "effect c h h' r"
  using run_effectE[OF assms] by auto

lemma effect_run:
  assumes "effect c h h' r"
  shows "run c (Some h) (Some h') r"
  using assms
  unfolding effect_def
  by (auto intro: run.intros)

lemma success_run:
  assumes "success f h"
  obtains h' r where "run f (Some h) (Some h') r"
proof -
  from assms obtain r h'
    where "Heap_Monad.execute f h = Some (r, h')"
    unfolding success_def by auto
  then show thesis by (rule that[OF regular[of "Some h", simplified]])
qed

text \<open>run always yields a result\<close>
lemma run_complete:
  obtains \<sigma>' r where "run c \<sigma> \<sigma>' r"
  apply (cases "is_exn \<sigma>")
  apply (auto intro: run.intros)
  apply (cases "execute c (the_state \<sigma>)")
  by (auto intro: run.intros)

lemma run_detE:
  assumes "run c \<sigma> \<sigma>' r" "run c \<sigma> \<tau> s"
          "\<not>is_exn \<sigma>"
  obtains "is_exn \<sigma>'" "\<sigma>' = \<tau>" | "\<not> is_exn \<sigma>'" "\<sigma>' = \<tau>" "r = s"
  using assms
  by (auto simp add: run.simps)

lemma run_detI:
  assumes "run c (Some h) (Some h') r" "run c (Some h) \<sigma> s"
  shows "\<sigma> = Some h' \<and> r = s"
  using assms
  by (auto simp add: run.simps)

lemma run_exn:
  assumes "run f \<sigma> \<sigma>' r"
          "is_exn \<sigma>"
  obtains "\<sigma>'=\<sigma>"
  using assms
  apply (cases \<sigma>)
  apply (auto elim!: run.cases intro: that)
  done

subsubsection \<open>Elimination Rules for Basic Combinators\<close>

named_theorems run_elims "elemination rules for run"

lemma runE[run_elims]:
  assumes "run (f \<bind> g) \<sigma> \<sigma>'' r"
  obtains \<sigma>' r' where
    "run f \<sigma> \<sigma>' r'"
    "run (g r') \<sigma>' \<sigma>'' r"
using assms
apply (cases "is_exn \<sigma>")
apply (simp add: run.simps)
apply (cases "execute f (the_state \<sigma>)")
apply (simp add: run.simps bind_def)
by (auto simp add: bind_def run.simps)

lemma runE'[run_elims]:
  assumes "run (f \<then> g) \<sigma> \<sigma>'' res"
  obtains \<sigma>t rt where
    "run f \<sigma> \<sigma>t rt"
    "run g \<sigma>t \<sigma>'' res"
  using assms
  by (rule_tac runE)

lemma run_return[run_elims]:
  assumes "run (return x) \<sigma> \<sigma>' r"
  obtains "r = x" "\<sigma>' = \<sigma>" "\<not> is_exn \<sigma>" | "\<sigma> = None"
  using assms  apply (cases \<sigma>) apply (simp add: run.simps)
  by (auto simp add: run.simps execute_simps)

lemma run_raise_iff: "run (raise s) \<sigma> \<sigma>' r \<longleftrightarrow> (\<sigma>'=None)"
  apply (cases \<sigma>)
  by (auto simp add: run.simps execute_simps)

lemma run_raise[run_elims]:
  assumes "run (raise s) \<sigma> \<sigma>' r"
  obtains "\<sigma>' = None"
  using assms by (simp add: run_raise_iff)

lemma run_raiseI:
  "run (raise s) \<sigma> None r" by (simp add: run_raise_iff)

lemma run_if[run_elims]:
  assumes "run (if c then t else e) h h' r"
  obtains "c" "run t h h' r"
        | "\<not>c" "run e h h' r"
  using assms
  by (auto split: if_split_asm)

lemma run_case_option[run_elims]:
  assumes "run (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) \<sigma> \<sigma>' r"
          "\<not>is_exn \<sigma>"
  obtains "x = None" "run n \<sigma> \<sigma>' r"
        | y where "x = Some y" "run (s y) \<sigma> \<sigma>' r"
  using assms
  by (cases x) simp_all

lemma run_heap[run_elims]:
  assumes "run (Heap_Monad.heap f) \<sigma> \<sigma>' res"
          "\<not>is_exn \<sigma>"
  obtains "\<sigma>' = Some (snd (f (the_state \<sigma>)))"
  and "res = (fst (f (the_state \<sigma>)))"
  using assms
  apply (cases \<sigma>)
  apply simp
  apply (auto simp add: run.simps)
  apply (simp add: execute_simps)

  apply (simp only: execute_simps)
  apply hypsubst_thin
  subgoal premises prems for a h'
  proof -
    from prems(2) have "h' = snd (f a)" "res = fst (f a)" by simp_all
    from prems(1)[OF this] show ?thesis .
  qed
  done

subsection \<open>Array Commands\<close>

lemma run_length[run_elims]:
  assumes "run (Array.len a) \<sigma> \<sigma>' r"
          "\<not>is_exn \<sigma>"
  obtains "\<not>is_exn \<sigma>" "\<sigma>' = \<sigma>" "r = Array.length (the_state \<sigma>) a"
  using assms
  apply (cases \<sigma>)
  by (auto simp add: run.simps execute_simps)

lemma run_new_array[run_elims]:
  assumes "run (Array.new n x) \<sigma> \<sigma>' r"
          "\<not>is_exn \<sigma>"
  obtains "\<sigma>' = Some (snd (Array.alloc (replicate n x) (the_state \<sigma>)))"
  and "r = fst (Array.alloc (replicate n x) (the_state \<sigma>))"
  and "Array.get (the_state \<sigma>') r = replicate n x"
  using assms
  apply (cases \<sigma>)
  apply simp
  apply (auto simp add: run.simps)
  apply (simp add: execute_simps)
  apply (simp add: Array.get_alloc)
  apply hypsubst_thin
  subgoal premises prems for a h'
  proof -
    from prems(2) have "h' = snd (Array.alloc (replicate n x) a)"
      "r = fst (Array.alloc (replicate n x) a)" by (auto simp add: execute_simps)
    then show ?thesis by (rule prems(1))
  qed
  done

lemma run_make[run_elims]:
  assumes "run (Array.make n f) \<sigma> \<sigma>' r"
          "\<not>is_exn \<sigma>"
  obtains "\<sigma>' = Some (snd (Array.alloc (map f [0 ..< n]) (the_state \<sigma>)))"
          "r = fst (Array.alloc (map f [0 ..< n]) (the_state \<sigma>))"
          "Array.get (the_state \<sigma>') r = (map f [0 ..< n])"
  using assms
  apply (cases \<sigma>)
  subgoal by simp
  subgoal by (simp add: run.simps execute_simps Array.get_alloc; fastforce)
  done

lemma run_upd[run_elims]:
  assumes "run (Array.upd i x a) \<sigma> \<sigma>' res"
          "\<not>is_exn \<sigma>"
  obtains "\<not> i < Array.length (the_state \<sigma>) a"
          "\<sigma>' = None"
  |
          "i < Array.length (the_state \<sigma>) a"
          "\<sigma>' = Some (Array.update a i x (the_state \<sigma>))"
          "res = a"
  using assms
  apply (cases \<sigma>)
  apply simp
  apply (cases "i < Array.length (the_state \<sigma>) a")
  apply (auto simp add: run.simps)
  apply (simp_all only: execute_simps)
  prefer 3
  apply auto[2]
  apply hypsubst_thin
  subgoal premises prems for aa h'
  proof -
    from prems(3) have "h' = Array.update a i x aa" "res = a" by auto
    then show ?thesis by (rule prems(1))
  qed
  done

lemma run_nth[run_elims]:
  assumes "run (Array.nth a i) \<sigma> \<sigma>' r"
          "\<not>is_exn \<sigma>"
  obtains "\<not>is_exn \<sigma>"
    "i < Array.length (the_state \<sigma>) a"
    "r = (Array.get (the_state \<sigma>) a) ! i"
    "\<sigma>' = \<sigma>"
  |
    "\<not> i < Array.length (the_state \<sigma>) a"
    "\<sigma>' = None"
  using assms
  apply (cases \<sigma>)
  apply simp
  apply (cases "i < Array.length (the_state \<sigma>) a")
  apply (auto simp add: run.simps)
  apply (simp_all only: execute_simps)
  prefer 3
  apply auto[2]
  apply hypsubst_thin
  subgoal premises prems for aa h'
  proof -
    from prems(3) have "r = Array.get aa a ! i" "h' = aa" by auto
    then show ?thesis by (rule prems(1))
  qed
  done

lemma run_of_list[run_elims]:
  assumes "run (Array.of_list xs) \<sigma> \<sigma>' r"
          "\<not>is_exn \<sigma>"
  obtains "\<sigma>' = Some (snd (Array.alloc xs (the_state \<sigma>)))"
          "r = fst (Array.alloc xs (the_state \<sigma>))"
          "Array.get (the_state \<sigma>') r = xs"
  using assms
  apply (cases \<sigma>)
  apply simp
  apply (auto simp add: run.simps)
  apply (simp add: execute_simps)
  apply (simp add: Array.get_alloc)
  apply hypsubst_thin
  subgoal premises prems for a h'
  proof -
    from prems(2) have "h' = snd (Array.alloc xs a)"
      "r = fst (Array.alloc xs a)" by (auto simp add: execute_simps)
    then show ?thesis by (rule prems(1))
  qed
  done

lemma run_freeze[run_elims]:
  assumes "run (Array.freeze a) \<sigma> \<sigma>' r"
          "\<not>is_exn \<sigma>"
  obtains "\<sigma>' = \<sigma>"
          "r = Array.get (the_state \<sigma>) a"
  using assms
  apply (cases \<sigma>)
  by (auto simp add: run.simps execute_simps)

subsection \<open>Reference Commands\<close>

lemma run_new_ref[run_elims]:
  assumes "run (ref x) \<sigma> \<sigma>' r"
          "\<not>is_exn \<sigma>"
  obtains "\<sigma>' = Some (snd (Ref.alloc x (the_state \<sigma>)))"
          "r = fst (Ref.alloc x (the_state \<sigma>))"
          "Ref.get (the_state \<sigma>') r = x"
  using assms
  apply (cases \<sigma>)
  apply simp
  apply (auto simp add: run.simps)
  apply (simp add: execute_simps)
  apply hypsubst_thin
  subgoal premises prems for a h'
  proof -
    from prems(2) have
      "h' = snd (Ref.alloc x a)"
      "r = fst (Ref.alloc x a)"
      by (auto simp add: execute_simps)
    then show ?thesis by (rule prems(1))
  qed
  done

lemma "fst (Ref.alloc x h) = Ref (lim h)"
  unfolding alloc_def
  by (simp add: Let_def)

lemma run_update[run_elims]:
  assumes "run (p := x) \<sigma> \<sigma>' r"
          "\<not>is_exn \<sigma>"
  obtains "\<sigma>' = Some (Ref.set p x (the_state \<sigma>))" "r = ()"
  using assms
  unfolding Ref.update_def
  by (auto elim: run_heap)

lemma run_lookup[run_elims]:
  assumes "run (!p) \<sigma> \<sigma>' r"
          "\<not> is_exn \<sigma>"
  obtains "\<not>is_exn \<sigma>" "\<sigma>' = \<sigma>" "r = Ref.get (the_state \<sigma>) p"
  using assms
  apply (cases \<sigma>)
  by (auto simp add: run.simps execute_simps)

end

subset_name: curated


TITLE: Rewriting (or bounding) $\sum_{j=0}^k\frac{1}{(1-r)^j}$ in terms of the exponential function
QUESTION [0 upvotes]: I know the common formula:
$$
\sum_{j=0}^\infty r^j = \frac{1}{1-r},
$$
for $r<1$.
What about $\frac{1}{(1-r)^k}$ though? I'm asking this because I want to utilise rewrite
$$\sum_{j=0}^k\frac{1}{(1-r)^j}$$
for $r<1$ and possibly connect that with the exponential function.

REPLY [0 votes]: $$\sum_{j=0}^\infty \frac{1}{(1-r)^j} = \frac{1}{1-\frac{1}{1-r}}$$
with natural restrictions on $r$. And for finite sum:
$$\sum_{j=0}^n \frac{1}{(1-r)^j} = \frac{1- \frac{1}{(1-r)^n}}{1-\frac{1}{1-r}}-1$$