text:
(*  Author:     Tobias Nipkow, 2007  *)

theory QEdlo_inf
imports DLO
begin

subsection "Quantifier elimination with infinitesimals"

text\<open>This section presents a new quantifier elimination procedure
for dense linear orders based on (the simulation of) infinitesimals.
It is a fairly straightforward adaptation of the analogous algorithm
by Loos and Weispfenning for linear arithmetic described in
\S\ref{sec:lin-inf}.\<close>

fun asubst_peps :: "nat \<Rightarrow> atom \<Rightarrow> atom fm" ("asubst\<^sub>+") where
"asubst_peps k (Less 0 0) = FalseF" |
"asubst_peps k (Less 0 (Suc j)) = Atom(Less k j)" |
"asubst_peps k (Less (Suc i) 0) = (if i=k then TrueF
   else Or (Atom(Less i k)) (Atom(Eq i k)))" |
"asubst_peps k (Less (Suc i) (Suc j)) = Atom(Less i j)" |
"asubst_peps k (Eq 0 0) = TrueF" |
"asubst_peps k (Eq 0 _) = FalseF" |
"asubst_peps k (Eq _ 0) = FalseF" |
"asubst_peps k (Eq (Suc i) (Suc j)) = Atom(Eq i j)"

abbreviation subst_peps :: "atom fm \<Rightarrow> nat \<Rightarrow> atom fm" ("subst\<^sub>+") where
"subst\<^sub>+ \<phi> k \<equiv> amap\<^sub>f\<^sub>m (asubst\<^sub>+ k) \<phi>"

definition "nolb \<phi> xs l x = (\<forall>y\<in>{l<..<x}. y \<notin> LB \<phi> xs)"

lemma nolb_And[simp]:
  "nolb (And \<phi>\<^sub>1 \<phi>\<^sub>2) xs l x = (nolb \<phi>\<^sub>1 xs l x \<and> nolb \<phi>\<^sub>2 xs l x)"
apply(clarsimp simp:nolb_def)
apply blast
done

lemma nolb_Or[simp]:
  "nolb (Or \<phi>\<^sub>1 \<phi>\<^sub>2) xs l x = (nolb \<phi>\<^sub>1 xs l x \<and> nolb \<phi>\<^sub>2 xs l x)"
apply(clarsimp simp:nolb_def)
apply blast
done

context notes [[simp_depth_limit=3]]
begin

