text:
(* ========================================================================= *)
(* Rob Arthan's "Descartes's Rule of Signs by an Easy Induction".            *)
(* ========================================================================= *)

needs "Multivariate/realanalysis.ml";;

(* ------------------------------------------------------------------------- *)
(* A couple of handy lemmas.                                                 *)
(* ------------------------------------------------------------------------- *)

let OPPOSITE_SIGNS = prove
 (`!a b:real. a * b < &0 <=> &0 < a /\ b < &0 \/ a < &0 /\ &0 < b`,
  REWRITE_TAC[REAL_ARITH `a * b < &0 <=> &0 < a * --b`; REAL_MUL_POS_LT] THEN
  REAL_ARITH_TAC);;

let VARIATION_SET_FINITE = prove
 (`FINITE s ==> FINITE {p,q | p IN s /\ q IN s /\ P p q}`,
  REWRITE_TAC[SET_RULE
   `{p,q | p IN s /\ q IN t /\ R p q} =
    {p,q | p IN s /\ q IN {q | q IN t /\ R p q}}`] THEN
  SIMP_TAC[FINITE_PRODUCT_DEPENDENT; FINITE_RESTRICT]);;

(* ------------------------------------------------------------------------- *)
(* Variation in a sequence of coefficients.                                  *)
(* ------------------------------------------------------------------------- *)

let variation = new_definition
 `variation s (a:num->real) =
     CARD {(p,q) | p IN s /\ q IN s /\ p < q /\
                   a(p) * a(q) < &0 /\
                   !i. i IN s /\ p < i /\ i < q ==> a(i) = &0 }`;;

let VARIATION_EQ = prove
 (`!a b s. (!i. i IN s ==> a i = b i) ==> variation s a = variation s b`,
  REPEAT STRIP_TAC THEN REWRITE_TAC[variation] THEN AP_TERM_TAC THEN
  REWRITE_TAC[EXTENSION; FORALL_PAIR_THM; IN_ELIM_PAIR_THM] THEN
  ASM_MESON_TAC[]);;

let VARIATION_SUBSET = prove
 (`!a s t. t SUBSET s /\ (!i. i IN (s DIFF t) ==> a i = &0)
           ==> variation s a = variation t a`,
  REWRITE_TAC[IN_DIFF; SUBSET] THEN REPEAT STRIP_TAC THEN
  REWRITE_TAC[variation] THEN AP_TERM_TAC THEN
  REWRITE_TAC[EXTENSION; FORALL_PAIR_THM; IN_ELIM_PAIR_THM] THEN
  ASM_MESON_TAC[REAL_MUL_LZERO; REAL_MUL_RZERO; REAL_LT_REFL]);;

let VARIATION_SPLIT = prove
 (`!a s n.
        FINITE s /\ n IN s /\ ~(a n = &0)
        ==> variation s a = variation {i | i IN s /\ i <= n} a +
                            variation {i | i IN s /\ n <= i} a`,
  REWRITE_TAC[variation] THEN REPEAT STRIP_TAC THEN
  CONV_TAC SYM_CONV THEN MATCH_MP_TAC CARD_UNION_EQ THEN
  ASM_SIMP_TAC[VARIATION_SET_FINITE; FINITE_RESTRICT] THEN
  REWRITE_TAC[EXTENSION; FORALL_PAIR_THM] THEN CONJ_TAC THENL
   [REWRITE_TAC[IN_INTER; NOT_IN_EMPTY; IN_ELIM_PAIR_THM; IN_NUMSEG] THEN
    REWRITE_TAC[IN_ELIM_THM] THEN ARITH_TAC;
    REWRITE_TAC[IN_UNION; IN_ELIM_PAIR_THM; IN_NUMSEG] THEN
    REPEAT GEN_TAC THEN EQ_TAC THENL
     [STRIP_TAC;
      STRIP_TAC THEN FIRST_X_ASSUM(fun th ->
        MP_TAC(SPEC `n:num` th) THEN ASM_REWRITE_TAC[] THEN ASSUME_TAC th) THEN
      SIMP_TAC[TAUT `~(a /\ b) <=> ~b \/ ~a`] THEN MATCH_MP_TAC MONO_OR] THEN
    RULE_ASSUM_TAC(REWRITE_RULE[IN_ELIM_THM]) THEN
    ASM_REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN
    TRY(FIRST_ASSUM MATCH_MP_TAC) THEN
    FIRST_ASSUM(fun th -> MP_TAC(SPEC `n:num` th) THEN ASM_REWRITE_TAC[]) THEN
    ASM_ARITH_TAC]);;

let VARIATION_SPLIT_NUMSEG = prove
 (`!a m n p. n IN m..p /\ ~(a n = &0)
             ==> variation(m..p) a = variation(m..n) a + variation(n..p) a`,
  REPEAT GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP
   (REWRITE_RULE[TAUT `a /\ b /\ c ==> d <=> b /\ c ==> a ==> d`]
     VARIATION_SPLIT)) THEN
  REWRITE_TAC[FINITE_NUMSEG] THEN DISCH_THEN SUBST1_TAC THEN
  BINOP_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
  REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_NUMSEG] THEN
  RULE_ASSUM_TAC(REWRITE_RULE[IN_NUMSEG]) THEN ASM_ARITH_TAC);;

let VARIATION_1 = prove
 (`!a n. variation {n} a = 0`,
  REWRITE_TAC[variation; IN_SING] THEN
  REWRITE_TAC[ARITH_RULE `p:num = n /\ q = n /\ p < q /\ X <=> F`] THEN
  MATCH_MP_TAC(MESON[CARD_CLAUSES] `s = {} ==> CARD s = 0`) THEN
  REWRITE_TAC[EXTENSION; FORALL_PAIR_THM; IN_ELIM_PAIR_THM; NOT_IN_EMPTY]);;

let VARIATION_2 = prove
 (`!a m n. variation {m,n} a = if a(m) * a(n) < &0 then 1 else 0`,
  GEN_TAC THEN MATCH_MP_TAC WLOG_LT THEN REPEAT CONJ_TAC THENL
   [REWRITE_TAC[INSERT_AC; VARIATION_1; GSYM REAL_NOT_LE; REAL_LE_SQUARE];
    REWRITE_TAC[INSERT_AC; REAL_MUL_SYM];
    REPEAT STRIP_TAC THEN REWRITE_TAC[variation; IN_INSERT; NOT_IN_EMPTY] THEN
    ONCE_REWRITE_TAC[TAUT
     `a /\ b /\ c /\ d /\ e <=> (a /\ b /\ c) /\ d /\ e`] THEN
    ASM_SIMP_TAC[ARITH_RULE
     `m:num < n
      ==> ((p = m \/ p = n) /\ (q = m \/ q = n) /\ p < q <=>
           p = m /\ q = n)`] THEN
    REWRITE_TAC[MESON[] `(p = m /\ q = n) /\ X p q <=>
                         (p = m /\ q = n) /\ X m n`] THEN
    REWRITE_TAC[ARITH_RULE `(i:num = m \/ i = n) /\ m < i /\ i < n <=> F`] THEN
    ASM_CASES_TAC `a m * a(n:num) < &0` THEN ASM_REWRITE_TAC[] THENL
     [REWRITE_TAC[SET_RULE `{p,q | p = a /\ q = b} = {(a,b)}`] THEN
      SIMP_TAC[CARD_CLAUSES; FINITE_RULES; NOT_IN_EMPTY; ARITH];
      MATCH_MP_TAC(MESON[CARD_CLAUSES] `s = {} ==> CARD s = 0`) THEN
      SIMP_TAC[EXTENSION; FORALL_PAIR_THM; IN_ELIM_PAIR_THM; NOT_IN_EMPTY]]]);;

let VARIATION_3 = prove
 (`!a m n p.
        m < n /\ n < p
        ==> variation {m,n,p} a = if a(n) = &0 then variation{m,p} a
                                  else variation {m,n} a + variation{n,p} a`,
  REPEAT STRIP_TAC THEN COND_CASES_TAC THENL
   [MATCH_MP_TAC VARIATION_SUBSET THEN ASM SET_TAC[];
    MP_TAC(ISPECL [`a:num->real`; `{m:num,n,p}`; `n:num`] VARIATION_SPLIT) THEN
    ASM_SIMP_TAC[FINITE_INSERT; FINITE_EMPTY; IN_INSERT; NOT_IN_EMPTY] THEN
    DISCH_THEN SUBST1_TAC THEN BINOP_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
    REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_INSERT; NOT_IN_EMPTY] THEN
    ASM_ARITH_TAC]);;

let VARIATION_OFFSET = prove
 (`!p m n a. variation(m+p..n+p) a = variation(m..n) (\i. a(i + p))`,
  REPEAT GEN_TAC THEN REWRITE_TAC[variation] THEN
  MATCH_MP_TAC BIJECTIONS_CARD_EQ THEN MAP_EVERY EXISTS_TAC
   [`\(i:num,j). i - p,j - p`; `\(i:num,j). i + p,j + p`] THEN
  REWRITE_TAC[FORALL_IN_GSPEC] THEN REWRITE_TAC[IN_ELIM_PAIR_THM] THEN
  SIMP_TAC[VARIATION_SET_FINITE; FINITE_NUMSEG] THEN
  REWRITE_TAC[IN_NUMSEG; PAIR_EQ] THEN
  REPEAT STRIP_TAC THEN TRY ASM_ARITH_TAC THENL
   [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
     `y < &0 ==> x = y ==> x < &0`)) THEN
    BINOP_TAC THEN AP_TERM_TAC THEN ASM_ARITH_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
    FIRST_X_ASSUM(MP_TAC o SPEC `i - p:num`) THEN
    ANTS_TAC THENL [ASM_ARITH_TAC; MATCH_MP_TAC EQ_IMP] THEN
    AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN ASM_ARITH_TAC]);;

(* ------------------------------------------------------------------------- *)
(* The crucial lemma (roughly Lemma 2 in the paper).                         *)
(* ------------------------------------------------------------------------- *)

