TITLE: What is a(n algebro-geometric) family of modular forms?
QUESTION [10 upvotes]: We know that a family of elliptic curves is a morphism of schemes $f:X \to Y$ such that the fiber of every point of $Y$ is an elliptic curve (and we usually require the morphism to be smooth, proper, etc).
Given such a family, we can take the $\ell$-adic representation associated to any given fiber, and in this sense we also have a "family" of Galois representations. (Alternatively, by the proper base change theorem in étale cohomology, we can take $R^1f_*(\mathbb{Z}_{\ell})$, which is a sheaf on $Y$, and the stalks of this sheaf are the duals of the above Galois representations).
Now consider different question. Can we have a "family" of cuspidal eigenforms whose associated Galois representations fit into a family in the above sense?
I'll consider the case of weight 2 (though I'm most interested in higher weight). Then such family should lead to a family of RM abelian varieties, i.e. those associated to the weight 2 cusp forms.
Let's go back to the elliptic curve (or abelian variety) side a bit, and think about what this would mean. The level of a modular form corresponds to the conductor of the associated elliptic curve, so the level of the modular forms in such a family should be just as bizarre a function of the base as is the conductor of a family of curves.
To try to engineer such a family, suppose we had a family of elliptic curves that were all known to be modular. I'm most interested in rational families, i.e. with open subsets of projective space as bases. Then if the family is defined over $\mathbb{Q}$, we at least know that the fibers of rational points are modular, and we get a "family" of modular forms over the rational points. What would this "family" look like? I have a feeling it would be pretty strange from the point of view of modular forms.
A different approach is to try to to construct a family of modular curves, then view a family of modular forms as a section of the relative cotangent sheaf or some power thereof. Maybe one could try to make it an "eigensection" of some sort of relative Hecke operators. Of course, the very idea of a family of modular curves seems strange, as there are countably-many modular curves!
In fact, this points to a general problem with this attempt: modular forms are based on discrete data, a discrete set of levels, and a discrete set of eigenforms within each level.
I have a feeling that it's impossible to make this notion work, but please let me know if you have good ideas. In particular, it's possible that experts in modular forms and curves would have more ideas.

REPLY [3 votes]: Perhaps it is easier to explain what's going on here in the context of Galois representations. I know of two almost wholly disjoint ideas that are, confusingly, both described using phrases like "families of Galois representations".

One can consider "families of representations" of any group, which are just homomorphisms from G to GL_n(A) for some (usually commutative) ring A, or more generally GL(V) for some locally free sheaf V on a base scheme S, etc. These are "families" in the sense that the image of a group element is a matrix whose entries are functions on Spec(A) (resp. on S, etc). Note that, intuitively, the group is fixed and the coefficients are varying.
One can also consider the kind of "geometric" family you mentioned in your question and Michigan J Frog enlarged upon: given a family of geometric objects over a base S, you can do various kinds of relative cohomology to give sheaves on S whose fibres have an action of some kind of Galois group depending on the fibre, and in particular the generic fibre has an action of something like the fundamental group of S. So here the group is, so to speak, varying in the family as well.

The first kind of family, over a p-adic base and with G being a Galois group, comes up a lot in the context of modular forms (Hida, Coleman-Mazur, etc). These can be viewed as sections of a family of sheaves on a subvariety of the rigid-analytic space you get by analytifying the modular curve. Note that we are varying the coefficients and not the group, again.
The second kind of family doesn't come up so much in modular form theory, although it makes a notable appearance in Kato's work on Iwasawa theory for modular forms.


TITLE: MRB constant proofs wanted
QUESTION [5 upvotes]: This article has been edited for a bounty.
$C$ MRB, the MRB constant, is defined at http://mathworld.wolfram.com/MRBConstant.html .
There is an excellent 56 page paper whose author has passed away. You can find it in Google Scholar "MRB constant," Better yet, use the following link http://web.archive.org/web/20130430193005/http://www.perfscipress.com/papers/UniversalTOC25.pdf. You find a cached copy there.
Just before the author, Richerd Crandall, died I wrote him about a possible small error. What I'm worried about is formula 44 on page 29 and below. When I naively worked formula 44 it needed a negative sign in front of it. Crandall did write me back admitting to a typo, but he died before he had a chance to correct it.
  Is there anyone out there competent enough to check, correct and prove the corrected
formulas for me? Thank you. I will use the proofs often and try to get the formulas published more.

Here is how I worked formula 44 and got -B:
(*define the Dirichlet eta function*)
eta[s_] := (1 - 2^(1 - s)) Zeta[s];
(*define the higher derivatives of the eta(0)*)
a[i_] := Derivative[i][eta][0];
(*Define c:*)
c[j_] := Sum[Binomial[j, d](-1)^dd^(j - d), {d, 1, j}]
(*formula (44)*)
N[Sum[c[m]/m!*a[m], {m, 1, 40}], 100]

REPLY [1 votes]: The first equality can be reproduced by formally stating the double sum: write down the expanded exponantial series for each term in one row, sum then column-wise to get the derivatives of the $\eta()$ and sum then the $\eta()$-expressions. Here the $\eta(s)$ is the alternating $\zeta(s)$ and $\eta^{(m)}(s)$ the $m$'th derivative.
$$ \begin{array} {rclll}
 -\exp( {\log(1) \over 1})+1 & = & -{\log(1) \over 1}
                                   &-{\log(1)^2 \over 1^2 2!}
                                   &-{\log(1)^3 \over 1^3 3!} & - \cdots \\
 +\exp( {\log(2) \over 2})-1 & = &+{\log(2) \over 2}
                                   &+{\log(2)^2 \over 2^2 2!}
                                   &+{\log(2)^3 \over 2^3 3!} & + \cdots \\
 -\exp( {\log(3) \over 3})+1 & = &-{\log(3) \over 3}
                                   &-{\log(3)^2 \over 3^2 2!}
                                   &-{\log(3)^3 \over 3^3 3!} & - \cdots \\
    \vdots \qquad                  & \vdots & \quad\vdots & \quad\vdots& \quad\vdots
         & \ddots \\
\hline \\
    B \qquad & = &   {\eta^{(1)}(1) \over 1!}
                  &- {\eta^{(2)}(2) \over 2!}
                  &+ {\eta^{(3)}(3) \over 3!} & - \cdots
\end{array}$$
I've not yet the expansion into the formula with the derivatives of $\eta()$ at zero; perhaps I can supply that tomorrow.