lemma innermost_intvl:
 "\<lbrakk> nqfree \<phi>; nolb \<phi> xs l x; l < x; x \<notin> EQ \<phi> xs; DLO.I \<phi> (x#xs); l < y; y \<le> x\<rbrakk>
  \<Longrightarrow> DLO.I \<phi> (y#xs)"
proof(induct \<phi>)
  case (Atom a)
  show ?case
  proof (cases a)
    case (Less i j)
    then show ?thesis using Atom
      unfolding nolb_def
      by (clarsimp simp: nth.simps Ball_def split:if_split_asm nat.splits)
         (metis not_le_imp_less order_antisym order_less_trans)+
  next
    case (Eq i j) thus ?thesis using Atom
      apply(clarsimp simp:EQ_def nolb_def nth_Cons')
      apply(case_tac "i=0 \<and> j=0") apply simp
      apply(case_tac "i\<noteq>0 \<and> j\<noteq>0") apply simp
      apply(case_tac "i=0 \<and> j\<noteq>0") apply (fastforce split:if_split_asm)
      apply(case_tac "i\<noteq>0 \<and> j=0") apply (fastforce split:if_split_asm)
      apply arith
      done
  qed
next
  case And thus ?case by (fastforce)
next
  case Or thus ?case by (fastforce)
qed simp+

lemma I_subst_peps2:
 "nqfree \<phi> \<Longrightarrow> xs!l < x \<Longrightarrow> nolb \<phi> xs (xs!l) x \<Longrightarrow> x \<notin> EQ \<phi> xs
 \<Longrightarrow> \<forall>y \<in> {xs!l <.. x}. DLO.I \<phi> (y#xs)
 \<Longrightarrow> DLO.I (subst\<^sub>+ \<phi> l) xs"
proof(induct \<phi>)
  case FalseF thus ?case
    by simp (metis antisym_conv1 linorder_neq_iff)
next
  case (Atom a)
  show ?case
  proof(cases "(l,a)" rule:asubst_peps.cases)
    case 3 thus ?thesis using Atom
      by (auto simp: nolb_def EQ_def Ball_def)
         (metis One_nat_def antisym_conv1 not_less_iff_gr_or_eq)
  qed (insert Atom, auto simp: nolb_def EQ_def Ball_def)
next
  case Or thus ?case by(simp add: Ball_def)(metis order_refl innermost_intvl)
qed simp_all

end

lemma dense_interval:
assumes "finite L" "l \<in> L" "l < x" "P(x::'a::dlo)"
and dense: "\<And>y l. \<lbrakk> \<forall>y\<in>{l<..<x}. y \<notin> L; l<x; l<y; y\<le>x \<rbrakk> \<Longrightarrow> P y"
shows "\<exists>l\<in>L. l<x \<and> (\<forall>y\<in>{l<..<x}. y \<notin> L) \<and> (\<forall>y. l<y \<and> y\<le>x \<longrightarrow> P y)"
proof -
  let ?L = "{l\<in>L. l < x}"
  let ?ll = "Max ?L"
  have "?L \<noteq> {}" using \<open>l \<in> L\<close> \<open>l<x\<close> by (blast intro:order_less_imp_le)
  hence "\<forall>y. ?ll<y \<and> y<x \<longrightarrow> y \<notin> L" using \<open>finite L\<close> by force
  moreover have "?ll \<in> L"
  proof
    show "?ll \<in> ?L" using \<open>finite L\<close> Max_in[OF _ \<open>?L \<noteq> {}\<close>] by simp
    show "?L \<subseteq> L" by blast
  qed
  moreover have "?ll < x" using \<open>finite L\<close> \<open>?L \<noteq> {}\<close> by simp
  ultimately show ?thesis using \<open>l < x\<close> \<open>?L \<noteq> {}\<close>
    by(blast intro!:dense greaterThanLessThan_iff[THEN iffD1])
qed

lemma I_subst_peps:
  "nqfree \<phi> \<Longrightarrow> DLO.I (subst\<^sub>+ \<phi> l) xs \<longrightarrow>
  (\<exists>leps>xs!l. \<forall>x. xs!l < x \<and> x \<le> leps \<longrightarrow> DLO.I \<phi> (x#xs))"
proof(induct \<phi>)
  case TrueF thus ?case by simp (metis no_ub)
next
  case (Atom a)
  show ?case
  proof (cases "(l,a)" rule: asubst_peps.cases)
    case 2 thus ?thesis using Atom
      apply(auto)
      apply(drule dense)
      apply(metis One_nat_def xt1(7))
      done
  next
    case 3 thus ?thesis using Atom
      apply(auto)
        apply (metis no_ub)
       apply (metis no_ub less_trans)
      apply (metis no_ub)
      done
  next
    case 4 thus ?thesis using Atom by(auto)(metis no_ub)
  next
    case 5 thus ?thesis using Atom by(auto)(metis no_ub)
  next
    case 8 thus ?thesis using Atom by(auto)(metis no_ub)
  qed (insert Atom, auto)
next
  case And thus ?case
    apply clarsimp
    apply(rule_tac x="min leps lepsa" in exI)
    apply simp
    done
next
  case Or thus ?case by force
qed simp_all

definition
"qe_eps\<^sub>1(\<phi>) =
(let as = DLO.atoms\<^sub>0 \<phi>; lbs = lbounds as; ebs = ebounds as
 in list_disj (inf\<^sub>- \<phi> # map (subst\<^sub>+ \<phi>) lbs @ map (subst \<phi>) ebs))"

theorem I_qe_eps1:
assumes "nqfree \<phi>" shows "DLO.I (qe_eps\<^sub>1 \<phi>) xs = (\<exists>x. DLO.I \<phi> (x#xs))"
  (is "?QE = ?EX")
proof
  let ?as = "DLO.atoms\<^sub>0 \<phi>" let ?ebs = "ebounds ?as"
  assume ?QE
  { assume "DLO.I (inf\<^sub>- \<phi>) xs"
    hence ?EX using \<open>?QE\<close> min_inf[of \<phi> xs] \<open>nqfree \<phi>\<close>
      by(auto simp add:qe_eps\<^sub>1_def amap_fm_list_disj)
  } moreover
  { assume "\<forall>i \<in> set ?ebs. \<not>DLO.I \<phi> (xs!i # xs)"
           "\<not> DLO.I (inf\<^sub>- \<phi>) xs"
    with \<open>?QE\<close> \<open>nqfree \<phi>\<close> obtain l where "DLO.I (subst\<^sub>+ \<phi> l) xs"
      by(fastforce simp: I_subst qe_eps\<^sub>1_def set_ebounds set_lbounds)
    then obtain leps where "DLO.I \<phi> (leps#xs)"
      using I_subst_peps[OF \<open>nqfree \<phi>\<close>] by fastforce
    hence ?EX .. }
  ultimately show ?EX by blast
next
  let ?as = "DLO.atoms\<^sub>0 \<phi>" let ?ebs = "ebounds ?as"
  assume ?EX
  then obtain x where x: "DLO.I \<phi> (x#xs)" ..
  { assume "DLO.I (inf\<^sub>- \<phi>) xs"
    hence ?QE using \<open>nqfree \<phi>\<close> by(auto simp:qe_eps\<^sub>1_def)
  } moreover
  { assume "\<exists>k \<in> set ?ebs. DLO.I (subst \<phi> k) xs"
    hence ?QE by(auto simp:qe_eps\<^sub>1_def) } moreover
  { assume "\<not> DLO.I (inf\<^sub>- \<phi>) xs"
    and "\<forall>k \<in> set ?ebs. \<not> DLO.I (subst \<phi> k) xs"
    hence noE: "\<forall>e \<in> EQ \<phi> xs. \<not> DLO.I \<phi> (e#xs)" using \<open>nqfree \<phi>\<close>
      by (auto simp:set_ebounds EQ_def I_subst nth_Cons' split:if_split_asm)
    hence "x \<notin> EQ \<phi> xs" using x by fastforce
    obtain l where "l \<in> LB \<phi> xs" "l < x"
      using LBex[OF \<open>nqfree \<phi>\<close> x \<open>\<not> DLO.I(inf\<^sub>- \<phi>) xs\<close> \<open>x \<notin> EQ \<phi> xs\<close>] ..
    have "\<exists>l\<in>LB \<phi> xs. l<x \<and> nolb \<phi> xs l x \<and>
            (\<forall>y. l < y \<and> y \<le> x \<longrightarrow> DLO.I \<phi> (y#xs))"
      using dense_interval[where P = "\<lambda>x. DLO.I \<phi> (x#xs)", OF finite_LB \<open>l\<in>LB \<phi> xs\<close> \<open>l<x\<close> x] x innermost_intvl[OF \<open>nqfree \<phi>\<close> _ _ \<open>x \<notin> EQ \<phi> xs\<close>]
      by (simp add:nolb_def)
    then obtain m
      where *: "Less (Suc m) 0 \<in> set ?as \<and> xs!m < x \<and> nolb \<phi> xs (xs!m) x
            \<and> (\<forall>y. xs!m < y \<and> y \<le> x \<longrightarrow> DLO.I \<phi> (y#xs))"
      by blast
    then have "DLO.I (subst\<^sub>+ \<phi> m) xs"
      using noE by(auto intro!: I_subst_peps2[OF \<open>nqfree \<phi>\<close>])
    with * have ?QE
      by(simp add:qe_eps\<^sub>1_def bex_Un set_lbounds set_ebounds) metis
  } ultimately show ?QE by blast
qed

lemma qfree_asubst_peps: "qfree (asubst\<^sub>+ k a)"
by(cases "(k,a)" rule:asubst_peps.cases) simp_all

lemma qfree_subst_peps: "nqfree \<phi> \<Longrightarrow> qfree (subst\<^sub>+ \<phi> k)"
by(induct \<phi>) (simp_all add:qfree_asubst_peps)

lemma qfree_qe_eps\<^sub>1: "nqfree \<phi> \<Longrightarrow> qfree(qe_eps\<^sub>1 \<phi>)"
apply(simp add:qe_eps\<^sub>1_def)
apply(rule qfree_list_disj)
apply (auto simp:qfree_min_inf qfree_subst_peps qfree_map_fm)
done

definition "qe_eps = DLO.lift_nnf_qe qe_eps\<^sub>1"

lemma qfree_qe_eps: "qfree(qe_eps \<phi>)"
by(simp add: qe_eps_def DLO.qfree_lift_nnf_qe qfree_qe_eps\<^sub>1)

lemma I_qe_eps: "DLO.I (qe_eps \<phi>) xs = DLO.I \<phi> xs"
by(simp add:qe_eps_def DLO.I_lift_nnf_qe qfree_qe_eps\<^sub>1 I_qe_eps1)

end

subset_name: curated


TITLE: Why can't unequal current sources be connected in series?
QUESTION [1 upvotes]: Imagine two power sources: PS-1 that can supply $5A$ at $100V$, and PS-2 can supply  $10A$ at $40V$. Due to conservation of charge and Kirchoff's current law (KCL), this is incorrect, and  would lead to a lot of problems to a circuit.
But, why can't currents add up? Just like voltage.

REPLY [0 votes]: Would you ask why two unequal voltage sources cannot be places in parallel? In that case the answer would that infinte current would flow between them. In your case, with two unequal current sources in series, infinite voltage would be generated.


TITLE: Question about hyperbolic space-forms
QUESTION [2 upvotes]: I have a map between hyperbolic space-forms $\varphi:B^n/\Gamma \longrightarrow B^n/H$ (where $\Gamma, H$ are discrete groups of isometries that act freely), and a lift to a map $\tilde{\varphi}:B^n \longrightarrow B^n$. Then, calling $\pi:B^n \longrightarrow B^n/\Gamma$ and $\eta:B^n \longrightarrow B^n/H$ the projections, I have a commutative diagram such that $\eta \tilde{\varphi} = \varphi \pi$.
Let $g \in \Gamma$. Then I have the equation $\eta \tilde{\varphi} g = \eta \tilde{\varphi}$. I want to prove that, in this situation, I have a unique isometry $\varphi_*(g)$ such that $\tilde{\varphi}g=\varphi_*(g) \tilde{\varphi}$.
What I can get is that for every $x \in B^n$ there is an isometry $h_x \in H$ such that $\tilde{\varphi}g(x) = h_x \tilde{\varphi}(x)$, but I don't know how to prove that this isometry $h_x$ does not depend on the point $x$. How can I prove it?
Thanks in advance.

REPLY [0 votes]: $\tilde \varphi : B^n \to B^n$ is invertible, so $\varphi_*(g) = \tilde \varphi g \tilde \varphi^{-1}$.


TITLE: Deriving the Rayleigh Distribution from the Gaussian
QUESTION [3 upvotes]: Take a complex number $z=u+iv$ and call its magnitude $x$.
Consider the real and imaginary parts to be Gaussian distributed:
$$
f_{U}(u)=\frac{1}{\sqrt{2\pi\sigma^{2}}}\exp\left(\frac{-u^{2}}{2\sigma^{2}}\right)
$$
and similarily for $v$.
Then the magnitude of $z$ is distributed as
$$
f(x,\sigma)=\frac{1}{2\pi\sigma^{2}}\int_{-\infty}^{\infty}du\int_{-\infty}^{\infty}dv\,\exp\left(\frac{-u^{2}}{2\sigma^{2}}\right)\exp\left(\frac{-v^{2}}{2\sigma^{2}}\right)\delta\left(x-\sqrt{u^{2}+v^{2}}\right)
$$
if we convert to polar co-ordinates then evaluate we have
$$
f(x,\sigma)=\frac{x}{\sigma^{2}}\exp\left(\frac{-x^{2}}{2\sigma^{2}}\right)
$$
which is the Rayleigh distribution.
Can anyone explain where the second expression for $f(x,\sigma)$ comes from? How is this the distribution of the length of $z$?
Cheers!

REPLY [2 votes]: $P\{Z \leq \alpha\} = P\{U^2+V^2 \leq \alpha^2\}$ is the integral of the joint density of $U$ and $V$ over the disc of radius $\alpha$ centered at the origin.
Changing to polar coordinates (as you have done) gives us that
$$F_Z(\alpha) = P\{Z \leq \alpha\} = 1 - \exp(-\alpha^2/2\sigma^2)$$
especially after you remember that $(r/\sigma^2)\cdot e^{-r^2/2\sigma^2}$
is a perfect integral whose antiderivative is $-e^{-r^2/2\sigma^2}$).
Now differentiate with respect to $\alpha$ to get the density of $Z$.


TITLE: Differentiability of the function $x^{n+\frac{1}{2}}$
QUESTION [0 upvotes]: How can I prove that the function $x^{n+\frac{1}{2}}$ is differentiable?
Do I split it up into $x^n$ and $x^{\frac{1}{2}}$? Any suggestions would be great.

REPLY [1 votes]: To see that $f(x) = x^{n+\frac{1}{2}}$ is differentiable, it suffices to show that
$$ \lim_{x \to c} \frac{f(x)-f(c)}{x-c} $$
exists.
However, if you are allowed to use the fact that $x^n$ and $x^\frac{1}{2}$ are differentiable, then you could appeal to the product rule to show that $x^{n+\frac{1}{2}} = x^n x^\frac{1}{2}$ is indeed differentiable.


TITLE: Gröbner/SAGBI bases for non-commutative setting
QUESTION [4 upvotes]: It is well known that SAGBI/Gröbner bases are important for commutative and non-commutative algebra. The references for commutative scenery is ample and vast, but I am in trouble to find a good reference for the general theory of SAGBI/Gröbner bases for non-commutative setting. Actually, I am interesting in the following subjects:
(1) Where can I find the general construction of these bases for non-commutative setting?
(2) Is there some reference for the specific case of the Universal enveloping algebra of a finite-dimensional  semi-simple Lie algebra over $\mathbb{C}$?
(3) Does exist a reference using this bases in representation theory? For instance, in the study of universal objects defined by generators and relations.
THANKS!

REPLY [5 votes]: There are lots of papers dealing with representation-theoretic questions and universal enveloping algebras using Gröbner bases. Some examples are given by these: 1, 2, 3, 4.


TITLE: Minkowski sums of convex and bounded sets
QUESTION [0 upvotes]: I am trying to prove the following.
Question. Suppose $A,B,C\subset E^n$ and that
$$A+C \subset B+C.$$
If $A,B$ are both convex, $B$ is closed, $C$ is bounded, show that $A\subset B$.
So far I have done the following. Where am I going wrong?
Proof. Let $a\in A$. Then,
$$a+c_0\in A+C,\ \forall c_0\in C$$
$$ \Rightarrow a+c_0 \in B+C, \forall c_0\in C$$
$$ \Rightarrow a+c_0 = b+c_1,\ \text{for some}\ b\in B,c_1\in C.$$
For every line $\lambda a_0 + (1-\lambda)a_1 + c_0,\ 0\leq \lambda \leq 1,$ that contain $a$, there must exist a closed line $\lambda b_0 + (1-\lambda)b_1 + c_1, 0\leq \lambda \leq 1,$ that contains $b$ and $\lambda a_0 + (1-\lambda)a_1 + c_0$. Now, since $C$ is bounded $a$ is contained in $\lambda b_0 + (1-\lambda)b_1\in B$.

REPLY [4 votes]: Suppose on the contrary that $A \not \subset B$. Then there exists $a \in A$ such that $a \not \in B$. Since $B$ is closed and convex and so is $\{a\}$, from some version of the geometric Hahn-Banach theorem, there are a real number $r$ and a nonzero linear map $l : E^n \to \mathbb{R}$ such that $l(a) > r$ and $l(B) \le r$. Set $\epsilon = l(a)-r > 0$.
Since $C$ is bounded, since $l$ is linear and since we work in finite dimension $n$, the number $M := \sup_{c \in C} l(c)$ is finite. Observe that for $x \in B+C$, $l(x) \le r + M$. Consider $c_0 \in C$ such that $l(c_0) > M - (\epsilon/2)$. Then by the linearity of $l$,
$$l(a+c_0) = l(a) + l(c_0) > r + \epsilon + M - (\epsilon/2) = r + M + (\epsilon/2) > r+M \, .$$
It follows that $a + c_0 \not \in B+C$, which contradicts the assumption that $A+C \subset B+C$. Notice that we did not use the convexity of $A$.

The geometric Hahn-Banach theorem used above is a rather accessible statement in finite dimensions. Let $B \subset E^n$ be a closed convex set and $\{a\} \in E^n \setminus B$.
Since convexity is a property invariant under changes of equivalent norms, and since all norms on a finite dimensional space are equivalent, we can without loss of generality consider the strictly convex norm $\|-\|$ on $E^n$ associated to the 'usual' Euclidean scalar product on $\mathbb{R}^n$.
Let $d = d(a, B) = \mathrm{inf}_{b \in B} \, d(a,b)$ where $d(x,y) := \|y-x\|$; we claim that this infimum is achieved. Indeed, for $n \in \mathbb{N}$, let $b_n \in B$ be such that $d(a,b_n) \le d + (1/n)$. (Observe interestingly that this relies on the countable axiom of choice, but this is a weaker axiom than the usual axiom of choice and it is somewhat more 'intuitive' than Zorn's lemma...) Since the sequence $\{b_n\}$ lies inside the bounded closed (hence compact) set $B \cap \bar{B}(a, 1)$, a subsequence of it converges say towards $b_0 \in B$. Of course, $d = d(a,b_0)$.
We claim that $b_0$ is the unique element in $b \in B$ such that $d = d(a,b)$. Assuming otherwise, let $b_1 \in B \setminus \{b_0\}$ satisfy $d = d(a,b_1)$. Since $B$ is convex, the segment $b_{\lambda} = \lambda b_0 + (1- \lambda) b_1$ with $\lambda \in [0,1]$ lies in $B$. Hence for $\lambda \in (0,1)$
$$ d \le d(a, b_{\lambda}) = \| b_{\lambda} - a \| = \| \lambda (b_0 - a) + (1- \lambda)(b_1 - a)  \| < \lambda d(a,b_0) + (1- \lambda) d(a,b_1) = d$$
where the strict inequality holds since the euclidean norm is strictly convex. This is a contradiction, hence $b_0$ is unique.
Let $v = a-b_0$ and $w = (b_0 + a)/2$. Consider the linear map $l : E^n \to \mathbb{R} : x \mapsto x \cdot v$ and set $r := l(w)$. Then $l(a) > r$ and $l(b_0) < r$. Moreover $l(B) < r$, in fact $\mathrm{max}_{b \in B} l(b) = l(b_0)$; this follows from the fact that the hyperplane $[x:l(x) = l(b_0)]$ is the tangent plane at $b_0$ to the sphere $\partial B(a, d)$. Indeed, for $x \in \bar{B}(a,d)$, $l(x) \ge l(b_0)$ with equality if and only if $x=b_0$. If there were to exist $b_1 \in B$ such that $l(b_1) > l(b_0)$, a part of the segment joining $b_0$ to $b_1$ would lie strictly inside $\bar{B}(a,d)$ hence contradicting the definition of $b_0$.


TITLE: Does weak convergence in a Sobolev space implies uniform convergence?
QUESTION [3 upvotes]: Let $\Omega$ be a nice open, bounded domain in $\mathbb{R}^n$. (e.g suppose $\bar \Omega$ is a smooth manifold with boundary).
Let $f_n \in W^{1,p}(\Omega),p>n$ and suppose that $f_n \rightharpoonup f$ in $W^{1,p}(\Omega)$.

Question: Is it true that $f_n$ converges uniformly to $f$?

(Since $p>n$ the $f_n$ are continuous, so this is well-defined).
I know two things:

If $f_n$ converges uniformly to some function $g$, then $g=f$.
There is always a subsequence of $f_n $ which converges uniformly to $f$. Indeed, any weakly convergent sequence is bounded in $W^{1,p}$, hence by the Rellich-Kondrachov theorem it has a subsequence which converges in $C(\Omega)$. By point $(1)$ the limit must be $f$.

So, the question is can we can conclude directly that the original sequence was uniformly convergent, without passing to a subsequence.
(This is the case when we have strong Sobolev convergence, by the way).

REPLY [3 votes]: If $\{f_n\}$ does not converge to $f$ in $C(\Omega)$, then there is $\epsilon_0>0$ and a subsequence $\{f_{n_k}\}$ so that $\|f_{n_k} - f\|_{C^0} \ge \epsilon_0$.
But by taking further subsequence if necessary, $f_{n_k} \to g$ in $C^0$ for some $g$. Then $g$ has to be $f$. This is a contradiction.


TITLE: Prove that $\lim_{n \to \infty} {\sqrt[n]{n}} = 1$ using the inequality that $(1+x)^n\geq 1 + nx + \frac{n(n-1)}{2}x^2 $
QUESTION [2 upvotes]: $(1+x)^n\geq 1 + nx + \frac{n(n-1)}{2}x^2 $ holds  for all  $ n \in \mathbb{N} $ and  $x \ge  0$
I proved that $ a \geq b \Leftrightarrow a^n \geq b^n $.
Then I plug $x_{n} $  into the inequality.
But I don't know what to do next. Please help me

REPLY [2 votes]: An alternative way is to exploit the AM-GM inequality. Since for any $n\geq 2$ we have
$$ n=\prod_{k=1}^{n-1}\left(1+\frac{1}{k}\right),\qquad \sqrt[n]{n}=\text{GM}\left(1,1+\frac{1}{1},\ldots,1+\frac{1}{n-1}\right)$$
we also have
$$ \sqrt[n]{n}\leq \text{AM}\left(1,1+\frac{1}{1},\ldots,1+\frac{1}{n-1}\right) = 1+\frac{H_{n-1}}{n}\leq 1+\frac{\log n}{n} $$
and $\lim_{n\to +\infty}\sqrt[n]{n}=1$ follows by squeezing.


TITLE: Why is the twin prime conjecture hard?
QUESTION [4 upvotes]: If $\pi_2(x)$ is the number of twin primes of magnitude less than or equal to $x$. We want to prove that
$$\lim_{x\,\to\,\infty}\pi_2(x)=\infty$$
which should be easier than finding and proving an asymptotic formula like $x/\log(x)$ for $\pi(x)$. How is it that modern mathematics cannot prove even the awful estimate
$$\pi_2(x)\ge \log\log\,...\log x\quad\quad x\text{ big enough}$$
with $100$ or $1000$ nested $\log$s? Any function with unbounded growth (no matter how slow) does the trick. It seems so weird that no argument, sieve-theoretic nor analytic or algebraic, can prove such a "simple result".
I am asking for a concrete obstacle in a would-be proof of this type.
Thanks!

REPLY [4 votes]: Most of the ways of proving the infinitude of primes rely on their being a basis of the set of natural numbers under multiplication — that is to say, that they generate all the naturals. For instance, the Euler product for the Zeta function takes this form: it's essentially an analytic statement of the fact that each natural number has a unique prime factorization and each product of (possibly repeated) primes corresponds to a single natural number. There's also an information-theoretic proof that goes through this notion of basis: if there were a finite number of primes $p_1, p_2, \ldots, p_m$, then we could write any number $n$ as $p_1^{e_1}p_2^{e_2}\cdots p_m^{e_m}$ and represent $n$ via the list of exponents $\langle e_1, e_2, \ldots, e_m\rangle$. But each of these is at most $\log_2(n)$ and can therefore be represented in $\log_2\log_2(n)$ bits, so that $n$ itself could be represented in $m\lg\lg n$ bits, contradicting the theorem that there are numbers $n$ which require at least $C\lg n$ bits to describe.
But none of this machinery reflects over to the question of twin primes, and worse, twin primes require (gasp) addition, something that plays notoriously poorly with factorization — the abc conjecture being maybe the canonical example of it. The factorizations of $n$ and $n+1$ seem largely independent (aside from, of course, not containing any of the same primes) and likewise the factorizations of $n$ and $n+2$, but as of right now none of the machinery we have really serves to prove this, and so this independence is entirely conjectural.


TITLE: General solution of the equation $\sin^{2015}(x)+\cos^{2015}(x) = 1\; \forall \; x\in \mathbb{R}$
QUESTION [2 upvotes]: Calculation of General solution of the equation $\sin^{2015}(x)+\cos^{2015}(x) = 1\; \forall \;x\in \mathbb{R}$.

$\bf{My\; Try:}$ We can Write the equation as $$\sin^{2015}(x)+\cos^{2015}(x)\leq \sin^2(x)+\cos^2(x)=1.$$
And equality hold when $$\sin(x)=1$$ and $$\cos (x) = 0.$$
So we get $$\displaystyle x=n\pi+(-1)^n\cdot \frac{\pi}{2}$$ and $$\displaystyle x=2n\pi\pm \frac{\pi}{2}.$$
Now How can I calculate common solution of $\sin (x) = 0$ and $\cos (x) = 0$.
Please help me. Thanks.

REPLY [1 votes]: $\sin^{2015}(x) + \cos^{2015}(x) = 1 = \sin^2(x) + \cos^2(x)$
or, $\left[\sin^2(x) \left(\sin^{2013}(x)-1 \right) \right]+ \left[ \cos^2(x) \left( \cos^{2013}(x)-1 \right) \right]= 0$
Since $\sin^2(x) \geq 0$ and $\cos^2(x) \geq 0$, this is possible only if both
$\left[\sin^2(x) \left(\sin^{2013}(x)-1 \right) \right]= 0$
and
$\left[ \cos^2(x) \left( \cos^{2013}(x)-1 \right) \right]= 0$
That is possible if either

$\sin^2(x) = 0$ and $\left( \cos^{2013}(x)-1 \right) = 0$
$\implies \sin(x) = 0$ and $\cos(x) = 1 \implies x = 2n \pi$

or

$\cos^2(x) = 0$ and $\left(\sin^{2013}(x)-1 \right) = 0$
$\implies \cos(x) = 0$ and $\sin(x) = 1 \implies x = (4n+1)\frac{\pi}{2}$


TITLE: Volume related to rotating over y=-1
QUESTION [0 upvotes]: Use the method of cylindrical shells to find the volume of the solid obtained by rotating the region bounded by the following curves about the line y=−1.
$y=x^2$ and $x=y^2$
Visual of ^^
What I got so far was $\int_{0}^1 2\pi (y+1) (y^2-y^\frac{1}{2}) dy$, when I solve it though I get $-\frac{29\pi}{30}$. This is the wrong answer can someone tell me where I did something wrong? Because I can not tell.

REPLY [1 votes]: What doobdood said was right all I had to do was changed $y^2-y^\frac{1}{2}$ to $y^\frac{1}{2} - y^2$, where the answer to the question would be $\frac{29\pi}{30}$ if the correct answer.
Thank you Doobdood.


TITLE: What is the historical origin of the term action
QUESTION [14 upvotes]: In Physics ordinary terms often acquire a strange meaning, action is one of them. Most people I talk to about the term action just respond with "its dimension is energy*time". But what is its historial origin?
http://en.wikipedia.org/wiki/Action_(physics)#History doesn't really give much insight, as it lacks citations and depth.
So, how did "action" become to mean what it means now?
Cheers

REPLY [9 votes]: See this better introduction to the history:

http://en.wikipedia.org/wiki/Principle_of_least_action#Origins.2C_statement.2C_and_the_controversy

Of course, the notion of "action" only becomes meaningful when one actually knows what the purpose of the action is - to be minimized. Around 1744 and 1746, Pierre Louis Maupertuis figured out that this could be a way to formulate laws of physics when he generalized Fermat's 17th century "principle of least time" (for the trajectory taken by light in any environment with a variable index of refraction) by this proverb:

Nature is thrifty in all its actions.

Obviously, some word had to be constructed or borrowed to describe the new quantity whose importance was previously unknown to the humans (and remains to be unknown to most humans even today).
Note that the word "actions" appeared as the only noun of the quote in the context of these minimization problems, so it became known as Wirkung ($W$) in German and action ($S$) in English. I am actually not sure why the letter $S$ was chosen.
There have been claims that Leibniz had found the principle as early as in 1707.
Maupertuis also wrote:

The laws of movement and of rest deduced from this principle being precisely the same as those observed in nature, we can admire the application of it to all phenomena. The movement of animals, the vegetative growth of plants ... are only its consequences; and the spectacle of the universe becomes so much the grander, so much more beautiful, the worthier of its Author, when one knows that a small number of laws, most wisely established, suffice for all movements.


TITLE: Takesaki theorem 2.6
QUESTION [1 upvotes]: Consider the following theorem in Takesaki's book "Theory of operator algebras". In particular, I'm focussed on understanding (ii). It is not mentioned in the picture, but $S$ is the unit ball of $\mathscr{L}(\mathfrak{h}).$

I can see that $(ii.1) \iff (ii.2)\iff (ii.3)\iff (ii.4)$ and that $(ii.5)\implies (ii.6)\implies (ii.7)$. Also, since the 'weaker' topologies agree with their $\sigma$-counterparts on bounded subsets, it is also clear that $(ii.x)\implies (ii.x+4)$ for $x=1,2,3$.
However, why do the other implications hold? The author just says that this follows by general theory of topological vector spaces, so if anyone can fill in the gap that would be great. In particular, I think it will be sufficient to know how I can prove $(ii.7)\implies (ii.3).$

REPLY [0 votes]: This question has been asked afterwards in Math Overflow, where it received three very good answers.

I don't know how Takesaki thinks of this. I do know that it takes Kadison-Ringrose several pages to prove the implication (ii.6)$\implies$(ii.4).
Roughly, they show

that strongly continuous on the ball implies normal
that normal (via complete additivity) implies (ii.4). This is Theorem 7.1.9 in Kadison-Ringrose II (and the result comparable to the one you quote is 7.1.12). The proof (including 7.1.8, that is used) is about 2 pages long.