let ARTHAN_LEMMA = prove
 (`!n a b.
        ~(a n = &0) /\ (b n = &0) /\ (!m. sum(0..m) a = b m)
        ==> ?d. ODD d /\ variation (0..n) a = variation (0..n) b + d`,
  MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN
  DISCH_THEN(LABEL_TAC "*") THEN
  REPEAT STRIP_TAC THEN ASM_CASES_TAC `n = 0` THENL
   [FIRST_X_ASSUM(MP_TAC o SPEC `0`) THEN
    ASM_REWRITE_TAC[SUM_SING_NUMSEG] THEN
    ASM_MESON_TAC[];
    ALL_TAC] THEN
  FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP (ARITH_RULE
   `~(n = 0) ==> n = 1 \/ 2 <= n`))
  THENL
   [FIRST_X_ASSUM SUBST_ALL_TAC THEN EXISTS_TAC `1` THEN
    CONV_TAC NUM_REDUCE_CONV THEN
    CONV_TAC(ONCE_DEPTH_CONV NUMSEG_CONV) THEN
    REWRITE_TAC[VARIATION_2; OPPOSITE_SIGNS] THEN
    FIRST_X_ASSUM(fun th -> MP_TAC(SPEC `0` th) THEN MP_TAC(SPEC `1` th)) THEN
    SIMP_TAC[num_CONV `1`; SUM_CLAUSES_NUMSEG] THEN
    CONV_TAC NUM_REDUCE_CONV THEN COND_CASES_TAC THEN REWRITE_TAC[] THEN
    ASM_ARITH_TAC;
    ALL_TAC] THEN
  SUBGOAL_THEN `?p. 1 < p /\ p <= n /\ ~(a p = &0)` MP_TAC THENL
   [ASM_MESON_TAC[ARITH_RULE `2 <= n ==> 1 < n`; LE_REFL];
    GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN
    REWRITE_TAC[TAUT `a ==> ~(b /\ c /\ ~d) <=> a /\ b /\ c ==> d`] THEN
    STRIP_TAC] THEN
  REMOVE_THEN "*" (MP_TAC o SPEC `n - 1`) THEN
  ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN DISCH_THEN(MP_TAC o SPECL
   [`(\i. if i + 1 = 1 then a 0 + a 1 else a(i + 1)):num->real`;
    `(\i. b(i + 1)):num->real`]) THEN
  ASM_SIMP_TAC[ARITH_RULE `2 <= n ==> ~(n = 1) /\ n - 1 + 1 = n`] THEN
  REWRITE_TAC[GSYM(SPEC `1` VARIATION_OFFSET)] THEN ANTS_TAC THENL
   [X_GEN_TAC `m:num` THEN MATCH_MP_TAC EQ_TRANS THEN
    EXISTS_TAC `sum(0..m+1) a` THEN CONJ_TAC THENL
     [SIMP_TAC[SUM_CLAUSES_LEFT; LE_0; ARITH_RULE `0 + 1 <= n + 1`] THEN
      CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[REAL_ADD_ASSOC] THEN
      AP_TERM_TAC THEN REWRITE_TAC[ARITH_RULE `2 = 1 + 1`; SUM_OFFSET] THEN
      MATCH_MP_TAC SUM_EQ_NUMSEG THEN ARITH_TAC;
      ASM_REWRITE_TAC[]];
    ABBREV_TAC `a':num->real = \m. if m = 1 then a 0 + a 1 else a m` THEN
    ASM_SIMP_TAC[ARITH_RULE
     `2 <= n ==> n - 1 + 1 = n /\ n - 1 - 1 + 1 = n - 1`] THEN
    CONV_TAC NUM_REDUCE_CONV] THEN
  SUBGOAL_THEN
   `variation (1..n) a' = variation {1,p} a' + variation (p..n) a /\
    variation (0..n) a = variation {0,1,p} a + variation (p..n) a`
   (CONJUNCTS_THEN SUBST1_TAC)
  THENL
   [CONJ_TAC THEN MATCH_MP_TAC EQ_TRANS THENL
     [EXISTS_TAC `variation(1..p) a' + variation(p..n) a'`;
      EXISTS_TAC `variation(0..p) a + variation(p..n) a`] THEN
    (CONJ_TAC THENL
      [MATCH_MP_TAC VARIATION_SPLIT_NUMSEG THEN EXPAND_TAC "a'" THEN
       REWRITE_TAC[IN_NUMSEG] THEN ASM_ARITH_TAC;
       BINOP_TAC THENL
        [MATCH_MP_TAC VARIATION_SUBSET; MATCH_MP_TAC VARIATION_EQ] THEN
       EXPAND_TAC "a'" THEN REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN
       REWRITE_TAC[IN_NUMSEG] THEN TRY(GEN_TAC THEN ASM_ARITH_TAC) THEN
       (CONJ_TAC THENL [ASM_ARITH_TAC; REWRITE_TAC[IN_DIFF]]) THEN
       REWRITE_TAC[IN_NUMSEG; IN_INSERT; NOT_IN_EMPTY] THEN
       REPEAT STRIP_TAC THEN TRY COND_CASES_TAC THEN
       TRY(FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_ARITH_TAC]);
    ALL_TAC] THEN
  DISCH_THEN(X_CHOOSE_THEN `d:num` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
  REWRITE_TAC[GSYM INT_OF_NUM_EQ; GSYM INT_OF_NUM_ADD] THEN
  DISCH_THEN(ASSUME_TAC o MATCH_MP (INT_ARITH
   `a + b:int = c + d ==> c = (a + b) - d`)) THEN
  REWRITE_TAC[INT_ARITH `a + b:int = c + d <=> d = (a + b) - c`] THEN
  ASM_CASES_TAC `a 0 + a 1 = &0` THENL
   [SUBGOAL_THEN `!i. 0 < i /\ i < p ==> b i = &0` ASSUME_TAC THENL
     [REPEAT STRIP_TAC THEN
      FIRST_X_ASSUM(SUBST1_TAC o SYM o SPEC `i:num`) THEN
      ASM_SIMP_TAC[SUM_CLAUSES_LEFT; LE_0;
                   ARITH_RULE `0 < i ==> 0 + 1 <= i`] THEN
      CONV_TAC NUM_REDUCE_CONV THEN
      ASM_REWRITE_TAC[REAL_ADD_ASSOC; REAL_ADD_LID] THEN
      MATCH_MP_TAC SUM_EQ_0_NUMSEG THEN REPEAT STRIP_TAC THEN
      FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
      ALL_TAC] THEN
    SUBGOAL_THEN `(b:num->real) p = a p` ASSUME_TAC THENL
     [FIRST_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [GSYM th]) THEN
      SIMP_TAC[SUM_CLAUSES_RIGHT; ASSUME `1 < p`;
                 ARITH_RULE `1 < p ==> 0 < p /\ 0 <= p`] THEN
      ASM_REWRITE_TAC[REAL_EQ_ADD_RCANCEL_0] THEN
      FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
      ALL_TAC] THEN
    SUBGOAL_THEN `variation(0..n) b = variation {0,p} b + variation(1..n) b`
    SUBST1_TAC THENL
     [MATCH_MP_TAC EQ_TRANS THEN
      EXISTS_TAC `variation(0..p) b + variation(p..n) b` THEN CONJ_TAC THENL
       [MATCH_MP_TAC VARIATION_SPLIT_NUMSEG THEN REWRITE_TAC[IN_NUMSEG] THEN
        CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
        FIRST_ASSUM(SUBST1_TAC o SYM o SPEC `p:num`) THEN
        SIMP_TAC[SUM_CLAUSES_RIGHT; ASSUME `1 < p`;
                 ARITH_RULE `1 < p ==> 0 < p /\ 0 <= p`] THEN
        ASM_REWRITE_TAC[] THEN
        FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
         `~(ap = &0) ==> s = &0 ==> ~(s + ap = &0)`)) THEN
        FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
        BINOP_TAC THENL [ALL_TAC; CONV_TAC SYM_CONV] THEN
        MATCH_MP_TAC VARIATION_SUBSET THEN
        REWRITE_TAC[SUBSET; IN_DIFF; IN_NUMSEG; IN_INSERT; NOT_IN_EMPTY] THEN
        (CONJ_TAC THENL [ASM_ARITH_TAC; REPEAT STRIP_TAC]) THEN
        FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC];
      ALL_TAC];
    SUBGOAL_THEN `variation(0..n) b = variation {0,1} b + variation(1..n) b`
    SUBST1_TAC THENL
     [MATCH_MP_TAC EQ_TRANS THEN
      EXISTS_TAC `variation(0..1) b + variation(1..n) b` THEN CONJ_TAC THENL
       [MATCH_MP_TAC VARIATION_SPLIT_NUMSEG THEN REWRITE_TAC[IN_NUMSEG] THEN
        CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
        FIRST_ASSUM(SUBST1_TAC o SYM o SPEC `1`) THEN
        SIMP_TAC[SUM_CLAUSES_NUMSEG; num_CONV `1`] THEN
        CONV_TAC NUM_REDUCE_CONV THEN ASM_REWRITE_TAC[];
        AP_THM_TAC THEN AP_TERM_TAC THEN MATCH_MP_TAC VARIATION_SUBSET THEN
        REWRITE_TAC[SUBSET; IN_DIFF; IN_NUMSEG; IN_INSERT; NOT_IN_EMPTY] THEN
        ARITH_TAC];
      SUBGOAL_THEN `(b:num->real) 1 = a 0 + a 1` ASSUME_TAC THENL
       [FIRST_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [GSYM th]) THEN
        SIMP_TAC[num_CONV `1`; SUM_CLAUSES_NUMSEG] THEN
        CONV_TAC NUM_REDUCE_CONV;
        ALL_TAC]]] THEN
  REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `0`)) THEN CONV_TAC NUM_REDUCE_CONV THEN
  REWRITE_TAC[SUM_SING_NUMSEG] THEN DISCH_TAC THEN
  ASM_REWRITE_TAC[GSYM INT_OF_NUM_ADD] THEN
  ASM_SIMP_TAC[VARIATION_3; ARITH; OPPOSITE_SIGNS] THEN COND_CASES_TAC THEN
  REWRITE_TAC[VARIATION_2; OPPOSITE_SIGNS; REAL_LT_REFL] THEN
  EXPAND_TAC "a'" THEN CONV_TAC NUM_REDUCE_CONV THEN
  ASM_SIMP_TAC[ARITH_RULE `1 < p ==> ~(p = 1)`; REAL_LT_REFL] THEN
  REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
  CONV_TAC NUM_REDUCE_CONV THEN
  CONV_TAC(BINDER_CONV(RAND_CONV(RAND_CONV INT_POLY_CONV))) THEN
  REWRITE_TAC[INT_ARITH `x:int = y + --z <=> x + z = y`] THEN
  REWRITE_TAC[INT_OF_NUM_ADD; INT_OF_NUM_EQ] THEN
  ONCE_REWRITE_TAC[CONJ_SYM] THEN ASM_REWRITE_TAC[UNWIND_THM2] THEN
  ASM_REWRITE_TAC[ODD_ADD; ARITH_ODD; ARITH_EVEN] THEN ASM_REAL_ARITH_TAC);;

(* ------------------------------------------------------------------------- *)
(* Relate even-ness or oddity of variation to signs of end coefficients.     *)
(* ------------------------------------------------------------------------- *)

let VARIATION_OPPOSITE_ENDS = prove
 (`!a m n.
    m <= n /\ ~(a m = &0) /\ ~(a n = &0)
    ==> (ODD(variation(m..n) a) <=> a m * a n < &0)`,
  REPEAT GEN_TAC THEN WF_INDUCT_TAC `n - m:num` THEN REPEAT STRIP_TAC THEN
  ASM_CASES_TAC `!i:num. m < i /\ i < n ==> a i = &0` THENL
   [MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `ODD(variation {m,n} a)` THEN
    CONJ_TAC THENL
     [AP_TERM_TAC THEN MATCH_MP_TAC VARIATION_SUBSET THEN
      ASM_REWRITE_TAC[INSERT_SUBSET; IN_NUMSEG; IN_DIFF; EMPTY_SUBSET] THEN
      REWRITE_TAC[LE_REFL; IN_INSERT; NOT_IN_EMPTY] THEN
      REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
      REWRITE_TAC[VARIATION_2] THEN COND_CASES_TAC THEN
      ASM_REWRITE_TAC[ARITH]];
    FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_FORALL_THM]) THEN
    REWRITE_TAC[NOT_IMP] THEN
    DISCH_THEN(X_CHOOSE_THEN `p:num` STRIP_ASSUME_TAC) THEN
    FIRST_X_ASSUM(fun th ->
        MP_TAC(SPECL [`n:num`; `p:num`] th) THEN
        MP_TAC(SPECL [`p:num`; `m:num`] th)) THEN
    ASM_SIMP_TAC[LT_IMP_LE] THEN
    REPEAT(ANTS_TAC THENL [ASM_ARITH_TAC; DISCH_TAC]) THEN
    MATCH_MP_TAC EQ_TRANS THEN
    EXISTS_TAC `ODD(variation(m..p) a + variation(p..n) a)` THEN CONJ_TAC THENL
     [AP_TERM_TAC THEN MATCH_MP_TAC VARIATION_SPLIT_NUMSEG THEN
      ASM_SIMP_TAC[LT_IMP_LE; IN_NUMSEG];
      ASM_REWRITE_TAC[ODD_ADD; OPPOSITE_SIGNS] THEN ASM_REAL_ARITH_TAC]]);;

(* ------------------------------------------------------------------------- *)
(* Polynomial with odd variation has at least one positive root.             *)
(* This is the only "analytical" part of the proof.                          *)
(* ------------------------------------------------------------------------- *)