Numerical check
In Pari/GP I get for the original sum
$$ B = \sum_{k=1}^\infty (-1)^k( \exp( \log(k)/k)-1)$$
                           B=sumalt(k=1,(-1)^k * (exp( log(k)/k) -1)

well converging the value
       B=0.187859642462067120248517934054273230055903094900138786172005...

as well for
                         B = -sum(k=1,6,(-1)^k*aetad(k,k)/k!)

(but to fewer digits).
My user-defined function aetad(s,d) gives the d'th derivative of $\eta()$ at $s$ and I implemented that aeta() using the $\eta()$ / $\zeta()$ conversion formula
              aeta(s) = if(s==1,return(log(2));return( (1-2/2^s)*zeta(s)  )
              {aetad(s=1,d=0)=local(h1=1e-12,z);
                      z= sum(k=0,d,  (-1)^k*binomial(d,k)*aeta(s +(d/2-k)*h1));
                         return( z/h1^d); }

I have also another implementation of the $\eta()$ and its derivatives which allows to access higher derivatives (in the above version the 10'th or even 20'th derivative were impractical). This version is also independent of the software-included zeta-function but uses Pari/GP's sumalt() procedure which allows to evaluate alternating (moderately) divergent series. My approach computes the taylor-expansion for the $\eta()$ function by default centered around zero but can easily be generalized to any center:
fmt(200,12)  \\ user defined; set internal precision to 200 digits, display to 12 digits
default(seriesexpansion,24)          \\ set expansion-limit for power series
m_coeffs = vectorv(24);              \\ vector for 24 aeta-taylor-series
{for(m=0,23,
    tay_aeta = sumalt(k=0,(-1)^k/(1+k)^(x+m));  \\ taylorseries for aeta around m
    m_coeffs[1+m]= polcoeffs(tay_aeta,24);      \\ store leading 24 taylorcoefficients
   );
  m_coeffs = Mat(m_coeffs);}        \\ make a matrix from the list of taylor series

After that, the desired coefficients (the derivatives of the $\eta(m)$ )  nicely divided by the factorials, occur on the diagonal of the coefficients-matrix, and we only need sum them with alternating sign:
   B = sum (k=1,23, -(-1)^k*m_coeffs[1+k,1+k])
   \\ 0.1878596424620671202485179340542732... the leading correct digits


TITLE: Solution of Exponential Cauchy Equation $ f ( x + y ) = f ( x ) f ( y ) $
QUESTION [1 upvotes]: I was reading Functional Equations and I came across the following theorem regarding the solution of the exponential Cauchy functional equation:
$$ f ( x + y ) = f ( x ) f ( y ) \text . $$

Let $ f : D \to \mathbb R $ be a solution of the exponential Cauchy equation, where $ D = \mathbb R $ or $ D = ( 0 , + \infty ) $. Then either $ f \equiv 0 $ or $ f ( x ) = 10 ^ { g ( x ) } $, where $ g : D \to \mathbb R $ is an additive function.

Please help me by providing a pedantic proof to the very theorem as I am unable to find it online.

REPLY [1 votes]: Let $ D \in \{ \mathbb R , ( 0 , + \infty ) \} $ and $ f : D \to \mathbb R $ be such that
$$ f ( x + y ) = f ( x ) f ( y ) \tag 0 \label 0 $$
forall $ x , y \in D $. Substituting $ \frac x 2 $ for both $ x $ and $ y $ in \eqref{0} we get $ f ( x ) = f \left( \frac x 2 \right) ^ 2 \ge 0 $ and thus
$$ \operatorname {ran} f \subseteq [ 0 , + \infty ) \text . \tag 1 \label 1 $$
Case $ D = \mathbb R $:
We can put $ x = y = 0 $ in \eqref{0} and find out that $ f ( 0 ) \in \{ 0 , 1 \} $. If $ f ( 0 ) = 0 $, setting $ y = 0 $ in \eqref{0} shows that $ f $ is constantly zero. If $ f ( 0 ) = 1 $, substituting $ - x $ for $ y $ in \eqref{0} we get $ f ( x ) f ( - x ) = 1 $, which in particular shows that $ f ( x ) \ne 0 $, and thus by \eqref{1}, $ f ( x ) > 0 $. This lets us define $ g : \mathbb R \to \mathbb R $ by $ g ( x ) = \log _ { 10 } f ( x ) $, and taking base $ 10 $ logarithm from both sides of \eqref{0}, we find out that $ g $ is additive. Thus we found an additive function $ g : D \to \mathbb R $ such that $ f ( x ) = 10 ^ { g ( x ) } $ for all $ x \in D $.
Case $ D = ( 0 , + \infty ) $:
If there is $ a \in D $ such that $ f ( a ) = 0 $, letting $ y = a $ in \eqref{0}, we get $ f ( x + a ) = 0 $ for all $ x \in D $. For every $ x > a $, $ x - a \in D $ and thus we can substitue $ x - a $ for $ x $ in the last equation, which gives $ f ( x ) = 0 $ for all $ x > a $. We can also use induction to derive $ f ( n x ) = f ( x ) ^ n $ for all $ x \in D $ and all positive integers $ n $, from \eqref{0}. Choosing $ n $ so that $ n x > a $, we can conclude that $ f $ is constantly zero. So assume that there is no $ a \in D $ with $ f ( a ) = 0 $. By \eqref{1}, we find out that $ \operatorname {ran} f \subseteq ( 0 , + \infty ) $, and we can conclude that there is an additive function $ g : D \to \mathbb R $ such that $ f ( x ) = 10 ^ { g ( x ) } $ for all $ x \in D $, similar to before.


text:
(*
    File:     Set_Multiplication.thy
    Author:   Joseph Thommes, TU München
*)
section \<open>Set Multiplication\<close>

theory Set_Multiplication
  imports "HOL-Algebra.Multiplicative_Group"
begin

text \<open>This theory/section is of auxiliary nature and is mainly used to establish a connection
between the set multiplication and the multiplication of subgroups via the \<open>IDirProd\<close> (although this
particular notion is introduced later). However, as in every section of this entry, there are some
lemmas that do not have any further usage in this entry, but are of interest just by themselves.\<close>

lemma (in group) set_mult_union:
  "A <#> (B \<union> C) = (A <#> B) \<union> (A <#> C)"
  unfolding set_mult_def by auto

lemma (in group) set_mult_card_single_el_eq:
  assumes "J \<subseteq> carrier G" "x \<in> carrier G"
  shows "card (l_coset G x J) = card J" unfolding l_coset_def
proof -
  have "card ((\<otimes>) x ` J) = card J"
    using inj_on_cmult[of x] card_image[of "(\<otimes>) x" J] assms inj_on_subset[of "(\<otimes>) x" "carrier G" J]
    by blast
  moreover have "(\<Union>y\<in>J. {x \<otimes> y}) = (\<otimes>) x ` J" using image_def[of "(\<otimes>) x" J] by blast
  ultimately show "card (\<Union>h\<in>J. {x \<otimes> h}) = card J" by presburger
qed

text \<open>We find an upper bound for the cardinality of a set product.\<close>

lemma (in group) set_mult_card_le:
  assumes "finite H" "H \<subseteq> carrier G" "J \<subseteq> carrier G"
  shows "card (H <#> J) \<le> card H * card J"
  using assms
proof (induction "card H" arbitrary: H)
  case 0
  then have "H = {}" by force
  then show ?case using set_mult_def[of G H J] by simp
next
  case (Suc n)
  then obtain a where a_def: "a \<in> H" by fastforce
  then have c_n: "card (H - {a}) = n" using Suc by force
  then have "card ((H - {a}) <#> J) \<le> card (H - {a}) * card J" using Suc by blast
  moreover have "card ({a} <#> J) = card J"
    using Suc(4, 5) a_def set_mult_card_single_el_eq[of J a] l_coset_eq_set_mult[of G a J] by auto
  moreover have "H <#> J = (H - {a} <#> J) \<union> ({a} <#> J)" using set_mult_def[of G _ J] a_def by auto
  moreover have "card (H - {a}) * card J + card J = Suc n * card J" using c_n mult_Suc by presburger
  ultimately show ?case using card_Un_le[of "H - {a} <#> J" "{a} <#> J"] c_n \<open>Suc n = card H\<close> by auto
qed

lemma (in group) set_mult_finite:
  assumes "finite H" "finite J" "H \<subseteq> carrier G" "J \<subseteq> carrier G"
  shows "finite (H <#> J)"
  using assms set_mult_def[of G H J] by auto

text \<open>The next lemma allows us to later to derive that two finite subgroups $J$ and $H$ are complementary
if and only if their product has the cardinality $|J| \cdot |H|$.\<close>

lemma (in group) set_mult_card_eq_impl_empty_inter:
  assumes "finite H" "finite J" "H \<subseteq> carrier G" "J \<subseteq> carrier G" "card (H <#> J) = card H * card J"
  shows "\<And>a b. \<lbrakk>a \<in> H; b \<in> H; a \<noteq> b\<rbrakk> \<Longrightarrow> ((\<otimes>) a ` J) \<inter> ((\<otimes>) b ` J) = {}"
  using assms
proof (induction H rule: finite_induct)
  case empty
  then show ?case by fast
next
  case step: (insert x H)
  from step have x_c: "x \<in> carrier G" by simp
  from step have H_c: "H \<subseteq> carrier G" by simp
  from set_mult_card_single_el_eq[of J x] have card_x: "card ({x} <#> J) = card J"
    using \<open>J \<subseteq> carrier G\<close> x_c l_coset_eq_set_mult by metis
  moreover have ins: "(insert x H) <#> J = (H <#> J) \<union> ({x} <#> J)"
    using set_mult_def[of G _ J] by auto
  ultimately have "card (H <#> J) \<ge> card H * card J"
    using card_Un_le[of "H <#> J" "{x} <#> J"] \<open>card (insert x H <#> J) = card (insert x H) * card J\<close>
    by (simp add: step.hyps(1) step.hyps(2))
  then have card_eq:"card (H <#> J) = card H * card J"
    using set_mult_card_le[of H J] step H_c by linarith
  then have ih: "\<And>a b. \<lbrakk>a \<in> H; b \<in> H; a \<noteq> b\<rbrakk> \<Longrightarrow> ((\<otimes>) a ` J) \<inter> ((\<otimes>) b ` J) = {}"
    using step H_c by presburger

  have "card (insert x H) * card J = card H * card J + card J" using \<open>x \<notin> H\<close> using step by simp
  then have "({x} <#> J) \<inter> (H <#> J) = {}"
    using card_eq card_x ins card_Un_Int[of "H <#> J" "{x} <#> J"] step set_mult_finite by auto
  then have "\<And>a. a \<in> H \<Longrightarrow> (\<Union>y\<in>J. {a \<otimes> y}) \<inter> (\<Union>y\<in>J. {x \<otimes> y}) = {}"
    using set_mult_def[of G _ J] by blast
  then have "\<And>a b. \<lbrakk>a \<in> (insert x H); b \<in> (insert x H); a \<noteq> b\<rbrakk> \<Longrightarrow> ((\<otimes>) a ` J) \<inter> ((\<otimes>) b ` J) = {}"
    using \<open>x \<notin> H\<close> ih by blast
  then show ?case using step by presburger
qed

lemma (in group) set_mult_card_eq_impl_empty_inter':
  assumes "finite H" "finite J" "H \<subseteq> carrier G" "J \<subseteq> carrier G" "card (H <#> J) = card H * card J"
  shows "\<And>a b. \<lbrakk>a \<in> H; b \<in> H; a \<noteq> b\<rbrakk> \<Longrightarrow> (l_coset G a J) \<inter> (l_coset G b J) = {}"
  unfolding l_coset_def
  using set_mult_card_eq_impl_empty_inter image_def[of "(\<otimes>) _" J] assms by blast

lemma (in comm_group) set_mult_comm:
  assumes "H \<subseteq> carrier G" "J \<subseteq> carrier G"
  shows "(H <#> J) = (J <#> H)"
  unfolding set_mult_def
proof -
  have 1: "\<And>a b. \<lbrakk>a \<in> carrier G; b \<in> carrier G\<rbrakk> \<Longrightarrow> {a \<otimes> b} = {b \<otimes> a}" using m_comm by simp
  then have "\<And>a b.\<lbrakk>a \<in> H; b \<in> J\<rbrakk> \<Longrightarrow> {a \<otimes> b} = {b \<otimes> a}" using assms by auto
  moreover have "\<And>a b.\<lbrakk>b \<in> H; a \<in> J\<rbrakk> \<Longrightarrow> {a \<otimes> b} = {b \<otimes> a}" using assms 1 by auto
  ultimately show "(\<Union>h\<in>H. \<Union>k\<in>J. {h \<otimes> k}) = (\<Union>k\<in>J. \<Union>h\<in>H. {k \<otimes> h})"  by fast
qed

lemma (in group) set_mult_one_imp_inc:
  assumes "\<one> \<in> A" "A \<subseteq> carrier G" "B \<subseteq> carrier G"
  shows "B \<subseteq> (B <#> A)"
proof
  fix x
  assume "x \<in> B"
  thus "x \<in> (B <#> A)" using assms unfolding set_mult_def by force
qed

text \<open>In all cases, we know that the product of two sets is always contained in the subgroup
generated by them.\<close>
lemma (in group) set_mult_subset_generate:
  assumes "A \<subseteq> carrier G" "B \<subseteq> carrier G"
  shows "A <#> B \<subseteq> generate G (A \<union> B)"
proof
  fix x
  assume "x \<in> A <#> B"
  then obtain a b where ab: "a \<in> A" "b \<in> B" "x = a \<otimes> b" unfolding set_mult_def by blast
  then have "a \<in> generate G (A \<union> B)" "b \<in> generate G (A \<union> B)"
    using generate.incl[of _ "A \<union> B" G] by simp+
  thus "x \<in> generate G (A \<union> B)" using ab generate.eng by metis
qed

text \<open>In the case of subgroups, the set product is just the subgroup generated by both
of the subgroups.\<close>

lemma (in comm_group) set_mult_eq_generate_subgroup:
  assumes "subgroup H G" "subgroup J G"
  shows "generate G (H \<union> J) = H <#> J" (is "?L = ?R")
proof
  show "?L \<subseteq> ?R"
  proof
    fix x
    assume "x \<in> ?L"
    then show "x \<in> ?R"
    proof(induction rule: generate.induct)
      case one
      have "\<one> \<otimes> \<one> = \<one>" using nat_pow_one[of 2] by simp
      thus ?case
        using assms subgroup.one_closed[OF assms(1)]
              subgroup.one_closed[OF assms(2)] set_mult_def[of G H J] by fastforce
    next
      case (incl x)
      have H1: "\<one> \<in> H" using assms subgroup.one_closed by auto
      have J1: "\<one> \<in> J" using assms subgroup.one_closed by auto
      have lx: "x \<otimes> \<one> = x" using r_one[of x] incl subgroup.subset assms by blast
      have rx: "\<one> \<otimes> x = x" using l_one[of x] incl subgroup.subset assms by blast
      show ?case
      proof (cases "x \<in> H")
        case True
        then show ?thesis using set_mult_def J1 lx by fastforce
      next
        case False
        then show ?thesis using set_mult_def H1 rx incl by fastforce
      qed
    next
      case (inv h)
      then have inv_in:"(inv h) \<in> H \<union> J" (is "?iv \<in> H \<union> J")
        using assms subgroup.m_inv_closed[of _ G h] by (cases "h \<in> H"; blast)
      have H1: "\<one> \<in> H" using assms subgroup.one_closed by auto
      have J1: "\<one> \<in> J" using assms subgroup.one_closed by auto
      have lx: "?iv \<otimes> \<one> = ?iv" using r_one[of "?iv"] subgroup.subset inv_in assms by blast
      have rx: "\<one> \<otimes> ?iv = ?iv" using l_one[of "?iv"] incl subgroup.subset inv_in assms by blast
      show ?case
      proof (cases "?iv \<in> H")
        case True
        then show ?thesis using set_mult_def[of G H J] J1 lx by fastforce
      next
        case False
        then show ?thesis using set_mult_def[of G H J] H1 rx inv_in by fastforce
      qed
    next
      case (eng h g)
      from eng(3) obtain a b where aH: "a \<in> H" and bJ: "b \<in> J" and h_def: "h = a \<otimes> b"
        using set_mult_def[of G H J] by fast
      have a_carr: "a \<in> carrier G" by (metis subgroup.mem_carrier assms(1) aH)
      have b_carr: "b \<in> carrier G" by (metis subgroup.mem_carrier assms(2) bJ)
      from eng(4) obtain c d where cH: "c \<in> H" and dJ: "d \<in> J" and g_def: "g = c \<otimes> d"
        using set_mult_def[of G H J] by fast
      have c_carr: "c \<in> carrier G" by (metis subgroup.mem_carrier assms(1) cH)
      have d_carr: "d \<in> carrier G" by (metis subgroup.mem_carrier assms(2) dJ)
      then have "h \<otimes> g = (a \<otimes> c) \<otimes> (b \<otimes> d)"
        using a_carr b_carr c_carr d_carr g_def h_def m_assoc m_comm by force
      moreover have "a \<otimes> c \<in> H" using assms(1) aH cH subgroup.m_closed by fast
      moreover have "b \<otimes> d \<in> J" using assms(2) bJ dJ subgroup.m_closed by fast
      ultimately show ?case using set_mult_def by fast
    qed
  qed
next
  show "?R \<subseteq> ?L" using set_mult_subset_generate[of H J] subgroup.subset assms by blast
qed

end

subset_name: curated


TITLE: Tricks - Prove Homomorphism Maps Identity to Identity - Fraleigh p. 128 Theorem 13.12(1.)
QUESTION [11 upvotes]: Let $\phi$ be a homomorphism of a group G into a group G'.
If $e =$ the identity element in G, then $\phi(e) =$ the identity element in G'.
Is this what Sharkos is trying to answer:
About homomorphisms, you only know $\phi(a) \phi(b) = \phi(ab)$.
ab is more complicated than anything we want to think about, hence just presuppose $b = e$.
Then $ \begin{align} \phi(a)\phi(e) & = \phi(a\color{magenta}{e}) \\ & = \phi(a) \end{align} $
Left multiply the last equation  by $\color{green}{\phi(a)^{-1}}$: $\quad \phi(e) =  id_{G'}.$

(1.) How do you predestine to rewrite $a$ as   $ a = a\color{magenta}{e}$?
  Or to 'presuppose $b = e$' ? I understand neither tricks.
(2.) What's the intuition?

REPLY [1 votes]: Without digging into any thing deep or complicated, you only have three pieces of knowledge:

$e'$ is the only element that ever satisfies an equation in $G'$ of the form $e'x = x$ or $ye' = y$
$e$ satisfies equations in $G$ of the form $ex = x$ and $ye = y$
$\phi(xy) = \phi(x) \phi(y)$  (and similarly for products of more than two things)

By the first point, if you want to prove $\phi(e) = e'$, the only option we have (if we want to use these simple pieces of knowledge) is to find an equation $\phi(e)x = x$ or $y \phi(e) = y$. Trying to figure out how to use the other pieces of information to do this leads to a proof.
The proof could also have been derived from a simple approach of "I have facts, I'll do something with them and see if the result is useful". e.g. looking at the second and third points and seeing that you can combine them... so you do so, and see if the result is useful. (and it turns out to be exactly what you need to use the first point to complete the proof)


TITLE: An identity involving the stationary measure of a Markov Chain
QUESTION [0 upvotes]: (Note this is a problem from Durrett, so I apologize if the notation is not standard)
Let $X_n$ be a Markov Chain, and $x$ a recurrent state. If we let $T= \inf \{n\ge 1: X_n=x\}$, then
$$
\mu_x(y) := \mathbb{E}_x \left ( \sum_{n=0}^{T-1} 1_{\{X_n=y\}} \right)
$$
is a stationary measure. If we let $T_x$ and $T_y$ be the first time we hit/return to $x$ and $y$ respectively, define $w_{xy} = P_x(T_y <T_x)$. I would like to show $\mu_x(y) = w_{xy} / w_{yx}$.
Unfortunately, I'm not sure where to begin. I know that if the transition probability $p$ is both irreducible and recurrent, then the above measure is unique up to constant multiples, which I can then perhaps abuse as in other problems in this section, but unfortunately I'm not given that.
I'd greatly appreciate a hint on where to start.

REPLY [3 votes]: This is not a complete answer, but I hope it is complete enough for you fill the gaps, ok?
So, $\mu_x(y)$ counts the number of visits to $y$ before we return to $x$. In order to $\mu_x(y)$ be non-zero, the Markov chain $(X_n)_{n\ge 0}$ must hit $y$ before $x$, this explains the factor $P_x(T_y < T_x^{+})$.
Now we hit $y$ for the first time, using the Strong Markov Property, we restart the process starting from $y$ and now we hit $y$ again with probability $P_y(T_x > T_y^{+})$. So, the number of returning to $y$ follows a Geometric distribution with parameter $P_y(T_x > T_y^{+})$.
A success here is returning to $y$ before $X$ hits $x$.
In case you have any problem understanding the argument, I can elaborate it.


TITLE: What are good resources for learning predicate logic / predicate calculus?
QUESTION [9 upvotes]: I'm trying to learn predicate logic.
And I'm looking for some good resources on it:
I've seen that I learn better when I can program
So I was wondering if there was a 'predicate logic' programning language?
Maybe an interactive tutorial?
Maybe lots of examples, something like: Predicate Logic by Example?
Or at least some pretty basic books?
TIA

REPLY [3 votes]: There are lots of good books on symbolic logic, Understanding Symbolic Logic being one.
However, there aren't many of them using a "programming" approach, Haskell Road to Logic, Maths, and programming being such a gem.


TITLE: Expected value from covariances and variances
QUESTION [1 upvotes]: I am given three r.v $X_1, X_2, X_3$, $Cov(X_1,X_2), Cov(X_2, X_3), Cov(X_1,X_3)$ and $Var(X_1), Var(X_2), Var(X_3)$. From the given, is it possible to find $E(Y)$ where $Y = a_1X_1 + a_2X_2 + a_3X_3$?

REPLY [1 votes]: No, that is not possible without further information.
If for $i=1,2,3$ we have $X_i'=X_i+p_i$ then we find exactly the same covariances and variances in the sense that: $$\mathsf{Cov}(X_i',X_j')=\mathsf{Cov}(X_i,X_j)$$for $i,j=1,2,3$.
However this with: $$Y'=a_1X_1'+a_2X_2'+a_3X_3'=Y+a_1p_1+a_2p_2+a_3p_3$$ so that: $$\mathbb EY'=\mathbb EY+a_1p_1+a_2p_2+a_3p_3$$


TITLE: 3D cohen-sutherland clliping algorithm
QUESTION [0 upvotes]: I would like to know what is the right way to convert the known 2d algorithm into a 3d algorithm.
Thanks!

REPLY [2 votes]: Look up
"cohen-sutherland 3d clipping".
You will get a number of hits.
This is one:
//www.cs.drexel.edu/~david/Classes/CS430/Lectures/L-14_Color.6.pdf


TITLE: O-minimal Theories with Non-Dense Order Type
QUESTION [5 upvotes]: In this paper, Knight, Pillay, and Steinhorn prove that for any O-minimal structure $\mathfrak{A}$, in which the underlying order types is dense, and if $\mathfrak{B} \equiv \mathfrak{A}$, then $\mathfrak{B}$ is also O-minimal. Is there a counterexample for when the underlying order type is not dense? I haven't been able to construct one.
Thanks

REPLY [3 votes]: Pillay and Steinhorn extended the result to o-minimal structures of arbitrary order-type in the third paper in the series.


TITLE: When the maximum of sum is equal to the sum of maxima
QUESTION [0 upvotes]: Consider a function $f:\mathcal{X\times \mathcal{Y}}\rightarrow [0,1]$ where

$\mathcal{X}\equiv \{x_1,x_2,x_3,x_4\}$.
$\mathcal{Y}\equiv \{y_1,y_2\}$.
$g(x)\equiv \sum_{y\in \mathcal{Y}}f(x,y)\in (0,1)$ $\forall x\in \mathcal{X}$
$h(y)\equiv \sum_{x\in \mathcal{X}}f(x,y)\in (0,1)$ $\forall y\in \mathcal{Y}$
$\sum_{x\in \mathcal{X}}g(x)=1$
$\sum_{y\in \mathcal{Y}}h(y)=1$
$g(x_1)>g(x_2)>g(x_3)>g(x_4)$

By the relations above
$$
g(x_1)=\max_{x\in \mathcal{X}} g(x)
$$
Is it correct that
$$
g(x_1)=\max_{x\in \mathcal{X}}f(x,y_1)+\max_{x\in \mathcal{X}}f(x,y_2)
$$
?

My thoughts:
Note that, by definition,
$$
g(x_1)=\max_{x\in \mathcal{X}} (f(x,y_1)+f(x,y_2))
$$
I know that in general the maximum of sums is, at most, sum of maximums (e.g., Elegant proof that maximum of sums is, at most, sum of maximums). However, I'm wondering whether the above relations are sufficient for such relation to hold with equality. I cannot find a counter-example where the equality is not satisfied. Could you help?

REPLY [2 votes]: Let $f(x_1, y_1) = f(x_1, y_2) = \frac{1}{6}$, $f(x_2, y_1) =  \frac{1}{4}$,$f(x_3, y_2) =  \frac{1}{4} - \epsilon$, $f(x_2, y_2) = f(x_3, y_1) = 0$, $f(x_4, y_1) = f(x_4, y_2) = \frac{1}{12} + \frac{\epsilon}{2}$, and let $\epsilon = \frac{1}{100}$ Note that this satisfies all your conditions, but $g(x_1) = \frac{1}{3} < \frac{1}{4} + \frac{1}{4} - \frac{1}{100} = \max_x f(x, y_1) + \max_x f(x, y_2)$


TITLE: Proving that $\lim\limits_{R\to\infty}\int_0^\pi e^{-R\sin\theta}d\theta=0$
QUESTION [1 upvotes]: I want to show that the limit below is zero.
$$\lim_{R\to\infty}\int_0^\pi e^{-R\sin\theta}d\theta$$
Wolframalpha and my intuition say that the limit is truly zero but I cannot approach.
Any hints will be appreciated. Thanks.

REPLY [3 votes]: This is a very nice question.
First split the integral involves  at $\theta=\frac{\pi}{2}$ then take the change of variable $\theta'=\pi -\theta$
$$ \int_0^\pi e^{-R\sin\theta}d\theta =2\int_0^{\frac{\pi}{2}} e^{-R\sin\theta}d\theta$$
afterward shows by studying the function $[0,\frac{\pi}{2}]\ni\theta \mapsto\frac{\sin\theta}{\theta}$ that
$$ \color{blue}{\sin\theta \geq \frac{2}{\pi}\theta ~~ \forall \theta\in [0,\frac{\pi}{2}] } $$
therefore we get that
$$\lim_{R\to\infty}\int_0^{\frac{\pi}{2}} e^{-R\sin\theta}d\theta\leq\lim_{R\to\infty}\int_0^{\frac{\pi}{2}} e^{-\frac{2R}{\pi}\theta}d\theta =\lim_{R\to\infty}\frac{\pi}{2R}(1-e^{-R}) =0$$


TITLE: Solving Initial Value Problem based on Advection Equation
QUESTION [0 upvotes]: Having some trouble with an Initial value problem based on the advection equation:
$$ u_t + cu_x = 0,    t > 0 $$
The problem itself is:
$$ u_t - x^2tu_x = 0, u(x,0) = x + 1 $$
Using the same method as I have other problems of this nature, I end up with a solution that doesn't fit the initial conditions, so perhaps someone can point out where I have gone wrong? Following the example of other problems of this format:
Slope of characteristic curves is $$ dx/dt = c(x,t) = -x^2t $$
Solving this for the characteristic curve equation I obtain:
$$-\int_{} 1/x^2 dx = \int_{}t dt$$
$$ x = 2/t^2 + K $$    (where K is a constant).
Letting (x,t) be an arbitrary point where we want to obtain a solution, it can be said the characteristic curve passing through (x,t) will pass through the x axis at (E,0) where the equation is:
$$x = 2/t^2 + E $$
Since u is constant along this curve:
$$ u(x,t) = u(E,0) = E + 1 = x - 2/t^2 + 1$$
However this fails the initial conditions. I can't see where I've gone wrong though, having followed a method that worked for a simpler c(x,t).Any help is appreciated.

REPLY [1 votes]: As far as I can see, I think you just did your algebra wrong.
After integrating separately 'x' and 't' and then solving for 'x', I believe you made an error.
The integrals give:
$$\frac{1}{x} = \frac{t^{2}}{2} + K$$
Simplifying
$$x = \frac{1}{(\frac{t^{2}}{2}+K)}$$
You could (if you wanted) pull out a factor of 1/2 in the denominator to get:
$$x = \frac{2}{t^{2}+2K}$$
But generally speaking, you cannot just invert the t^2/2 term like you have or divide the numerator by each term in the denominator. That algebra is incorrect.


TITLE: Length of supporting ropes in a two-pulley system
QUESTION [0 upvotes]: Say I want to find the length of each component. I thought that in an ideal two-pulley system, each side of the supporting rope has a length 1/2 of the effort distance. So if I want to lift an object 3m in the air, I would think each supporting rope has a length of 3m and the effort distance is 6m. According to Kaplan MCAT Physics book, “If, for example, the crate must be lifted to a shelf 3 m above the ground, then both sides of the supporting rope must be shortened by 3 meters, and the only way to accomplish this is by pulling through  6 meters of rope”. Why aren’t the supporting ropes 3 m each?

REPLY [0 votes]: The supporting ropes are not necessarily 3 metres each just because they are each shortened by 3 metres when the body is lifted through that height - they could be any length $l \geq 3$ metres and will just wind up 3 metres shorter, of length $l -3$ metres, once the action is complete. To summarise: "because the problem presented never implies it, and because that information is not needed to work out everything there is to know about the system".
This of course applies to an idealised system where we are assuming that

The physical components of the pulley, wheels, rope, et cetera, don't get in the way of one another, have negligible mass, and -
The supporting ropes are all perfectly vertical, such that the total length of rope reduced is exactly twice the displacement through which the weight is lifted.


TITLE: Sum of dependent Binomial distributions
QUESTION [0 upvotes]: In one of my classes, we stated that if $X_i$ are independent Bernoulli random variables with p proportion of success, then the distribution of the sum $\sum X_i$ is Binomial(n,p). I already proved this, but it got me thinking: if there is a distribution for the sum of these n Bernoulli random variables, is there a special distribution of the sum of n Binomial random variables?
I know there is a relationship between the Binomial distribution and the Binomial coefficient, and moreover that there is a relation between the Binomial coefficient and the Multinomial coefficient (i.e. the Binomial coefficient is a special case of the Multinomial coefficient). I know there is also such a thing as the Multinomial distribution, so my suspicion is that this distribution of the sum of Binomial random variables is somehow Multinomial. But, that's well beyond the scope of my class, so I was curious if there was some intuitive explanation about why it is or is not the Multinomial distribution.
Thanks so much!

REPLY [0 votes]: Consider the sequence $(X_k)_{k=1}^m$ where  $\forall k\in\Bbb N\cap [1;m] : X_k\sim\mathcal{Bin}(n,p)$ .
Each $X_k$ is a count of successes among $n$ independent Bernoulli distributions with identical success rate $p$.
Therefore $\sum\limits_{k=1}^m X_k$ is the count of successes among $m$ times $n$ independent Bernoulli distributions with identical success rate $p$.
Thus the sum on $m$ random variables with distribution $\mathcal{Bin}(n,p)$, is a random variable with a distribution of $\mathcal{Bin}(nm,p)$.

Remark: it is somewhat more complicated when the success rate is not identical.


text:
(*  Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com> *)

section \<open>Functions from A to B up to a Permutation on A and B\<close>

theory Twelvefold_Way_Entry10
imports Equiv_Relations_on_Functions
begin

subsection \<open>Definition of Bijections\<close>

definition number_partition_of :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set \<Rightarrow> nat multiset"
where
  "number_partition_of A B F = univ (\<lambda>f. image_mset (\<lambda>X. card X) (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) F"

definition functions_of :: "'a set \<Rightarrow> 'b set \<Rightarrow> nat multiset \<Rightarrow> ('a \<Rightarrow> 'b) set"
where
  "functions_of A B N = {f \<in> A \<rightarrow>\<^sub>E B. image_mset (\<lambda>X. card X) (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})) = N}"

subsection \<open>Properties for Bijections\<close>

lemma card_setsum_partition:
  assumes "finite A" "finite B" "f \<in> A \<rightarrow>\<^sub>E B"
  shows "sum card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card A"
proof -
  have "finite ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})"
    using \<open>finite B\<close> by blast
  moreover have "\<forall>X\<in>(\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}. finite X"
    using \<open>finite A\<close> by auto
  moreover have "\<Union>((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = A"
    using \<open>f \<in> A \<rightarrow>\<^sub>E B\<close> by auto
  ultimately show ?thesis
    by (subst card_Union_disjoint[symmetric]) (auto simp: pairwise_def disjnt_def)
qed

lemma number_partition_of:
  assumes "finite A" "finite B"
  assumes "F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B"
  shows "number_partition (card A) (number_partition_of A B F)"
  and "size (number_partition_of A B F) \<le> card B"
proof -
  from \<open>F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B\<close> obtain f where "f \<in> A \<rightarrow>\<^sub>E B"
    and F_eq: "F = domain_and_range_permutation A B `` {f}" using quotientE by blast
  have number_partition_of_eq: "number_partition_of A B F = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))"
  proof -
    have "number_partition_of A B F = univ (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) F"
      unfolding number_partition_of_def ..
    also have "\<dots> = univ (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) (domain_and_range_permutation A B `` {f})"
      unfolding F_eq ..
    also have "\<dots> = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))"
      using \<open>finite B\<close> equiv_domain_and_range_permutation multiset_of_partition_cards_respects_domain_and_range_permutation \<open>f \<in> A \<rightarrow>\<^sub>E B\<close>
      by (subst univ_commute') auto
    finally show ?thesis .
  qed
  show "number_partition (card A) (number_partition_of A B F)"
  proof -
    have "sum_mset (number_partition_of A B F) = card A"
      using number_partition_of_eq \<open>finite A\<close> \<open>finite B\<close> \<open>f \<in> A \<rightarrow>\<^sub>E B\<close>
      by (simp only: sum_unfold_sum_mset[symmetric] card_setsum_partition)
    moreover have "0 \<notin># number_partition_of A B F"
    proof -
      have "\<forall>X \<in> (\<lambda>b. {x \<in> A. f x = b}) ` B. finite X"
        using \<open>finite A\<close> by simp
      from this have "\<forall>X \<in> (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}. card X \<noteq> 0" by auto
      from this show ?thesis
        using number_partition_of_eq \<open>finite B\<close> by (simp add: image_iff)
    qed
    ultimately show ?thesis unfolding number_partition_def by simp
  qed
  show "size (number_partition_of A B F) \<le> card B"
    using number_partition_of_eq \<open>finite A\<close> \<open>finite B\<close>
    by (metis (no_types, lifting) card_Diff1_le card_image_le finite_imageI le_trans size_image_mset size_mset_set)
qed

lemma functions_of:
  assumes "finite A" "finite B"
  assumes "number_partition (card A) N"
  assumes "size N \<le> card B"
  shows "functions_of A B N \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B"
proof -
  obtain f where "f \<in> A \<rightarrow>\<^sub>E B" and eq_N: "image_mset (\<lambda>X. card X) (mset_set (((\<lambda>b. {x \<in> A. f x = b})) ` B - {{}})) = N"
    using obtain_extensional_function_from_number_partition \<open>finite A\<close> \<open>finite B\<close> \<open>number_partition (card A) N\<close> \<open>size N \<le> card B\<close> by blast
  have "functions_of A B N = (domain_and_range_permutation A B) `` {f}"
  proof
    show "functions_of A B N \<subseteq> domain_and_range_permutation A B `` {f}"
    proof
      fix f'
      assume "f' \<in> functions_of A B N"
      from this have eq_N': "N = image_mset (\<lambda>X. card X) (mset_set (((\<lambda>b. {x \<in> A. f' x = b})) ` B - {{}}))"
        and "f' \<in> A \<rightarrow>\<^sub>E B"
        unfolding functions_of_def by auto
      from \<open>finite A\<close> \<open>finite B\<close> \<open>f \<in> A \<rightarrow>\<^sub>E B\<close> \<open>f' \<in> A \<rightarrow>\<^sub>E B\<close>
      obtain p\<^sub>A p\<^sub>B where "p\<^sub>A permutes A" "p\<^sub>B permutes B" "\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))"
        using eq_N eq_N' multiset_of_partition_cards_eq_implies_permutes[of A B f f'] by blast
      from this show "f' \<in> domain_and_range_permutation A B `` {f}"
        using \<open>f \<in> A \<rightarrow>\<^sub>E B\<close> \<open>f' \<in> A \<rightarrow>\<^sub>E B\<close>
        unfolding domain_and_range_permutation_def by auto
    qed
  next
    show "domain_and_range_permutation A B `` {f} \<subseteq> functions_of A B N"
    proof
      fix f'
      assume "f' \<in> domain_and_range_permutation A B `` {f}"
      from this have in_equiv_relation: "(f, f') \<in> domain_and_range_permutation A B" by auto
      from eq_N \<open>finite B\<close> have "image_mset (\<lambda>X. card X) (mset_set (((\<lambda>b. {x \<in> A. f' x = b})) ` B - {{}})) = N"
        using congruentD[OF multiset_of_partition_cards_respects_domain_and_range_permutation in_equiv_relation]
        by metis
      moreover from \<open>(f, f') \<in> domain_and_range_permutation A B\<close> have "f' \<in> A \<rightarrow>\<^sub>E B"
        unfolding domain_and_range_permutation_def by auto
      ultimately show "f' \<in> functions_of A B N"
        unfolding functions_of_def by auto
    qed
  qed
  from this \<open>f \<in> A \<rightarrow>\<^sub>E B\<close> show ?thesis by (auto intro: quotientI)
qed

lemma functions_of_number_partition_of:
  assumes "finite A" "finite B"
  assumes "F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B"
  shows "functions_of A B (number_partition_of A B F) = F"
proof -
  from \<open>F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B\<close> obtain f where "f \<in> A \<rightarrow>\<^sub>E B"
    and F_eq: "F = domain_and_range_permutation A B `` {f}" using quotientE by blast
  have "number_partition_of A B F = univ (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) F"
    unfolding number_partition_of_def ..
  also have "\<dots> = univ (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) (domain_and_range_permutation A B `` {f})"
    unfolding F_eq ..
  also have "\<dots> = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))"
    using \<open>finite B\<close>
    using equiv_domain_and_range_permutation multiset_of_partition_cards_respects_domain_and_range_permutation \<open>f \<in> A \<rightarrow>\<^sub>E B\<close>
    by (subst univ_commute') auto
  finally have number_partition_of_eq: "number_partition_of A B F = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))" .
  show ?thesis
  proof
    show "functions_of A B (number_partition_of A B F) \<subseteq> F"
    proof
      fix f'
      assume "f' \<in> functions_of A B (number_partition_of A B F)"
      from this have "f' \<in> A \<rightarrow>\<^sub>E B"
        and eq: "image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}})) = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))"
        unfolding functions_of_def by (auto simp add: number_partition_of_eq)
      note \<open>f \<in> A \<rightarrow>\<^sub>E B\<close> \<open>f' \<in> A \<rightarrow>\<^sub>E B\<close>
      moreover obtain p\<^sub>A p\<^sub>B where "p\<^sub>A permutes A" "p\<^sub>B permutes B" "\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))"
        using \<open>finite A\<close> \<open>finite B\<close> \<open>f \<in> A \<rightarrow>\<^sub>E B\<close> \<open>f' \<in> A \<rightarrow>\<^sub>E B\<close> eq
          multiset_of_partition_cards_eq_implies_permutes[of A B f f']
        by metis
      ultimately show "f' \<in> F"
        unfolding F_eq domain_and_range_permutation_def by auto
    qed
  next
    show "F \<subseteq> functions_of A B (number_partition_of A B F)"
    proof
      fix f'
      assume "f' \<in> F"
      from \<open>f' \<in> F\<close> obtain p\<^sub>A p\<^sub>B where "p\<^sub>A permutes A" "p\<^sub>B permutes B" "\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))"
        unfolding F_eq domain_and_range_permutation_def by auto
      have eq: "image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})) = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}))"
      proof -
        have "(\<lambda>b. {x \<in> A. f x = b}) ` B = (\<lambda>b. {x \<in> A. p\<^sub>B (f' (p\<^sub>A x)) = b}) ` B"
          using \<open>\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))\<close> by auto
        from this have "image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})) =
          image_mset card (mset_set ((\<lambda>b. {x \<in> A. p\<^sub>B (f' (p\<^sub>A x)) = b}) ` B - {{}}))" by simp
        also have "\<dots> = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}))"
          using \<open>p\<^sub>A permutes A\<close> \<open>p\<^sub>B permutes B\<close> permutes_implies_multiset_of_partition_cards_eq by blast
        finally show ?thesis .
      qed
      moreover from \<open>f' \<in> F\<close> have "f' \<in> A \<rightarrow>\<^sub>E B"
        unfolding F_eq domain_and_range_permutation_def by auto
      ultimately show "f' \<in> functions_of A B (number_partition_of A B F)"
        unfolding functions_of_def number_partition_of_eq by auto
    qed
  qed
qed

lemma number_partition_of_functions_of:
  assumes "finite A" "finite B"
  assumes "number_partition (card A) N" "size N \<le> card B"
  shows "number_partition_of A B (functions_of A B N) = N"
proof -
  from assms have "functions_of A B N \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B"
    using functions_of assms by fastforce
  from this obtain f where "f \<in> A \<rightarrow>\<^sub>E B" and "functions_of A B N = domain_and_range_permutation A B `` {f}"
    by (meson quotientE)
  from this have "f \<in> functions_of A B N"
    using equiv_domain_and_range_permutation equiv_class_self by fastforce
  have "number_partition_of A B (functions_of A B N) = univ (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) (functions_of A B N)"
    unfolding number_partition_of_def ..
  also have "\<dots> = univ (\<lambda>f.  image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) (domain_and_range_permutation A B `` {f})"
    unfolding \<open>functions_of A B N = domain_and_range_permutation A B `` {f}\<close> ..
  also have "\<dots> = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))"
    using \<open>finite B\<close> \<open>f \<in> A \<rightarrow>\<^sub>E B\<close> equiv_domain_and_range_permutation
      multiset_of_partition_cards_respects_domain_and_range_permutation
    by (subst univ_commute') auto
  also have "image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})) = N"
    using \<open>f \<in> functions_of A B N\<close> unfolding functions_of_def by simp
  finally show ?thesis .
qed

subsection \<open>Bijections\<close>

lemma bij_betw_number_partition_of:
  assumes "finite A" "finite B"
  shows "bij_betw (number_partition_of A B) ((A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B) {N. number_partition (card A) N \<and> size N \<le> card B}"
proof (rule bij_betw_byWitness[where f'="\<lambda>M. functions_of A B M"])
  show "\<forall>F\<in>(A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B. functions_of A B (number_partition_of A B F) = F"
    using \<open>finite A\<close> \<open>finite B\<close> by (auto simp add: functions_of_number_partition_of)
  show "\<forall>N\<in>{N. number_partition (card A) N \<and> size N \<le> card B}. number_partition_of A B (functions_of A B N) = N"
    using \<open>finite A\<close> \<open>finite B\<close> by (auto simp add: number_partition_of_functions_of)
  show "number_partition_of A B ` ((A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B) \<subseteq> {N. number_partition (card A) N \<and> size N \<le> card B}"
    using number_partition_of[of A B] \<open>finite A\<close> \<open>finite B\<close> by auto
  show "functions_of A B ` {N. number_partition (card A) N \<and> size N \<le> card B} \<subseteq> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B"
    using functions_of \<open>finite A\<close> \<open>finite B\<close> by blast
qed

subsection \<open>Cardinality\<close>

lemma card_domain_and_range_permutation:
  assumes "finite A" "finite B"
  shows "card ((A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B) = Partition (card A + card B) (card B)"
proof -
  have "bij_betw (number_partition_of A B) ((A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B) {N. number_partition (card A) N \<and> size N \<le> card B}"
    using \<open>finite A\<close> \<open>finite B\<close> by (rule bij_betw_number_partition_of)
  from this have "card ((A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B) = card {N. number_partition (card A) N \<and> size N \<le> card B}"
    by (rule bij_betw_same_card)
  also have "card {N. number_partition (card A) N \<and> size N \<le> card B} = Partition (card A + card B) (card B)"
    by (rule card_number_partitions_with_atmost_k_parts)
  finally show ?thesis .
qed

end


TITLE: Swapping integral and sum using dominated convergence theorem
QUESTION [5 upvotes]: Show that
  $$
\sum_{n=1}^\infty \int_0^\infty t^{s/2-1}e^{-\pi n^2t}dt
 = \int_0^\infty t^{s/2-1} \sum_{n=1}^\infty e^{-\pi n^2t} dt
$$
  with $s > 1$ using the dominated convergence theorem.

If I have understood correctly, I can define $f_k:= \sum_{n=1}^k t^{s/2-1}e^{-\pi n^2t}$ which I have already been able to show integrable and that it converges pointwise ($f = \lim_{k \rightarrow \infty} f_k$). Now the last part of the requirements of the theorem: I struggle to find an integrable function $g$ with $|f_k| \leq g$ for all $k \in \mathbb{N}$.

REPLY [2 votes]: As mentioned in the comments, what you are trying to do is overkill since monotone convergence is enough. But if you want to use dominated convergence you can do
\begin{align}
|f_k|&= \sum_{n=1}^k t^{s/2-1}e^{-\pi n^2t}=t^{s/2-1}e^{-\pi t}\,\sum_{n=1}^k e^{-\pi (n^2-1)t}\\ \ \\
&\leq t^{s/2-1}e^{-\pi t}\,\sum_{n=1}^\infty e^{-\pi (n^2-1)t}\\ \ \\
&\leq t^{s/2-1}e^{-\pi t}\,\sum_{n=0}^\infty e^{-\pi nt}\\ \ \\
&=t^{s/2-1}e^{-\pi t}\,\frac1 {1-e^{-\pi t}}\\ \ \\
\end{align}


TITLE: Range reduction for the exponential integral?
QUESTION [0 upvotes]: I would like to compute $\operatorname{Ei}(x)$ to a reasonable precision. Fortunately, I have a computer algebra system (PARI/GP) which includes this function as a built-in, but unfortunately, $\operatorname{Ei}(x)$ causes an overflow. However, it's not that far away: I can compute $\operatorname{Ei}(x/8).$
Is there some sort of 'argument reduction' strategy that would let me take advantage of the existing function, or do I need to code something from the ground up for this?

REPLY [1 votes]: To a first estimate,
$$
\operatorname{Ei}(x) \approx \operatorname{Ei}(x/k)^k
$$
for $k$ small and $x$ large.
But we can improve on this with
$$
\operatorname{Ei}(x) = e^xf(x)
$$
where
$$
f(x)=\frac1x + \frac{1}{x^2} + \frac{2}{x^3} + \frac{6}{x^4} + O\left(\frac{1}{x^5}\right)
$$
so
$$
\begin{array}{ll}
\operatorname{Ei}(x/k) &= e^{x/k}f(x/k)\\
\log\operatorname{Ei}(x/k) &= x/k + \log f(x/k)\\
k\log\operatorname{Ei}(x/k) &= x + k\log f(x/k)\\
x &= k\log\operatorname{Ei}(x/k) - k\log f(x/k)\\
\end{array}
$$
and so
$$
\begin{array}{ll}
\log\operatorname{Ei}(x) &= x + \log f(x)\\
\log\operatorname{Ei}(x) &= k\log\operatorname{Ei}(x/k) - k\log f(x/k) + \log f(x)\\
\operatorname{Ei}(x) &= \exp\big(k\log\operatorname{Ei}(x/k) - k\log f(x/k) + \log f(x)\big)\\
\operatorname{Ei}(x) &= \operatorname{Ei}(x/k)^kf(x)/f(x/k)^k\\
\end{array}
$$
which can be approximated with the series. Of course you can take any finite number of terms in $f$, but you can't remove the error term that way.
I'm sure there are better approaches but this is a decent quick-and-dirty approach.


text:
\subsection{Proof of lemma~\ref{lem:aux}} \label{appsec:lemmaproof}

\begin{proof}

To begin with, we prove result \eqref{eq:lemmaboundh} then we prove the other results, \eqref{eq:lemmaboundx}--\eqref{eq:lemmabound1}, inductively.

\paragraph{Result \eqref{eq:lemmaboundh}.}  We first show that \eqref{eq:lemmaboundh} follows immediately from theorem~\ref{thm:sym}.  Before we do so we establish upper and lower bounds on $\tau_n^t$ defined in  \eqref{eq:state_evolution2}.  Notice that for the Bernoulli case,

\begin{align*}
\tau^n_{t+1}=\mathbb{E}\Big[\frac{\rho_n^2}{\rho_n+(1-\rho_n)\exp\{-\frac12\lambda_n \tau^n_{t}-\sqrt{\lambda_n\tau^n_{t}} Z\}} \Big],
\end{align*}

where $Z \sim \mathcal{N}(0,1)$, as shown in appendix \ref{app:AMPtrans} result \eqref{eq:tau_rep}.  Therefore, trivially

$
\tau^n_{t+1}\leq \rho_n.
$

We also wish to establish a lower bound.  First, by Jensen's Inequality applied to the convex function $f(x) = 1/x$ on $x \in (0, \infty)$, we have that

\begin{align*}
\tau^n_{t+1} \geq \frac{\rho_n^2}{\rho_n+(1-\rho_n) \mathbb{E}\Big[\exp\{-\frac12\lambda_n \tau^n_{t}-\sqrt{\lambda_n\tau^n_{t}} Z\}\Big]} \overset{(a)}{=} \rho_n^2,
\end{align*}

where step $(a)$ uses that
$\mathbb{E}[\exp\{-\frac12\lambda_n \tau^n_{t}-\sqrt{\lambda_n\tau^n_{t}} Z\}] = 1$ since $\mathbb{E}[\exp\{-t Z\}] = \exp\{\frac12 t^2\}$.

Thus, $\rho_n^2 \leq \tau^n_{t+1} \leq \rho_n$ and, in the regime of interest where $\lambda_n = \kappa \rho_n^{-2}$, using that $\mu^n_t = \sqrt{\lambda_n} \tau^n_t$ by \eqref{eq:state_evolution2}, we find
$(\mu^n_t)^2 = \lambda_n (\tau^n_t)^2 = \kappa \rho_n^{-2} (\tau^n_t)^2$ and therefore
\begin{equation}
\label{eq:mu_bound}
\kappa' \rho_n^{2} \leq  (\mu^n_t)^2 =  \kappa \rho_n^{-2} (\tau^n_t)^2 \leq \kappa.
\end{equation}

Now we demonstrate \eqref{eq:lemmaboundh}.  Using theorem~\ref{thm:sym} with pseudo-Lipschitz function $\phi(h^{t}_i, X^n_i) = (\mu_t^n)^{-1} h^{t}_i +  X^n_i$, having constant $L_{\phi} = \sqrt{2}\max\{1, (\mu_t^n)^{-1}\}$ as is shown in lemma~\ref{lem:PL_second},

 \begin{equation}
 \label{eq:hbound1}
 \mathbb{P} \Big(\Big| \frac{1}{n} \sum_{i=1}^n  \frac{h^{t}_i }{\mu_t^n }+ X^n_i - \rho_n \Big| \geq \epsilon \Big) \leq C C_t \exp\Big\{ \frac{-c c_t n \epsilon^2}{  \max\{1, (\mu_t^n)^{-2}\}  \widetilde{\gamma}_n^{t}}\Big\} \leq C C_t \exp\Big\{ \frac{-c c_t n \epsilon^2}{  \rho_n^{-2} \widetilde{\gamma}_n^{t}}\Big\},
 \end{equation}

where the final inequality follows from the bound $ \max\{1, (\mu_t^n)^{-2}\} \leq \kappa' \rho_n^{-2}$ justified above in \eqref{eq:mu_bound}. We have also used that $\mathbb{E}[\phi(\sqrt{\tau_t^n} Z, X_0^n)] = \mathbb{E}[ (\sqrt{\tau_t^n} /\mu_t^n)Z + X_0^n] = \mathbb{E}[X_0^n] = \rho_n$.
The result in \eqref{eq:lemmaboundh} follows from \eqref{eq:hbound1} since, when $\rho_n \leq 1/4$,

 \begin{equation*}
 \begin{split}
  &  \mathbb{P} \Big( \frac{1}{n}  \sum_{i=1}^n  h^{t}_i  + \mu_t^nX_i \geq \frac{\mu_t^n}{2} \Big)  =   \mathbb{P} \Big( \frac{1}{n}  \sum_{i=1}^n  \frac{h^{t}_i }{\mu_t^n }  + X_i \geq \frac{1}{2} \Big) \\
    &\qquad \leq  \mathbb{P} \Big( \Big\lvert \frac{1}{n}  \sum_{i=1}^n   \frac{h^{t}_i }{\mu_t^n }  + X_i -  \rho_n \big \lvert \geq \frac{1}{2} - \rho_n \Big) \leq  \mathbb{P} \Big( \Big\lvert \frac{1}{n}  \sum_{i=1}^n \frac{h^{t}_i }{\mu_t^n }   +  X_i -  \rho_n \big \lvert \geq \frac{1}{4} \Big).
   \end{split}
  \end{equation*}

Similarly, for the first result in \eqref{eq:lemmaboundh}, we use the pseudo-Lipschitz function $\phi(h^{t}_i, X^n_i) = (h^{t}_i + \mu_t^n X^n_i)^2$, having constant $L_{\phi} = 2\max\{1, (\mu_t^n)^2\}$,  as is shown in lemma~\ref{lem:PL_second}. Then by theorem~\ref{thm:sym},

 \begin{equation}
  \label{eq:hbound2}
 \mathbb{P} \Big(\Big| \frac{1}{n} \| \bh^{t} + \mu_t^n \bX^n\|^2 - (\mu_t^n)^2 \rho_n - \tau_t^n \Big| \geq \epsilon \Big) \leq C C_t \exp\Big\{ \frac{-c c_t n \epsilon^2}{\max\{1, (\mu_t^n)^4\}  \widetilde{\gamma}_n^{t}}\Big\} \leq \textsf{bound}_t,
 \end{equation}

where the final inequality follows since $(\mu^n_t)^4 \leq \kappa$ as discussed above in \eqref{eq:mu_bound}. We have also used that $\mathbb{E}[\phi(\sqrt{\tau_t^n}  Z, X_0^n)] = \mathbb{E}[ (\sqrt{\tau_t^n} Z +  \mu_t^n X_0^n)^2] = \tau_t^n + ( \mu_t^n)^2 \rho_n$.
Then, since $(\mu_t^n)^2 \rho_n \leq 1$, choosing $ \kappa_h^2  = 3 >  1 + (\mu_t^n)^2 \rho_n +\tau_t^n$, we recover the first result in \eqref{eq:lemmaboundh} with

 \begin{equation*}
   \mathbb{P} \Big( \frac{1}{\sqrt{n}}   \Big\| \bh^{t} + \mu_{t}^n \bX  \Big\| \geq \kappa_h \Big)  \leq   \mathbb{P} \Big(  \Big\lvert \frac{1}{n}   \Big\| \bh^{t} + \mu_{t}^n \bX \Big\|^2 - (\mu_t^n)^2 \rho_n - \tau_t^n \Big \lvert  \geq 1\Big).
  \end{equation*}

\paragraph{Other results \eqref{eq:lemmaboundx}--\eqref{eq:lemmabound1}.}
The proof is inductive on the iteration $t$. We first show the initialization case $t=1$. Consider \eqref{eq:lemmabound3}, then using the definitions of $\bx^{1} = \frac{\sqrt{\lambda_n}}{n}  \bX \langle \bX, f_0(\bx^{0}) \rangle  +  \bZ  f_0(\bx^{0})$  from \eqref{eq:AMP3} and $\bh^{1} =  \bZ g_{0}(\bh^{0}, \bX)$ from \eqref{eq:AMP_correct} along with the fact that $f_{0}(\bx^{0}) = g_{0}(\bh^{0}, \bX)$,
\begin{equation*}
\bx^{1} - \bh^{1} - \mu_{1}^n \bX = \bX \Big(\frac{\sqrt{\lambda_n}}{n}  \langle \bX, f_0(\bx^{0}) \rangle  - \mu_{1}^n\Big) = 0,
\end{equation*}
where the final inequality follows since $ \mu^n_{1} = \sqrt{\lambda_n} \langle f_0(\bx^0), \bX \rangle/n$  by \eqref{eq:state_evolution_start}. Next for result \eqref{eq:lemmaboundx}, first notice that by the Triangle Inequality, $ \| \bx^{1}  \| \leq \| \bx^{1} - \bh^{1} - \mu_{1}^n \bX \| + \|  \bh^{1} + \mu_{1}^n \bX  \|$.  Then let $ \kappa_x = 2 \kappa_h + 2\kappa$ and therefore, by lemma~\ref{sums},

\begin{equation*}
\begin{split}
    \mathbb{P} \Big( \frac{1}{\sqrt{n}}   \| \bx^{1}  \| \geq \kappa_x \Big)  &=  \mathbb{P} \Big( \frac{1}{\sqrt{n}} \| \bx^{1} - \bh^{1} - \mu_{1}^n \bX  \| +   \frac{1}{\sqrt{n}} \|  \bh^{1} + \mu_{1}^n \bX  \|  \geq 2 \kappa_h + 2\kappa \Big)  \\
&\leq  \mathbb{P} \Big( \frac{1}{\sqrt{n}}  \| \bx^{1} - \bh^{1} - \mu_{1}^n \bX  \|  \geq  \kappa \Big)  +  \mathbb{P} \Big(   \frac{1}{\sqrt{n}} \|  \bh^{1} + \mu_{1}^n \bX \|  \geq  \kappa_h  \Big).
\end{split}
\end{equation*}

Then the upper bound follows by \eqref{eq:lemmaboundh} and \eqref{eq:lemmabound3}.

Next, notice that with the bound on $   \mathbb{P} ( \frac{1}{\sqrt{n}}   \| \bx^{1}  \| \geq \kappa_x )$ established above, one can prove the $t=1$ case for \eqref{eq:lemmabound2} and \eqref{eq:lemmabound1},  as justified in the work in \eqref{eq:CS_split1} -- \eqref{eq:tobebounded} along with results \eqref{eq:lemmaboundh} and \eqref{eq:lemmabound3}.
Thus, for the second result we would like to show in \eqref{eq:lemmaboundx}, namely the bound on $\mathbb{P}( \frac{1}{n}  \sum_{i=1}^n x^{t}_i \geq \frac{\mu_t^n}{2} )$, we note that we can employ the result \eqref{eq:lemmabound1} with pseudo-Lipschitz function $ \psi(a, b) = b/\mu^n_{1}$ with constant $L_{\psi} = (\mu^n_{1})^{-1}$ to give

\begin{equation*}
\mathbb{P} \Big(\Big| \frac{1}{n} \sum_{i=1}^n \frac{x^{1}_i}{\mu^n_{1}} -  \rho_n \Big| \geq \epsilon \Big)  \leq C C_{1} \exp\Big\{\frac{-c c_{1} n \epsilon^2}{(\mu^n_{1})^{-2}\widetilde{\gamma}_n^{1}}\Big\}  \leq C C_{1} \exp\Big\{\frac{-c c_{1} n \epsilon^2}{\rho_n^{-2}\widetilde{\gamma}_n^{1}}\Big\},
\end{equation*}

where the final inequality follows from the bound $(\mu_t^n)^{-2} \leq \kappa' \rho_n^{-2}$ justified above in \eqref{eq:mu_bound}.  Then the desired result in \eqref{eq:lemmaboundx} follows from the above since, when $\rho_n \leq 1/4$,

 \begin{equation*}
 \begin{split}
    \mathbb{P} \Big( \frac{1}{n}  \sum_{i=1}^n x^{1}_i  \geq \frac{\mu_1^n}{2} \Big) & =   \mathbb{P} \Big( \frac{1}{n}  \sum_{i=1}^n  \frac{x^{1}_i}{\mu_1^n }  \geq \frac{1}{2} \Big) \\
    &\leq  \mathbb{P} \Big( \Big\lvert \frac{1}{n}  \sum_{i=1}^n   \frac{x^{1}_i}{\mu_1^n }  -  \rho_n \big \lvert \geq \frac{1}{2} - \rho_n \Big) \leq  \mathbb{P} \Big( \Big\lvert \frac{1}{n}  \sum_{i=1}^n \frac{x^{1}_i}{\mu_1^n } -  \rho_n \big \lvert \geq \frac{1}{4} \Big).
   \end{split}
  \end{equation*}

Now assume that all results \eqref{eq:lemmaboundx}--\eqref{eq:lemmabound1} hold up until iteration $t-1$ and we prove the results for iteration $t$.  As justified in the work in \eqref{eq:CS_split1} -- \eqref{eq:tobebounded}, the results \eqref{eq:lemmabound2} and  \eqref{eq:lemmabound1} follow immediately from \eqref{eq:lemmaboundh} -- \eqref{eq:lemmabound3} so we only aim to prove \eqref{eq:lemmabound3} and  \eqref{eq:lemmaboundx} here.  We begin by proving \eqref{eq:lemmabound3}  which we will then use to prove \eqref{eq:lemmaboundx}.

\paragraph{Result \eqref{eq:lemmabound3}.} Next we consider result \eqref{eq:lemmabound3}. Using the definitions of $\bx^{t+1}$ and $\bh^{t+1}$ from \eqref{eq:AMP3} and \eqref{eq:AMP_correct} along with Cauchy-Schwarz inequality, we have that

 \begin{equation}
 \begin{split}
  \label{eq:bound2}
& \frac{1}{n} \sum_{i=1}^n  \Big| x^{t}_i - h^{t}_i- \mu_{t}^n X_i  \Big|^2\\

 &\leq   \frac{3}{n}\Big\lvert  \frac{\sqrt{\lambda_n}}{n}  \langle \bX, f_{t-1}(\bx^{t-1}) \rangle  - \mu_{t}^n\Big \lvert^2 \sum_{i=1}^n  X_i^2 +   \frac{3}{n} \sum_{i=1}^n  \Big|   [\bZ  f_{t-1}(\bx^{t-1})]_i -   [\bZ g_{t-1}(\bh^{t-1}, \bX)]_i \Big|^2 \\%
 & \quad  +  \frac{3}{n} \sum_{i=1}^n  \Big|  \mathsf{b}_{t-1}  f_{t-2}(x^{t-2}_i) - \mathsf{c}_{t-1} g_{t-2}(h^{t-2}_i, X_i)  \Big|^2 \\

  &=3  \Big \lvert \frac{\sqrt{\lambda_n}}{n}  \langle \bX, f_{t-1}(\bx^{t-1}) \rangle  - \mu_{t}^n \Big\lvert^2  \frac{1}{n}  \sum_{i=1}^n  X_i^2  +   \frac{3}{n}  \Big \|  \bZ \big( f_{t-1}(\bx^{t-1}) -   g_{t-1}(\bh^{t-1}, \bX) \big) \Big\|^2 \\%
 &\quad  +  \frac{3}{n}   \Big\|  \mathsf{b}_{t-1}  f_{t-2}(\bx^{t-2}) - \mathsf{c}_{t-1} g_{t-2}(\bh^{t-2}, \bX)  \Big \|^2.
\end{split}
 \end{equation}

Now we use the upper bounds in  \eqref{eq:bound2} along with lemma~\ref{sums} to give the following upper bound on the probability on the LHS of \eqref{eq:lemmabound3}:

 \begin{equation}
 \begin{split}
\mathbb{P} \Big( \frac{1}{n}   \Big\| \bx^{t} - \bh^{t} - \mu_{t}^n \bX  \Big\|^2 \geq \frac{\kappa \epsilon^2}{ L_{\psi}^2} \Big)  &\leq \mathbb{P} \Big( \Big \lvert \frac{\sqrt{\lambda_n}}{n}  \langle \bX, f_{t-1}(\bx^{t-1}) \rangle  - \mu_{t}^n \Big\lvert^2 \frac{1}{n}  \sum_{i=1}^n   X_i^2  \geq \frac{\kappa \epsilon}{ L_{\psi}^2 } \Big) \\

 &+ \mathbb{P} \Big(\frac{1}{n}  \Big \|  \bZ \big( f_{t-1}(\bx^{t-1}) -   g_{t-1}(\bh^{t-1}, \bX) \big) \Big\|^2  \geq \frac{\kappa \epsilon}{L_{\psi}^2} \Big) \\

 &+ \mathbb{P} \Big( \frac{1}{n}   \Big\|  \mathsf{b}_{t-1}  f_{t-2}(\bx^{t-2}) - \mathsf{c}_{t-1} g_{t-2}(\bh^{t-2}, \bX)  \Big \|^2 \geq \frac{\kappa \epsilon}{L_{\psi}^2} \Big).

 \label{eq:three_terms}
 \end{split}
 \end{equation}

We label the three terms in the above $T_1,T_2,T_3$ and provide an upper bound for each.

First consider term $T_1$ of \eqref{eq:three_terms}, and recall that $ \mu^n_{t-1} = \sqrt{\lambda_n}  \tau^n_{t-1}$.  Thus, we have the upper bound

\begin{equation}
  \begin{split}

&T_1 \leq  \mathbb{P} \Big(  \Big|   \frac{1}{n} \langle \bX, f_{t-1}(\bx^{t-1}) \rangle  -  \tau^n_{t-1}  \Big| \geq \frac{\kappa \sqrt{\epsilon}}{ \sqrt{\rho_n \lambda_n} L_{\psi}}  \Big)  +  \mathbb{P} \Big(   \frac{ 1}{n} \sum_{i=1}^nX_i^2  \geq2 \rho_n \Big).

\label{eq:T1_bound}
 \end{split}
 \end{equation}

Notice that we can upper bound the second term in \eqref{eq:T1_bound} with using $2 e^{-{ n \rho_n}/{2 }}$ Chernoff's bounds (lemma~\ref{lem:chernoff}).
We can upper bound the first term  in \eqref{eq:T1_bound} using the induction hypothesis for result \eqref{eq:lemmabound3} for the pseudo-Lipschitz function $\widetilde{\psi}(a, b) = a f_{t-1}(b)$ with constant $L_{\widetilde{\psi}} = L_f$. Thus,

\begin{equation*}
  \begin{split}

\mathbb{P} \Big(  \Big|   \frac{1}{n} \langle \bX, f_{t-1}(\bx^{t-1}) \rangle  -  \tau^n_{t-1}  \Big| \geq \frac{\kappa \sqrt{\epsilon}}{ \sqrt{\rho_n \lambda_n} L_{\psi}}  \Big)  \leq C C_{t-1} \exp\Big\{\frac{-c c_{t-1} n \epsilon^2}{L_{\psi}^2 L_f^2 \lambda_n \rho_n \widetilde{\gamma}_n^{t-1}}\Big\}.

 \end{split}
 \end{equation*}

Finally we notice that the desired result follows since $ \lambda_n^2 \rho_n \widetilde{\gamma}_n^{t-1} \leq  \widetilde{\gamma}_n^{t}$ using the definition of $ \widetilde{\gamma}_n^{t}$ in \eqref{eq:tilde_gamma}. Indeed, it follows using $L_f = \sqrt{\lambda_n}$, proved in lemma~\ref{lem:PL_cond}, that

\begin{equation*}
  \begin{split}

C C_{t-1} \exp\Big\{\frac{-c c_{t-1} n \epsilon^2}{L_{\psi}^2 L_f^2   \lambda_n \rho_n \widetilde{\gamma}_n^{t-1}}\Big\} \leq C C_{t-1} \exp\Big\{\frac{-c c_{t-1} n \epsilon^2}{L_{\psi}^2   \lambda_n^2 \rho_n \widetilde{\gamma}_n^{t-1}}\Big\} \leq \textsf{bound}_t.

 \end{split}
 \end{equation*}

Now consider term $T_2$ of \eqref{eq:three_terms}. We define an event

\begin{equation}
\label{eq:Fdef}
\mathcal{F}_{t-1} := \left\{\max_i \{x^{t-1}_i\} \leq  \frac{\mu^n_{t-1}}{2} \, \cap \, \max_i\{h^{t-1}_i +  \mu_{t-1}^n X_i\} \leq  \frac{\mu^n_{t-1}}{2}\right\},
\end{equation}

and when considering term $T_2$ of \eqref{eq:three_terms} we define $\Pi$ to be the event of interest so that $T_2 = \mathbb{P}(\Pi)$. Clearly, then

\begin{equation}
\label{eq:F_bound}
T_2 = \mathbb{P}(\Pi) = \mathbb{P}(\Pi \, \cap \, \mathcal{F}_{t-1}) + \mathbb{P}(\Pi \, \cap \, \mathcal{F}_{t-1}^c) \leq  \mathbb{P}( \mathcal{F}_{t-1}) \mathbb{P}(\Pi \, \lvert \, \mathcal{F}_{t-1}) + \mathbb{P}(\mathcal{F}_{t-1}^c).
\end{equation}

So in what follows we bound $\mathbb{P}(\mathcal{F}_{t-1}^c)$, the probability of the complement of the event in $\mathcal{F}_{t-1}$ defined in \eqref{eq:Fdef}, and

\begin{equation}
\label{eq:conditioned}
 \mathbb{P}( \mathcal{F}_{t-1}) \mathbb{P}(\Pi \, \lvert \, \mathcal{F}_{t-1}) =  \mathbb{P} \Big(\frac{1}{n}  \Big \|  \bZ \big( f_{t-1}(\bx^{t-1}) -   g_{t-1}(\bh^{t-1}, \bX) \big) \Big\|^2  \geq \frac{\kappa \epsilon}{L_{\psi}^2}  \, \big \lvert  \, \mathcal{F}_{t-1}\Big)  \mathbb{P}(\mathcal{F}_{t-1}).
\end{equation}

The idea is that, conditional on $\mathcal{F}_{t-1}$, the function $f_{t-1}$ has a Lipschitz constant $\sqrt{\lambda_n} \rho_n$ (instead of $\sqrt{\lambda_n}$, its Lipschitz constant over the real line) as proved in lemma~\ref{lem:PL_cond}.

First we bound $\mathbb{P}(\mathcal{F}_{t-1}^c)$. First, notice that

\begin{equation*}
\begin{split}

&\mathbb{P}\Big(\max_i \{x^{t-1}_i\} \leq  \frac{\mu^n_{t-1}}{2} \, \cap \, \max_i\{h^{t-1}_i +  \mu_{t-1}^n X_i\} \leq  \frac{\mu^n_{t-1}}{2}\Big) \\

&\leq \mathbb{P}\Big(\max_i\{x^{t-1}_i\} \leq  \frac{\mu^n_{t-1}}{2}\Big) + \mathbb{P}\Big( \max_i\{h^{t-1}_i +  \mu_{t-1}^n X_i\} \leq  \frac{\mu^n_{t-1}}{2}\Big)\\

&\overset{(a)}{\leq}\mathbb{P}\Big(\frac{1}{n} \sum_{i=1}^n x^{t-1}_i \leq  \frac{\mu^n_{t-1}}{2}\Big) + \mathbb{P}\Big( \frac{1}{n} \sum_{i=1}^n h^{t-1}_i +  \mu_{t-1}^n X_i \leq  \frac{\mu^n_{t-1}}{2}\Big) \overset{(b)}{\leq} \textsf{bound}_t,

\end{split}
\end{equation*}

where the  step $(a)$ follows since if $\max_i(x_i) \leq B$ then $\bar{x} \leq B$ and step $(b)$ follows from results \eqref{eq:lemmaboundx} and \eqref{eq:lemmaboundh} at iteration $t-1$ (i.e.\ the inductive hypothesis for \eqref{eq:lemmaboundx}) and the fact that $\rho_n^{-2} \widetilde{\gamma}_n^{t-1} \leq \lambda_n \widetilde{\gamma}_n^{t-1} \leq \widetilde{\gamma}_n^{t}$ in the regime of interest where $\lambda_n = \kappa \rho_n^{-2}$.

Now we upper bound the probability in \eqref{eq:conditioned}. First notice that, conditioned on event $\mathcal{F}_{t-1}$,

\begin{equation*}
\begin{split}

&\frac{1}{\sqrt{n}}  \Big \|  \bZ \big( f_{t-1}(\bx^{t-1}) -   g_{t-1}(\bh^{t-1}, \bX) \big) \Big\| \leq \frac{1}{\sqrt{n}}   \|  \bZ \|_{op} \Big\| f_{t-1}(\bx^{t-1}) -   g_{t-1}(\bh^{t-1}, \bX) \Big\| \\

&\overset{(a)}{\leq} \frac{1}{\sqrt{n}}   \|  \bZ \|_{op} \Big\| f_{t-1}(\bx^{t-1}) -  f_{t-1}(\bh^{t-1} + \mu_{t-1}^n \bX) \Big\| \overset{(b)}{\leq} \|  \bZ \|_{op} \frac{\sqrt{\lambda_n} \rho_n}{\sqrt{n}}  \Big\| \bx^{t-1} -   \bh^{t-1} - \mu_{t-1}^n \bX \Big\|,

\end{split}
\end{equation*}

where step $(a)$ uses that $g_{t-1}(\bh^{t-1}, \bX) = f_{t-1}(\bh^{t-1} + \mu_{t-1}^n \bX)$ and step $(b)$ uses the Lipschitz property of $f_{t-1}$, conditioned on event $\mathcal{F}_{t-1}$.

Therefore,

\begin{equation*}
  \begin{split}

& \mathbb{P} \Big(\frac{1}{\sqrt{n}}  \Big \|  \bZ \big( f_{t-1}(\bx^{t-1}) -   g_{t-1}(\bh^{t-1}, \bX) \big) \Big\|  \geq \frac{\kappa \sqrt{\epsilon}}{L_{\psi}}  \, \big \lvert  \, \mathcal{F}_{t-1}\Big) \mathbb{P}(\mathcal{F}_{t-1})\\

& \leq   \mathbb{P} \Big( \|  \bZ \|_{op}   \frac{1}{\sqrt{n}} \sqrt{\lambda_n} \rho_n \Big\| \bx^{t-1} -   \bh^{t-1} - \mu_{t-1}^n \bX \Big\| \geq \frac{\kappa \epsilon}{L_{\psi} }  \, \big \lvert  \, \mathcal{F}_{t-1}\Big) \mathbb{P}(\mathcal{F}_{t-1}) \\

& \leq   \mathbb{P} \Big( \|  \bZ \|_{op}   \frac{1}{\sqrt{n}} \sqrt{\lambda_n} \rho_n \Big\| \bx^{t-1} -   \bh^{t-1} - \mu_{t-1}^n \bX \Big\| \geq \frac{\kappa \epsilon}{L_{\psi} } \Big) \\

&\leq  \mathbb{P} \Big(   \frac{1}{\sqrt{n}} \Big\| \bx^{t-1} -   \bh^{t-1} - \mu_{t-1}^n \bX \Big\| \geq \frac{\kappa \ep}{L_{\psi} \sqrt{\lambda_n} \rho_n} \Big) + \mathbb{P} \Big(   \|  \bZ \|_{op}   \geq \kappa  \Big) \\

&\leq C C_{t-1} \exp\Big\{\frac{-c c_{t-1} n \epsilon^2}{L_{\psi}^2  \widetilde{\gamma}_n^{t}}\Big\} +C \exp\{- c n\},

 \end{split}
 \end{equation*}

 where the final inequality follows from the inductive hypothesis for \eqref{eq:lemmabound3} and standard results about tail bounds for operator norms of GOE matrices.  In particular, we have used the  inductive hypothesis to find

\begin{equation*}
  \begin{split}

 \mathbb{P} \Big(   \frac{1}{n} \Big\| \bx^{t-1} -   \bh^{t-1} + \mu_{t-1}^n \bX \Big\|^2 \geq \frac{\kappa \ep^2}{L^2_{\psi} \lambda_n \rho_n^2} \Big) &\leq  C C_{t-1} \exp\Big\{\frac{-c c_{t-1} n \epsilon^2}{L_{\psi}^2  \lambda_n \rho_n^2 \widetilde{\gamma}_n^{t-1}}\Big\} \\

 &\leq C C_{t-1} \exp\Big\{\frac{-c c_{t-1} n \epsilon^2}{L_{\psi}^2     \widetilde{\gamma}_n^{t}}\Big\},

 \end{split}
 \end{equation*}

where the final inequality follows since $\lambda_n \rho_n^2 \widetilde{\gamma}_n^{t-1} \leq   \widetilde{\gamma}_n^{t}$.

 Finally, consider term $T_3$ of \eqref{eq:three_terms}.  To bound this term, we use a strategy as we did for term $T_2$ in \eqref{eq:Fdef}-\eqref{eq:F_bound}: conditioning on an event that makes sure the input to the denoiser is small enough that the Lipschitz constant can be assumed to be $\sqrt{\lambda_n} \rho_n$ instead of $\sqrt{\lambda_n}$.  However, we do not go through this argument in detail since it is analogous to that for term $T_2$.

 We first give an upper bound using  the definition of $g_t$ and the Lipschitz property of $f_t$ with $L_f = \sqrt{\lambda_n} \rho_n$ as follows:

\begin{equation}
\begin{split}
\label{eq:termT3_1}
 & \Big\|  \mathsf{b}_{t-1}  f_{t-2}(\bx^{t-2}) - \mathsf{c}_{t-1} g_{t-2}(\bh^{t-2}, \bX)  \Big \| =  \Big\|  \mathsf{b}_{t-1}  f_{t-2}(\bx^{t-2}) - \mathsf{c}_{t-1}  f_{t-2}(\bh^{t-2} +  \mu_{t-2}^n \bX)  \Big \| \\

 & \leq  |\mathsf{b}_{t-1}| \Big\|   f_{t-2}(\bx^{t-2}) -  f_{t-2}(\bh^{t-2} +  \mu_{t-2}^n \bX) \Big \| +  | \mathsf{b}_{t-1}   - \mathsf{c}_{t-1} |  \Big \|  f_{t-2}(\bh^{t-2} +  \mu_{t-2}^n \bX) \Big \| \\

 & \leq   \lambda_n \rho_n^2 \Big\|  \bx^{t-2} -  \bh^{t-2} - \mu_{t-2}^n \bX \Big \| +  | \mathsf{b}_{t-1}   - \mathsf{c}_{t-1} | \sqrt{n}.
  \end{split}
  \end{equation}

In the final step we use the lemma~\ref{lem:PL_cond} results

 \begin{equation*}
 | \mathsf{b}_{t-1}   | \leq  \frac{1}{n} \sum_{i=1}^n \big| f'_{t-1}(x^{t-1}_i)  \big | \leq  \sqrt{\lambda_n} \rho_n, \qquad \text{ and } \qquad \Big \|  f_{t-2}(\bh^{t-2} + \mu_{t-2}^n \bX)  \Big \|^2 \leq n.
 \end{equation*}

 We investigate the term $| \mathsf{b}_{t-1}   - \mathsf{c}_{t-1} |$ and recall from their definitions in \eqref{eq:AMP} and \eqref{eq:AMP_correct},

 \begin{equation}
 \begin{split}
& | \mathsf{b}_{t-1}   - \mathsf{c}_{t-1} | \leq  \frac{1}{n} \sum_{i=1}^n \big| f'_{t-1}(x^{t-1}_i) -  g'_{t-1}(h^{t-1}_i, X_i) \big |=\frac{1}{n} \sum_{i=1}^n \big|  f'_{t-1}(x^{t-1}_i) -    f'_{t-1}(h^{t-1}_i - \mu_{t-1}^n X_i ) \big | \\
&\overset{(a)}{=}   \frac{\sqrt{\lambda_n}}{n} \sum_{i=1}^n   \Big|f_{t-1}(x^{t-1}_i)(1- f_{t-1}(x^{t-1}_i)) -  f_{t-1}(h^{t-1}_i - \mu_{t-1}^n X_i)(1- f_{t-1}(h^{t-1}_i - \mu_{t-1}^n X_i) )\Big | \\
&\overset{(b)}{\leq} \frac{\sqrt{\lambda_n}}{n} \sum_{i=1}^n \Big|   f_{t-1}(x^{t-1}_i) -  f_{t-1}(h^{t-1}_i - \mu_{t-1}^n X_i)  \Big | \overset{(c)}{\leq} \frac{\lambda_n  \rho_n}{\sqrt{n}}  \Big\|   \bx^{t-1} - \bh^{t-1} - \mu_{t-1}^n \bX  \Big \|.
\label{eq:sfterms}
 \end{split}
 \end{equation}

In the above, step $(a)$ uses lemma~\ref{lem:PL_cond} for computing the derivative $f_t$, step $(b)$ uses the bound
  \begin{equation*}
 \begin{split}
 \big| f(a)(1- f(a)) -  f(b)(1- f(b)) \big | &\leq  \big| f(a) -  f(b)\big |   + \big |  [f(a)]^2 -  [f(b)]^2 \big | \leq  \kappa \big| f(a) -  f(b)\big |,
 \end{split}
 \end{equation*}
 for $0 \leq f(a) \leq 1$ for all $a \in \mathbb{R}$, and step $(c)$ uses the Lipschitz property of $f_{t}$, namely $L_f = \sqrt{\lambda_n} \rho_n$, and Cauchy Schwarz to give $\sum_{i=1}^n |a_i| \leq \sqrt{n} ||\textbf{a}||$.
Plugging the bound in \eqref{eq:sfterms} into \eqref{eq:termT3_1},

 \begin{equation*}
\begin{split}
 & \Big\|  \mathsf{b}_{t-1}  f_{t-2}(\bx^{t-2}) - \mathsf{c}_{t-1} g_{t-2}(\bh^{t-2}, \bX)  \Big \| \\

  & \leq   \lambda_n \rho_n^2 \Big\|  \bx^{t-2} -  \bh^{t-2} - \mu_{t-2}^n \bX \Big \| + \lambda_n \rho_n   \Big\|   \bx^{t-1} - \bh^{t-1} - \mu_{t-1}^n \bX  \Big \|.

  \end{split}
  \end{equation*}

 Now we have from lemma~\ref{sums} that

 \begin{equation*}
\begin{split}
T_3 &\leq 2 \mathbb{P} \Big(\frac{1}{n}  \Big\|   \bx^{t-1} - \bh^{t-1} - \mu_{t-1}^n \bX  \Big \|^2 \geq \frac{\kappa \epsilon}{L^2_{\psi}  \lambda^2_n \rho_n^2} \Big),
  \end{split}
  \end{equation*}

and the final bound  follows from the inductive hypothesis for \eqref{eq:lemmabound2} using that $\lambda^2_n \rho_n^2 \widetilde{\gamma}_n^{t-1} \leq \lambda^2_n \rho_n \widetilde{\gamma}_n^{t-1} \leq   \widetilde{\gamma}_n^{t}$.

\paragraph{Result \eqref{eq:lemmaboundx}.} To complete the proof, we consider result \eqref{eq:lemmaboundx}. First notice that by the Triangle Inequality, $ \| \bx^{t}  \| \leq \| \bx^{t} - \bh^{t} - \mu_{t}^n \bX \| + \|  \bh^{t} + \mu_{t}^n \bX  \|$.  Then let $ \kappa_x = 2 \kappa_h + \frac{2\kappa}{ L_{\psi}}$ and therefore, by lemma~\ref{sums},

\begin{equation*}
\begin{split}
    \mathbb{P} \Big( \frac{1}{\sqrt{n}}   \| \bx^{t}  \| \geq \kappa_x \Big)  &=  \mathbb{P} \Big( \frac{1}{\sqrt{n}} \| \bx^{t} - \bh^{t} - \mu_{t}^n \bX  \| +   \frac{1}{\sqrt{n}} \|  \bh^{t} + \mu_{t}^n \bX  \|  \geq2 \kappa_h + \frac{2\kappa}{ L_{\psi}} \Big)  \\
&\leq  \mathbb{P} \Big( \frac{1}{\sqrt{n}}  \| \bx^{t} - \bh^{t} - \mu_{t}^n \bX  \|  \geq  \frac{\kappa}{ L_{\psi}} \Big)  +  \mathbb{P} \Big(   \frac{1}{\sqrt{n}} \|  \bh^{t} + \mu_{t}^n \bX \|  \geq  \kappa_h  \Big).
\end{split}
\end{equation*}

Then the bound follows by \eqref{eq:lemmaboundx} and \eqref{eq:lemmabound3}.  Note that with the bound on $   \mathbb{P} ( \frac{1}{\sqrt{n}}   \| \bx^{t}  \| \geq \kappa_x )$ established above, one can prove \eqref{eq:lemmabound1} and \eqref{eq:lemmabound2}, thus for the second result we would like to show in \eqref{eq:lemmaboundx}, namely the bound on $\mathbb{P}( \frac{1}{n}  \sum_{i=1}^n x^{t}_i \geq \frac{\mu_t^n}{2} )$, we note that we can employ the result \eqref{eq:lemmabound1}.  The proof proceeds then as in the same case for \eqref{eq:lemmaboundh}.
\end{proof}

config: arxiv