text:
(* ========================================================================= *)
(*                (c) Copyright, Bill Richter 2013                           *)
(*          Distributed under the same license as HOL Light                  *)
(*                                                                           *)
(* Proof of the Bug Puzzle conjecture of the HOL Light tutorial: Any two     *)
(* triples of points in the plane with the same oriented area can be         *)
(* connected in 5 moves or less (FivemovesOrLess).  Much of the code is      *)
(* due to John Harrison: a proof (NOTENOUGH_4) showing this is the best      *)
(* possible result; an early version of Noncollinear_2Span; the              *)
(* definition of move, which defines a closed subset                         *)
(*       {(A,B,C,A',B',C') | move (A,B,C) (A',B',C')} of R^6 x R^6,          *)
(* i.e. the zero set of a continuous function; FivemovesOrLess_STRONG,       *)
(* which handles the degenerate case (collinear or non-distinct triples),    *)
(* giving a satisfying answer using this "closed" definition of move.        *)
(*                                                                           *)
(* The mathematical proofs are essentially due to Tom Hales.  The code       *)
(* tries to mix declarative and procedural proof styles, using ideas due     *)
(* to John Harrison (section 12.1 "Towards more readable proofs" of the      *)
(* HOL Light tutorial), Freek Wiedijk (arxiv.org/pdf/1201.3601 "A            *)
(* Synthesis of the Procedural and Declarative Styles of Interactive         *)
(* Theorem Proving"), Marco Maggesi, who wrote the tactic constructs         *)
(* INTRO_TAC & HYP, which goes well with the older SUBGOAL_TAC, and Petros   *)
(* Papapanagiotou, coauthor of IsabelleLight, who wrote BuildExist below, a  *)
(* a crucial part of consider.                                               *)
(* ========================================================================= *)

needs "Multivariate/determinants.ml";;

new_type_abbrev("triple",`:real^2#real^2#real^2`);;

let so = fun tac -> FIRST_ASSUM MP_TAC THEN tac;;

let BuildExist x t =
  let try_type tp tm =
    try inst (type_match (type_of tm) tp []) tm
    with Failure _ -> tm in

  (* Check if two variables match allowing only type instantiations: *)
  let vars_match tm1 tm2 =
    let inst = try term_match [] tm1 tm2 with Failure _ -> [],[tm2,tm1],[] in
      match inst with
        [],[],_ -> tm2
      | _  -> failwith "vars_match: no match" in

  (* Find the type of a matching variable in t. *)
  let tp = try type_of (tryfind (vars_match x) (frees t))
  with Failure _ ->
  warn true ("BuildExist: `" ^ string_of_term x ^ "` not be found in
  `" ^ string_of_term t ^ "`") ;
  type_of x in
  (* Try to force x to type tp. *)
  let x' = try_type tp x in
  mk_exists (x',t);;

let consider vars_SuchThat t prfs lab =
  (* Functions ident and parse_using borrowed from HYP in tactics.ml *)
  let ident = function
      Ident s::rest when isalnum s -> s,rest
    | _ -> raise Noparse in
  let parse_using = many ident in
  let rec findSuchThat = function
      n -> if String.sub vars_SuchThat n 9 = "such that" then n
      else findSuchThat (n + 1) in
  let n = findSuchThat 1 in
  let vars = String.sub vars_SuchThat 0 (n - 1) in
  let xl = map parse_term ((fst o parse_using o lex o explode) vars) in
  let tm = itlist BuildExist xl t in
  match prfs with
    p::ps -> (warn (ps <> []) "consider: additional subproofs ignored";
    SUBGOAL_THEN tm (DESTRUCT_TAC ("@" ^ vars ^ "." ^ lab))
    THENL [p; ALL_TAC])
  | [] -> failwith "consider: no subproof given";;

let cases sDestruct disjthm tac =
  SUBGOAL_TAC "" disjthm tac THEN FIRST_X_ASSUM
  (DESTRUCT_TAC sDestruct);;

let raa lab t tac = SUBGOAL_THEN (mk_imp(t, `F`)) (LABEL_TAC lab) THENL
  [INTRO_TAC lab; tac];;

let VEC2_TAC =
  SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_2; SUM_2; DIMINDEX_2; VECTOR_2;
           vector_add; vec; dot; orthogonal; basis;
           vector_neg; vector_sub; vector_mul; ARITH] THEN
  CONV_TAC REAL_RING;;

let COLLINEAR_3_2Dzero = prove
 (`!y z:real^2. collinear{vec 0,y,z} <=>
                  z$1 * y$2 = y$1 * z$2`,
  REWRITE_TAC[COLLINEAR_3_2D] THEN VEC2_TAC);;

let Noncollinear_3ImpliesDistinct = prove
  (`~collinear {a,b,c}  ==>  ~(a = b) /\ ~(a = c) /\ ~(b = c)`,
  MESON_TAC[COLLINEAR_BETWEEN_CASES; BETWEEN_REFL]);;

let collinearSymmetry = prove
(`collinear {A,B,C}
         ==> collinear {A,C,B} /\ collinear {B,A,C} /\
             collinear {B,C,A} /\ collinear {C,A,B} /\ collinear {C,B,A}`,
  MESON_TAC[SET_RULE `{A,C,B} SUBSET {A,B,C} /\  {B,A,C} SUBSET {A,B,C} /\
  {B,C,A} SUBSET {A,B,C} /\  {C,A,B} SUBSET {A,B,C} /\  {C,B,A} SUBSET {A,B,C}`;
  COLLINEAR_SUBSET]);;

let Noncollinear_2Span = prove
 (`!u v w:real^2. ~collinear  {vec 0,v,w} ==> ? s t. s % v + t % w = u`,
  INTRO_TAC "!u v w; H1" THEN
  SUBGOAL_TAC "H1'" `~(v$1 * w$2 - (w:real^2)$1 * (v:real^2)$2 = &0)`
  [HYP MESON_TAC "H1" [COLLINEAR_3_2Dzero; REAL_SUB_0]] THEN
  consider "M such that"
  `M = transp(vector[v:real^2;w:real^2]):real^2^2` [MESON_TAC[]] "Mexists" THEN
  SUBGOAL_TAC "MatMult" `~(det (M:real^2^2) = &0) /\
  (! x. (M ** x)$1 = (v:real^2)$1 * x$1 + (w:real^2)$1 * x$2  /\
  (M ** x)$2 = v$2 * x$1 + w$2 * x$2)`
  [HYP SIMP_TAC "H1' Mexists" [matrix_vector_mul; DIMINDEX_2; SUM_2;
  TRANSP_COMPONENT; VECTOR_2; LAMBDA_BETA; ARITH; CART_EQ; FORALL_2; DET_2] THEN VEC2_TAC] THEN
  consider "x such that" `(M:real^2^2) ** (x:real^2) = u`
  [so (MESON_TAC [ARITH_RULE `~(r < n)  /\  r <= MIN n n  ==>  r = n`;
  DET_EQ_0_RANK; RANK_BOUND; MATRIX_FULL_LINEAR_EQUATIONS])] "xDef" THEN
  MAP_EVERY EXISTS_TAC [`(x:real^2)$1`; `(x:real^2)$2`] THEN SUBGOAL_TAC ""
  `(x:real^2)$1 * (v:real^2)$1 + (x:real^2)$2 * (w:real^2)$1 = (u:real^2)$1  /\
  x$1 * v$2 + x$2 * w$2 = u$2` [HYP MESON_TAC "MatMult xDef" [REAL_MUL_SYM]]
  THEN so (SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_2; SUM_2; DIMINDEX_2; VECTOR_2; vector_add; vector_mul; ARITH]));;

let oriented_area = new_definition
  `oriented_area (a:real^2,b:real^2,c:real^2) =
  ((b$1 - a$1) * (c$2 - a$2) - (c$1 - a$1) * (b$2 - a$2)) / &2`;;

let oriented_areaSymmetry = prove
 (`oriented_area (A,B,C) = oriented_area(A',B',C')  ==>
  oriented_area (B,C,A) = oriented_area (B',C',A')  /\
  oriented_area (C,A,B) = oriented_area (C',A',B')  /\
  oriented_area (A,C,B) = oriented_area (A',C',B')  /\
  oriented_area (B,A,C) = oriented_area (B',A',C')  /\
  oriented_area (C,B,A) = oriented_area (C',B',A')`,
  REWRITE_TAC[oriented_area] THEN VEC2_TAC);;

let move = new_definition
  `!A B C A' B' C':real^2. move (A,B,C) (A',B',C') <=>
  (B = B' /\ C = C' /\ collinear {vec 0,C - B,A' - A} \/
  A = A' /\ C = C' /\ collinear {vec 0,C - A,B' - B} \/
  A = A' /\ B = B' /\ collinear {vec 0,B - A,C' - C})`;;

let moveInvariant = prove
  (`!p p'. move p p' ==> oriented_area p = oriented_area p'`,
  REWRITE_TAC[FORALL_PAIR_THM; move; oriented_area; COLLINEAR_LEMMA;  vector_mul] THEN VEC2_TAC);;

let reachable = new_definition
  `!p p'.
  reachable p p' <=> ?n. ?s.
  s 0 = p /\ s n = p' /\
  (!m. 0 <= m /\ m < n ==> move (s m) (s (SUC m)))`;;

let reachableN = new_definition
  `!p p'. !n.
  reachableN p p' n <=> ?s.
  s 0 = p /\ s n = p' /\
  (!m. 0 <= m /\ m < n ==> move (s m) (s (SUC m)))`;;

let ReachLemma = prove
 (`!p p'. reachable p p'  <=>  ?n.  reachableN p p' n`,
  REWRITE_TAC[reachable; reachableN]);;

let reachableN_CLAUSES = prove
 (`! p p'. (reachableN p p' 0  <=>  p = p') /\
  ! n. reachableN p p' (SUC n)  <=>  ? q. reachableN p q n  /\ move q p'`,
  INTRO_TAC "!p p'" THEN
  consider "s0 such that" `s0 =  \m:num. p':triple` [MESON_TAC[]] "s0exists" THEN
  SUBGOAL_TAC "0CLAUSE" `reachableN p p' 0  <=>  p = p'`
  [HYP MESON_TAC "s0exists" [LE_0; reachableN; LT]] THEN SUBGOAL_TAC "Imp1"
  `! n. reachableN p p' (SUC n)  ==>  ? q. reachableN p q n  /\ move q p'`
  [INTRO_TAC "!n; H1" THEN
  consider "s such that"
  `s 0 = p /\ s (SUC n) = p' /\ !m. m < SUC n ==> move (s m) (s (SUC m))`
  [HYP MESON_TAC "H1" [LE_0; reachableN]] "sDef" THEN
  consider "q such that" `q:triple = s n` [MESON_TAC[]]  "qDef" THEN
  HYP MESON_TAC "sDef qDef" [LE_0; reachableN; LT]] THEN SUBGOAL_TAC "Imp2"
  `!n. (? q. reachableN p q n  /\ move q p')  ==>  reachableN p p' (SUC n)`
  [INTRO_TAC "!n" THEN REWRITE_TAC[IMP_CONJ; LEFT_IMP_EXISTS_THM] THEN
  INTRO_TAC "!q; nReach; move_qp'" THEN
  consider "s such that"
  `s 0 = p /\ s n = q /\ !m. m < n ==> move (s m) (s (SUC m))`
  [HYP MESON_TAC "nReach" [reachableN; LT; LE_0]] "sDef" THEN
  REWRITE_TAC[reachableN; LT; LE_0] THEN
  EXISTS_TAC `\m. if m < SUC n then s m else p':triple` THEN
  HYP MESON_TAC "sDef move_qp'" [LT_0; LT_REFL; LT; LT_SUC]] THEN
  HYP MESON_TAC "0CLAUSE Imp1 Imp2" []);;

let reachableInvariant = prove
 (`!p p'. reachable p p'  ==>  oriented_area p = oriented_area p'`,
  SIMP_TAC[ReachLemma; LEFT_IMP_EXISTS_THM; SWAP_FORALL_THM] THEN
  INDUCT_TAC THEN ASM_MESON_TAC[reachableN_CLAUSES; moveInvariant]);;

let move2Cond = new_definition
  `! A B A' B':real^2. move2Cond A B A' B'  <=>
  ~collinear {B,A,A'} /\ ~collinear {A',B,B'}   \/
  ~collinear {A,B,B'} /\ ~collinear {B',A,A'}`;;

let reachableN_One = prove
 (`reachableN P0 P1 1 <=> move P0 P1`,
  MESON_TAC[ONE; reachableN; reachableN_CLAUSES]);;

let reachableN_Two = prove
 (`reachableN P0 P2 2 <=> ?P1. move P0 P1 /\ move P1 P2`,
  MESON_TAC[TWO; reachableN_One; reachableN_CLAUSES]);;

let reachableN_Three = prove
 (`reachableN P0 P3 3  <=>  ?P1 P2. move P0 P1 /\ move P1 P2 /\ move P2 P3`,
  MESON_TAC[ARITH_RULE `3 = SUC 2`; reachableN_Two; reachableN_CLAUSES]);;

let reachableN_Four = prove
 (`reachableN P0 P4 4  <=>  ?P1 P2 P3. move P0 P1 /\ move P1 P2 /\
  move P2 P3 /\ move P3 P4`,
  MESON_TAC[ARITH_RULE `4 = SUC 3`; reachableN_Three; reachableN_CLAUSES]);;

let reachableN_Five = prove
 (`reachableN P0 P5 5  <=>  ?P1 P2 P3 P4. move P0 P1 /\ move P1 P2 /\
  move P2 P3 /\ move P3 P4 /\ move P4 P5`,
  REWRITE_TAC[ARITH_RULE `5 = SUC 4`; reachableN_CLAUSES] THEN
  MESON_TAC[reachableN_Four]);;

let moveSymmetry = prove
 (`move (A,B,C) (A',B',C') ==>
  move (B,C,A) (B',C',A') /\ move (C,A,B) (C',A',B') /\
  move (A,C,B) (A',C',B') /\ move (B,A,C) (B',A',C') /\ move (C,B,A) (C',B',A')`,
  SUBGOAL_TAC "" `!A B C A':real^2. collinear {vec 0, C - B, A' - A}
  ==> collinear {vec 0, B - C, A' - A}`
  [REWRITE_TAC[COLLINEAR_3_2Dzero] THEN VEC2_TAC] THEN
  so (REWRITE_TAC[move]) THEN MESON_TAC[]);;

let reachableNSymmetry = prove
 (`! n. ! A B C A' B' C'. reachableN (A,B,C) (A',B',C') n  ==>
reachableN (B,C,A) (B',C',A') n  /\  reachableN (C,A,B) (C',A',B') n /\
reachableN (A,C,B) (A',C',B') n  /\  reachableN (B,A,C) (B',A',C') n /\
reachableN (C,B,A) (C',B',A') n`,
  MATCH_MP_TAC num_INDUCTION THEN REWRITE_TAC[reachableN_CLAUSES] THEN
  SIMP_TAC[PAIR_EQ] THEN
  INTRO_TAC "!n;nStep; !A B C A' B' C'" THEN
  REWRITE_TAC[LEFT_IMP_EXISTS_THM; FORALL_PAIR_THM] THEN
  MAP_EVERY X_GEN_TAC [`X:real^2`; `Y:real^2`; `Z:real^2`] THEN
  INTRO_TAC "XYZexists" THEN
  REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_AND_EXISTS_THM] THEN
  MAP_EVERY EXISTS_TAC [`(Y,Z,X):triple`; `(Z,X,Y):triple`;
  `(X,Z,Y):triple`; `(Y,X,Z):triple`; `(Z,Y,X):triple`] THEN
  HYP SIMP_TAC "nStep XYZexists" [moveSymmetry]);;

let ORIENTED_AREA_COLLINEAR_CONG = prove
 (`! A B C A' B' C.
        oriented_area (A,B,C) = oriented_area (A',B',C')
        ==> (collinear {A,B,C} <=> collinear {A',B',C'})`,
  REWRITE_TAC[COLLINEAR_3_2D; oriented_area] THEN CONV_TAC REAL_RING);;

let Basic2move_THM = prove
 (`! A B C A'. ~collinear {A,B,C} /\ ~collinear {B,A,A'} ==>
  ?X. move (A,B,C) (A,B,X)  /\  move (A,B,X) (A',B,X)`,
  INTRO_TAC "!A B C A'; H1 H2" THEN SUBGOAL_TAC "add0vector_mul"
  `!r. r % ((A:real^2) - B) = (--r) % (B - A)  /\
  r % (A - B) = r % (A - B) + &0 % (C - B)` [VEC2_TAC] THEN
  SUBGOAL_TAC "H2'" `~ ? r. A' - (A:real^2) = r % (A - B)`
  [so (HYP MESON_TAC "H2" [COLLINEAR_3; COLLINEAR_LEMMA])] THEN
  consider "r t such that" `A' - (A:real^2) = r % (A - B) + t % (C - B)`
  [HYP MESON_TAC "H1" [COLLINEAR_3; Noncollinear_2Span]] "rExists" THEN
  SUBGOAL_TAC "tNonzero" `~(t = &0)`
  [so (HYP MESON_TAC "add0vector_mul H2'" [])] THEN
  consider "s X such that" `s = r / t  /\  X:real^2 = C + s % (A - B)`
  [HYP MESON_TAC "rExists" []] "Xexists" THEN
  SUBGOAL_TAC "" `A' - (A:real^2) = (t * s) % (A - B) + t % (C - B)`
  [so (HYP MESON_TAC "rExists tNonzero" [REAL_DIV_LMUL])] THEN SUBGOAL_TAC ""
  `A' - (A:real^2) = t % (X - B) /\ X - C = (-- s) % (B - (A:real^2))`
  [(so (HYP REWRITE_TAC "Xexists" [])) THEN VEC2_TAC] THEN SUBGOAL_TAC ""
  `collinear {vec 0,B - (A:real^2),X - C}  /\  collinear {vec 0,X - B,A' - A}`
  [so (HYP MESON_TAC "" [COLLINEAR_LEMMA])] THEN so (MESON_TAC [move]));;

let FourStepMoveAB = prove
 (`!A B C A' B'. ~collinear {A,B,C} ==>
  ~collinear {B,A,A'} /\ ~collinear {A',B,B'} ==>
  ? X Y. move (A,B,C) (A,B,X)  /\  move (A,B,X) (A',B,X)  /\
  move (A',B,X) (A',B,Y)  /\  move (A',B,Y) (A',B',Y)`,
  INTRO_TAC "!A B C A' B'; H1; H2" THEN
  consider "X such that" `move (A,B,C) (A,B,X)  /\  move (A,B,X) (A',B,X)`
  [HYP MESON_TAC "H1 H2" [Basic2move_THM]]"ABX" THEN
  SUBGOAL_TAC "" `~collinear {(A:real^2),B,X} /\ ~collinear {A',B,X}`
  [so (HYP MESON_TAC "H1" [moveInvariant; ORIENTED_AREA_COLLINEAR_CONG])]
  THEN SUBGOAL_TAC "" `~collinear {(B:real^2),A',X}`
  [so (MESON_TAC [collinearSymmetry])] THEN
  consider "Y such that" `move (B,A',X) (B,A',Y)  /\  move (B,A',Y) (B',A',Y)`
  [so (HYP MESON_TAC "H2" [Basic2move_THM])]  "BA'Y" THEN
  SUBGOAL_TAC "" `move (A',B,X) (A',B,Y)  /\  move (A',B,Y) (A',B',Y)`
  [HYP MESON_TAC "BA'Y" [moveSymmetry]] THEN so (HYP MESON_TAC "ABX" []));;

let FourStepMoveABBAreach = prove
 (`!A B C A' B'. ~collinear {A,B,C} /\ move2Cond A B A' B' ==>
  ? Y. reachableN (A,B,C) (A',B',Y) 4`,
  INTRO_TAC "!A B C A' B'; H1 H2" THEN
  cases "Case1 | Case2"
  `~collinear {B,(A:real^2),A'} /\ ~collinear {A',B,B'}  \/
  ~collinear {A,B,B'} /\ ~collinear {B',A,A'}`
  [HYP MESON_TAC "H2" [move2Cond]]
  THENL
  [so (HYP MESON_TAC "H1" [FourStepMoveAB; reachableN_Four]);
  SUBGOAL_TAC "" `~collinear {B,(A:real^2),C}`
  [HYP MESON_TAC "H1" [collinearSymmetry]]] THEN
  SUBGOAL_TAC "" `~collinear {B,(A:real^2),C}`
  [HYP MESON_TAC "H1" [collinearSymmetry]] THEN
  consider "X Y such that"
  `move (B,A,C) (B,A,X)  /\  move (B,A,X) (B',A,X)  /\
  move (B',A,X) (B',A,Y)  /\  move (B',A,Y) (B',A',Y)`
  [so (HYP MESON_TAC "Case2" [FourStepMoveAB])] "BAX" THEN
  HYP MESON_TAC "BAX" [moveSymmetry; reachableN_Four]);;

let NotMove2ImpliesCollinear = prove
 (`!A B C A' B' C'. ~collinear {A,B,C} /\ ~collinear {A',B',C'} /\
  ~(A = A') /\ ~(B = B') /\ ~move2Cond A B A' B' ==>
  collinear {A,B,A',B'}`,
  INTRO_TAC "!A B C A' B' C'; H1 H1' H2 H2' H3" THEN
  SUBGOAL_TAC "Distinct" `~((A:real^2) = B) /\ ~((A':real^2) = B')`
  [HYP MESON_TAC "H1 H1'" [Noncollinear_3ImpliesDistinct]] THEN
  SUBGOAL_TAC "set4symmetry" `{(A:real^2),B,A',B'} SUBSET {A,A',B,B'}  /\
  {A,B,A',B'} SUBSET {B,B',A',A}  /\  {A,B,A',B'} SUBSET {A',B',B,A}` [SET_TAC[]] THEN
  cases "Case1 | Case2 | Case3 | Case4"
  `collinear {B,(A:real^2),A'} /\ collinear {A,B,B'}  \/
  collinear {B,A,A'} /\ collinear {B',A,A'}  \/
  collinear {A',B,B'} /\ collinear {A,B,B'}  \/
  collinear {A',B,B'} /\ collinear {B',A,A'}`
  [HYP MESON_TAC "H3" [move2Cond]] THEN
  so (HYP MESON_TAC "Distinct H2 H2' set4symmetry"
  [collinearSymmetry; COLLINEAR_4_3; COLLINEAR_SUBSET]));;

let DistinctImplies2moveable = prove
 (`!A B C A' B' C'. ~collinear {A,B,C} /\ ~collinear {A',B',C'} /\
  ~(A = A') /\ ~(B = B') /\ ~(C = C')  ==>
  move2Cond A B A' B' \/ move2Cond B C B' C'`,
  INTRO_TAC "!A B C A' B' C'; H1 H1' H2a H2b H2c" THEN SUBGOAL_TAC "3subset4"
  `{(A:real^2),B,B'} SUBSET {A,B,A',B'} /\ {B,B',C} SUBSET {B,C,B',C'}`
  [SET_TAC[]] THEN
  raa "Con" `~move2Cond A B A' B'  /\
  ~move2Cond B C B' C'` (HYP MESON_TAC "Con" []) THEN
  SUBGOAL_TAC "" `collinear {(A:real^2),B,A',B'} /\ collinear {B,C,B',C'}`
  [so (HYP MESON_TAC "H1 H1' H2a H2b H2c" [collinearSymmetry; NotMove2ImpliesCollinear])]
  THEN SUBGOAL_TAC "" `collinear {(A:real^2),B,C}`
  [so (HYP MESON_TAC "3subset4 H2a H2b H2c" [COLLINEAR_SUBSET; COLLINEAR_3_TRANS])]
  THEN so (HYP MESON_TAC "H1 H1'" []));;

let SameCdiffAB = prove
 (`!A B C A' B' C'.  ~collinear {A,B,C} /\ ~collinear {A',B',C'} ==>
 C = C' /\ ~(A = A') /\ ~(B = B') ==>
  ? Y. reachableN (A,B,C) (Y,B',C') 2  \/ reachableN (A,B,C) (A',B',Y) 4`,
  INTRO_TAC "!A B C A' B' C'; H1; H2" THEN SUBGOAL_TAC "easy_set"
  `{B,B',(A:real^2)} SUBSET {A,B,A',B'}  /\  {A,B,C} SUBSET {B,B',A,C}` [SET_TAC[]]  THEN
  cases "Ncol | move | col_Nmove"
  `~collinear {C,B,B'}  \/
  move2Cond A B A' B'  \/
  collinear {C,B,B'} /\ ~move2Cond A B A' B'`
  [MESON_TAC[]] THENL
  [consider "X such that" `move (B,C,A) (B,C,X) /\ move (B,C,X) (B',C',X)`
  [so (HYP MESON_TAC "easy_set H1 H2" [collinearSymmetry; Basic2move_THM])] "BCX"
  THEN HYP MESON_TAC "BCX" [reachableN_Two; reachableNSymmetry];
  so (HYP MESON_TAC "H1" [FourStepMoveABBAreach]);
  SUBGOAL_TAC "" `collinear {(B:real^2),B',A} /\ collinear {B,B',C}`
  [so (HYP MESON_TAC "H1 H2 easy_set"
  [NotMove2ImpliesCollinear; COLLINEAR_SUBSET; collinearSymmetry])]  THEN
  so (HYP MESON_TAC "H2 easy_set H1" [COLLINEAR_4_3; COLLINEAR_SUBSET])]);;

let FourMovesToCorrectTwo = prove
 (`!A B C A' B' C'. ~collinear {A,B,C} /\ ~collinear {A',B',C'} ==>
  ? n. n < 5 /\ ? Y. reachableN (A,B,C) (A',B',Y) n  \/
  reachableN (A,B,C) (A',Y,C') n  \/ reachableN (A,B,C) (Y,B',C') n`,
  INTRO_TAC "!A B C A' B' C'; H1" THEN
  SUBGOAL_TAC "H1'" `~collinear {B,C,(A:real^2)} /\
  ~collinear{B',C',(A':real^2)} /\ ~collinear {C,A,B} /\ ~collinear {C',A',B'}`
  [HYP MESON_TAC "H1" [collinearSymmetry]]   THEN
  SUBGOAL_TAC "easy_arith" `0 < 5 /\ 2 < 5 /\ 3 < 5 /\ 4 < 5` [ARITH_TAC] THEN
  cases "case01 | case2 | case3"
  `((A:real^2) = A' /\ (B:real^2) = B' /\ (C:real^2) = C'  \/
  A = A' /\ B = B' /\ ~(C = C')  \/  A = A' /\ ~(B = B') /\ C = C' \/
  ~(A = A') /\ B = B' /\ C = C')  \/
  (A = A' /\ ~(B = B') /\ ~(C = C')  \/
  ~(A = A') /\ B = B' /\ ~(C = C')  \/  ~(A = A') /\ ~(B = B') /\ C = C')  \/
  ~(A = A') /\ ~(B = B') /\ ~(C = C')`
  [MESON_TAC []] THENL
  [so (HYP MESON_TAC "easy_arith" [reachableN_CLAUSES]);
  so (HYP MESON_TAC "H1 H1' easy_arith" [SameCdiffAB; reachableNSymmetry]);
  EXISTS_TAC `4` THEN HYP SIMP_TAC "easy_arith" [] THEN
  so (HYP MESON_TAC "H1  H1'" [DistinctImplies2moveable; FourStepMoveABBAreach;
  reachableNSymmetry; reachableN_Four])]);;

let CorrectFinalPoint = prove
 (`oriented_area (A,B,C) = oriented_area (A,B,C') ==>
  move (A,B,C) (A,B,C')`,
  REWRITE_TAC [move; oriented_area; COLLINEAR_3_2Dzero]  THEN VEC2_TAC);;

let FiveMovesOrLess = prove
 (`!A B C A' B' C'. ~collinear {A,B,C} ==>
  oriented_area (A,B,C) = oriented_area (A',B',C') ==>
  ? n. n <= 5 /\ reachableN (A,B,C) (A',B',C') n`,
  INTRO_TAC "!A B C A' B' C'; H1; H2"  THEN
  SUBGOAL_TAC "H1'" `~collinear {(A':real^2),B',C'}`
  [HYP MESON_TAC "H1 H2" [ORIENTED_AREA_COLLINEAR_CONG]]  THEN
  SUBGOAL_TAC "Distinct" `~((A:real^2) = B) /\ ~(A = C) /\ ~(B = C) /\
  ~((A':real^2) = B') /\ ~(A' = C') /\ ~(B' = C')`
  [so (HYP MESON_TAC "H1" [Noncollinear_3ImpliesDistinct])]  THEN
  consider "n Y such that"
  `n < 5 /\ (reachableN (A,B,C) (A',B',Y) n \/
  reachableN (A,B,C) (A',Y,C') n \/ reachableN (A,B,C) (Y,B',C') n)`
  [HYP MESON_TAC "H1 H1'" [FourMovesToCorrectTwo]] "2Correct" THEN
  cases "A'B'Y | A'YC' | YB'C'"
  `reachableN (A,B,C) (A',B',Y) n  \/
  reachableN (A,B,C) (A',Y,C') n  \/
  reachableN (A,B,C) (Y,B',C') n` [HYP MESON_TAC "2Correct" []] THENL
  [SUBGOAL_TAC "" `oriented_area (A',B',Y) = oriented_area (A',B',C')`
  [so (HYP MESON_TAC "H2" [ReachLemma; reachableInvariant])]  THEN
  SUBGOAL_TAC "" `move (A',B',Y) (A',B',C')`
  [so (HYP MESON_TAC "Distinct" [CorrectFinalPoint])]  THEN
  so (HYP MESON_TAC "A'B'Y 2Correct" [reachableN_CLAUSES; LE_SUC_LT]);
  SUBGOAL_TAC "" `oriented_area (A',C',Y) = oriented_area (A',C',B')`
  [so (HYP MESON_TAC "H2" [ReachLemma; reachableInvariant; oriented_areaSymmetry])]
  THEN SUBGOAL_TAC "" `move (A',Y,C') (A',B',C')`
  [so (HYP MESON_TAC "Distinct" [CorrectFinalPoint; moveSymmetry])]  THEN
  so (HYP MESON_TAC "A'YC' 2Correct" [reachableN_CLAUSES; LE_SUC_LT]);
SUBGOAL_TAC "" `oriented_area (B',C',Y) = oriented_area (B',C',A')`
  [so (HYP MESON_TAC "H2" [ReachLemma; reachableInvariant; oriented_areaSymmetry])]
  THEN SUBGOAL_TAC "" `move (Y,B',C') (A',B',C')`
  [so (HYP MESON_TAC "Distinct" [CorrectFinalPoint; moveSymmetry])]  THEN
  so (HYP MESON_TAC "YB'C' 2Correct" [reachableN_CLAUSES; LE_SUC_LT])]);;

let NOTENOUGH_4 = prove
 (`?p0 p4. oriented_area p0 = oriented_area p4 /\ ~reachableN p0 p4 4`,
  consider "p0 p4 such that"
  `p0:triple = vector [&0;&0],vector [&0;&1],vector [&1;&0]  /\
  p4:triple = vector [&1;&1],vector [&1;&2],vector [&2;&1]`
  [MESON_TAC []] "p04Def" THEN
  SUBGOAL_TAC "equal_areas" `oriented_area p0 = oriented_area p4`
  [HYP REWRITE_TAC "p04Def" [oriented_area] THEN VEC2_TAC] THEN
  SUBGOAL_TAC "" `~reachableN p0 p4 4`
  [HYP REWRITE_TAC "p04Def" [reachableN_Four; NOT_EXISTS_THM; FORALL_PAIR_THM;  move; COLLINEAR_3_2Dzero; FORALL_VECTOR_2] THEN VEC2_TAC] THEN
  so (HYP MESON_TAC "equal_areas" []));;

let FiveMovesOrLess_STRONG = prove
 (`!A B C A' B' C'.
  oriented_area (A,B,C) = oriented_area (A',B',C') ==>
  ?n. n <= 5 /\ reachableN (A,B,C) (A',B',C') n`,
  INTRO_TAC "!A B C A' B' C'; H1" THEN
  SUBGOAL_TAC "EZcollinear"
  `(!X Y:real^2. collinear {X,Y,Y}) /\
  (!A B A'. move (A,B,B) (A',B,B))  /\
  !A B C B'. (collinear {A,B,C} /\ collinear {A,B',C}  ==>
  move (A,B,C) (A,B',C))`
  [REWRITE_TAC[move; COLLINEAR_3_2D] THEN VEC2_TAC] THEN
  cases "ABCncol | ABCcol"
  `~collinear {(A:real^2),B,C}  \/  collinear {A,B,C}`
  [MESON_TAC []] THENL
  [so (HYP MESON_TAC "H1" [FiveMovesOrLess]);
  SUBGOAL_TAC "A'B'C'col" `collinear {(A':real^2),B',C'}`
  [so (HYP MESON_TAC "H1" [ORIENTED_AREA_COLLINEAR_CONG])] THEN
  consider "P1 P2 P3 P4 such that"
  `P1:triple = A,C,C  /\  P2:triple = B',C,C  /\  P3 = B',B',C  /\
  P4:triple = B',B',C'` [MESON_TAC []] "P1234exist" THEN
  SUBGOAL_TAC "" `move (A,B,C) (P1:triple)  /\  move P1 P2  /\
  move P2 P3  /\  move P3 P4  /\  move P4 (A',B',C')`
  [HYP MESON_TAC "ABCcol A'B'C'col EZcollinear P1234exist"
  [collinearSymmetry; moveSymmetry]] THEN
  so (MESON_TAC [reachableN_Five; LE_REFL])]);;

subset_name: curated


TITLE: Why does $y=x^a$ flicker around the x-axis as you adjust $a$?
QUESTION [2 upvotes]: I know raising to an even power makes things positive and raising to an odd power preserves sign, but if you graph fractional powers they seem to alternate. Why is this?
GIF demonstrating

REPLY [0 votes]: It's because of how your calculator chooses to define, or not define, exponentiation when $x$ is a negative number and $a$ is a real number.
In particular, what I suspect it is using is the definition that, for negative $x$,
$$x^a := \begin{cases} -\sqrt[q]{(-x)^p},\ \mbox{if $a = \frac{p}{q}$, rational in reduced form},\\ \mbox{undefined},\ \mbox{if $a$ is irrational} \end{cases}$$
This definition is basically one that generalizes how that
$$(-1)^{1/2}$$
is undefined on the real domain if thought of as a square root, because there is no real number who squares to -1, but
$$(-1)^{1/3}$$
can be thought of as a cube root, and, it turns out, -1 cubes to -1, thus we might be tempted (and a lot succumb to such temptation) to define
$$(-1)^{1/3} := -1$$
More generally, even roots are undefined for negatives, odd roots are defined. The problem with this definition is, of course, just what you've observed: it behaves pretty badly because the rationals densely intermix fractions with even and odd denominators, and looks really weerd (esp. try and contemplate graphing $y = (-2)^x$ ... lurkey ... VAAWQH!), while for positive $x$, things behave nicely.
To me, this is good reason I'd think to instead simply leave $x^a$ undefined when $x$ is a real number less than 0 and $a$ is a real number who is not an integer. (There are no problems defining when $a$ is an integer, of course.) And this doesn't mean you lose the ability to find the real solution of
$$x^3 = -1$$
and similar, it's just that you have to write it as
$$x = -(1^{1/3})$$
and not
$$x = (-1)^{1/3}$$
.
Sadly, the problem is convincing calculator manufacturers of this idea.
Cheers.


TITLE: Integral $\int_1^{\sqrt{2}}\frac{1}{x}\ln\left(\frac{2-2x^2+x^4}{2x-2x^2+x^3}\right)dx$
QUESTION [15 upvotes]: Calculate the following integral:
  \begin{equation}
\int_1^{\sqrt{2}}\frac{1}{x}\ln\left(\frac{2-2x^2+x^4}{2x-2x^2+x^3}\right)dx
\end{equation}

I am having trouble to calculate the integral. I tried to use by parts method but it didn't help. Wolfram Alpha gives me $0$ as the answer but I don't know how to get it. I also tried to search the similar question here and I got this:
$$I=\int_{-1}^1\frac1x\sqrt{\frac{1+x}{1-x}}\ln\left(\frac{2\,x^2+2\,x+1}{2\,x^2-2\,x+1}\right)\ \mathrm dx,$$
yet it didn't help much. Besides, I don't understand the answers there. Could anyone here please help me to calculate the integral preferably (if possible) with elementary ways (high school methods)? Any help would be greatly appreciated. Thank you.

REPLY [11 votes]: Similar problem (two answers)
$$
I = \int_1^{\sqrt{2}}\frac{1}{x}\log\left(\frac{2-2x^2+x^4}{2x-2x^2+x^3}\right)\mathrm{d}x
$$
Integrate by parts
$$
I = \left.\log(x)\log\left(\frac{2-2x^2+x^4}{2x-2x^2+x^3}\right)\right|_1^{\sqrt{2}}- \int_1^{\sqrt{2}}\log(x)\left(\frac{x^6-4 x^5+8 x^4-10 x^2+8 x-4}{x \left(x^2-2 x+2\right) \left(x^4-2 x^2+2\right)}\right)\mathrm{d}x
$$
Partial fractions
$$I = \frac{1}{2} \log (2) \log \left(\frac{2}{4 \sqrt{2}-4}\right) - \int_1^{\sqrt{2}}\log(x)\left(-\frac{2 (x-1)}{x^2-2 x+2}+\frac{4 \left(x^3-x\right)}{x^4-2 x^2+2}-\frac{1}{x}\right)\mathrm{d}x$$
It should be easy enough to show that $\int_1^\sqrt{2} \log(x)/x \,\mathrm{d}x = \left.\tfrac12 \log(x)^2\right|_1^\sqrt{2} = \tfrac18\log(2)^2$.
We are left with (after simplification)
$$I = -\frac{1}{8} \log (2) \left(\log (8)-4 \log \left(1+\sqrt{2}\right)\right) - \int_1^{\sqrt{2}}\log(x)\left(-\frac{2 (x-1)}{x^2-2 x+2}+\frac{4\! \left(x^3-x\right)}{x^4-2 x^2+2}\right)\mathrm{d}x$$
I will now show how to finish the evaluation$\def\I{\mathcal{I}}$
$$I_1 = \int_1^\sqrt{2} \frac{2(x-1)\log(x)}{x^2-2x+2} \mathrm{d}x$$
$$I_2 = \int_1^\sqrt{2} \frac{4x(x^2-1)\log(x)}{x^4-2x^2+2} \mathrm{d}x$$
The technique employ involves a partial fractions into the complex numbers. The first expression has a quadratic in the denominator and the second has a quadratic in $x^2$ in the denominator. It should be clear that it is sufficient to solve the equation in terms of
$$\I_1(a) = \int \frac{\log(x)}{x-a} \mathrm{d}x$$
$$\I_2(b) = \int \frac{x\log(x)}{x^2-b^2} \mathrm{d}x$$
The technique used will be geometric series expansions.
$$\I_1(a) = \int \frac{\log(x)}{1-x/a} \mathrm{d}x =  -\frac1a \sum_{n=0}^{\infty}\int\log(x)\frac{x^n}{a^n} \mathrm{d}x$$
Integrate by parts
$$\I_1(a) = -\sum_{n=0}^\infty \frac{a^{-(n+1)} x^{n+1}}{(n+1)^2}-\sum_{n=0}^\infty\frac{a^{-(n+1)} x^{n+1} \log (x)}{(n+1)}$$
The first sum is a series expansion of the polylogarithm function of order $2$. The second is also a series for the polylogarithm but it is of order $1$ so it is easily expressible in terms of the logarithm. In all,
$$\I_1(a) = \operatorname{Li}_2\!\left(\frac{x}{a}\right) + \log (x) \log \!\left(1-\frac{x}{a}\right)$$
A similar procedure shows that
$$\I_2(b) = \frac{1}{4}\! \left(\operatorname{Li}_2\left(\frac{x^2}{b^2}\right)+2\log (x) \log \left(1-\frac{x^2}{b^2}\right)\right)$$
Without adding unnecessary details, we need to find
$$2\I_2(\sqrt{1+i}) + 2\I_2(\sqrt{1-i}) -\I_1(1+i) - \I_1(1-i)$$
and then evaluate at $x = 1$ and $x = \sqrt{2}$. A large part of the evaluation goes to zero at $x = 1$ but we are not so fortunate at $x = \sqrt{2}$. What remains is a product of logarithms and a sum of several dilogarithms. These dilogarithms are very easy to evaluate because they all fit under certain dilogarithm identities which can be found here.
For the time being, I will not explicitly evaluate the final sum but that may come in the near future. With the dilogaithm identities, evaluation is more of a nuisance than anything. I will assure you that you do come across the value which zeros out the integral. Feel free to ask if you have any questions.


TITLE: Where I can find the Pythagorean theorem deduced from Hilbert's axioms?
QUESTION [6 upvotes]: Hilbert took years to make a rigorous revision and formalization of Euclidean geometry in his Foundations of Geometry. As he intended to organize only the most basic aspects of the theory, he didn't write about things like the Pythagorean Theorem or the sum of the angles of a triangle. He would say "it is easily deduced from the previous theorems." Even though it can be easy I don't seem to find any book where there is the Euclidean geometry presented as in the Euclid's Elements, but using Hilbert's axioms.
What I mean is: Is there an Elements of geometry as Euclid's, but deduced from Hilbert's rigorous axiomatic?

REPLY [3 votes]: Try Robin Hartshorne's book http://www.amazon.com/Geometry-Euclid-Beyond-Robin-Hartshorne/dp/0387986502.


text:
\section{Appendix C:Analysis of Section~\ref{sec:compress}}

First we prove the following lemma that will be useful in our subsequent calculations. Consider that $\cQ(\hat{\p})= \frac{1}{|B|}\sum_{i \in B}\cQ(\hat{\p}_i)$. And also we use the following notation
$ \zeta_B= \nu(\frac{\eta}{\sqrt{|B|}}+ \frac{\eta^2}{1-\eta})$,  $\nu= \frac{\sigma_{max}(\bA^{\top}\bA)}{\sigma_{max}(\bA^{\top}\bA)+n\lambda} \leq 1$.

\begin{lemma}\label{lem: useful}
If $\cQ(\hat{\p}_i)$ is the local update direction and $\p^*$ is the optimal solution to the quadratic function $\phi$ then
\begin{align*}
\left\| \bH^{\frac{1}{2}} (\cQ(\hat{\p}_i)-\p^* )\right\|^2 \leq  1+ \kappa (1-\rho) )\epsilon^2 + (\zeta^2_B + \kappa (1-\rho)((1+\zeta^2_1))\left\|\bH^{\frac{1}{2}} \p^* \right\|^2,
\end{align*}
 where $\bH$ is the exact Hessian and
  \begin{align*}
 \epsilon_1 &= \sqrt{(1+ \kappa (1-\rho) )}\epsilon, \\
 \zeta^2_{comp,B}&= (\zeta^2_B + \kappa (1-\rho)((1+\zeta^2_1)).
 \end{align*}
 $\epsilon$ is defined in equation~\eqref{eps} and
 \end{lemma}

 \begin{proof}
 \begin{align}
 \left\| \bH^{\frac{1}{2}} (\cQ(\hat{\p})-\p^* )\right\|^2 & = \left\| \bH^{\frac{1}{2}} (\cQ(\hat{\p}) -\hat{\p} +\hat{\p}-\p^* )\right\|^2 \nonumber \\
& \leq 2 \left( \underbrace{ \left\| \bH^{\frac{1}{2}} (\cQ(\hat{\p}) -\hat{\p}) \right\|^2}_{Term 1}  + \underbrace{ \left\|\bH^{\frac{1}{2}}( \hat{\p}-\p^* )\right\|^2}_{Term 2} \right). \label{u1}
 \end{align}
Following the proof of Lemma~\ref{lem:onernd}  we get
\begin{align}
 \left\| \bH^{\frac{1}{2}} (\hat{\p}_i -\p^*) \right\|^2 \leq \epsilon^2 +\zeta_1\left\|\bH^{\frac{1}{2}} \p^* \right\|^2,  \label{u2}
\end{align}
 where $\epsilon$ is as  defined in \eqref{eps}.Now we consider the term
 \begin{align*}
 \left\| \bH^{\frac{1}{2}} (\cQ(\hat{\p}_i) -\hat{\p}_i \right\|^2 & \leq \sigma_{max}(\bH)(1-\rho)  \left\| \hat{\p}_i \right\|^2 \\
 & \leq \sigma_{max}(\bH)(1-\rho) \left(  \left\| \hat{\p}_i -\p^* \right\|^2 +  \left\| \p^* \right\|^2 \right) \\
 & \leq \frac{\sigma_{max}}{\sigma_{min}}(1-\rho) \left(  \left\| \bH^{\frac{1}{2}} (\hat{\p}_i -\p^*) \right\|^2 +  \left\|\bH^{\frac{1}{2}} \p^* \right\|^2 \right)\\
&= \kappa(1-\rho) \left(  \left\| \bH^{\frac{1}{2}} (\hat{\p}_i -\p^*) \right\|^2 +  \left\|\bH^{\frac{1}{2}} \p^* \right\|^2 \right)\\
& \leq  \kappa(1-\rho) \left(  \epsilon^2 +  (1+\zeta_1^2)\left\|\bH^{\frac{1}{2}} \p^* \right\|^2 \right) \quad \text{Using \eqref{u2}}.
 \end{align*}
 Now we use the above calculation and  bound  Term1
\begin{align}
\left\| \bH^{\frac{1}{2}} (\cQ(\hat{\p}) -\hat{\p}) \right\|^2 & \leq \frac{1}{|B|}\sum_{i \in B} \left\| \bH^{\frac{1}{2}} (\cQ(\hat{\p}_i) -\hat{\p}_i \right\|^2 \nonumber \\
& \leq  \kappa (1-\rho) \left(  \epsilon^2 +  (1+\zeta^2_1)\left\|\bH^{\frac{1}{2}} \p^* \right\|^2 \right).  \label{u3}
\end{align}
 We can bound the Term2  directly using the proof of  Lemma~\ref{lem:onernd}
 \begin{align}
 \left\|\bH^{\frac{1}{2}}( \hat{\p}-\p^* )\right\|^2 \leq \epsilon^2 + \zeta^2_B\left\|\bH^{\frac{1}{2}} \p^* \right\|^2. \label{u4}
 \end{align}
Now we use \eqref{u3} and \eqref{u4} and plug them in \eqref{u1}
\begin{align*}
\left\| \bH^{\frac{1}{2}} (\cQ(\hat{\p})-\p^* )\right\|^2 & \leq (1+ \kappa (1-\rho) )\epsilon^2 + (\zeta^2_B + \kappa (1-\rho)((1+\zeta^2_1))\left\|\bH^{\frac{1}{2}} \p^* \right\|^2.
\end{align*}
 Now we define
 \begin{align*}
 \epsilon_1 &= \sqrt{(1+ \kappa (1-\rho) )}\epsilon \\
 \zeta^2_{comp,B}&= (\zeta^2_B + \kappa (1-\rho)((1+\zeta^2_1)).
 \end{align*}
\end{proof}
Now we have the robust update in iteration $t$ to be $\cQ(\hat{\p}) = \frac{1}{|\cU_t|} \sum_{i \in \cU_t}\cQ(\hat{p}_{i,t})$.
\begin{lemma}\label{lem:combyzone}
Let $\{\bS_i\}_{i=1}^m \in \mathbb{R}^{n \times s}$  be sketching matrices based on  Lemma~\ref{lem:Hessketch}. Let $\phi_t$ be defined in \eqref{quad} and $\cQ(\hat{\p}_t)$ be the update with $\cQ$ being $\rho$-approximate compressor. It holds that
\begin{align*}
\min_{\p}\phi_t(\p) \leq \phi_t(\cQ(\hat{\p}_t))& \leq \epsilon_{comp,byz}^2 + (1 - \zeta^2_{comp,byz})\phi_t(\p^*),
\end{align*}
where $\epsilon_{comp,byz}$ and $\zeta^2_{comp,byz}$ is as defined in ~\eqref{ceps} and ~\eqref{calpha} respectively.
\end{lemma}
\begin{proof}
In the following analysis we omit the subscript '$t$'. From the definition of the quadratic function \eqref{quad} we know that
\begin{align*}
    \phi(\cQ(\hat{\p})) - \phi(\p^*) & = \frac{1}{2}\|\bH^{\frac12}(\cQ(\hat{\p})-\p^*)\|^2.
\end{align*}
Now we consider
\vspace{-10pt}
\begin{align*}
  \frac{1}{2} \|\bH^{\frac12}(\cQ(\hat{\p})-\p^*)\|^2 & = \frac{1}{2}\|\bH^{\frac12}(\frac{1}{|\cU|}\sum_{i \in \cU}\cQ(\hat{\p}_i)-\p^*)\|^2  \\
   &=\frac{1}{2}\|\bH^{\frac12}\frac{1}{|\cU|}(\sum_{i \in \cM}(\cQ(\hat{\p}_i)-\p^*) -\sum_{i \in (\cM\cap\cT)}(\cQ(\hat{\p}_i)-\p^*)+\sum_{i \in (\cU\cap\cB)}(\cQ(\hat{\p}_i)-\p^*) )\|^2 \\
   &\leq \underbrace{ \|\bH^{\frac12}\frac{1}{|\cU|}(\sum_{i \in \cM}(\cQ(\hat{\p}_i)-\p^*)\|^2}_{Term 1} + \underbrace{ 2\|\bH^{\frac12}\frac{1}{|\cU|}\sum_{i \in (\cM\cap\cT)}(\cQ(\hat{\p}_i)-\p^*)\|^2 }_{Term 2} \\
   &+ \underbrace{2\|\bH^{\frac12}\frac{1}{|\cU|}\sum_{i \in (\cU\cap\cB)}(\cQ(\hat{\p}_i)-\p^*) )\|^2}_{Term 3}.
\end{align*}
Now we bound each term separately and use the Lemma~\ref{lem: useful}
\begin{align*}
    Term 1 &=  \|\bH^{\frac12}\frac{1}{|\cU|}(\sum_{i \in \cM}(\cQ(\hat{\p}_i)-\p^*)\|^2 \\& = (\frac{1-\alpha}{1-\beta})^2 \|\bH^{\frac12}\frac{1}{|\cM|}(\sum_{i \in \cM}(\cQ(\hat{\p}_i)-\p^*)\|^2 \\
   & \leq (\frac{1-\alpha}{1-\beta})^2 [\epsilon_1^2+ \zeta^2_{comp,\cM}\|\bH^{\frac{1}{2}}\p^*\|^2],
\end{align*}
where $\zeta^2_{comp,\cM} = (\zeta^2_{\cM} + \kappa (1-\rho)((1+\zeta^2_1)$. Similarly  the Term 2 can be bonded as it is a bound on good machines
\begin{align*}
    Term 2 & = 2\|\bH^{\frac12}\frac{1}{|\cU|}\sum_{i \in (\cM\cap\cT)}(\cQ(\hat{\p}_i)-\p^*)\|^2 \\
    & = 2 (\frac{1-\alpha}{1-\beta})^2 \|\bH^{\frac12}\frac{1}{|\cM\cap\cT|}\sum_{i \in (\cM\cap\cT)}(\cQ(\hat{\p}_i)-\p^*)\|^2\\
    & \leq 2(\frac{1-\alpha}{1-\beta})^2 [\epsilon_1^2 + \zeta^2_{comp,\cM\cap\cT}\|\bH^{\frac{1}{2}}\p^*\|^2].
\end{align*}
For the Term 3 we know that $\beta > \alpha $ so all the untrimmed worker norm is bounded by a good machine as at least one good machine gets trimmed.
\begin{align*}
    Term 3 & = 2\|\bH^{\frac12}\frac{1}{|\cU|}\sum_{i \in (\cU\cap\cB)}(\cQ(\hat{\p}_i)-\p^*) )\|^2 \\
    & \leq 2\sigma_{max}(\bH)(\frac{|\cU\cap\cB|}{|\cU|})^2 \|\frac{1}{|\cU\cap\cB|}\sum_{i \in (\cU\cap\cB)}(\cQ(\hat{\p}_i)-\p^*) )\|^2 \\
    & \leq 2\sigma_{max}(\bH)(\frac{|\cU\cap\cB|}{|\cU|})^2 \frac{1}{|\cU\cap\cB|}\sum_{i \in (\cU\cap\cB)}\|(\cQ(\hat{\p}_i)-\p^*) )\|^2\\
   & \leq 4\sigma_{max}(\bH)(\frac{|\cU\cap\cB|}{|\cU|})^2 \frac{1}{|\cU\cap\cB|}\sum_{i \in (\cU\cap\cB)}(\|\cQ(\hat{\p}_i)\|^2+ \|\p^*\|^2) \\
   & \leq 4\sigma_{max}(\bH)(\frac{|\cU\cap\cB|}{|\cU|})^2 \max_{i \in \cM}(\|\cQ(\hat{\p}_i)\|^2+ \|\p^*\|^2)\\
   & \leq 4\sigma_{max}(\bH)(\frac{|\cU\cap\cB|}{|\cU|})^2 \max_{i \in \cM}(\|\cQ(\hat{\p}_i)- \p^*\|^2+ 2\|\p^*\|^2)\\
   & \leq 4\kappa (\frac{|\cU\cap\cB|}{|\cU|})^2 \max_{i \in \cM}(\|\bH^{\frac{1}{2}}(\cQ(\hat{\p}_i)- \p^*)\|^2+ 2\|\bH^{\frac{1}{2}}\p^*\|^2)\\
   &\leq   4\kappa (\frac{|\cU\cap\cB|}{|\cU|})^2(\epsilon_1^2 + (2+\zeta^2_{1})\|\bH^{\frac{1}{2}}\p^*\|^2)\\
   &\leq   4\kappa (\frac{\alpha}{1-\beta})^2(\epsilon_1^2 + (2+\zeta^2_{1})\|\bH^{\frac{1}{2}}\p^*\|^2).

\end{align*}
Combining all the bounds on Term1 , Term2 and Term3 we have
\begin{align*}
  \frac{1}{2} \|\bH^{\frac12}(\hat{\p}-\p^*)\|^2 & \leq    \epsilon_{byz}^2+ \zeta^2_{byz}\|\bH^{\frac{1}{2}}\p^*\|^2,
\end{align*}
where
\begin{align*}
    \epsilon_{comp,byz}^2 &= \left(3 \left(\frac{1-\alpha}{1-\beta} \right)^2 +4\kappa \left(\frac{\alpha}{1-\beta}\right)^2 \right)\epsilon_1^2 \\

    \zeta^2_{comp,byz} & =2\left(\frac{1-\alpha}{1-\beta}\right)^2\zeta^2_{comp,\cM\cap\cT} + \left(\frac{1-\alpha}{1-\beta}\right)^2\zeta^2_{comp,\cM} + 4\kappa  \left(\frac{\alpha}{1-\beta}\right)^2 (2+\zeta^2_{comp,1}).
\end{align*}
Finally we have
\begin{align*}
 \phi(\hat{\p}) - \phi(\p^*) &  \leq  \epsilon_{comp,byz}^2- \zeta^2_{comp,byz}\phi(\p^*) \\
 \Rightarrow \phi(\hat{\p}) & \leq \epsilon_{comp,byz}^2 + (1 - \zeta^2_{comp,byz})\phi(\p^*).
\end{align*}
\end{proof}

\begin{lemma}\label{lem:compbyzdelta}
Let $\zeta_{comp,byz} \in (0,1),\epsilon_{comp,byz}$ be any fixed parameter. And $\cQ(\hat{p}_t)$ satisfies $\phi_t(\cQ(\hat{p}_t)) \leq \epsilon_{byz}^2+ (1 -\zeta_{byz}^2) \min_{\p}\phi_t(\p)$. Under the Assumption~\ref{asm:hess}(Hessian $L$-Lipschitz) and
$\mathbf{\Delta}_t =\w_t-\w^*$ satisfies
\begin{align*}
\mathbf{\Delta}^T_{t+1}\bH_t\mathbf{\Delta}_{t+1}& \leq L\| \mathbf{\Delta}_{t+1}\|\|\mathbf{\Delta}_t\|^2 +  \frac{\zeta^2_{comp,byz}}{1-\zeta^2_{comp,byz}}\mathbf{\Delta}_t^T\bH_t\mathbf{\Delta}_t + 2\epsilon_{comp,byz}^2.
\end{align*}
\end{lemma}

\begin{proof}
 We choose $\zeta= \zeta_{comp,byz}$ and $\epsilon=\epsilon_{comp,byz}$ from the Lemma~\ref{lem:combyzone} and follow  the proof of Lemma~\ref{lem:delta} to obtain the desired bound.
\end{proof}

\textbf{Proof of Theorem~\ref{thm:compbyzsmooth} }
\begin{proof}
 We get the desired bound by developing from the result of the Lemma~\ref{lem:compbyzdelta} and following the proof of Theorem~\ref{thm:smooth}
\end{proof}

config: arxiv


TITLE: Functional Square Root of Digit Sum?
QUESTION [4 upvotes]: Define $\text{sdig}(n)$ to be the sum of the decimal digits of $n$, where $n$ is a positive integer. My question is as follows:

Does there exist a function $h:\mathbb Z^+\mapsto\mathbb Z^+$ such that
  $$(h\circ h)(n)=\text{sdig}(n)$$
  for all $n\in\mathbb Z^+$? That is, does there exist a functional square root of the digit sum function?

So far, this problem has stumped me. I've shown that if such $h$ exists, it must commute with the digit sum function. I've also shown that if $S_a$ is the set of numbers whose digit sum is $a$, then for all $a$, there exists some $b$ such that the function $h$ maps all elements of $S_a$ to elements of $S_b$. However, whether these discoveries lead to the construction of such a function or the proof of its nonexistence I do not know.
Any ideas?

REPLY [2 votes]: I think you can by building $h(n)$ up by digit sums.  It seems natural to set $h(n)=n$ for $n \lt 10$.  Now you can let $h(n)=\operatorname{sdig}(n)$ if $10 \le 10\le 18$.  Then we can let $h(n)=\operatorname{sdig}(n)+9$ if $\operatorname{sdig}(n)\le 9$ The first value we have not yet accounted for is $h(19)$.  If $h(19)=a,$ we need $h(a)=10$ and then we need $h(h(a))=1$, so we pick a convenient $a$ like $100$ and set $h(19)=100$.  Now we can set $h(n)=100$ if $\operatorname{sdig}(n) = 10$.  The next one we need to handle is $h(29)$.  Again, if $h(29)=b,$ we need $h(b)=11$ and $h(h(b))=2$, so $\operatorname{sdig}(b)=2$. We can set $h(n)=101$ if $\operatorname{sdig}(n) = 11$.  I think you can just keep building up $h(n)$ from the digit sums this way.  We have two tables
$$\begin {array} {r |r}n&h(n)\\ \hline 1-9&n\\10-18&n-9 \end {array}$$
$$\begin {array} {r |r}\operatorname{sdig}(n)&h(n)\\ \hline
1-9&\operatorname{sdig}(n)
\\10-19&\operatorname{sdig}(n)+90
\\20-99&\operatorname{sdig}(n)+900 \end {array}$$
Now if we have a number $k$ with sum of digits $19$ we need $h(h(k))=19$ and $h(k)$ needs a digit sum of $10$.  $109$ works well and we can extend the bottom row of the table to cover $\operatorname{sdig}(n)$ of $19$.  Because $h(20)=11$ wherever we send digit sums of $20$ has to have a digit sum of $11$.  $920$ looks like a nice number and we can add a line to the table.  For a sum of digits of $30$ we have $h(30)=12$ so we need to send it somewhere that has a sum of digits of $12$.  We observe that we can extend the bottom line to cover digit sums up to $99$.  It seems clear we can keep going.


TITLE: Prove that $\mathbb{P}[(\limsup A_n)-A_n]\rightarrow 0$
QUESTION [1 upvotes]: Problem: This is a problem from Problems in Probability by Shiryaev (Problem 2.1.16). It is worded as following: Let $A^*=\limsup A_n$. Prove that $\mathbb{P}(A^* -A_n)\rightarrow 0$
Attempt: I tried rewriting the expression in different forms. But none of them works. I think the following observation is crucial: let $\{x_n\}_{n\in\mathbb{N}}$ be defined as $x_n=\mathbb{P}(\bigcup_{k=1}^{n}A_k)$. Then we know $x_n$ converges to limit $x:=\mathbb{P}(\bigcup_{n=1}^{\infty}A_n)$. So for sufficiently large $n$, we have that $x-x_N=\mathbb{P}([\bigcup_{n=1}^{\infty}A_n]\backslash[\bigcup_{n=1}^{N}A_n])<\epsilon$, where $\epsilon$ is arbitrary.

REPLY [1 votes]: Let $(\Omega,\mathcal{F},P)$ be a probability space. Let $(A_{n})_n$
be a sequence in $\mathcal{F}$. Define $A=\limsup_{n}A_{n}:=\cap_{n=1}^{\infty}\cup_{k=n}^{\infty}A_{k}$.
We go to prove that $\lim_{n\rightarrow\infty}P(A_{n}\setminus A)=0$.
Proof: For each $n$, let $B_{n}=\cup_{k\geq n}A_{k}$. Then $(B_{n}\cap A^{c})_n$
is a decreasing sequence and $\cap_{n}(B_{n}\cap A^{c})=(\cap_{n}B_{n})\cap A^{c}=A\cap A^{c}=\emptyset$.
By continuity of finite measure, we have $\lim_{n\rightarrow\infty}P(B_{n}\cap A^{c})=P(\cap_{n}(B_{n}\cap A^{c}))=0$.
Finally, observe that $A_{n}\cap A^{c}\subseteq B_{n}\cap A^{c}$.
It follows that $\lim_{n\rightarrow\infty}P(A_{n}\cap A^{c})=0$.


TITLE: matrix logarithm, determination and trace maxmimzation
QUESTION [0 upvotes]: Let $A = A^\ast \in M_n$ be a positive definite matrix ($\lambda_i(A) > 0$). Show that
$\log\det(A)-Tr(A)$
is maximized by $A = I$.

REPLY [1 votes]: Note that if $\lambda_i>0$, $i=1,\ldots,n$, are the eigenvalues of $A$, then
$$\tag{$*$}
\log\det(A)-\mathrm{tr}(A)=\log\prod_{i=1}^n\lambda_i-\sum_{i=1}^n\lambda_i=\sum_{i=1}^n f(\lambda_i), \quad f(\lambda)=\log\lambda-\lambda.
$$
The function $f$ has on $(0,\infty)$ the global maximum at $\lambda=1$ and hence ($*$) has the global maximum at $\lambda_1=\cdots=\lambda_n=1$. Hence $A=I$ maximises ($*$).


TITLE: Restricted Compositions
QUESTION [7 upvotes]: Number Composition studies the number ways of compositing a number.
I wanna know the number of compositions of $m$ with $n$ parts with the size of the max part equal to or less than $k$.
Is there a closed form for this problem?

REPLY [4 votes]: For big $N$, $K$, an coarse approximation can be obtained by a probabilistic argument. I get
$$C(N,M,K) \approx \left( 1 - \left( 1- \frac{K}{N}\right)^M \right)^K {N-1 \choose K-1}$$
The approximation is good if the first factor (which represents the restriction) is not very small (say, $>0.1$)
Some examples: (exact and approximate values
 N   K   M      exact        approx      factor
 40  20  5    3.556E+010   3.653E+010    0.523
 40  20  8    6.610E+010   6.373E+010    0.924
 40  20  3    3.774E+008   4.770E+009    0.069


TITLE: Why do two different approaches using matrix algebra yield different results?
QUESTION [2 upvotes]: I am solving a problem involving linear regression and I am finding that two different approaches to the matrix algebra is yielding different results.
In the second approach, I am merely simplifying the second component of the expression first. As you can see, the results are vastly different. Intuitively, I think the first approach is correct but I can't figure out what is wrong with the second approach to yield such a different answer.
Here, we assume $M_{x} = I -X(X'X)^{-1}X'$ and $X'X$ is non-singular. I am hoping that your answer will help me better understand matrix algebra!
Approach 1:
$$
X'(M_{x})^{-1}X - X'(M_{x})^{-1}X(X'X)^{-1}(X'X) \\
X'(M_{x})^{-1}[I -X(X'X)^{-1}X']X \\
X'(M_{x})^{-1}M_{x}X \\
X'X
$$
Approach 2:
$$
X'(M_{x})^{-1}X - X'(M_{x})^{-1}X(X'X)^{-1}(X'X) \\
X'(M_{x})^{-1}X - X'(M_{x})^{-1}X \\
0
$$

REPLY [3 votes]: As @Rahul noted in comment, $M_x$ is not invertible since
$$
X'M_x=X'(I -X(X'X)^{-1}X') = X' - (X'X)(X'X)^{-1}X' = \mathbb 0
$$
where the result is zero rectangular matrix. It means that all rows of $M_x$ are linearly dependent and $M_x$ is singular.


TITLE: How fast is the area of the rectangle increasing?
QUESTION [2 upvotes]: The length of a rectangle is increasing at a rate of 8 cm/s and its width is increasing at a rate of 3 cm/s . When the length is 20 cm and the width is 10 cm, how fast is the area of the rectangle increasing?
To set up the equation, I have $A=lw$. Differentiate both sides of the equation, I have $\dfrac{dA}{dt}=\dfrac{dl}{dt}l+\dfrac{dw}{dt}w=\dfrac{dA}{dt}=(8.20)+(10.3)=510$.
The solution manual says $140$ and the equation is set$\dfrac{dA}{dt}=\dfrac{dw}{dt}l+\dfrac{dl}{dt}w$. Why does the equation is set this way? I thought that the rate of increase of the length must be paired with length and the rate of change of width should be paired with width? So what's going on here?

REPLY [0 votes]: I think you want to know why the terms $l$ and $\frac{dl}{dt}$ are not related and the terms $l$ and $\frac{dw}{dt}$ are related in the formula for area of a rectangle. Let us consider a simple case of a rectangle with length $l$ and width $w$.

 Now let us increase the length by an amount $dl$ and the width by an amount $dw$. So what will be the change in the area? You can see that as soon as you increase both length as well as the width the rectangle changes from $OPRS$ to rectangle $OLMN$. The change in the area is the additional area of the rectangle $RBMC$.
The area of the rectangle initially was $A=lw$.
The area of the rectangle after increasing the length and width becomes $A+dA$.
$$A+dA=(l+dl)(w+dw)$$
$$A+dA=lw+dl(w)+l(dw)+(dl)(dw)$$
$$lw+dA=lw+dl(w)+l(dw)+(dl)(dw)$$
$$dA=dl(w)+l(dw)+(dl)(dw)$$
Now, we assume two things, first this change in length as well as width is very small and tends to $0$. So we can ignore the term, $(dl)(dw)$ in the formula to get:
$$dA=dl(w)+l(dw)$$
Now maybe you are getting the pattern of the formula and why the rate $dw$ is related with $l$ instead of $w$. The second assumption is we change the length and width in a very short period of time $dt$ which is very small and tends to $0$.
So we can calculate the rate of change of area as :
$$\frac{dA}{dt}=w\frac{dl}{dt}+l\frac{dw}{dt}$$
Actually, the changes are denoted by $\triangle$, and then we let this change tend to $0$, so the change $\triangle l \rightarrow dl$.
The rest of the calculations are easy and have been told wonderfully by other members.
Hope this helps...


TITLE: How to find $\lim\limits_{n\rightarrow \infty}\frac{(\log n)^p}{n}$
QUESTION [1 upvotes]: How to solve $$\lim_{n\rightarrow \infty}\frac{(\log n)^p}{n}$$

REPLY [0 votes]: If $p\leq 0$,then the result is $0$, which is trivial. We need consider the case when $p>0$ only. Let $ \alpha=\frac1 p>0$, then
\begin{align*} \lim_{n \to \infty}\frac{\ln n}{n^{\alpha}}&=\lim_{n \to \infty}\frac{\ln(n+1)-\ln n}{(n+1)^{\alpha}-n^{\alpha}}&\text{Stolz}\\ &=\lim_{n \to \infty}\frac{\ln\left(1+\frac{1}{n}\right)}{n^{\alpha}\left[\left(1+\frac{1}{n}\right)^{\alpha}-1\right]}&\ln(1+x)\sim x,(1+x)^{\alpha}\sim \alpha x(x \to 0)\\ &=\lim_{n \to \infty}\frac{\frac{1}{n}}{n^{\alpha}\cdot\frac{\alpha}{n}}\\ &=\lim_{n \to \infty}\frac{1}{\alpha n^{\alpha}}\\ &=0 .\end{align*}
Therefore
$$\lim_{n \to \infty}\frac{\ln^p n}{n}=\lim_{n \to \infty}\left(\frac{\ln n}{n^{\alpha}}\right)^p=\left(\lim_{n \to \infty}\frac{\ln n}{n^{\alpha}}\right)^p=0.$$


TITLE: Characterization finitely generated $\mathbb{Z}$-module of $\mathbb{Q}$
QUESTION [0 upvotes]: It is well-known that $\mathbb{Q}$ is not finitely generated as $\mathbb{Z}$-module. Moreover, if we consider $\mathbb{Z}_{(2)}$, it is a proper $\mathbb{Z}$-submodule of $\mathbb{Q}$ which is not finitely generated.
Well, my question is: there exists a characterization of finitely generated $\mathbb{Z}$-submodules of $\mathbb{Q}$?

REPLY [4 votes]: Yes: they're exactly the cyclic submodules, because if you call $m=\prod_{j=1}^k m_j$, then $$\Bbb Z\frac{n_1}{m_1}+\cdots+\Bbb Z\frac{n_k}{m_k}=\Bbb Z\frac{\operatorname{gcd}\left(\frac m{m_1}n_1,\cdots, \frac{m}{m_k}n_k\right)}{m}$$
by Bézout's theorem.


TITLE: Difference between $c=1$ Dirac CFT and two copies of $c=\frac{1}{2}$ Majorana CFT?
QUESTION [7 upvotes]: The $c = \frac{1}{2}$ (non-chiral) Majorana CFT has six primary fields: the vacuum 1, the two Majorana fields $\eta, \bar \eta$ $\left( \Delta_\eta = \Delta_{\bar \eta} = \frac{1}{2}\right)$, the energy field $\varepsilon$ $\left( \Delta_\varepsilon =1\right)$, the twist field $\sigma$ $\left( \Delta_\sigma =\frac{1}{8}\right)$ and the disorder field $\mu$ $\left( \Delta_\mu =\frac{1}{8}\right)$. The latter two are non-local, whereas the rest are local. (This is relevant as it means that e.g. for anti-periodic spatial boundary conditions (APBC), the first four fields determine the finite-size energy spectrum.)
Now my question: to what extent can I think of the $c=1$ Dirac CFT as two copies of this $c = \frac{1}{2}$ CFT? I think that from a finite-size scaling point of view, this should be fine, hence I would expect both theories to have the same set of local primary fields (e.g., I guess the Dirac CFT has four primary fields with scaling dimension $\Delta =\frac{1}{2}$, is that true?). However, two copies of the $c=\frac{1}{2}$ CFT would, for example, have two twist fields $\sigma_{1,2}$, but I would be surprised if the Dirac CFT has two such fields?

REPLY [3 votes]: Alright, let me try to answer my own question.
First off, I suspect the $c=1$ Dirac CFT can indeed be seen as a stack of two $c=\frac{1}{2}$ Majorana CFTs. However, the subtlety lies elsewhere: the stack of two such fermionic CFTs is somewhat non-trivial. Indeed, fermions are never fully decoupled: they always anti-commute. For that reason, one can (as I was implicitly doing in my question above) consider a field $\boldsymbol{\sigma \times 1}$ (where we take a twist field of one of the $c=\frac{1}{2}$ CFTs and the vacuum of the other) but it is a most curious beast: it is neither bosonic or fermionic. For example, it anti-commutes with the fermionic field $\psi \times 1$ but commutes with the fermionic field $1\times \psi$. Now, I don't have enough affinity with these matters to see whether or not this means that we should exclude it all-together (honestly, I don't strictly see why), but at the very least it means it is not a conventional twist field. Instead, we can construct (parity-odd) twist fields $\boldsymbol{\sigma \times \mu}$ and $\boldsymbol{\mu \times \sigma}$. Hence we expect two parity-odd twist fields, each with dimension $\left( \frac{1}{8}, \frac{1}{8} \right)$ ---to be contrasted to the $\left( \frac{1}{16}, \frac{1}{16} \right)$ that we would have assigned to $\sigma \times 1$ and $1\times \sigma$. (Similarly we expect the two 'disorder'/parity-even twist fields $\mu \times \mu$ and $\sigma \times \sigma$.)
Now we can check whether this is compatible from the $c=1$ Dirac CFT point of view. As for example discussed in the beautiful lecture notes by McGreevy, one can consider the primary fields
$$ \mathcal V_{\alpha,\beta} (z, \bar z)= e^{\boldsymbol{\mathrm i} \left( \alpha \phi_L(z) + \beta \phi_R(\bar z) \right)}  $$
for any (half-)integer $\alpha,\beta$ with the conditions $\alpha-\beta,\alpha+\beta \in \mathbb Z$. This has the conformal dimension $\left( \frac{\alpha^2}{2}, \frac{\beta^2}{2}\right)$.
Firstly, there are the four fermionic fields $\mathcal V_{\pm 1,0}, \mathcal V_{0,\pm 1}$, all with scaling dimension $\Delta = h + \bar h = \frac{1}{2}$. These operators are local (in the fermionic language) and correspond to the four fields I mentioned in the original post above (or more precisely, some linear combination thereof). So far, so good.
Then moving on to the twist fields. We have the two parity-odd $\mathcal V_{\frac{1}{2},\frac{1}{2}}$ and $V_{-\frac{1}{2},-\frac{1}{2}}$. This has the conformal dimension $\left( \frac{1}{8},\frac{1}{8} \right)$. This is compatible with the two twist fields I discussed in the first paragraph of this answer. Similarly, we have the parity-even $\mathcal V_{\frac{1}{2},-\frac{1}{2}}$ and $V_{-\frac{1}{2},\frac{1}{2}}$, consistent with the two 'disorder' fields derived at from the above 'stacked $c=\frac{1}{2}$' point of view.
Now, while I do suspect that the above forms the essential answer to my question, it is quite likely that there are some further subtleties that deserve mentioning (or that I simply screwed something up). I hope some people who know their CFT are willing to comment to clear such things up :)


TITLE: Why does my fireplace shoot flames out the front until I open my backdoor?
QUESTION [14 upvotes]: I have a natural gas fireplace with fake logs in it. I open the flue, turn on the gas for a couple seconds, and throw a match in. The flames kind of go up and out of the flue, but most of the flames go out of the fireplace, towards the front (almost burning the wall).
Then, when I open my backdoor, something "equalizes" and the flames start going perfectly straight up and out of the flue.
The flue connects to a chimney that goes up about two stories.
To give some context, I live in Texas where there's pretty high humidity, and right now the outside temperature is about 40 degrees F, and the inside temperature is about 75 degrees F.
EDIT
Thank you for all the helpful answers. I just want to clarify, once I open the backdoor one time, the flames go up the flue and through the chimney like they're supposed to and stay that way, even if I close the door again. The flames only come out of the front of the fireplace until I open and shut the door one time, and then everything works like it's supposed to.

REPLY [0 votes]: To understand what's happening here, let's start with understanding what a fireplace is: A fireplace is a heat engine that does work by sucking the air from your room and ejecting it as hot fumes via the flue. Your backdoor serves as a kind of throttle.
What happens when you fire it up for the first time: the air in the flue forms a "cold plug". It's not very cold, as the air is at room temperature and it's not a real plug - but it's way colder than the hot fumes should be and it doesn't float up as they do. From the point of view of your heat engine - it's a plugged exhaust. So the flames have nowhere to go but your room (probably, you have another form of ventilation that serves as a flue for the moment). The engine is seized, too weak to pull more air in through the closed door and too weak to push the plug out.
So what happens when you open the door once? With inflow air unrestricted, the engine finally has enough power to push the cold air through the chimney and the machinery (that is: hot fumes flowing up the flue) cranks up to full speed.
When you close the door now, it won't change much: the obstruction is cleared: the flue is hot and the engine is revving: It has enough power to suck enough air through the closed door.


TITLE: Series question,related to telescopic series, 1/2*4+ 1*3/2*4*6+ 1*3*5/2*4*6*8 ...infinity
QUESTION [3 upvotes]: The series is $$\frac{1}{2*4}+ \frac{1*3}{2*4*6}+ \frac{1*3*5}{2*4*6*8}+....$$
It continues to infinity.I tried multiplying  with $2$ and dividing each term by$(3-1)$,$(5-3)$ etc,starting from the second term which gives me $$\frac{1}{8} -\frac{1}{4*6} -\frac{1}{4*6*8}-\frac{1}{4*6*8*10}$$.
Also if anybody is wondering the answer 0.5

REPLY [2 votes]: We have
$$
\begin{align}
\frac{1\cdot 3\cdot 5 \cdots(2n-1)}{2\cdot 4\cdot 6\cdots(2n+2)}&=\frac{1\cdot 2\cdot 3\cdot 4 \cdot 5\cdot6\cdots(2n-1)\cdot 2n}{(2\cdot 4\cdot 6\cdots (2n))^2(2n+2)}\\\\
&=\frac{(2n)!}{(2^{n} \cdot 1\cdot 2\cdot 3 \cdot 4 \cdots n)^2 \cdot (2n+2)}\\\\
& =\frac{(2n)!}{2^{2n} (n!)^2 \cdot (2n+2)}\\\\
&=\frac{1}{(2n+2)\,4^n}\binom{2n}{n}\\\\&=\frac{1}{4^n}\binom{2n}{n}-\frac{1}{4^{n+1}}\binom{2n+2}{n+1}.
\end{align}
$$
The series is then telescopic:
$$\sum_{n=1}^{N}\frac{1\cdot 3\cdot 5 \cdots(2n-1)}{2\cdot 4\cdot 6\cdots(2n+2)}=\frac{1}{2}-\frac{1}{4^{N+1}}\binom{2N+2}{N+1}.
$$As $N$ is great, one may prove that
$$\frac{1}{4^{N+1}}\binom{2N+2}{N+1}=O\left(\frac{1}{\sqrt{N}}\right).
$$
The series is thus equal to $\dfrac{1}{2}$:

$$\sum_{n=1}^{\infty}\frac{1\cdot 3\cdot 5 \cdots(2n-1)}{2\cdot 4\cdot 6\cdots(2n+2)}=\frac{1}{2}.
$$


TITLE: Set containing another set but having same measure
QUESTION [3 upvotes]: A set of real numbers is said to be a $G_{\delta}$ set provided it is the intersection of a countable collection of open sets. Show that for any bounded set $E$, there is a $G_{\delta}$ set $G$ for which $$E\subseteq G\text{ and }m^*(G)=m^*(E)$$

I want to define $G_n$ to be the the union of open balls of size $1/n$ around every point in $E$, i.e. $G_n=\bigcup_{x\in E}B_{1/n}(x)$. Then take $G=\bigcap_{n\in\mathbb{Z}^+}G_n$
Clearly $E\subseteq G$. Also, $G_n$ is an open set, since it's a union of open balls. Then $G$ is an intersection of a countable collection of open sets.
I need to prove $m^*(G)=m^*(E)$. Since $E\subseteq G$, I know $m^*(G)\geq m^*(E)$. How can I prove they're equal?

REPLY [1 votes]: As written, this is not the case. Consider the rationals in $[0,1]$. This is measure $0$ but each $G_n$ will have at least measure $1$.
Try directly using the definition of outer measure to get a countable collection of open sets that approximate the measure of $E$.


text:
\begin{document}

\maketitle

\begin{abstract}
 \input{0_Abstract}
\end{abstract}

\tableofcontents

\input{1_Introduction}

\input{2_Model_problem}

\input{3_Numerical_Methods}

\input{4_Error_bound_semidiscrete_Lobatto}

\input{5_Error_bound_semidiscrete_Gauss}

\input{6_Numerics}

\input{7_Generalisation}

\input{8_Summary}

\input{Appendix}

\section*{Acknowledgements}

This first author was supported by SVF project ``Solving advection dominated
problems with high order schemes with polygonal meshes: application to compressible
and incompressible flow problems''
and the second author was supported by the German Research Foundation (DFG,
Deutsche Forschungsgemeinschaft) under Grant SO~363/14-1.

\bibliographystyle{spmpsci}
\bibliography{literature}

\end{document}


TITLE: Given any subset of $[1, 2, ..., n]$, can its sum mod $(n) + 1$ be changed to any value between $1$ and $n$?
QUESTION [0 upvotes]: Given any subset of $[1, 2, ..., n]$, can its sum $\bmod n + 1$ be changed to any value between $1$ and $n$ by adding a value from the original set or removing a value from the subset?
For example: given $n = 4$ and the subset $[1, 3, 4]$ from the original set $[1, 2, 3, 4]$, it's possible to change the subset sum, which is $8$, taken $\bmod 4 + 1$, which is $1$, to $4$ by removing $1$ from the subset. Thus, we have $((3 + 4) \bmod 4) + 1 = 4$.

REPLY [1 votes]: No.
If $a$ is in the subset and $n-a$ is not, then adding $n-a$ to the subset has the same effect as removing $a$. Hence in such a situation, the $n$ possible actions you can take cannot produce $n$ distinct results. Indeed, in the worst case (e.g., picking the subset $\{1,2,\ldots\lfloor \frac n2\rfloor\}$ you can only achieve about 50% of the desired results


TITLE: Standard deviation of phase for a random phasor sum
QUESTION [2 upvotes]: I have a phasor sum
$a e^{j \theta} = \frac{1}{\sqrt{N}} \sum_{k=1}^{N} \alpha_k e^{j \phi_k }$
where $\phi_k = [-\pi, \pi]$, the standard deviation $\sigma_{\phi}$ of the phase is known and the mean of the phase is $\mu_\phi = 0$.
What is the standard deviation of $\theta$?

REPLY [2 votes]: In general is very unlikely to get closed form expression in $\theta$ and this is why:
Variance of the left side can be calculated by using Taylor expression for the exponent. Doing this we have to engage not only mean and variance of $\theta$ but all higher moments. Higher moments expression can be presented in closed form for only certain probability distribution functions. Then we get an equation on $\theta$ that, in general case, can not be solved analytically.
Right side can be calculated knowing probability distribution function for $\phi_i$ and its higher moments. If all $\phi_i$ are independent and means are zero - it simplify the calculation, but knowledge of all higher moments or probability distribution function is necessary.
If your variables come from certain known physical process where distribution function is known - it still require some effort to plug everything in and put some effort to come with closed form solution.