let REAL_POLYFUN_SGN_AT_INFINITY = prove
 (`!a n. ~(a n = &0)
         ==> ?B. &0 < B /\
                 !x. B <= abs x
                     ==> real_sgn(sum(0..n) (\i. a i * x pow i)) =
                         real_sgn(a n * x pow n)`,
  let lemma = prove
   (`abs(x) < abs(y) ==> real_sgn(x + y) = real_sgn y`,
    REWRITE_TAC[real_sgn] THEN REAL_ARITH_TAC) in
  REPEAT STRIP_TAC THEN ASM_CASES_TAC `n = 0` THENL
   [EXISTS_TAC `&1` THEN ASM_REWRITE_TAC[REAL_LT_01; SUM_SING_NUMSEG];
    ALL_TAC] THEN
  ABBREV_TAC `B = sum (0..n-1) (\i. abs(a i)) / abs(a n)` THEN
  SUBGOAL_THEN `&0 <= B` ASSUME_TAC THENL
   [EXPAND_TAC "B" THEN SIMP_TAC[REAL_LE_DIV; REAL_ABS_POS; SUM_POS_LE_NUMSEG];
    ALL_TAC] THEN
  EXISTS_TAC `&1 + B` THEN CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
  X_GEN_TAC `x:real` THEN STRIP_TAC THEN
  ASM_SIMP_TAC[SUM_CLAUSES_RIGHT; LE_0; LE_1] THEN MATCH_MP_TAC lemma THEN
  MATCH_MP_TAC REAL_LET_TRANS THEN
  EXISTS_TAC `sum(0..n-1) (\i. abs(a i)) * abs x pow (n - 1)` THEN
  CONJ_TAC THENL
   [REWRITE_TAC[GSYM SUM_RMUL] THEN MATCH_MP_TAC SUM_ABS_LE THEN
    REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN
    X_GEN_TAC `i:num` THEN STRIP_TAC THEN REWRITE_TAC[REAL_ABS_MUL] THEN
    MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS; REAL_ABS_POW] THEN
    MATCH_MP_TAC REAL_POW_MONO THEN ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC;
    SUBGOAL_THEN `(x:real) pow n = x * x pow (n - 1)` SUBST1_TAC THENL
     [SIMP_TAC[GSYM(CONJUNCT2 real_pow)] THEN AP_TERM_TAC THEN ASM_ARITH_TAC;
      REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_POW; REAL_MUL_ASSOC] THEN
      MATCH_MP_TAC REAL_LT_RMUL THEN CONJ_TAC THENL
       [ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
        ASM_SIMP_TAC[GSYM REAL_LT_LDIV_EQ; GSYM REAL_ABS_NZ] THEN
        ASM_REAL_ARITH_TAC;
        MATCH_MP_TAC REAL_POW_LT THEN ASM_REAL_ARITH_TAC]]]);;

let REAL_POLYFUN_HAS_POSITIVE_ROOT = prove
 (`!a n. a 0 < &0 /\ &0 < a n
         ==> ?x. &0 < x /\ sum(0..n) (\i. a i * x pow i) = &0`,
  REPEAT STRIP_TAC THEN
  SUBGOAL_THEN `?x. &0 < x /\ &0 <= sum(0..n) (\i. a i * x pow i)`
  STRIP_ASSUME_TAC THENL
   [MP_TAC(ISPECL [`a:num->real`; `n:num`] REAL_POLYFUN_SGN_AT_INFINITY) THEN
    ASM_SIMP_TAC[REAL_LT_IMP_NZ] THEN MATCH_MP_TAC MONO_EXISTS THEN
    X_GEN_TAC `x:real` THEN
    DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `x:real`)) THEN
    ANTS_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
    SUBGOAL_THEN `real_sgn(a n * x pow n) = &1` SUBST1_TAC THEN
    ASM_SIMP_TAC[REAL_SGN_EQ; REAL_LT_MUL; REAL_POW_LT; real_gt] THEN
    REWRITE_TAC[REAL_LT_IMP_LE];
    MP_TAC(ISPECL [`\x. sum(0..n) (\i. a i * x pow i)`;
                   `&0`; `x:real`; `&0`] REAL_IVT_INCREASING) THEN
    ASM_SIMP_TAC[REAL_LT_IMP_LE; IN_REAL_INTERVAL;
                 REAL_POW_ZERO; COND_RAND] THEN
    REWRITE_TAC[REAL_MUL_RID; REAL_MUL_RZERO; SUM_DELTA; IN_NUMSEG; LE_0] THEN
    ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN ANTS_TAC THENL
     [MATCH_MP_TAC REAL_CONTINUOUS_ON_SUM THEN
      REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN REPEAT STRIP_TAC THEN
      MATCH_MP_TAC REAL_CONTINUOUS_ON_LMUL THEN
      MATCH_MP_TAC REAL_CONTINUOUS_ON_POW THEN
      REWRITE_TAC[REAL_CONTINUOUS_ON_ID];
      MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `y:real` THEN
      SIMP_TAC[REAL_LT_LE] THEN ASM_CASES_TAC `y:real = &0` THEN
      ASM_SIMP_TAC[REAL_POW_ZERO; COND_RAND; REAL_MUL_RZERO; REAL_MUL_RID] THEN
      REWRITE_TAC[SUM_DELTA; IN_NUMSEG; LE_0] THEN ASM_REAL_ARITH_TAC]]);;

let ODD_VARIATION_POSITIVE_ROOT = prove
 (`!a n. ODD(variation(0..n) a)
         ==> ?x. &0 < x /\ sum(0..n) (\i. a i * x pow i) = &0`,
  REPEAT STRIP_TAC THEN
  SUBGOAL_THEN `?M. !i. i IN 0..n /\ ~(a i = &0) ==> i <= M` MP_TAC THENL
   [EXISTS_TAC `n:num` THEN SIMP_TAC[IN_NUMSEG]; ALL_TAC] THEN
  SUBGOAL_THEN `?i. i IN 0..n /\ ~(a i = &0)` MP_TAC THENL
   [MATCH_MP_TAC(MESON[] `((!i. P i ==> Q i) ==> F) ==> ?i. P i /\ ~Q i`) THEN
    DISCH_TAC THEN SUBGOAL_THEN `variation (0..n) a = variation {0} a`
     (fun th -> SUBST_ALL_TAC th THEN ASM_MESON_TAC[VARIATION_1; ODD]) THEN
    MATCH_MP_TAC VARIATION_SUBSET THEN
    ASM_SIMP_TAC[IN_DIFF] THEN REWRITE_TAC[IN_NUMSEG; SING_SUBSET; LE_0];
    ALL_TAC] THEN
  ONCE_REWRITE_TAC[TAUT `a ==> b ==> c <=> a ==> a /\ b ==> c`] THEN
  GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN REWRITE_TAC[num_MAX] THEN
  REWRITE_TAC[TAUT `p ==> ~(q /\ r) <=> p /\ q ==> ~r`; IN_NUMSEG] THEN
  DISCH_THEN(X_CHOOSE_THEN `p:num` STRIP_ASSUME_TAC) THEN
  ONCE_REWRITE_TAC[TAUT `p /\ ~q ==> r <=> p /\ ~r ==> q`] THEN
  DISCH_THEN(X_CHOOSE_THEN `q:num` STRIP_ASSUME_TAC) THEN
  SUBGOAL_THEN `p:num <= q` ASSUME_TAC THENL
   [ASM_MESON_TAC[NOT_LT]; ALL_TAC] THEN
  SUBGOAL_THEN `(a:num->real) p * a q < &0` ASSUME_TAC THENL
   [ASM_SIMP_TAC[GSYM VARIATION_OPPOSITE_ENDS] THEN
    FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (MESON[]
     `ODD p ==> p = q ==> ODD q`)) THEN
    MATCH_MP_TAC VARIATION_SUBSET THEN
    REWRITE_TAC[SUBSET_NUMSEG; IN_NUMSEG; IN_DIFF; DE_MORGAN_THM] THEN
    CONJ_TAC THENL [ASM_ARITH_TAC; REPEAT STRIP_TAC] THEN
    FIRST_X_ASSUM(fun th -> MATCH_MP_TAC th THEN ASM_ARITH_TAC);
    ALL_TAC] THEN
  MP_TAC(ISPECL [`\i. (a:num->real)(p + i) / a q`; `q - p:num`]
        REAL_POLYFUN_HAS_POSITIVE_ROOT) THEN
  ASM_SIMP_TAC[ADD_CLAUSES; ARITH_RULE `p:num <= q ==> p + q - p = q`] THEN
  ANTS_TAC THENL
   [REWRITE_TAC[real_div; OPPOSITE_SIGNS; REAL_MUL_POS_LT] THEN
    FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [OPPOSITE_SIGNS]) THEN
    REWRITE_TAC[REAL_ARITH `x < &0 <=> &0 < --x`; GSYM REAL_INV_NEG] THEN
    REWRITE_TAC[REAL_LT_INV_EQ] THEN REAL_ARITH_TAC;
    ALL_TAC] THEN
  MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `x:real` THEN
  MATCH_MP_TAC MONO_AND THEN REWRITE_TAC[] THEN MATCH_MP_TAC(REAL_RING
   `!a. y = a * x ==> x = &0 ==> y = &0`) THEN
  EXISTS_TAC `(a:num->real) q * x pow p` THEN
  REWRITE_TAC[GSYM SUM_LMUL; REAL_ARITH
   `(aq * xp) * api / aq * xi:real = (aq / aq) * api * (xp * xi)`] THEN
  ASM_CASES_TAC `(a:num->real) q = &0` THENL
   [ASM_MESON_TAC[REAL_MUL_LZERO; REAL_LT_REFL]; ALL_TAC] THEN
  ASM_SIMP_TAC[GSYM REAL_POW_ADD; REAL_DIV_REFL; REAL_MUL_LID] THEN
  ONCE_REWRITE_TAC[ADD_SYM] THEN MP_TAC(SPEC `p:num` SUM_OFFSET) THEN
  DISCH_THEN(fun th -> REWRITE_TAC[GSYM th]) THEN
  MATCH_MP_TAC SUM_SUPERSET THEN
  REWRITE_TAC[SUBSET_NUMSEG; IN_NUMSEG; IN_DIFF; DE_MORGAN_THM] THEN
  CONJ_TAC THENL [ASM_ARITH_TAC; REPEAT STRIP_TAC] THEN
  REWRITE_TAC[REAL_ENTIRE] THEN DISJ1_TAC THEN
  FIRST_X_ASSUM(fun th -> MATCH_MP_TAC th THEN ASM_ARITH_TAC));;

(* ------------------------------------------------------------------------- *)
(* Define root multiplicities.                                               *)
(* ------------------------------------------------------------------------- *)

let multiplicity = new_definition
 `multiplicity f r =
        @k. ?a n. ~(sum(0..n) (\i. a i * r pow i) = &0) /\
                  !x. f(x) = (x - r) pow k * sum(0..n) (\i. a i * x pow i)`;;

let MULTIPLICITY_UNIQUE = prove
 (`!f a r b m k.
        (!x. f(x) = (x - r) pow k * sum(0..m) (\j. b j * x pow j)) /\
        ~(sum(0..m) (\j. b j * r pow j) = &0)
        ==> k = multiplicity f r`,
  let lemma = prove
   (`!i j f g. f real_continuous_on (:real) /\ g real_continuous_on (:real) /\
               ~(f r = &0) /\ ~(g r = &0)
               ==> (!x. (x - r) pow i * f(x) = (x - r) pow j * g(x))
                   ==> j = i`,
    MATCH_MP_TAC WLOG_LT THEN
    REWRITE_TAC[] THEN CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
    MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN REPEAT STRIP_TAC THEN
    MATCH_MP_TAC(TAUT `F ==> p`) THEN
    MP_TAC(ISPECL [`atreal r`; `f:real->real`;
                   `(f:real->real) r`; `&0`]
          REALLIM_UNIQUE) THEN
    ASM_REWRITE_TAC[TRIVIAL_LIMIT_ATREAL] THEN CONJ_TAC THENL
     [REWRITE_TAC[GSYM REAL_CONTINUOUS_ATREAL] THEN
      ASM_MESON_TAC[REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT; REAL_OPEN_UNIV;
                    IN_UNIV];
      MATCH_MP_TAC REALLIM_TRANSFORM_EVENTUALLY THEN
      EXISTS_TAC `\x:real. (x - r) pow (j - i) * g x` THEN
      REWRITE_TAC[] THEN CONJ_TAC THENL
       [REWRITE_TAC[EVENTUALLY_ATREAL] THEN EXISTS_TAC `&1` THEN
        REWRITE_TAC[REAL_LT_01; REAL_ARITH `&0 < abs(x - r) <=> ~(x = r)`] THEN
        X_GEN_TAC `x:real` THEN STRIP_TAC THEN MATCH_MP_TAC(REAL_RING
         `!a. a * x = a * y /\ ~(a = &0) ==> x = y`) THEN
        EXISTS_TAC `(x - r:real) pow i` THEN
        ASM_REWRITE_TAC[REAL_MUL_ASSOC; GSYM REAL_POW_ADD; REAL_POW_EQ_0] THEN
        ASM_SIMP_TAC[REAL_SUB_0; ARITH_RULE `i:num < j ==> i + j - i = j`];
        SUBST1_TAC(REAL_ARITH `&0 = &0 * (g:real->real) r`) THEN
        MATCH_MP_TAC REALLIM_MUL THEN CONJ_TAC THENL
         [REWRITE_TAC[] THEN MATCH_MP_TAC REALLIM_NULL_POW THEN
          REWRITE_TAC[GSYM REALLIM_NULL; REALLIM_ATREAL_ID] THEN ASM_ARITH_TAC;
          REWRITE_TAC[GSYM REAL_CONTINUOUS_ATREAL] THEN
          ASM_MESON_TAC[REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT;
                        REAL_OPEN_UNIV; IN_UNIV]]]]) in
  REPEAT STRIP_TAC THEN REWRITE_TAC[multiplicity] THEN
  CONV_TAC SYM_CONV THEN MATCH_MP_TAC SELECT_UNIQUE THEN
  X_GEN_TAC `j:num` THEN EQ_TAC THEN ASM_SIMP_TAC[LEFT_IMP_EXISTS_THM] THENL
   [REPEAT GEN_TAC THEN
    DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
    MATCH_MP_TAC lemma THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THEN
    MATCH_MP_TAC REAL_CONTINUOUS_ON_SUM THEN
    REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN REPEAT STRIP_TAC THEN
    MATCH_MP_TAC REAL_CONTINUOUS_ON_LMUL THEN
    MATCH_MP_TAC REAL_CONTINUOUS_ON_POW THEN
    REWRITE_TAC[REAL_CONTINUOUS_ON_ID];
    DISCH_THEN SUBST1_TAC THEN
    MAP_EVERY EXISTS_TAC [`b:num->real`; `m:num`] THEN ASM_REWRITE_TAC[]]);;

let MULTIPLICITY_WORKS = prove
 (`!r n a.
    (?i. i IN 0..n /\ ~(a i = &0))
    ==> ?b m.
        ~(sum(0..m) (\i. b i * r pow i) = &0) /\
        !x. sum(0..n) (\i. a i * x pow i) =
            (x - r) pow multiplicity (\x. sum(0..n) (\i. a i * x pow i)) r *
            sum(0..m) (\i. b i * x pow i)`,
  REWRITE_TAC[multiplicity] THEN CONV_TAC(ONCE_DEPTH_CONV SELECT_CONV) THEN
  GEN_TAC THEN MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN
  DISCH_TAC THEN X_GEN_TAC `a:num->real` THEN
  ASM_CASES_TAC `(a:num->real) n = &0` THENL
   [ASM_CASES_TAC `n = 0` THEN
    ASM_REWRITE_TAC[NUMSEG_SING; IN_SING; UNWIND_THM2]
    THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
    DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `n - 1`) THEN
    ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
    DISCH_THEN(MP_TAC o SPEC `a:num->real`) THEN
    ASM_SIMP_TAC[SUM_CLAUSES_RIGHT; LE_0; LE_1] THEN
    REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_RID] THEN
    DISCH_THEN MATCH_MP_TAC THEN
    FIRST_X_ASSUM(X_CHOOSE_THEN `i:num` MP_TAC) THEN
    REWRITE_TAC[IN_NUMSEG] THEN STRIP_TAC THEN
    EXISTS_TAC `i:num` THEN ASM_REWRITE_TAC[] THEN
    ASM_CASES_TAC `i:num = n` THENL [ASM_MESON_TAC[]; ASM_ARITH_TAC];
    ALL_TAC] THEN
  DISCH_THEN(K ALL_TAC) THEN
  ASM_CASES_TAC `sum(0..n) (\i. a i * r pow i) = &0` THENL
   [ASM_CASES_TAC `n = 0` THENL
     [UNDISCH_TAC `sum (0..n) (\i. a i * r pow i) = &0` THEN
      ASM_REWRITE_TAC[NUMSEG_SING; IN_SING; UNWIND_THM2; SUM_SING] THEN
      REWRITE_TAC[real_pow; REAL_MUL_RID] THEN ASM_MESON_TAC[];
      ALL_TAC] THEN
    MP_TAC(GEN `x:real` (ISPECL [`a:num->real`; `x:real`; `r:real`; `n:num`]
        REAL_SUB_POLYFUN)) THEN ASM_SIMP_TAC[LE_1; REAL_SUB_RZERO] THEN
    ABBREV_TAC `b j = sum (j + 1..n) (\i. a i * r pow (i - j - 1))` THEN
    DISCH_THEN(K ALL_TAC) THEN
    FIRST_X_ASSUM(ASSUME_TAC o GEN_REWRITE_RULE I [GSYM FUN_EQ_THM]) THEN
    FIRST_X_ASSUM(MP_TAC o SPEC `n - 1`) THEN
    ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
    DISCH_THEN(MP_TAC o SPEC `b:num->real`) THEN ANTS_TAC THENL
     [EXISTS_TAC `n - 1` THEN REWRITE_TAC[IN_NUMSEG; LE_REFL; LE_0] THEN
      EXPAND_TAC "b" THEN REWRITE_TAC[] THEN
      ASM_SIMP_TAC[SUB_ADD; LE_1; SUM_SING_NUMSEG; real_pow; REAL_MUL_RID;
                   ARITH_RULE `n - (n - 1) - 1 = 0`];
      ALL_TAC] THEN
    DISCH_THEN(X_CHOOSE_THEN `k:num` (fun th ->
        EXISTS_TAC `SUC k` THEN MP_TAC th)) THEN
    REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN
    STRIP_TAC THEN ASM_REWRITE_TAC[real_pow; GSYM REAL_MUL_ASSOC];
    MAP_EVERY EXISTS_TAC [`0`; `a:num->real`; `n:num`] THEN
    ASM_REWRITE_TAC[real_pow; REAL_MUL_LID]]);;

let MULTIPLICITY_OTHER_ROOT = prove
 (`!a n r s.
    ~(r = s) /\ (?i. i IN 0..n /\ ~(a i = &0))
     ==> multiplicity (\x. (x - r) pow m * sum(0..n) (\i. a i * x pow i)) s =
         multiplicity (\x.  sum(0..n) (\i. a i * x pow i)) s`,
  REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN
  CONV_TAC SYM_CONV THEN MATCH_MP_TAC MULTIPLICITY_UNIQUE THEN
  REWRITE_TAC[] THEN
  MP_TAC(ISPECL [`s:real`; `n:num`; `a:num->real`]
        MULTIPLICITY_WORKS) THEN
  ASM_REWRITE_TAC[] THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
  MAP_EVERY X_GEN_TAC [`c:num->real`; `p:num`] THEN
  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (ASSUME_TAC o GSYM)) THEN
  SUBGOAL_THEN
   `?b q. !x. sum(0..q) (\j. b j * x pow j) =
              (x - r) pow m * sum (0..p) (\i. c i * x pow i)`
  MP_TAC THENL
   [ALL_TAC;
    REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN
    STRIP_TAC THEN
    ASM_REWRITE_TAC[REAL_RING `r * x = s * r * y <=> r = &0 \/ s * y = x`] THEN
    ASM_REWRITE_TAC[REAL_ENTIRE; REAL_POW_EQ_0; REAL_SUB_0]] THEN
  MAP_EVERY (fun t -> SPEC_TAC(t,t)) [`c:num->real`; `p:num`; `m:num`] THEN
  POP_ASSUM_LIST(K ALL_TAC) THEN INDUCT_TAC THEN REPEAT GEN_TAC THENL
   [MAP_EVERY EXISTS_TAC [`c:num->real`; `p:num`] THEN
    ASM_REWRITE_TAC[real_pow; REAL_MUL_LID];
    ALL_TAC] THEN
  FIRST_X_ASSUM(MP_TAC o SPECL [`p:num`; `c:num->real`]) THEN
  REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
  MAP_EVERY X_GEN_TAC [`a:num->real`; `n:num`] THEN
  DISCH_THEN(ASSUME_TAC o GSYM) THEN
  ASM_REWRITE_TAC[real_pow; GSYM REAL_MUL_ASSOC] THEN
  EXISTS_TAC `\i. (if 0 < i then a(i - 1) else &0) -
                  (if i <= n then r * a i else &0)` THEN
  EXISTS_TAC `n + 1` THEN
  REWRITE_TAC[REAL_SUB_RDISTRIB; SUM_SUB_NUMSEG] THEN X_GEN_TAC `x:real` THEN
  BINOP_TAC THENL
   [MP_TAC(ARITH_RULE `0 <= n + 1`) THEN SIMP_TAC[SUM_CLAUSES_LEFT] THEN
    DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[SUM_OFFSET; LT_REFL] THEN
    REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_LID; ARITH_RULE `0 < i + 1`] THEN
    REWRITE_TAC[GSYM SUM_LMUL; ADD_SUB; REAL_POW_ADD; REAL_POW_1];
    SIMP_TAC[SUM_CLAUSES_RIGHT; LE_0; ARITH_RULE `0 < n + 1`] THEN
    REWRITE_TAC[ADD_SUB; ARITH_RULE `~(n + 1 <= n)`] THEN
    SIMP_TAC[REAL_MUL_LZERO; REAL_ADD_RID; GSYM SUM_LMUL]] THEN
  MATCH_MP_TAC SUM_EQ_NUMSEG THEN REWRITE_TAC[REAL_MUL_AC]);;

(* ------------------------------------------------------------------------- *)
(* The main lemmas to be applied iteratively.                                *)
(* ------------------------------------------------------------------------- *)

let VARIATION_POSITIVE_ROOT_FACTOR = prove
 (`!a n r.
    ~(a n = &0) /\ &0 < r /\ sum(0..n) (\i. a i * r pow i) = &0
    ==> ?b. ~(b(n - 1) = &0) /\
            (!x. sum(0..n) (\i. a i * x pow i) =
                 (x - r) * sum(0..n-1) (\i. b i * x pow i)) /\
            ?d. ODD d /\ variation(0..n) a = variation(0..n-1) b + d`,
  REPEAT GEN_TAC THEN ASM_CASES_TAC `n = 0` THENL
   [ASM_SIMP_TAC[SUM_CLAUSES_NUMSEG; real_pow; REAL_MUL_RID] THEN MESON_TAC[];
    STRIP_TAC] THEN
  ABBREV_TAC `b = \j. sum (j + 1..n) (\i. a i * r pow (i - j - 1))` THEN
  EXISTS_TAC `b:num->real` THEN REPEAT CONJ_TAC THENL
   [EXPAND_TAC "b" THEN REWRITE_TAC[] THEN ASM_SIMP_TAC[SUB_ADD; LE_1] THEN
    ASM_SIMP_TAC[SUM_SING_NUMSEG; ARITH_RULE `n - (n - 1) - 1 = 0`] THEN
    ASM_REWRITE_TAC[real_pow; REAL_MUL_RID];
    MP_TAC(GEN `x:real` (SPECL [`a:num->real`; `x:real`; `r:real`; `n:num`]
        REAL_SUB_POLYFUN)) THEN
    ASM_SIMP_TAC[LE_1; REAL_SUB_RZERO] THEN DISCH_THEN(K ALL_TAC) THEN
    EXPAND_TAC "b" THEN REWRITE_TAC[];
    ALL_TAC] THEN
  SUBGOAL_THEN `(b:num->real) n = &0` ASSUME_TAC THENL
   [EXPAND_TAC "b" THEN REWRITE_TAC[] THEN MATCH_MP_TAC SUM_EQ_0_NUMSEG THEN
    ARITH_TAC;
    ALL_TAC] THEN
  MP_TAC(ISPECL
   [`n:num`; `\i. if i <= n then a i * (r:real) pow i else &0`;
    `\i. if i <= n then --b i * (r:real) pow (i + 1) else &0`]
   ARTHAN_LEMMA) THEN
  ASM_SIMP_TAC[REAL_ENTIRE; REAL_POW_EQ_0; REAL_LT_IMP_NZ; REAL_NEG_0;
               LE_REFL] THEN
  ANTS_TAC THENL
   [X_GEN_TAC `j:num` THEN EXPAND_TAC "b" THEN REWRITE_TAC[] THEN
    ASM_CASES_TAC `j:num <= n` THEN ASM_REWRITE_TAC[] THENL
     [SUBGOAL_THEN `!i:num. i <= j ==> i <= n` MP_TAC THENL
       [ASM_ARITH_TAC; SIMP_TAC[] THEN DISCH_THEN(K ALL_TAC)] THEN
      REWRITE_TAC[REAL_ARITH `a:real = --b * c <=> a + b * c = &0`] THEN
      REWRITE_TAC[GSYM SUM_RMUL; GSYM REAL_POW_ADD; GSYM REAL_MUL_ASSOC] THEN
      SIMP_TAC[ARITH_RULE `j + 1 <= k ==> k - j - 1 + j + 1 = k`] THEN
      ASM_SIMP_TAC[SUM_COMBINE_R; LE_0];
      REWRITE_TAC[GSYM SUM_RESTRICT_SET; IN_NUMSEG] THEN
      ASM_SIMP_TAC[ARITH_RULE
      `~(j <= n) ==> ((0 <= i /\ i <= j) /\ i <= n <=> 0 <= i /\ i <= n)`] THEN
      ASM_REWRITE_TAC[GSYM numseg]];
    MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d:num` THEN
    MATCH_MP_TAC MONO_AND THEN REWRITE_TAC[] THEN MATCH_MP_TAC(ARITH_RULE
     `x':num = x /\ y' = y ==> x' = y' + d ==> x = y + d`) THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC EQ_TRANS THEN
      EXISTS_TAC `variation(0..n) (\i. a i * r pow i)` THEN CONJ_TAC THENL
       [MATCH_MP_TAC VARIATION_EQ THEN SIMP_TAC[IN_NUMSEG];
        ALL_TAC];
      MATCH_MP_TAC EQ_TRANS THEN
      EXISTS_TAC `variation(0..n) (\i. --b i * r pow (i + 1))` THEN
      CONJ_TAC THENL
       [MATCH_MP_TAC VARIATION_EQ THEN SIMP_TAC[IN_NUMSEG];
        ALL_TAC] THEN
      MATCH_MP_TAC EQ_TRANS THEN
      EXISTS_TAC `variation(0..n-1) (\i. --b i * r pow (i + 1))` THEN
      CONJ_TAC THENL
       [MATCH_MP_TAC VARIATION_SUBSET THEN
        REWRITE_TAC[SUBSET_NUMSEG; IN_DIFF; IN_NUMSEG] THEN
        CONJ_TAC THENL [ARITH_TAC; X_GEN_TAC `i:num` THEN STRIP_TAC] THEN
        SUBGOAL_THEN `i:num = n` SUBST_ALL_TAC THENL
         [ASM_ARITH_TAC; ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC];
        ALL_TAC]] THEN
    REWRITE_TAC[variation] THEN
    ONCE_REWRITE_TAC[REAL_ARITH
      `(a * x) * (b * x'):real = (x * x') * a * b`] THEN
    SIMP_TAC[NOT_IMP; GSYM CONJ_ASSOC; GSYM REAL_POW_ADD;
             REAL_ARITH `--x * --y:real = x * y`] THEN
    ONCE_REWRITE_TAC[REAL_ARITH `x * y < &0 <=> &0 < x * --y`] THEN
    ASM_SIMP_TAC[REAL_LT_MUL_EQ; REAL_POW_LT] THEN
    ASM_SIMP_TAC[REAL_MUL_RNEG; REAL_ENTIRE; REAL_NEG_EQ_0; REAL_POW_EQ_0] THEN
    ASM_SIMP_TAC[REAL_LT_IMP_NZ]]);;

let VARIATION_POSITIVE_ROOT_MULTIPLE_FACTOR = prove
 (`!r n a.
    ~(a n = &0) /\ &0 < r /\ sum(0..n) (\i. a i * r pow i) = &0
    ==> ?b k m. 0 < k /\ m < n /\ ~(b m = &0) /\
                (!x. sum(0..n) (\i. a i * x pow i) =
                     (x - r) pow k * sum(0..m) (\i. b i * x pow i)) /\
                ~(sum(0..m) (\j. b j * r pow j) = &0) /\
                ?d. EVEN d /\ variation(0..n) a = variation(0..m) b + k + d`,
  GEN_TAC THEN MATCH_MP_TAC num_WF THEN
  X_GEN_TAC `n:num` THEN DISCH_TAC THEN X_GEN_TAC `a:num->real` THEN
  ASM_CASES_TAC `n = 0` THENL
   [ASM_SIMP_TAC[SUM_CLAUSES_NUMSEG; real_pow; REAL_MUL_RID] THEN MESON_TAC[];
    STRIP_TAC] THEN
  MP_TAC(ISPECL [`a:num->real`; `n:num`; `r:real`]
        VARIATION_POSITIVE_ROOT_FACTOR) THEN
  ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `c:num->real` MP_TAC) THEN
  REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
  DISCH_THEN(X_CHOOSE_THEN `d:num` STRIP_ASSUME_TAC) THEN
  ASM_CASES_TAC `sum(0..n-1) (\i. c i * r pow i) = &0` THENL
   [FIRST_X_ASSUM(MP_TAC o SPEC `n - 1`) THEN
    ANTS_TAC THENL [ASM_ARITH_TAC; DISCH_THEN(MP_TAC o SPEC `c:num->real`)] THEN
    ASM_REWRITE_TAC[] THEN
    MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `b:num->real` THEN
    ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
    MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `m:num` THEN
    DISCH_THEN(X_CHOOSE_THEN `k:num` MP_TAC) THEN
    REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
    DISCH_THEN(X_CHOOSE_THEN `e:num` STRIP_ASSUME_TAC) THEN
    EXISTS_TAC `SUC k` THEN ASM_REWRITE_TAC[real_pow; REAL_MUL_ASSOC] THEN
    REPEAT(CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC]) THEN
    REWRITE_TAC[ADD1; ADD_ASSOC] THEN EXISTS_TAC `d - 1 + e`;
    MAP_EVERY EXISTS_TAC [`c:num->real`; `1`; `n - 1`] THEN
    ASM_REWRITE_TAC[REAL_POW_1] THEN
    REPEAT(CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC]) THEN
    EXISTS_TAC `d - 1`] THEN
  UNDISCH_TAC `ODD d` THEN GEN_REWRITE_TAC LAND_CONV [ODD_EXISTS] THEN
  DISCH_THEN(X_CHOOSE_THEN `p:num` SUBST1_TAC) THEN
  ASM_REWRITE_TAC[SUC_SUB1; EVEN_ADD; EVEN_MULT; ARITH] THEN ARITH_TAC);;

let VARIATION_POSITIVE_ROOT_MULTIPLICITY_FACTOR = prove
 (`!r n a.
    ~(a n = &0) /\ &0 < r /\ sum(0..n) (\i. a i * r pow i) = &0
    ==> ?b m. m < n /\ ~(b m = &0) /\
              (!x. sum(0..n) (\i. a i * x pow i) =
                   (x - r) pow
                   (multiplicity (\x. sum(0..n) (\i. a i * x pow i)) r) *
                   sum(0..m) (\i. b i * x pow i)) /\
              ~(sum(0..m) (\j. b j * r pow j) = &0) /\
              ?d. EVEN d /\
                  variation(0..n) a = variation(0..m) b +
                     multiplicity (\x. sum(0..n) (\i. a i * x pow i)) r + d`,
  REPEAT GEN_TAC THEN
  DISCH_THEN(MP_TAC o MATCH_MP VARIATION_POSITIVE_ROOT_MULTIPLE_FACTOR) THEN
  MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `b:num->real` THEN
  DISCH_THEN(X_CHOOSE_THEN `k:num` MP_TAC) THEN
  MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `m:num` THEN
  DISCH_TAC THEN
  SUBGOAL_THEN `multiplicity (\x. sum(0..n) (\i. a i * x pow i)) r = k`
   (fun th -> ASM_REWRITE_TAC[th]) THEN
  CONV_TAC SYM_CONV THEN MATCH_MP_TAC MULTIPLICITY_UNIQUE THEN
  MAP_EVERY EXISTS_TAC [`b:num->real`; `m:num`] THEN ASM_REWRITE_TAC[]);;

(* ------------------------------------------------------------------------- *)
(* Hence the main theorem.                                                   *)
(* ------------------------------------------------------------------------- *)

let DESCARTES_RULE_OF_SIGNS = prove
 (`!f a n. f = (\x. sum(0..n) (\i. a i * x pow i)) /\
           (?i. i IN 0..n /\ ~(a i = &0))
           ==> ?d. EVEN d /\
                   variation(0..n) a =
                   nsum {r | &0 < r /\ f(r) = &0} (\r. multiplicity f r) + d`,
  REPEAT GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
  DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN
  MAP_EVERY (fun t -> SPEC_TAC(t,t)) [`a:num->real`; `n:num`] THEN
  MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
  X_GEN_TAC `a:num->real` THEN ASM_CASES_TAC `(a:num->real) n = &0` THENL
   [ASM_CASES_TAC `n = 0` THEN
    ASM_REWRITE_TAC[NUMSEG_SING; IN_SING; UNWIND_THM2]
    THENL [ASM_MESON_TAC[]; DISCH_TAC] THEN
    FIRST_X_ASSUM(MP_TAC o SPEC `n - 1`) THEN ANTS_TAC THENL
     [ASM_ARITH_TAC; DISCH_THEN(MP_TAC o SPEC `a:num->real`)] THEN
    ANTS_TAC THENL
     [ASM_MESON_TAC[IN_NUMSEG; ARITH_RULE `i <= n ==> i <= n - 1 \/ i = n`];
      MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d:num` THEN
      ASM_SIMP_TAC[LE_0; LE_1; SUM_CLAUSES_RIGHT] THEN
      REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_RID] THEN
      DISCH_THEN(SUBST1_TAC o SYM o CONJUNCT2) THEN
      MATCH_MP_TAC VARIATION_SUBSET THEN
      REWRITE_TAC[SUBSET_NUMSEG; IN_DIFF; IN_NUMSEG] THEN
      CONJ_TAC THENL [ASM_ARITH_TAC; X_GEN_TAC `i:num` THEN STRIP_TAC] THEN
      SUBGOAL_THEN `i:num = n` (fun th -> ASM_REWRITE_TAC[th]) THEN
      ASM_ARITH_TAC];
    DISCH_THEN(K ALL_TAC)] THEN
  ASM_CASES_TAC `{r | &0 < r /\ sum(0..n) (\i. a i * r pow i) = &0} = {}` THENL
   [ASM_REWRITE_TAC[NSUM_CLAUSES; ADD_CLAUSES] THEN
    ONCE_REWRITE_TAC[CONJ_SYM] THEN REWRITE_TAC[UNWIND_THM1] THEN
    ONCE_REWRITE_TAC[GSYM NOT_ODD] THEN
    DISCH_THEN(MP_TAC o MATCH_MP ODD_VARIATION_POSITIVE_ROOT) THEN
    ASM SET_TAC[];
    ALL_TAC] THEN
  FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
  REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
  X_GEN_TAC `r:real` THEN STRIP_TAC THEN
  MP_TAC(ISPECL [`r:real`; `n:num`; `a:num->real`]
    VARIATION_POSITIVE_ROOT_MULTIPLICITY_FACTOR) THEN
  ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
  MAP_EVERY X_GEN_TAC [`b:num->real`; `m:num`] THEN
  DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `m:num`) THEN
  ANTS_TAC THENL [ASM_REWRITE_TAC[]; ALL_TAC] THEN
  DISCH_THEN(MP_TAC o SPEC `b:num->real`) THEN ANTS_TAC THENL
   [EXISTS_TAC `m:num` THEN ASM_REWRITE_TAC[IN_NUMSEG; LE_REFL; LE_0];
    ALL_TAC] THEN
  DISCH_THEN(X_CHOOSE_THEN `d1:num`
    (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN
  FIRST_X_ASSUM(X_CHOOSE_THEN `d2:num`
    (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN
  EXISTS_TAC `d1 + d2:num` THEN
  CONJ_TAC THENL [ASM_REWRITE_TAC[EVEN_ADD]; ALL_TAC] THEN
  MATCH_MP_TAC(ARITH_RULE
   `x + y = z ==> (x + d1) + (y + d2):num = z + d1 + d2`) THEN
  SUBGOAL_THEN
   `{r | &0 < r /\ sum(0..n) (\i. a i * r pow i) = &0} =
    r INSERT {r | &0 < r /\ sum(0..m) (\i. b i * r pow i) = &0}`
  SUBST1_TAC THENL
   [MATCH_MP_TAC(SET_RULE `x IN s /\ s DELETE x = t ==> s = x INSERT t`) THEN
    CONJ_TAC THENL
     [REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[];
      ONCE_ASM_REWRITE_TAC[] THEN
      REWRITE_TAC[REAL_ENTIRE; REAL_POW_EQ_0; REAL_SUB_0] THEN
      REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_DELETE] THEN
      X_GEN_TAC `s:real` THEN
      FIRST_X_ASSUM(K ALL_TAC o SPEC_VAR) THEN
      ASM_CASES_TAC `s:real = r` THEN ASM_REWRITE_TAC[]];
    ALL_TAC] THEN
  SUBGOAL_THEN
   `FINITE {r | &0 < r /\ sum(0..m) (\i. b i * r pow i) = &0}`
  MP_TAC THENL
   [MATCH_MP_TAC FINITE_SUBSET THEN
    EXISTS_TAC `{r | sum(0..m) (\i. b i * r pow i) = &0}` THEN
    SIMP_TAC[SUBSET; IN_ELIM_THM; REAL_POLYFUN_FINITE_ROOTS] THEN
    EXISTS_TAC `m:num` THEN ASM_REWRITE_TAC[IN_NUMSEG; LE_0; LE_REFL];
    SIMP_TAC[NSUM_CLAUSES; IN_ELIM_THM] THEN DISCH_TAC] THEN
  FIRST_X_ASSUM(ASSUME_TAC o GEN_REWRITE_RULE I [GSYM FUN_EQ_THM]) THEN
  ASM_REWRITE_TAC[] THEN
  MATCH_MP_TAC(ARITH_RULE `s1:num = s2 ==> s1 + m = m + s2`) THEN
  MATCH_MP_TAC NSUM_EQ THEN
  X_GEN_TAC `s:real` THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
  FIRST_X_ASSUM(fun t -> GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [t]) THEN
  CONV_TAC SYM_CONV THEN MATCH_MP_TAC MULTIPLICITY_OTHER_ROOT THEN
  REWRITE_TAC[MESON[] `(?i. P i /\ Q i) <=> ~(!i. P i ==> ~Q i)`] THEN
  REPEAT STRIP_TAC THEN
  UNDISCH_TAC `~(sum (0..m) (\j. b j * r pow j) = &0)` THEN ASM_SIMP_TAC[] THEN
  REWRITE_TAC[REAL_MUL_LZERO; SUM_0]);;

subset_name: curated


TITLE: The conditional expectation $E(f(X) \mid \min(X,t))$ if $X \sim Exp(\lambda)$
QUESTION [0 upvotes]: Let $X \sim Exp(\lambda)$, $t \ge 0$ and $Y_t := \min(X,t)$. Let further be $f$ some measurable function with $\mathbb{E}(\lvert f(X) \rvert) < \infty$. Does it hold that:
$$\mathbb{E}(f(X) \mid Y_t) = f(Y_t)I_{[0,t)}(Y_t) + \mathbb{E}_{\{Y_t = t\}}(f(X))I_{\{t\}}(Y_t) \quad?$$

I recognise that the intent here is to split up according to cases:

The left summand covers the case that $X<t$, but I do not understand why there is $f(Y_t)$ instead of $\mathbb{E}(f(Y_t))$.
The right summand covers the case that $X \ge t$.

So all in all I get the feeling that this identity is true, however, I can not quite see how to argue that the left summand is correct.
For context; here is the definition of conditional expectation from my lecture:

Let $(\Omega, \mathcal{A}, \mathbb{P})$ be a probability space and let $X$ be a real RV with $E(\lvert X \rvert) < \infty$. $\mathbb{E}(X \mid \mathcal{F})$ is uniquely defined as a RV via the conditions

$\mathbb{E}(X \mid \mathcal{F})$ is $\mathcal{F}$ measurable,

$\mathbb{E}(X \mid \mathcal{F}) \in L^1(\mathbb{P})$

$\int_A \mathbb{E}(X \mid \mathcal{F}) d \mathbb{P} = \int_A X d \mathbb{P}$ for all $A \in \mathcal{F}$.

REPLY [1 votes]: Note that $f(X)=f(X)\mathbf{1}_{\{X<t\}}+f(X)\mathbf{1}_{\{X\geqslant t\}}$ and
$$
\operatorname{E}[f(X)\mathbf{1}_{\{X<t\}}|Y_t]=f(X)\mathbf{1}_{\{X<t\}}
$$
as $f(X)\mathbf{1}_{\{X<t\}}=f(Y_t)\mathbf{1}_{\{Y_t<t\}}$ is $\sigma (Y_t)$ measurable. By the other hand, for every Borel set $A\subset \mathbb{R}$ set $A_{\geqslant t}:=A\cap [t,\infty )$ and note that
$$
\{Y_t\in A_{\geqslant t}\}=\{Y_t\in A\}\cap \{Y_t=t\}=\{Y_t\in A\}\cap \{X\geqslant t\}
$$
Then for any chosen Borel set $A$ we find that
$$
\begin{align*}
\int_{\{Y_t\in A\}}\operatorname{E}[f(X)\mathbf{1}_{\{X\geqslant t\}}|Y_t]\,d P&=\int_{\{Y_t\in A\}}\mathbf{1}_{\{X\geqslant t\}}\operatorname{E}[f(X)|Y_t]\,d P\\
&=\int_{\{Y_t\in A_{\geqslant t}\}}\operatorname{E}[f(X)|Y_t]\,d P\\
&=\int_{\{Y_t\in A_{\geqslant t}\}}f(X)\,d P
\end{align*}
$$
as the function $\mathbf{1}_{\{X\geqslant t\}}=\mathbf{1}_{\{Y_t=t\}}$ is $\sigma (Y_t)$-measurable and $\{Y_t\in A_{\geqslant t}\}\in \sigma (Y_t)$. Finally note that
$$
\{Y_t\in A_{\geqslant t}\}=\begin{cases}
\{X\geqslant t\},&\text{ when }t\in A\\
\emptyset ,&\text{ otherwise }
\end{cases}
$$
Therefore
$$
\operatorname{E}[f(X)\mathbf{1}_{\{X\geqslant t\}}|Y_t]=\mathbf{1}_{\{Y_t=t\}}\operatorname{E}[f(X)|X\geqslant t]
$$
∎


TITLE: Relative interior of a set is the interior of a set and the relation with hyperplane
QUESTION [3 upvotes]: My question comes from the famous book: convex analysis, Rockafellar Ch. 13 p.113

Note:

$\delta^*(x^* \mid C) = \operatorname{sup}\{\langle x,x^*\rangle \mid x\in C\}$: a support function of a convex set $C$.

My question is how to explain the part underscored by red line?    Why it is the case?   I am also confused about the case where ri$(C)$ = int$(C)$ and the relation between hyperplane.

I know the concept of relative interior; however, I still cannot understand what the author was trying to say.

REPLY [2 votes]: A hyperplane contained in a Euclidean space $\mathbb{E}$ is an affine set of dimension $\text{dim}(\mathbb{E})-1$. If a set $C$ is not contained in any hyperplane, it means that $\text{dim}(C)=\text{dim}(\mathbb{E})$, in which case $\text{aff}(C)=\mathbb{E}$. In this context the definitions of interior and relative interior just match.


TITLE: What is the Mobius sum $\sum_{n=1}^\infty \frac{(-1)^{n+1}|\mu(n)|}{n^s}$?
QUESTION [5 upvotes]: It can be observed that,
$$A(s) := \sum_{n=1}^\infty \frac{\mu(n)}{n^s} = \frac{1}{\zeta(s)}$$
$$B(s) := \sum_{n=1}^\infty \frac{|\mu(n)|}{n^s} = \frac{\zeta(s)}{\zeta(2s)}$$
$$C(s) := \sum_{n=1}^\infty \frac{(-1)^{n+1}\mu(n)}{n^s} = \frac{2^s+1}{2^s-1}\frac{1}{\zeta(s)}$$

Q: Is it true that,

$$D(s) := \sum_{n=1}^\infty \frac{(-1)^{n+1}|\mu(n)|}{n^s} = \frac{2^s-1}{2^s+1}\frac{\zeta(s)}{\zeta(2s)}$$
hence,
$$A(s)\,B(s) = C(s)\,D(s) = \frac{1}{\zeta(2s)}?$$

REPLY [5 votes]: Yes, it is true.  Let $\mathbb{P}$ be the set of all positive primes.  For $T\subseteq\mathbb{P}$, write $\prod(T)$ for the product of elements in $T$.  Let $s\in\mathbb{C}$ with $\text{Re}(s)>1$.  We have
$$D(s)=\sum_{T\subseteq \mathbb{P}}\,\frac{(-1)^{\prod(T)+1}}{\big(\prod(T)\big)^s}=\sum_{T\subseteq \mathbb{P}\setminus\{2\}}\left(\frac{1}{\big(\prod(T)\big)^s}-\frac{1}{\big(2\,\prod(T)\big)^s}\right)\,.$$
Hence,
$$D(s)=\left(1-\frac{1}{2^s}\right)\,\sum_{T\subseteq \mathbb{P}\setminus\{2\}}\,\frac{1}{\big(\prod(T)\big)^s}=\frac{2^s-1}{2^s+1}\,\sum_{T\subseteq \mathbb{P}\setminus\{2\}}\left(\frac{1}{\big(\prod(T)\big)^s}+\frac{1}{\big(2\,\prod(T)\big)^s}\right)\,.$$
Therefore,
$$D(s)=\frac{2^s-1}{2^s+1}\,\sum_{T\subseteq \mathbb{P}}\,\frac{1}{\big(\prod(T)\big)^s}=\frac{2^s-1}{2^s+1}\,B(s)\,.$$


TITLE: Global Error Bound for Implicit Euler
QUESTION [3 upvotes]: I'm trying to derive an error bound for the approximate solution obtained with Backward Euler to the IVP
$$\frac{dy}{dt} = f(y), \hspace{.75cm} y(0) = y_0,$$
where $f \in C^2(\mathbb{R})$ with global Lipschitz constant $K$, and $t \in [0,T]$. I know that the local truncation error at each time step $\tau_n$ is bounded by $\frac{M h^2 }{2} $, where $$M = \sup_{t \in [0,T]} \left\{ f(y(t))f'(y(t)) \right\}.$$ Letting $e_n = y(t_n) - y_n$, we have that \begin{align*}
\frac{Mh^2}{2} &\geq \left|{\tau_n} \right| \\
&= \left| y(t_n) - y(t_{n-1}) - hf(y(t_n)) \right| \\
&= \left| y(t_n) - y(t_{n-1}) - hf(y(t_n)) - (y_n - y_{n-1} - hf_n) \right| \\
&= \left| e_{n}-e_{n-1} - h(f(y(t_n))-f_n) \right| \\
& \geq \left| e_n \right| - \left| e_{n-1} \right| - hK \left| e_n \right|   ,
\end{align*}
which implies that $$\left| e_n \right| \leq \frac{\left| e_{n-1} \right| + \frac{Mh^2}{2}}{1- hK}   $$
Continuing recursively, we find that \begin{align*} \left| e_n \right| &\leq \frac{Mh^2}{2(1 - hK)^n} \sum_{j = 0}^{n-1} (1- hK)^j \\
&\leq \frac{Mh^2}{2(1 - hK)^n} \frac{1}{1-(1-hK)} \\
&= \frac{Mh}{2K(1-hK)^n} \\
&= \frac{Mh}{2K(1-hK)^{t_n/h}} \\
&\leq \frac{Mh}{2K(1-hK)^{T/h}}
\end{align*}
Using L'hopital's rule, we find that $$\lim_{h \to 0} (1-hk)^{-T/h} =e^{TK},$$
which implies that $$ (1-hk)^{-T/h} = e^{TK} + O(h). $$
Therefore, $$\left| e_n \right| \leq \frac{Mhe^{TK}}{2K} + O(h^2). $$
Is this bound reasonable? If so, is there a way to make this bound tighter? Thanks in advance!

REPLY [2 votes]: This looks as tight as possible in this generality. You could use the estimate
$$
(1-x)^{-1}=\exp(-\ln(1-x))=\exp(x+\tfrac12x^2+\tfrac13x^3+...)\le\exp(x+x^2)
$$
for $0\le x\le\frac12$ to get an explicit bound in the last formula instead of the general $O(h^2)$ class.


TITLE: abstract Algebra (group theory)
QUESTION [2 upvotes]: Three coins are placed on a table; showing heads. Can you get all the coins to show tails, by turning over two coins at a time? Use Group Theory to prove your answer.
I know that the answer is no I cannot get all coins to show tails however I  have no idea how to put it in terms of group theory. Any help would be appreciated.

REPLY [2 votes]: You insist on using group theory to hide the parity check, so here it is.
In group-theoretic terms the situation is as follows: we have the group $G={\bf Z}_2^3$, and the subgroup $\langle(1,1,0),(1,0,1),(0,1,1)\rangle=H\leq G$, and we ask if $(1,1,1)\in H$.
The answer is no: consider the homomorphism $f\colon G\to {\bf Z}_2$ defined by $f(a,b,c)=a+b+c$. Clearly $H$ is contained in the kernel, while $(1,1,1)$ isn't, so $(1,1,1)\notin H$.
Alternately, you could just compose the generators of $H$ in all possible ways to see that actually $H=\{(0,0,0),(1,1,0),(1,0,1),(0,1,1)\}$, though this method doesn't generalise to a larger number of coins quite so well.


TITLE: Is there another method besides the minimum modulus theorem than can help me solve this problem?
QUESTION [1 upvotes]: The question is, find the minimum of $|exp(z^2)|$ for those z with $|z|\leq 1$. Im aware the modulus theorem would solve this, but we haven't gotten there yet. The section of the book this question is on is differentiation of elementary complex functions. Don't solve for me, just hints please

REPLY [0 votes]: The function $g(z):=z^2$ assumes the same values in $\bar D$ as does $f(z)=z$. Now $\bigl|e^z\bigr|=e^x\geq{1\over e}$ in $\bar D$, and the minimal value is taken at $z=-1$. In the original problem we therefore should choose $z$ such that $z^2=-1$, which is $z=\pm i$.


TITLE: Determine all $ α \in \mathbb{R} $ for which every solution of $ y'' − (2 α − 1) y' + α (α − 1) y = 0 $ tends to $ 0 $ as $ t \to \infty $.
QUESTION [0 upvotes]: Problem. Determine all values of $ \alpha \in \mathbb{R} $ for which every
    solution of
    $$
  y'' − (2 \alpha − 1) y' + \alpha (\alpha − 1) y = 0
  $$
    tends to $ 0 $ as $ t \to \infty $.

REPLY [0 votes]: To solve:
$$\text{y}''\left(t\right)−\left(2\cdot\alpha−1\right)\cdot\text{y}'\left(t\right)+\alpha\cdot\left(\alpha−1\right)\cdot\text{y}\left(t\right)=0$$
Use Laplace transform:
$$\mathcal{L}_t\left[\text{y}''\left(t\right)\right]_{\left(\text{s}\right)}−\mathcal{L}_t\left[\left(2\cdot\alpha−1\right)\cdot\text{y}'\left(t\right)\right]_{\left(\text{s}\right)}+\mathcal{L}_t\left[\alpha\cdot\left(\alpha−1\right)\cdot\text{y}\left(t\right)\right]_{\left(\text{s}\right)}=\mathcal{L}_t\left[0\right]_{\left(\text{s}\right)}$$
Now, use:

$$\mathcal{L}_t\left[\text{y}''\left(t\right)\right]_{\left(\text{s}\right)}=\text{s}^2\cdot\text{Y}\left(\text{s}\right)-\text{s}\cdot\text{y}\left(0\right)-\text{y}'\left(0\right)$$
$$\mathcal{L}_t\left[\left(2\cdot\alpha−1\right)\cdot\text{y}'\left(t\right)\right]_{\left(\text{s}\right)}=\left(2\cdot\alpha−1\right)\cdot\mathcal{L}_t\left[\text{y}'\left(t\right)\right]_{\left(\text{s}\right)}=\left(2\cdot\alpha−1\right)\cdot\left(\text{s}\cdot\text{Y}\left(\text{s}\right)-\text{y}\left(0\right)\right)$$
$$\mathcal{L}_t\left[\alpha\cdot\left(\alpha−1\right)\cdot\text{y}\left(t\right)\right]_{\left(\text{s}\right)}=\alpha\cdot\left(\alpha−1\right)\cdot\mathcal{L}_t\left[\text{y}\left(t\right)\right]_{\left(\text{s}\right)}=\alpha\cdot\left(\alpha−1\right)\cdot\text{Y}\left(\text{s}\right)$$
$$\mathcal{L}_t\left[0\right]_{\left(\text{s}\right)}=0$$

So, we get:
$$\text{s}^2\cdot\text{Y}\left(\text{s}\right)-\text{s}\cdot\text{y}\left(0\right)-\text{y}'\left(0\right)-\left(2\cdot\alpha−1\right)\cdot\left(\text{s}\cdot\text{Y}\left(\text{s}\right)-\text{y}\left(0\right)\right)+\alpha\cdot\left(\alpha−1\right)\cdot\text{Y}\left(\text{s}\right)=0$$
Solving $\text{Y}\left(\text{s}\right)$:
$$\text{Y}\left(\text{s}\right)=\frac{\text{y}'\left(0\right)+\text{y}\left(0\right)\cdot\left(1-2\cdot\alpha+\text{s}\right)}{\left(\alpha-\text{s}\right)\cdot\left(\alpha-1-\text{s}\right)}$$
Using inverse Laplace transform, gives us:
$$\text{y}\left(t\right)=e^{t\cdot\left(\alpha-1\right)}\cdot\left(e^t\cdot\left(\text{y}\left(0\right)+\text{y}'\left(0\right)\right)-\alpha\cdot\text{y}\left(0\right)\cdot\left(e^t-1\right)-\text{y}'\left(0\right)\right)$$


TITLE: Number of ways to split plane
QUESTION [0 upvotes]: Suppose we have $2 \leq n \leq 300$ points $p_i$ with coordinates $(x_i, y_i), \ x_i, y_i \in \mathbb{Z}$. Among all partitions of the set into two nonvoid subsets, how many are induced by a partition by a straight line splitting the plane into 2 halfplanes. We're allowed to  use some programming.
I've spent hours to do it, but i got nothing.

REPLY [1 votes]: In this answer, we'll assume that the points are in general position, i.e., that no three points line on the same line.  See the end for the changes when the points are not in general position.  With this assumption, then the number of ways to split a collection of points is independent of the arrangement of points.
We will also assume that all points have distinct $x$ and $y$ coordinates.  This is not a restrictive extra condition since a small rotation will result in this case without changing the relative position of lines and points.
To answer this question, I'll use point-line duality.  The duality transformation takes lines to points and points to lines:

The point $p=(p_x,p_y)$ to the line $y=p_xx-p_y$.  The corresponding line is called a dual point and is denoted $p^\ast$.
The line $y=mx+b$ to the point $(m,-b)$.  The corresponding point is called a dual line and if the original line is $\ell$, then the dual line is denoted $\ell^\ast$.

One can easily check that these operations are inverses of each other.  There are many nice properties of the dual, but the one that we need here is that if $\ell$ is a line and $\{p_1,\dots,p_k\}$ are points below $\ell$, then $\ell^\ast$ is a point and each of the lines $\{p_1^\ast,\dots,p_k^\ast\}$ are above $\ell^\ast$.
In your case, if you take each of your points $\{p_1,\dots,p_n\}$ and look at the dual points (i.e., lines) $\{p_1^\ast,\dots,p_n^\ast\}$, these lines divide up the plane into regions.  Note that:

The general position assumption implies that now three dual points have a common intersection.
The assumption that all points have distinct $x$ coordinates implies that the slops of the dual points are all different.

Let $q^\ast$ be a point in a region determined by the dual points, i.e., in their complement.  Then the points above the corresponding line $q$ in the primal (i.e., the original plane) correspond to the lines below $q^\ast$ in the dual.  Since this doesn't change in a region (i.e., connected component) determined by the dual points,
There is a bijection between connected regions in the dual and equivalence classes of lines with the same subsets of points below the line.
The next step is to count the number of regions formed by the dual points.  We can do this using the Euler characteristic of a sphere.  By putting a point at infinity, we can embed these dual points (lines) as great circles, which all intersect at infinity.  For the Euler characteristic for a sphere, we know that $$\#V-\#E+\#F=2.$$  Since the lines all have distinct slopes, they all intersect, resulting in
$$
\#V=\binom{n}{2}+1.
$$
The $+1$ comes from the point at infinity.  Since every line intersects every other line (and all $n-1$ lines intersect any fixed line), there are $n$ edges per line, resulting in
$$
\#E=n^2.
$$
Putting this all together, we have
$$
2=\binom{n}{2}+1-n^2+\#F
$$
or that the number of regions is
$$
\#F=1+n^2-\frac{n^2-n}{2}=1+\frac{n^2}{2}+\frac{n}{2}.
$$
Now, this does not quite answer your question because unbounded regions over-count some of the partitions (more details are below).  In fact, $n$ of the partitions are over-counted.  Therefore, we need to subtract $n$ from our count to get that the number of ways to split the data set into two subsets by lines (but allowing for an empty set) is
$$
1+\frac{n^2}{2}+\frac{n}{2}-n=1+\binom{n}{2}.
$$
Finally, we need to subtract the split of the entire set and the empty set, to get that the number of partitions is always
$$
\binom{n}{2}.
$$
Now, let's take a look this over-counting business.  The over-counting comes about because there are times when there are pairs of lines $\{\ell_1,\ell_2\}$ that are nearly vertical and the set of points below $\ell_1$ is equal to the set of points above $\ell_2$.  These over-counts correspond to the unbounded regions in the dual setting.  Alternatively, these correspond to vertical lines between points of the original data set (including the vertical line to the far right of the data set, which is identified with the vertical line to the far left of the data set).  There are $n$ such lines, so there are $2n$ unbounded regions which are identified in pairs.
Note that if the points are not in general position, then the number of vertices in the dual can change.  In particular, suppose that there are lines $\ell_1,\dots,\ell_k$ so that line $\ell_i$ has $n_i\geq 3$ points on it.  In this case, the dual points on this line don't have $\binom{n_i}{2}$ different intersection points, they have all been combined into into a single point.  Then, the number of points counted above must be reduced by $$
\sum_{i=1}^k\left(\binom{n_i}{2}-1\right)=-k+\sum_{i=1}^k\binom{n_i}{2}.
$$
Then, the rest of the argument proceeds as above (including the over-count).


TITLE: Helping provide intuition and clarity as to what exactly an "open set" is.
QUESTION [0 upvotes]: I have read What does "open set" mean in the concept of a topology? and studied the open set wiki, as well as reading through the open set definition of a topological space, but yet I am still not crystal clear on what exactly an open set actually is (and this concept of "open set" is required to be understood in order to dig into many areas of topology and elsewhere, so I am stuck currently, trying to resolve what open set actually means).
First, as one of the other answerer's in the first link points out:

In an abstract topological space, "open set" has no definition!

Which I think Wikipedia confirms, by saying:

A topological space is a set on which a topology is defined, which consists of a collection of subsets that are said to be open, and satisfy the axioms given below.

So basically, it sounds like a topological space is by definition composed of open sets? I am not sure.
The only example I really 80% get is the image:

The blue circle represents the set of points (x, y) satisfying x2 + y2 = r2. The red disk represents the set of points (x, y) satisfying x2 + y2 < r2. The red set is an open set, the blue set is its boundary set, and the union of the red and blue sets is a closed set.

That kind of makes sense, that the open set is everything except the boundary, but even then not really. Perhaps, is there another term we could pick other than calling it "open" (and "closed"), maybe taking inspiration from German or French or another language?
Anyways, we have this now to start (on the open sets wiki page):

A subset ${\displaystyle U}$ of the Euclidean n-space $R^n$ is open if, for every point x in ${\displaystyle U}$, there exists a positive real number $ε$ (depending on x) such that a point in $R^n$ belongs to ${\displaystyle U}$ as soon as its Euclidean distance from x is smaller than $ε$. Equivalently, a subset ${\displaystyle U}$ of $R^n$ is open if every point in ${\displaystyle U}$ is the center of an open ball contained in ${\displaystyle U}$.

Here I try to draw the first part out:

The green is the $R^n$, the blue is the open set $U$, the x is a random point in $U$, and the yellow is a point in $U$ because $ε$ is within a certain size. That's as much as I can understand from that sentence.
But even then, it doesn't make sense to me what we are talking about. And this is talking about in Euclidean space with the real numbers, so we are not even in the abstract realm of topological spaces yet.
Can you please try to provide an intuition closer to this? (which still doesn't make it easy to grok, but it is getting there)
What exactly is an open set? First if you could do better on my illustration (describing it better is all, no need to make an illustration unless it would help). And then but the main thing is, how to intuit the meaning of the topological notion of open set, given that you are defining the topology as being composed of open sets! Can you not compose a topology of closed sets? Either way, how do you conceptualize of the abstract notion of open sets?
Other resources that didn't quite help:

https://mathoverflow.net/questions/19152/why-is-a-topology-made-up-of-open-sets
Motivation for the concept of "open set" in topology

REPLY [1 votes]: To study topology before one has seen metric spaces (or at least Euclidean spaces) is like studying multiplication before addition: it is very likely not to make much sense. When one studies metric spaces an open set $A$ in a space $M$ is clearly defined: it is a set $A$ such that around every $a\in A$ there is some open ball $B_r(a)=\{x\in M | d(x,a)<r\}$ which is contained in $A$, or in other words, every point of $A$ is an interior point of $A$. So for instance $(0,1)\subseteq\mathbb{R}$ is an open set, but $[0,1)\subseteq\mathbb{R}$ is not open, because every open ball (i.e. interval) centered at $0$ is going to contain points from outside of $[0,1)$.
(Then one goes on to define a closed set as one of two equivalent conditions, either that its complement is open, or that every convergent sequence with elements of the set has limit inside that same set.)
After all this one studies all kinds of properties of open sets, including that the intersection of two (and hence a finite number) of open sets is an open set, and that the union of an arbitrary number of open sets is an open set. Together with the  fact that the empty set and the whole metric space are open sets (as follows easily from the definitions), this is exactly what motivates the definition of a topological space where an 'open set' is that which satisfies exactly these conditions.
In a metric space this definition gives us exactly the same old open sets, and in other more general contexts where we are not working with a metric space this turns out to be the most useful and interesting generalization. I highly suggest getting a good grip of the fundamentals of metric spaces before moving on to study topology, otherwise not only the definitions but many of the theorems are going to feel unmotivated as well.


TITLE: $B \subset A$ and dim $A$ = dim $B$ means $A$ an integral extension of $B$?
QUESTION [3 upvotes]: I'm referring here to the Krull dimension. Is this necessarily true for commutative rings with unity? How about for finitely-generated $k$-algebras?

REPLY [0 votes]: It is also false for finitely generated $k$-algebras, consider for example $k[x] \subseteq k[x,x^{-1}]$. Or just take $A \hookrightarrow A^n$ for some $A \neq 0$.


TITLE: Let $p$ be a prime. Prove that $p$ divides $ab^p−ba^p$ for all integers $a$ and $b$.
QUESTION [6 upvotes]: Let $p$ be a prime. Prove that $p$ divides $ab^p−ba^p$ for all integers
$a$ and $b$.

REPLY [5 votes]: Hint $\ $ little Fermat $\rm\Rightarrow mod\ p\!:\ n^p \equiv n\ \Rightarrow\ f(a,b^p)\equiv f(a,b)\equiv f(a^p,b)\ $ for all $\rm\:f\in \mathbb Z[x,y]$


TITLE: Proof of Cauchy sequence.
QUESTION [0 upvotes]: I'm facing this problem,
Let $\{ x_n \}_{ n\in \mathbb{N} }$ be a sequence of real numbers and $0 < r< 1$ such that $|x_{n+1} - x_n | < r^n$ for all $n \in \mathbb{N}$. Prove that $\{ x_n \}_{ n\in \mathbb{N}}$ is a Cauchy sequence.
My work based on other similar problems is:
Let's consider $|x_m-x_n|$ where $m$ y $n$ do not need to be consecutive numbers, assume $m\leq n$. Then $k=n-m\geq 0$,
$\\ \begin{aligned} |x_m-x_n| &=|x_m-x_{m+k}| \\
& =|x_m-x_{m+1}+x_{m+1}-x_{m+2}+...+x_{m+k-1}-x_{m+k}| \\
& \leq|x_{m}-x_{m+1}|+|x_{m+1}-x_{m+2}|+...+|x_{m+k-1}-x_{m+k}| \\
& < r^{m}+r^{m+1}+...+r^{m+k-1} \\
& = r^{m}(1+r^1+...+r^{k-1}) \\
& = (r^{m})\sum_{i=0}^{k-1}r^{i} \\
& \leq r^m(1/(1-r)). \\
\end{aligned}$
$\\ $ If $m>N_{\epsilon}$, then we have $r^{m}<r^{N_{\epsilon}}$ because $0<r<1$ (I think I need a strong argument to guarantee this). Then $r^m(1/(1-r))<r^{N_{\epsilon}}(1/(1-r))$
$\\ $ Can I guarantee that always exists $N_{\epsilon}\in \mathbb{N}$, such that $r^{N_{\epsilon}}(1/1-r)<\epsilon$ ? If so, then I get what I want
$$\\  |x_m-x_n|<r^m(1/(1-r))<r^{N_{\epsilon}}(1/(1-r))<\epsilon$$
$\ $ Whenever $m,n>N_{\epsilon}$
My greatest doubt. If $m>N_{\epsilon}$, then we have $r^{m}<r^{N_{\epsilon}}$ (Whenever $0<r<1$). Will this always be true? I'm thinking of mathematical induction to prove this.

REPLY [0 votes]: Generally if you didn't express doubts about some steps this proof would have been quite widely accepted.
Your first concern is if you can assume that if $m>N_\epsilon$ then $r^m<r^{N_\epsilon}$ or a proof of that. Now we have that $N_\epsilon = m + d$ for some $d>0$ so $r^m-r^{N_epsilon} = r^m - r^{m+d} = r^m(1-r^d)$. So what you need to know is that $0<r^d<1$ which is quite straight forward to prove with induction.
Your second concern is if you can guarantee that $r^{N_\epsilon}(1/(1-r))$ can be made arbitrarily small by selecting $N_\epsilon$. First of all $r$ is just a constant so we should focus on $r^{N_\epsilon}$. It's a well known fact and you could use the estimate that if $h>0$ then $(1+h)^n \ge 1+nh$ (which can be shown unsing induction) to see that
$$r^{N_\epsilon} \le {1\over (1+ (1/r-1))^{N_\epsilon}} \le {1\over1 + N_\epsilon(1/r-1)} \le {1\over N_\epsilon}{1\over1/r-1}$$
Which can be made arbitrarily small (while we know that it's also positive).


TITLE: Reduction of order method - Differential Equations
QUESTION [0 upvotes]: I need help with this question please.

Find the general solution by using reduction of order method to

$$ty'' -(t+1)y'+y = 0$$
given that $y_1(t) = e^t$ is a solution

REPLY [0 votes]: $$ty'' -(t+1)y'+y = 0$$
$$(ty''-y')-(ty'-y)=0$$
$$ \left ( \dfrac  {y'}{t} \right)'- \left ( \dfrac  yt \right)'=0$$
$$ \left ( \dfrac  {y'}{t} -\dfrac  y t\right)'=0$$
$$ \left ( \dfrac  {(ye^{-t})'}{te^{-t}} \right )'=0$$
Now substitute $y=y_1v=e^tv$ and integrate.
$$ \left ( \dfrac  {v'}{te^{-t}} \right )'=0$$


TITLE: To find a linear transformation such that $T^{2}( v) = -v $
QUESTION [0 upvotes]: Question is to find a linear transformation from $R^{2}$ to $R^{2}$ such that $T^{2}( v) = -v $ for all v .I used hit and trial method to do this but its has been a  long time i am stuck at it .Is there any systematic way to do this ? Thanks

REPLY [3 votes]: David's comment is bull on the money. Take for example
$$T\binom xy=\binom{-y}x$$
which comes from considering the rotation matrix
$$\begin{pmatrix}0&\!\!-1\\1&0\end{pmatrix}=\begin{pmatrix}\cos\frac\pi2&-\sin\frac\pi2\\\sin\frac\pi2&\cos\frac\pi2\end{pmatrix}$$


TITLE: How can I prove following density matrices have same eigenvalues?
QUESTION [1 upvotes]: I have the following two density operators, the paper I am reading says that these two operators have same eigenvalues

$$\rho^i = \frac{1}{3} ( |0\rangle \langle 0 | +|1\rangle \langle 1 |+|2\rangle \langle 2 |+a|0\rangle \langle 1 |+a|1\rangle \langle 0 |+c|1\rangle \langle 2 |+c|2\rangle \langle 1
 |),$$
$$\rho^f = \frac{1}{3} ( |0\rangle \langle 0 | +|1\rangle \langle 1 |+|2\rangle \langle 2 |+ax|0\rangle \langle 1 |+ax^*|1\rangle \langle 0 |+cy|1\rangle \langle 2 |+cy^*|2\rangle \langle 1
 |).$$
Here $a,c$ are real numbers and $x,y$ are unimodular complex numbers. Also $\{|0\rangle ,|1\rangle , |2\rangle \} $ are three orthonormal vectors of a 3-D Hilbert space.
My approach : its apparent that the operators are hermitian and thus have a spectral decomposition in terms of orthonormal vectors. Lets say one of the vectors in spectral decomposition of first operator is $$|\psi \rangle = A|0 \rangle + B|1\rangle,$$ then for the second operator the corresponding one would be $$|\psi \rangle = Ax^{\frac{1}{2}}|0 \rangle +(x^*)^{\frac{1}{2}} B|1\rangle$$ ( $A,B,C,D$ are some complex constants ). Similarly another vector in spectral decomposition of first operator will be of form $$|\psi \rangle = C|1 \rangle + D|2\rangle$$ and its counterpart in second operators spectral decomposition will be $$|\psi \rangle = y^{\frac{1}{2}}C|1 \rangle + (y^*)^{\frac{1}{2}}D|2\rangle.$$ Thus keeping eigen values same.
Doubt : But my approach seems to be an intuitive and vague proof, is there a way where it is evident that they have same eigenvalues in a simple manner?

REPLY [1 votes]: I have the following two density operators, the paper I am reading
  says that these two operators have same eigenvalues
$$\rho^i = \frac{1}{3} ( |0\rangle \langle 0 | +|1\rangle \langle 1
> |+|2\rangle \langle 2 |+a|0\rangle \langle 1 |+a|1\rangle \langle 0
> |+c|1\rangle \langle 2 |+c|2\rangle \langle 1  |),$$
$$\rho^f = \frac{1}{3} ( |0\rangle \langle 0 | +|1\rangle \langle 1
> |+|2\rangle \langle 2 |-ax|0\rangle \langle 1 |+ax^*|1\rangle \langle
> 0 |+cy|1\rangle \langle 2 |+cy^*|2\rangle \langle 1  |).$$

They don't.
Did you mean to write "+ax" instead of "-ax" in the second matrix?
If so, then they do... in either case (if you meant to write "+ax") the eigenvalue equation is:
$$
(1-\lambda)^3=(1-\lambda)(a^2+c^2)
$$
giving
$$
\lambda=1\;,\;1\pm\sqrt{a^2+c^2}
$$


TITLE: "double" fibre product
QUESTION [0 upvotes]: A (1-)fibre product (a.k.a. pullback) in a category consists of three distinct objects:
$$\require{AMScd}
\begin{CD}
X \times_Z Y @>q>> Y \\
@VpVV @VVV \\
X @>>> Z
\end{CD}$$
$(X \times_{Z}Y,p,q)$.
Now, in particular we have (often) non-trivial fibre products over the same objects, i.e. $X=Y$, this particular fibre products can be indicated as $X \times_Z X \rightrightarrows X$.
If I want to repeat the operation of fibre product considering $X \times_Z X \times_Z X$ how many arrows associated with this fibre product will I have?I have to take count of the two arrows within the first fibre product, so I think that the question is not trivial.

REPLY [1 votes]: I'd leave this as a comment, but I want to draw a couple of diagrams...
Suppose you have three arrows $f,g,h\colon X\to Z$ (possibly $f=g=h$, if you are interested in a "fibered cube" of the same object over $Z$). Then you may consider first the pullback with respect to $f$ and $g$:
$$\require{AMScd}\begin{CD}
X\times_Z X @>\overline{f}>> X\\
@VV\overline{g}V @VVgV\\
X @>f>> Z
\end{CD}$$
And then consider the pullback
$$\require{AMScd}\begin{CD}
(X\times_Z X) \times_Z X @>k>> X\\
@VV\overline{h}V @VVhV\\
X\times_Z X @>g\overline{f} = f\overline{g}>> Z
\end{CD}$$
This gives you three arrows:
\begin{align*}
(X\times_Z X)\times_Z X & \xrightarrow{k} X,\\
(X\times_Z X)\times_Z X & \xrightarrow{\overline{h}} X\times_Z X \xrightarrow{\overline{f}} X,\\
(X\times_Z X)\times_Z X & \xrightarrow{\overline{h}} X\times_Z X \xrightarrow{\overline{g}} X.
\end{align*}
In general, $\underbrace{X\times_Z \cdots \times_Z X}_n$ should come with $n$ arrows to $X$.
Is that what you need?