text:
(*  Title:      Well-Quasi-Orders
    Author:     Christian Sternagel <c.sternagel@gmail.com>
    Maintainer: Christian Sternagel
    License:    LGPL
*)

section \<open>Multiset Extension of Orders (as Binary Predicates)\<close>

(*TODO: move theory (and maybe rename)*)

theory Multiset_Extension
imports
  Open_Induction.Restricted_Predicates
  "HOL-Library.Multiset"
begin

definition multisets :: "'a set \<Rightarrow> 'a multiset set" where
  "multisets A = {M. set_mset M \<subseteq> A}"

lemma in_multisets_iff:
  "M \<in> multisets A \<longleftrightarrow> set_mset M \<subseteq> A"
  by (simp add: multisets_def)

lemma empty_multisets [simp]:
  "{#} \<in> multisets F"
  by (simp add: in_multisets_iff)

lemma multisets_union [simp]:
  "M \<in> multisets A \<Longrightarrow> N \<in> multisets A \<Longrightarrow> M + N \<in> multisets A"
  by (auto simp add: in_multisets_iff)

definition mulex1 :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
  "mulex1 P = (\<lambda>M N. (M, N) \<in> mult1 {(x, y). P x y})"

lemma mulex1_empty [iff]:
  "mulex1 P M {#} \<longleftrightarrow> False"
  using not_less_empty [of M "{(x, y). P x y}"]
  by (auto simp: mulex1_def)

lemma mulex1_add: "mulex1 P N (M0 + {#a#}) \<Longrightarrow>
  (\<exists>M. mulex1 P M M0 \<and> N = M + {#a#}) \<or>
  (\<exists>K. (\<forall>b. b \<in># K \<longrightarrow> P b a) \<and> N = M0 + K)"
  using less_add [of N a M0 "{(x, y). P x y}"]
  by (auto simp: mulex1_def)

lemma mulex1_self_add_right [simp]:
  "mulex1 P A (add_mset a A)"
proof -
  let ?R = "{(x, y). P x y}"
  thm mult1_def
  have "A + {#a#} = A + {#a#}" by simp
  moreover have "A = A + {#}" by simp
  moreover have "\<forall>b. b \<in># {#} \<longrightarrow> (b, a) \<in> ?R" by simp
  ultimately have "(A, add_mset a A) \<in> mult1 ?R"
    unfolding mult1_def by blast
  then show ?thesis by (simp add: mulex1_def)
qed

lemma empty_mult1 [simp]:
  "({#}, {#a#}) \<in> mult1 R"
proof -
  have "{#a#} = {#} + {#a#}" by simp
  moreover have "{#} = {#} + {#}" by simp
  moreover have "\<forall>b. b \<in># {#} \<longrightarrow> (b, a) \<in> R" by simp
  ultimately show ?thesis unfolding mult1_def by force
qed

lemma empty_mulex1 [simp]:
  "mulex1 P {#} {#a#}"
  using empty_mult1 [of a "{(x, y). P x y}"] by (simp add: mulex1_def)

definition mulex_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
  "mulex_on P A = (restrict_to (mulex1 P) (multisets A))\<^sup>+\<^sup>+"

abbreviation mulex :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
  "mulex P \<equiv> mulex_on P UNIV"

lemma mulex_on_induct [consumes 1, case_names base step, induct pred: mulex_on]:
  assumes "mulex_on P A M N"
    and "\<And>M N. \<lbrakk>M \<in> multisets A; N \<in> multisets A; mulex1 P M N\<rbrakk> \<Longrightarrow> Q M N"
    and "\<And>L M N. \<lbrakk>mulex_on P A L M; Q L M; N \<in> multisets A; mulex1 P M N\<rbrakk> \<Longrightarrow> Q L N"
  shows "Q M N"
  using assms unfolding mulex_on_def by (induct) blast+

lemma mulex_on_self_add_singleton_right [simp]:
  assumes "a \<in> A" and "M \<in> multisets A"
  shows "mulex_on P A M (add_mset a M)"
proof -
  have "mulex1 P M (M + {#a#})" by simp
  with assms have "restrict_to (mulex1 P) (multisets A) M (add_mset a M)"
    by (auto simp: multisets_def)
  then show ?thesis unfolding mulex_on_def by blast
qed

lemma singleton_multisets [iff]:
  "{#x#} \<in> multisets A \<longleftrightarrow> x \<in> A"
  by (auto simp: multisets_def)

lemma union_multisetsD:
  assumes "M + N \<in> multisets A"
  shows "M \<in> multisets A \<and> N \<in> multisets A"
  using assms by (auto simp: multisets_def)

lemma mulex_on_multisetsD [dest]:
  assumes "mulex_on P F M N"
  shows "M \<in> multisets F" and "N \<in> multisets F"
  using assms by (induct) auto

lemma union_multisets_iff [iff]:
  "M + N \<in> multisets A \<longleftrightarrow> M \<in> multisets A \<and> N \<in> multisets A"
  by (auto dest: union_multisetsD)

lemma add_mset_multisets_iff [iff]:
  "add_mset a M \<in> multisets A \<longleftrightarrow> a \<in> A \<and> M \<in> multisets A"
  unfolding add_mset_add_single[of a M] union_multisets_iff by auto

lemma mulex_on_trans:
  "mulex_on P A L M \<Longrightarrow> mulex_on P A M N \<Longrightarrow> mulex_on P A L N"
  by (auto simp: mulex_on_def)

lemma transp_on_mulex_on:
  "transp_on (mulex_on P A) B"
  using mulex_on_trans [of P A] by (auto simp: transp_on_def)

lemma mulex_on_add_right [simp]:
  assumes "mulex_on P A M N" and "a \<in> A"
  shows "mulex_on P A M (add_mset a N)"
proof -
  from assms have "a \<in> A" and "N \<in> multisets A" by auto
  then have "mulex_on P A N (add_mset a N)" by simp
  with \<open>mulex_on P A M N\<close> show ?thesis by (rule mulex_on_trans)
qed

lemma empty_mulex_on [simp]:
  assumes "M \<noteq> {#}" and "M \<in> multisets A"
  shows "mulex_on P A {#} M"
using assms
proof (induct M)
  case (add a M)
  show ?case
  proof (cases "M = {#}")
    assume "M = {#}"
    with add show ?thesis by (auto simp: mulex_on_def)
  next
    assume "M \<noteq> {#}"
    with add show ?thesis by (auto intro: mulex_on_trans)
  qed
qed simp

lemma mulex_on_self_add_right [simp]:
  assumes "M \<in> multisets A" and "K \<in> multisets A" and "K \<noteq> {#}"
  shows "mulex_on P A M (M + K)"
using assms
proof (induct K)
  case empty
  then show ?case by (cases "K = {#}") auto
next
  case (add a M)
  show ?case
  proof (cases "M = {#}")
    assume "M = {#}" with add show ?thesis by auto
  next
    assume "M \<noteq> {#}" with add show ?thesis
      by (auto dest: mulex_on_add_right simp add: ac_simps)
  qed
qed

lemma mult1_singleton [iff]:
  "({#x#}, {#y#}) \<in> mult1 R \<longleftrightarrow> (x, y) \<in> R"
proof
  assume "(x, y) \<in> R"
  then have "{#y#} = {#} + {#y#}"
    and "{#x#} = {#} + {#x#}"
    and "\<forall>b. b \<in># {#x#} \<longrightarrow> (b, y) \<in> R" by auto
  then show "({#x#}, {#y#}) \<in> mult1 R" unfolding mult1_def by blast
next
  assume "({#x#}, {#y#}) \<in> mult1 R"
  then obtain M0 K a
    where "{#y#} = add_mset a M0"
    and "{#x#} = M0 + K"
    and "\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> R"
    unfolding mult1_def by blast
  then show "(x, y) \<in> R" by (auto simp: add_eq_conv_diff)
qed

lemma mulex1_singleton [iff]:
  "mulex1 P {#x#} {#y#} \<longleftrightarrow> P x y"
  using mult1_singleton [of x y "{(x, y). P x y}"] by (simp add: mulex1_def)

lemma singleton_mulex_onI:
  "P x y \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> mulex_on P A {#x#} {#y#}"
  by (auto simp: mulex_on_def)

lemma reflclp_mulex_on_add_right [simp]:
  assumes "(mulex_on P A)\<^sup>=\<^sup>= M N" and "M \<in> multisets A" and "a \<in> A"
  shows "mulex_on P A M (N + {#a#})"
  using assms by (cases "M = N") simp_all

lemma reflclp_mulex_on_add_right' [simp]:
  assumes "(mulex_on P A)\<^sup>=\<^sup>= M N" and "M \<in> multisets A" and "a \<in> A"
  shows "mulex_on P A M ({#a#} + N)"
  using reflclp_mulex_on_add_right [OF assms] by (simp add: ac_simps)

lemma mulex_on_union_right [simp]:
  assumes "mulex_on P F A B" and "K \<in> multisets F"
  shows "mulex_on P F A (K + B)"
using assms
proof (induct K)
  case (add a K)
  then have "a \<in> F" and "mulex_on P F A (B + K)" by (auto simp: multisets_def ac_simps)
  then have "mulex_on P F A ((B + K) + {#a#})" by simp
  then show ?case by (simp add: ac_simps)
qed simp

lemma mulex_on_union_right' [simp]:
  assumes "mulex_on P F A B" and "K \<in> multisets F"
  shows "mulex_on P F A (B + K)"
  using mulex_on_union_right [OF assms] by (simp add: ac_simps)

text \<open>Adapted from @{thm all_accessible} in @{theory "HOL-Library.Multiset"}.\<close>
lemma accessible_on_mulex1_multisets:
  assumes wf: "wfp_on P A"
  shows "\<forall>M\<in>multisets A. accessible_on (mulex1 P) (multisets A) M"
proof
  let ?P = "mulex1 P"
  let ?A = "multisets A"
  let ?acc = "accessible_on ?P ?A"
  {
    fix M M0 a
    assume M0: "?acc M0"
      and "a \<in> A"
      and "M0 \<in> ?A"
      and wf_hyp: "\<And>b. \<lbrakk>b \<in> A; P b a\<rbrakk> \<Longrightarrow> (\<forall>M. ?acc (M) \<longrightarrow> ?acc (M + {#b#}))"
      and acc_hyp: "\<forall>M. M \<in> ?A \<and> ?P M M0 \<longrightarrow> ?acc (M + {#a#})"
    then have "add_mset a M0 \<in> ?A" by (auto simp: multisets_def)
    then have "?acc (add_mset a M0)"
    proof (rule accessible_onI [of "add_mset a M0"])
      fix N
      assume "N \<in> ?A"
        and "?P N (add_mset a M0)"
      then have "((\<exists>M. M \<in> ?A \<and> ?P M M0 \<and> N = M + {#a#}) \<or>
          (\<exists>K. (\<forall>b. b \<in># K \<longrightarrow> P b a) \<and> N = M0 + K))"
        using mulex1_add [of P N M0 a] by (auto simp: multisets_def)
      then show "?acc (N)"
      proof (elim exE disjE conjE)
        fix M assume "M \<in> ?A" and "?P M M0" and N: "N = M + {#a#}"
        from acc_hyp have "M \<in> ?A \<and> ?P M M0 \<longrightarrow> ?acc (M + {#a#})" ..
        with \<open>M \<in> ?A\<close> and \<open>?P M M0\<close> have "?acc (M + {#a#})" by blast
        then show "?acc (N)" by (simp only: N)
      next
        fix K
        assume N: "N = M0 + K"
        assume "\<forall>b. b \<in># K \<longrightarrow> P b a"
        moreover from N and \<open>N \<in> ?A\<close> have "K \<in> ?A" by (auto simp: multisets_def)
        ultimately have "?acc (M0 + K)"
        proof (induct K)
          case empty
          from M0 show "?acc (M0 + {#})" by simp
        next
          case (add x K)
          from add.prems have "x \<in> A" and "P x a" by (auto simp: multisets_def)
          with wf_hyp have "\<forall>M. ?acc M \<longrightarrow> ?acc (M + {#x#})" by blast
          moreover from add have "?acc (M0 + K)" by (auto simp: multisets_def)
          ultimately show "?acc (M0 + (add_mset x K))" by simp
        qed
        then show "?acc N" by (simp only: N)
      qed
    qed
  } note tedious_reasoning = this

  fix M
  assume "M \<in> ?A"
  then show "?acc M"
  proof (induct M)
    show "?acc {#}"
    proof (rule accessible_onI)
      show "{#} \<in> ?A" by (auto simp: multisets_def)
    next
      fix b assume "?P b {#}" then show "?acc b" by simp
    qed
  next
    case (add a M)
    then have "?acc M" by (auto simp: multisets_def)
    from add have "a \<in> A" by (auto simp: multisets_def)
    with wf have "\<forall>M. ?acc M \<longrightarrow> ?acc (add_mset a M)"
    proof (induct)
      case (less a)
      then have r: "\<And>b. \<lbrakk>b \<in> A; P b a\<rbrakk> \<Longrightarrow> (\<forall>M. ?acc M \<longrightarrow> ?acc (M + {#b#}))" by auto
      show "\<forall>M. ?acc M \<longrightarrow> ?acc (add_mset a M)"
      proof (intro allI impI)
        fix M'
        assume "?acc M'"
        moreover then have "M' \<in> ?A" by (blast dest: accessible_on_imp_mem)
        ultimately show "?acc (add_mset a M')"
          by (induct) (rule tedious_reasoning [OF _ \<open>a \<in> A\<close> _ r], auto)
      qed
    qed
    with \<open>?acc (M)\<close> show "?acc (add_mset a M)" by blast
  qed
qed

lemmas wfp_on_mulex1_multisets =
  accessible_on_mulex1_multisets [THEN accessible_on_imp_wfp_on]

lemmas irreflp_on_mulex1 =
  wfp_on_mulex1_multisets [THEN wfp_on_imp_irreflp_on]

lemma wfp_on_mulex_on_multisets:
  assumes "wfp_on P A"
  shows "wfp_on (mulex_on P A) (multisets A)"
  using wfp_on_mulex1_multisets [OF assms]
  by (simp only: mulex_on_def wfp_on_restrict_to_tranclp_wfp_on_conv)

lemmas irreflp_on_mulex_on =
  wfp_on_mulex_on_multisets [THEN wfp_on_imp_irreflp_on]

lemma mulex1_union:
  "mulex1 P M N \<Longrightarrow> mulex1 P (K + M) (K + N)"
  by (auto simp: mulex1_def mult1_union)

lemma mulex_on_union:
  assumes "mulex_on P A M N" and "K \<in> multisets A"
  shows "mulex_on P A (K + M) (K + N)"
using assms
proof (induct)
  case (base M N)
  then have "mulex1 P (K + M) (K + N)" by (blast dest: mulex1_union)
  moreover from base have "(K + M) \<in> multisets A"
    and "(K + N) \<in> multisets A" by (auto simp: multisets_def)
  ultimately have "restrict_to (mulex1 P) (multisets A) (K + M) (K + N)" by auto
  then show ?case by (auto simp: mulex_on_def)
next
  case (step L M N)
  then have "mulex1 P (K + M) (K + N)" by (blast dest: mulex1_union)
  moreover from step have "(K + M) \<in> multisets A" and "(K + N) \<in> multisets A" by blast+
  ultimately have "(restrict_to (mulex1 P) (multisets A))\<^sup>+\<^sup>+ (K + M) (K + N)" by auto
  moreover have "mulex_on P A (K + L) (K + M)" using step by blast
  ultimately show ?case by (auto simp: mulex_on_def)
qed

lemma mulex_on_union':
  assumes "mulex_on P A M N" and "K \<in> multisets A"
  shows "mulex_on P A (M + K) (N + K)"
  using mulex_on_union [OF assms] by (simp add: ac_simps)

lemma mulex_on_add_mset:
  assumes "mulex_on P A M N" and "m \<in> A"
  shows "mulex_on P A (add_mset m M) (add_mset m N)"
  unfolding add_mset_add_single[of m M] add_mset_add_single[of m N]
  apply (rule mulex_on_union')
  using assms by auto

lemma union_mulex_on_mono:
  "mulex_on P F A C \<Longrightarrow> mulex_on P F B D \<Longrightarrow> mulex_on P F (A + B) (C + D)"
  by (metis mulex_on_multisetsD mulex_on_trans mulex_on_union mulex_on_union')

lemma mulex_on_add_mset':
  assumes "P m n" and "m \<in> A" and "n \<in> A" and "M \<in> multisets A"
  shows "mulex_on P A (add_mset m M) (add_mset n M)"
  unfolding add_mset_add_single[of m M] add_mset_add_single[of n M]
  apply (rule mulex_on_union)
  using assms by (auto simp: mulex_on_def)

lemma mulex_on_add_mset_mono:
  assumes "P m n" and "m \<in> A" and "n \<in> A" and "mulex_on P A M N"
  shows "mulex_on P A (add_mset m M) (add_mset n N)"
  unfolding add_mset_add_single[of m M] add_mset_add_single[of n N]
  apply (rule union_mulex_on_mono)
  using assms by (auto simp: mulex_on_def)

lemma union_mulex_on_mono1:
  "A \<in> multisets F \<Longrightarrow> (mulex_on P F)\<^sup>=\<^sup>= A C \<Longrightarrow> mulex_on P F B D \<Longrightarrow>
    mulex_on P F (A + B) (C + D)"
  by (auto intro: union_mulex_on_mono mulex_on_union)

lemma union_mulex_on_mono2:
  "B \<in> multisets F \<Longrightarrow> mulex_on P F A C \<Longrightarrow> (mulex_on P F)\<^sup>=\<^sup>= B D \<Longrightarrow>
    mulex_on P F (A + B) (C + D)"
  by (auto intro: union_mulex_on_mono mulex_on_union')

lemma mult1_mono:
  assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> A; (x, y) \<in> R\<rbrakk> \<Longrightarrow> (x, y) \<in> S"
    and "M \<in> multisets A"
    and "N \<in> multisets A"
    and "(M, N) \<in> mult1 R"
  shows "(M, N) \<in> mult1 S"
  using assms unfolding mult1_def multisets_def
  by auto (metis (full_types) subsetD)

lemma mulex1_mono:
  assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> A; P x y\<rbrakk> \<Longrightarrow> Q x y"
    and "M \<in> multisets A"
    and "N \<in> multisets A"
    and "mulex1 P M N"
  shows "mulex1 Q M N"
  using mult1_mono [of A "{(x, y). P x y}" "{(x, y). Q x y}" M N]
    and assms unfolding mulex1_def by blast

lemma mulex_on_mono:
  assumes *: "\<And>x y. \<lbrakk>x \<in> A; y \<in> A; P x y\<rbrakk> \<Longrightarrow> Q x y"
    and "mulex_on P A M N"
  shows "mulex_on Q A M N"
proof -
  let ?rel = "\<lambda>P. (restrict_to (mulex1 P) (multisets A))"
  from \<open>mulex_on P A M N\<close> have "(?rel P)\<^sup>+\<^sup>+ M N" by (simp add: mulex_on_def)
  then have "(?rel Q)\<^sup>+\<^sup>+ M N"
  proof (induct rule: tranclp.induct)
    case (r_into_trancl M N)
    then have "M \<in> multisets A" and "N \<in> multisets A" by auto
    from mulex1_mono [OF * this] and r_into_trancl
      show ?case by auto
  next
    case (trancl_into_trancl L M N)
    then have "M \<in> multisets A" and "N \<in> multisets A" by auto
    from mulex1_mono [OF * this] and trancl_into_trancl
      have "?rel Q M N" by auto
    with \<open>(?rel Q)\<^sup>+\<^sup>+ L M\<close> show ?case by (rule tranclp.trancl_into_trancl)
  qed
  then show ?thesis by (simp add: mulex_on_def)
qed

lemma mult1_reflcl:
  assumes "(M, N) \<in> mult1 R"
  shows "(M, N) \<in> mult1 (R\<^sup>=)"
  using assms by (auto simp: mult1_def)

lemma mulex1_reflclp:
  assumes "mulex1 P M N"
  shows "mulex1 (P\<^sup>=\<^sup>=) M N"
  using mulex1_mono [of UNIV P "P\<^sup>=\<^sup>=" M N, OF _ _ _ assms]
  by (auto simp: multisets_def)

lemma mulex_on_reflclp:
  assumes "mulex_on P A M N"
  shows "mulex_on (P\<^sup>=\<^sup>=) A M N"
  using mulex_on_mono [OF _ assms, of "P\<^sup>=\<^sup>="] by auto

lemma surj_on_multisets_mset:
  "\<forall>M\<in>multisets A. \<exists>xs\<in>lists A. M = mset xs"
proof
  fix M
  assume "M \<in> multisets A"
  then show "\<exists>xs\<in>lists A. M = mset xs"
  proof (induct M)
    case empty show ?case by simp
  next
    case (add a M)
    then obtain xs where "xs \<in> lists A" and "M = mset xs" by auto
    then have "add_mset a M = mset (a # xs)" by simp
    moreover have "a # xs \<in> lists A" using \<open>xs \<in> lists A\<close> and add by auto
    ultimately show ?case by blast
  qed
qed

lemma image_mset_lists [simp]:
  "mset ` lists A = multisets A"
  using surj_on_multisets_mset [of A]
  by auto (metis mem_Collect_eq multisets_def set_mset_mset subsetI)

lemma multisets_UNIV [simp]: "multisets UNIV = UNIV"
  by (metis image_mset_lists lists_UNIV surj_mset)

lemma non_empty_multiset_induct [consumes 1, case_names singleton add]:
  assumes "M \<noteq> {#}"
    and "\<And>x. P {#x#}"
    and "\<And>x M. P M \<Longrightarrow> P (add_mset x M)"
  shows "P M"
  using assms by (induct M) auto

lemma mulex_on_all_strict:
  assumes "X \<noteq> {#}"
  assumes "X \<in> multisets A" and "Y \<in> multisets A"
    and *: "\<forall>y. y \<in># Y \<longrightarrow> (\<exists>x. x \<in># X \<and> P y x)"
  shows "mulex_on P A Y X"
using assms
proof (induction X arbitrary: Y rule: non_empty_multiset_induct)
  case (singleton x)
  then have "mulex1 P Y {#x#}"
    unfolding mulex1_def mult1_def
    by auto
  with singleton show ?case by (auto simp: mulex_on_def)
next
  case (add x M)
  let ?Y = "{# y \<in># Y. \<exists>x. x \<in># M \<and> P y x #}"
  let ?Z = "Y - ?Y"
  have Y: "Y = ?Z + ?Y" by (subst multiset_eq_iff) auto
  from \<open>Y \<in> multisets A\<close> have "?Y \<in> multisets A" by (metis multiset_partition union_multisets_iff)
  moreover have "\<forall>y. y \<in># ?Y \<longrightarrow> (\<exists>x. x \<in># M \<and> P y x)" by auto
  moreover have "M \<in> multisets A" using add by auto
  ultimately have "mulex_on P A ?Y M" using add by blast
  moreover have "mulex_on P A ?Z {#x#}"
  proof -
    have "{#x#} = {#} + {#x#}" by simp
    moreover have "?Z = {#} + ?Z" by simp
    moreover have "\<forall>y. y \<in># ?Z \<longrightarrow> P y x"
      using add.prems by (auto simp add: in_diff_count split: if_splits)
    ultimately have "mulex1 P ?Z {#x#}" unfolding mulex1_def mult1_def by blast
    moreover have "{#x#} \<in> multisets A" using add.prems by auto
    moreover have "?Z \<in> multisets A"
      using \<open>Y \<in> multisets A\<close> by (metis diff_union_cancelL multiset_partition union_multisetsD)
    ultimately show ?thesis by (auto simp: mulex_on_def)
  qed
  ultimately have "mulex_on P A (?Y + ?Z) (M + {#x#})" by (rule union_mulex_on_mono)
  then show ?case using Y by (simp add: ac_simps)
qed

text \<open>The following lemma shows that the textbook definition (e.g.,
``Term Rewriting and All That'') is the same as the one used below.\<close>
lemma diff_set_Ex_iff:
  "X \<noteq> {#} \<and> X \<subseteq># M \<and> N = (M - X) + Y \<longleftrightarrow> X \<noteq> {#} \<and> (\<exists>Z. M = Z + X \<and> N = Z + Y)"
  by (auto) (metis add_diff_cancel_left' multiset_diff_union_assoc union_commute)

text \<open>Show that @{const mulex_on} is equivalent to the textbook definition
of multiset-extension for transitive base orders.\<close>
lemma mulex_on_alt_def:
  assumes trans: "transp_on P A"
  shows "mulex_on P A M N \<longleftrightarrow> M \<in> multisets A \<and> N \<in> multisets A \<and> (\<exists>X Y Z.
    X \<noteq> {#} \<and> N = Z + X \<and> M = Z + Y \<and> (\<forall>y. y \<in># Y \<longrightarrow> (\<exists>x. x \<in># X \<and> P y x)))"
  (is "?P M N \<longleftrightarrow> ?Q M N")
proof
  assume "?P M N" then show "?Q M N"
  proof (induct M N)
    case (base M N)
    then obtain a M0 K where N: "N = M0 + {#a#}"
      and M: "M = M0 + K"
      and *: "\<forall>b. b \<in># K \<longrightarrow> P b a"
      and "M \<in> multisets A" and "N \<in> multisets A" by (auto simp: mulex1_def mult1_def)
    moreover then have "{#a#} \<in> multisets A" and "K \<in> multisets A" by auto
    moreover have "{#a#} \<noteq> {#}" by auto
    moreover have "N = M0 + {#a#}" by fact
    moreover have "M = M0 + K" by fact
    moreover have "\<forall>y. y \<in># K \<longrightarrow> (\<exists>x. x \<in># {#a#} \<and> P y x)" using * by auto
    ultimately show ?case by blast
  next
    case (step L M N)
    then obtain X Y Z
      where "L \<in> multisets A" and "M \<in> multisets A" and "N \<in> multisets A"
      and "X \<in> multisets A" and "Y \<in> multisets A"
      and M: "M = Z + X"
      and L: "L = Z + Y" and "X \<noteq> {#}"
      and Y: "\<forall>y. y \<in># Y \<longrightarrow> (\<exists>x. x \<in># X \<and> P y x)"
      and "mulex1 P M N"
      by blast
    from \<open>mulex1 P M N\<close> obtain a M0 K
      where N: "N = add_mset a M0" and M': "M = M0 + K"
      and *: "\<forall>b. b \<in># K \<longrightarrow> P b a" unfolding mulex1_def mult1_def by blast
    have L': "L = (M - X) + Y" by (simp add: L M)
    have K: "\<forall>y. y \<in># K \<longrightarrow> (\<exists>x. x \<in># {#a#} \<and> P y x)" using * by auto

    txt \<open>The remainder of the proof is adapted from the proof of Lemma 2.5.4. of
    the book ``Term Rewriting and All That.''\<close>
    let ?X = "add_mset a (X - K)"
    let ?Y = "(K - X) + Y"

    have "L \<in> multisets A" and "N \<in> multisets A" by fact+
    moreover have "?X \<noteq> {#} \<and> (\<exists>Z. N = Z + ?X \<and> L = Z + ?Y)"
    proof -
      have "?X \<noteq> {#}" by auto
      moreover have "?X \<subseteq># N"
        using M N M' by (simp add: add.commute [of "{#a#}"])
          (metis Multiset.diff_subset_eq_self add.commute add_diff_cancel_right)
      moreover have "L = (N - ?X) + ?Y"
      proof (rule multiset_eqI)
        fix x :: 'a
        let ?c = "\<lambda>M. count M x"
        let ?ic = "\<lambda>x. int (?c x)"
        from \<open>?X \<subseteq># N\<close> have *: "?c {#a#} + ?c (X - K) \<le> ?c N"
          by (auto simp add: subseteq_mset_def split: if_splits)
        from * have **: "?c (X - K) \<le> ?c M0" unfolding N by (auto split: if_splits)
        have "?ic (N - ?X + ?Y) = int (?c N - ?c ?X) + ?ic ?Y" by simp
        also have "\<dots> = int (?c N - (?c {#a#} + ?c (X - K))) + ?ic (K - X) + ?ic Y" by simp
        also have "\<dots> = ?ic N - (?ic {#a#} + ?ic (X - K)) + ?ic (K - X) + ?ic Y"
          using of_nat_diff [OF *] by simp
        also have "\<dots> = (?ic N - ?ic {#a#}) - ?ic (X - K) + ?ic (K - X) + ?ic Y" by simp
        also have "\<dots> = (?ic N - ?ic {#a#}) + (?ic (K - X) - ?ic (X - K)) + ?ic Y" by simp
        also have "\<dots> = (?ic N - ?ic {#a#}) + (?ic K - ?ic X) + ?ic Y" by simp
        also have "\<dots> = (?ic N - ?ic ?X) + ?ic ?Y" by (simp add: N)
        also have "\<dots> = ?ic L"
          unfolding L' M' N
          using ** by (simp add: algebra_simps)
        finally show "?c L = ?c (N - ?X + ?Y)" by simp
      qed
      ultimately show ?thesis by (metis diff_set_Ex_iff)
    qed
    moreover have "\<forall>y. y \<in># ?Y \<longrightarrow> (\<exists>x. x \<in># ?X \<and> P y x)"
    proof (intro allI impI)
      fix y assume "y \<in># ?Y"
      then have "y \<in># K - X \<or> y \<in># Y" by auto
      then show "\<exists>x. x \<in># ?X \<and> P y x"
      proof
        assume "y \<in># K - X"
        then have "y \<in># K" by (rule in_diffD)
        with K show ?thesis by auto
      next
        assume "y \<in># Y"
        with Y obtain x where "x \<in># X" and "P y x" by blast
        { assume "x \<in># X - K" with \<open>P y x\<close> have ?thesis by auto }
        moreover
        { assume "x \<in># K" with * have "P x a" by auto
          moreover have "y \<in> A" using \<open>Y \<in> multisets A\<close> and \<open>y \<in># Y\<close> by (auto simp: multisets_def)
          moreover have "a \<in> A" using \<open>N \<in> multisets A\<close> by (auto simp: N)
          moreover have "x \<in> A" using \<open>M \<in> multisets A\<close> and \<open>x \<in># K\<close> by (auto simp: M' multisets_def)
          ultimately have "P y a" using \<open>P y x\<close> and trans unfolding transp_on_def by blast
          then have ?thesis by force }
        moreover from \<open>x \<in># X\<close> have "x \<in># X - K \<or> x \<in># K"
          by (auto simp add: in_diff_count not_in_iff)
        ultimately show ?thesis by auto
      qed
    qed
    ultimately show ?case by blast
  qed
next
  assume "?Q M N"
  then obtain X Y Z where "M \<in> multisets A" and "N \<in> multisets A"
    and "X \<noteq> {#}" and N: "N = Z + X" and M: "M = Z + Y"
    and *: "\<forall>y. y \<in># Y \<longrightarrow> (\<exists>x. x \<in># X \<and> P y x)" by blast
  with mulex_on_all_strict [of X A Y] have "mulex_on P A Y X" by auto
  moreover from \<open>N \<in> multisets A\<close> have "Z \<in> multisets A" by (auto simp: N)
  ultimately show "?P M N" unfolding M N by (metis mulex_on_union)
qed

end

subset_name: curated


text:
\section{Missing Proofs for Section \ref{sec:structure}}\label{appstructure}

Even though the results in this section hold for any direction $\mathbf{w}\in \mathbb{R}^n$, we will prove the statements for $\mathbf{w} = \nabla f(\x_0)$ for readability in the context of the paper.

\subsection{Proof of Lemma \ref{basecase}}

\basecase*

\begin{proof} Note that by definition $g(\lambda) =\argmin_{\y \in P} \left \{ \frac {\| \x_0 - \y \|^2}{2\lambda} + \innerprod{\nabla f(\x_0) }{\y} \right\}$ for any $\lambda > 0$. Then, by optimality of $g(\lambda)$ we have
\begin{equation} \label{opt of prox}
    \frac {\| \x_0 -  g(\lambda)\|^2}{2\lambda}   +  \innerprod{\nabla f(\x_0) }{g(\lambda)} \leq  \frac {\| \x_0 -  \mathbf{z}\|^2}{2\lambda}   +\innerprod{\nabla f(\x_0) }{\mathbf{z}}
\end{equation}
for all $\mathbf{z}\in P$.

The condition $-\nabla f(\x_0) \in N_P(\x_0)$ is equivalent to $\innerprod{\nabla f(\x_0)}{\mathbf{z} -  \x_0} \geq 0$ for all $\mathbf{\mathbf{z}} \in P$. Plugging $\x_0$ in the left-hand side of \eqref{opt of prox}, we have that for any $\lambda > 0$
\begin{equation*}
    0 \leq \frac {\| \x_0 -  g(\lambda) \|^2}{2\lambda} \leq \innerprod{\nabla f(\x_0) }{\x_0 - g(\lambda)} \leq 0.
\end{equation*}
This implies $g(\lambda) =\x_0$ for all $\lambda > 0$.
\qed \end{proof}

\subsection{Proof of Lemma \ref{equivalence}}

\equivalence*

\begin{proof}
Recall from Section \ref{sec: prelims} that $\y^* = \Pi_P(\x_0 - \lambda \nabla f(\x_0))$ if and only if $(\x_0 - \lambda \nabla f(\x_0) - \y^*) \in N_P(\y^*)$. Thus, the optimality of $g(\lambda)$ implies
\begin{equation}\label{eq1 - lemma2}
    \x_0 - \lambda \nabla f(\x_0) - g(\lambda) \in N_P(g(\lambda)).
\end{equation}
Similarly, {using} the optimality of $g(\lambda^\prime)$ we have
\begin{equation}\label{eq2 - lemma2}
    \x_0 - \lambda^\prime \nabla f(\x_0) - g(\lambda^\prime) \in N_P(g(\lambda^\prime)).
\end{equation}
Aggregate equations \eqref{eq1 - lemma2} and \eqref{eq2 - lemma2} with weights $\delta$ and $(1 - \delta)$ respectively to obtain:
\begin{equation}\label{eq3 - lemma2}
    \x_0 - (\delta \lambda + (1 - \delta)\lambda^\prime)\nabla f(\x_0) - (\delta g(\lambda) + (1 - \delta)g(\lambda^\prime)) \in \delta N_P(g(\lambda)) + (1 - \delta) N_P(g(\lambda^\prime)).
\end{equation}

Now we claim that
\begin{equation}\label{eq4 - lemma2}
        \delta N_P(g(\lambda)) + (1 - \delta) N_P(g(\lambda^\prime)) = N_P(g(\lambda^\prime)) = N_P(g(\lambda)) = N_P(\delta g(\lambda) + (1 - \delta) g(\lambda^\prime)).
\end{equation}
The first two equalities follow from that fact that $\delta \in [0,1]$ and $N_P(g(\lambda)) = N_P(g(\lambda^\prime))$. To show the third equality, note from \eqref{def: normal cone} that $N_P(g(\lambda)) = N_P(g(\lambda^\prime))$ implies that $I(g(\lambda)) = I(g(\lambda^\prime))$ and hence $J(g(\lambda)) = J(g(\lambda^\prime))$. Therefore,
\begin{align*}
    \mathbf{A}_{I(g(\lambda))} (\delta g(\lambda) + (1 - \delta)g(\lambda^\prime)) &= \delta \mathbf{A}_{I(g(\lambda))}g(\lambda) +  (1 - \delta) \mathbf{A}_{I(g(\lambda^\prime))}g(\lambda^\prime) \\
    &= \delta \mathbf{b}_{I(g(\lambda))} +  (1 - \delta) \mathbf{b}_{I(g(\lambda^\prime))}\\
    &= \mathbf{b}_{I(g(\lambda))}
\end{align*}
Similarly,
\begin{align*}
    \mathbf{A}_{J(g(\lambda))} (\delta g(\lambda) + (1 - \delta)g(\lambda^\prime)) &= \delta \mathbf{A}_{J(g(\lambda))}g(\lambda) +  (1 - \delta) \mathbf{A}_{J(g(\lambda^\prime))}g(\lambda^\prime) \\
    &< \delta \mathbf{b}_{J(g(\lambda))} +  (1 - \delta) \mathbf{b}_{J(g(\lambda^\prime))}\\
    &= \mathbf{b}_{J(g(\lambda))}
\end{align*}
Thus, we have shown that $I(g(\lambda)) = I(\delta g(\lambda) + (1 - \delta)g(\lambda^\prime)) = I(g(\lambda^\prime))$ and $J(g(\lambda)) = J(\delta g(\lambda) + (1 - \delta)g(\lambda^\prime)) = J(g(\lambda^\prime))$, which completes the proof of \eqref{eq4 - lemma2}.

Now using \eqref{eq4 - lemma2}, we can equivalently write  \eqref{eq3 - lemma2} as follows:
\begin{equation*}
    \x_0 - (\delta \lambda + (1 - \delta)\lambda^\prime)\nabla f(\x_0) - (\delta g(\lambda) + (1 - \delta)g(\lambda^\prime)) \in N_P(\delta g(\lambda) + (1 - \delta) g(\lambda^\prime)).
\end{equation*}
This shows that $\delta g(\lambda) + (1 - \delta) g(\lambda^\prime)$ satisfies the optimality condition for $g(\delta \lambda + (1 - \delta) \lambda^\prime)$, which concludes the proof.
\qed \end{proof}

\subsection{Proof of Theorem \ref{existence-new}}
We prove this theorem in a sequence of steps given by the next couple of lemmas. We first show that the normal cones do not change in the {\it strict} neighborhood of $\x_0$, i.e., there exists a ball $B(\x_0,\delta)$ around $\x_0$ of radius $\delta>0$ such that the normal cone $N_P(g(\lambda)) = N_P(g(\lambda^\prime))$ for all $g(\lambda), g(\lambda^\prime) \in B(\x_0,\delta)\setminus \{\x_0\}$.
\iffalse
\begin{restatable}{theorem}{existencenew}
\label{existence-new}
Let $P \subseteq \mathbb{R}^n$ be a polytope defined using $m$ facet inequalities (e.g., as in \eqref{polytope}). Let $\x_0\in P$ and we are given $\nabla f(\x_0) \in \mathbb{R}^n$. Let $g(\lambda) = \Pi_P(\x_0 - \lambda \nabla f(\x_0))$ be the parametric projections curve. Then, there exists $\lambda_1^- \in \mathbb{R}_+$ ($\lambda_1^->0$) with $\x_1 = g(\lambda_1^-)$ such that
\begin{enumerate}
    \item[(i)] $N_P(g(\lambda)) = N_P(g(\lambda^\prime)) \subseteq N_P(\x_0)$, for all $0<\lambda<\lambda^\prime < \lambda_1^-$, and
    \item[(ii)] $N_P(\x_1) = N_P(g(\lambda_1^-)) \supset N_P(g(\lambda))$, for all $\lambda \in (0, \lambda_1^-)$.
\end{enumerate}
Moreover, for direction $\mathbf{d} = (\x_1 - \x_0)/\lambda_1^- \in \mathbb{R}^n$, we have
$ g(\lambda) = \x_0 +  \lambda \mathbf{d}, \text{ for all } \lambda \in [0,\lambda_1^-]. $
\end{restatable}
\fi

\begin{lemma} \label{constant normal cone}
Let $P \subseteq \mathbb{R}^n$ be a polytope defined using $m$ facet inequalities (e.g., as in \eqref{polytope}). Let $\x_0\in P$ and we are given $\nabla f(\x_0) \in \mathbb{R}^n$. Let $g(\lambda) = \Pi_P(\x_0 - \lambda \nabla f(\x_0))$ be the parametric projections curve. Then there exists a scalar $\delta > 0$ such that $N_P(g(\lambda)) = N_P(g(\lambda^\prime)) \subseteq N_P(\x_0)$, for all $0<\lambda<\lambda^\prime < \delta$.
\end{lemma}

To prove this lemma we will need a few properties about orthogonal projections. The first property is a simple fact, which follows from the fact that the Euclidean projection operator is non-expansive (see Section \ref{sec: prelims}):
\begin{equation}\label{nonexpansive}
   \|\x_0 - g(\epsilon)\| = \|g(0) - g(\epsilon)\| \leq \|\x_0 - (\x_0 - \epsilon \nabla f(\x_0)) \| = \epsilon \|\nabla f(\x_0)\|.
\end{equation}

The second property we need is that if for some $\lambda^\prime > \lambda$ the point $\mathbf{z} := \left(1 - \frac{\lambda^\prime}{\lambda}\right)\x_0 +  \frac{\lambda^\prime}{\lambda}g(\lambda)$ in the affine hull of $g(\lambda)$ and $\x_0$ is feasible, then it indeed coincides with the projection $g(\lambda^\prime)$:
\begin{restatable}[Affine hull expansion of projections]{lemma}{affinehull}
\label{affine-hull}
Let $\mathcal{X} \subseteq \mathbb{R}^n$ be a compact and convex set. Let $\x_0\in \mathcal{X}$ and we are given $\nabla f(\x_0) \in \mathbb{R}^n$. Further, let $g(\lambda) = \Pi_{\mathcal{X}}(\x_0 - \lambda \nabla f(\x_0))$ be the parametric projections curve. Then, if $\mathbf{z} := \left(1 - \frac{\lambda^\prime}{\lambda}\right)\x_0 +  \frac{\lambda^\prime}{\lambda}g(\lambda) \in \mathcal{X}$ for some $\lambda < \lambda^\prime$, then $g(\lambda^\prime) = \mathbf{z}$.
\end{restatable}

\begin{proof}
We will show that $\mathbf{z} := \left(1 - \frac{\lambda^\prime}{\lambda}\right)\x_0 +  \frac{\lambda^\prime}{\lambda}g(\lambda) = \x_0 + \frac{\lambda^\prime}{\lambda} (g(\lambda) - \x_0) \in \mathcal{X}$ satisfies first-order optimality for the projection at $\lambda^\prime$. Suppose for a contradiction, there exists some $\y \in \mathcal{X}$ with
\begin{align}
    &\innerprod{\x_0 - \lambda^\prime \nabla f(\x_0) - \mathbf{z}}{\y - \mathbf{z}} > 0\\
    = &\innerprod{\x_0 - \lambda^\prime \nabla f(\x_0) - \left(\x_0 + \frac{\lambda^\prime}{\lambda} (g(\lambda) - \x_0)\right)}{\y - \left(\x_0 + \frac{\lambda^\prime}{\lambda} (g(\lambda) - \x_0)\right)} > 0\\
     \Leftrightarrow & \frac{\lambda^\prime}{\lambda} \innerprod{\x_0 - \lambda \nabla f(\x_0) - g(\lambda)}{\y + \left(\frac{\lambda^\prime}{\lambda} -1\right) \x_0 - \frac{\lambda^\prime}{\lambda} g(\lambda)} > 0\\
     \Leftrightarrow &\left(\frac{\lambda^\prime}{\lambda}\right)^2 \innerprod{\x_0 - \lambda \nabla f(\x_0) - g(\lambda)}{\frac{\lambda}{\lambda^\prime} \y + \left(1 - \frac{\lambda}{\lambda^\prime} \right) \x_0 -  g(\lambda)} > 0.
\end{align}

Observe that $\frac{\lambda}{\lambda^\prime} \y + \left(1 - \frac{\lambda}{\lambda^\prime} \right) \x_0 \in \mathcal{X}$ since $\frac{\lambda}{\lambda^\prime} \in (0,1)$ and $\mathcal{X}$ is a convex set. This contradicts the first-order optimality condition of $g(\lambda)$:
\begin{equation*}
    \innerprod{\x_0 - \lambda \nabla f(\x_0) - g(\lambda)}{\mathbf{x} -  g(\lambda)} \leq 0 \quad \forall \mathbf{x} \in \mathcal{X}.
\end{equation*}
\qed \end{proof}

We are now ready to prove the lemma:
\begin{proof}[Proof of Lemma \ref{constant normal cone}]
Let $I$ and $J$ denote the index-set of active and inactive constraints at $\x_0$ respectively.
We will prove that any $\delta$ satisfying
\begin{equation} \label{M-value}
    0 < \delta \leq \min_{i \in {J}} \frac{b_i - \innerprod{\mathbf{a}_i}{\x_0}}{  \|\mathbf{a}_i\| \|\nabla  f(\x_0)\|},
\end{equation}
satisfies the condition stated in the lemma ($J$ is non-empty since otherwise the polytope contains only one point and the lemma follows trivially).

We first show that $N_P(g(\lambda)) \subseteq N_P(\x_0)$ for any $\lambda \in (0,\delta)$. Indeed, for any $j \in {J}$ (so that $\innerprod{\mathbf{a}_j}{\x_0} < b_j)$, we have
\begin{align}
    \innerprod{\mathbf{a}_j}{g(\lambda)} &= \innerprod{\mathbf{a}_j}{ \x_0 + g(\lambda) - \x_0} \nonumber\\
    & \leq \innerprod{\mathbf{a}_j}{\x_0} +  \| \mathbf{a}_j\|  \| g(\lambda) - \x\| \label{Lemma-5 - 2} &\quad \quad \text{by Cauchy-Schwartz inequality}\\
    &\leq \innerprod{\mathbf{a}_j}{\x_0} +  \lambda \| \mathbf{a}_j\|  \| \nabla f(\x_0)\| &\quad \quad \text{by non-expansivity of projections  \eqref{nonexpansive}}\label{Lemma-5 - 3} \\
    &< \innerprod{\mathbf{a}_j}{\x_0} +  \delta \| \mathbf{a}_j\|  \| \nabla f(\x_0)\|&\quad \quad \text{ since } \lambda \in (0, \delta)\label{Lemma-5 - 4}\\
    & \leq b_j & \quad \quad \text{choice of $\delta$ in \eqref{M-value}}.\label{Lemma-5 - 5}
\end{align}

This shows that the inactive constraints at $\x_0$ remain inactive at $g(\lambda)$ for any $0 < \lambda < \delta$, i.e., $N_P(g(\lambda)) \subseteq N_P(\x_0)$.
What remains to show is that active constraints at $g(\lambda)$ are the same as active constraints at $g(\lambda^\prime)$, i.e., for any $i \in I$, we have $\innerprod{\mathbf{a}_i}{g(\lambda)} = b_i $ if and only if  $\innerprod{\mathbf{a}_i}{g(\lambda^\prime)} = b_i$ for $0<\lambda <\lambda^\prime<\delta$.
To show that, we only need to show colinearity of $g(\lambda), g(\lambda^\prime), \x_0$, i.e.,
\begin{equation} \label{claim}
    g(\lambda^\prime) = \x_0 + \frac{\lambda^\prime}{\lambda} (g(\lambda) - \x_0) := \mathbf{z},
\end{equation}
since this implies
\begin{equation*}
 \innerprod{\mathbf{a}_i}{\x_0 - g(\lambda)} = 0 \Longleftrightarrow \innerprod{\mathbf{a}_i}{\x_0 - g(\lambda^\prime)} = 0 \Longleftrightarrow \innerprod{\mathbf{a}_i}{ g(\lambda^\prime)} = b_i \Longleftrightarrow \innerprod{\mathbf{a}_i}{g(\lambda)} = b_i.
\end{equation*}

Let us now prove colinearity of $g(\lambda), g(\lambda^\prime), \x_0$ \eqref{claim}. Using Lemma \ref{affine-hull}, we know that $g(\lambda^\prime) = \mathbf{z}$ as long as $\mathbf{z} \in P$. Hence, it suffices to show feasibility of $\mathbf{z}$:
\begin{itemize}
    \item[] {\bf Feasibility}: We claim $\x_0 + \frac{\lambda^\prime}{\lambda} (g(\lambda) - \x_0) \in P$.

    \textit{Proof.} Any inactive constraint $j \in {J}$ remains inactive, since:
\begin{equation*}
    \innerprod{\mathbf{a}_j}{ \x_0 + \frac{\lambda^\prime}{\lambda} (g(\lambda) - \x_0)} \leq \innerprod{\mathbf{a}_j}{\x_0} + \frac{\lambda^\prime}{\lambda}  \| \mathbf{a}_j\|  \| g(\lambda) - \x_0\| \leq \innerprod{\mathbf{a}_j}{\x_0} + \lambda^\prime \| \mathbf{a}_j\|  \| \nabla f(\x_0)\|
 < b_j
\end{equation*}
where the last inequality uses $\lambda^\prime < \delta$. Each active constraint $i \in I$ also remains feasible, since
\begin{equation*}
\innerprod{\mathbf{a}_i}{ \x_0 + (g(\lambda) - \x_0)} = \innerprod{\mathbf{a}_i}{g(\lambda)} \leq b_i \implies \innerprod{\mathbf{a}_i}{g(\lambda) - \x_0} \leq 0.
\end{equation*}
Multiplying the last inequality with  $\frac{\lambda^\prime}{\lambda} > 0$, and adding $\innerprod{\mathbf{a}_i}{\x_0} = b_i$, we get:
\begin{equation*}
    \innerprod{\mathbf{a}_i}{\x_0 + \frac{\lambda^\prime}{\lambda} (g(\lambda) - \x_0)} \leq b_i.
\end{equation*}
\end{itemize}
The result now follows from colinearity of $g(\lambda), g(\lambda^\prime)$ and $\x_0$.
\qed \end{proof}

Since $\lambda, \lambda^\prime \in (0, \delta)$ were arbitrary in the above proof, we get the following corollary:

\begin{corollary}\label{normal cone}
Let $P \subseteq \mathbb{R}^n$ be a polytope defined using $m$ facet inequalities (e.g., as in \eqref{polytope}). Let $\x_0\in P$ and we are given $\nabla f(\x_0) \in \mathbb{R}^n$. Let $g(\lambda) = \Pi_P(\x_0 - \lambda \nabla f(\x_0))$ be the parametric projections curve. Then, there exists a scalar $\delta > 0$ such that
\begin{equation*}
    g(\lambda) = \Pi_P(\x_0 - \lambda \nabla f(\x_0)) = \x_0 + \lambda \bd_{\x_0}^\Pi \quad \text{for all $\lambda \in [0,\delta)$}.
\end{equation*}

\end{corollary}

\begin{proof}
We have shown in Lemma \ref{constant normal cone} there exists a scalar $\delta > 0$ such that $g(\lambda)$, $g(\lambda^\prime)$ and $\x_0$ are co-linear for all $0<\lambda <\lambda^\prime<\delta$. In other words, this is equivalent to saying that $g(\lambda) = \x_0 + \lambda \mathbf{d}$ for all $\lambda \in [0,\delta)$, where $\bd = \frac{g(\lambda^\prime) - \x_0}{ \lambda^\prime} \in \mathbb{R}^n$ for an arbitrary $\lambda^\prime \in (0,\delta)$ (see \eqref{claim}). Now, the result follows by definition of the directional derivative:
\begin{equation} \label{directional}
    \bd_{\x_0}^\Pi = \lim_{\epsilon \downarrow 0} \frac{\Pi_P(\x_0 - \epsilon \nabla f(\x_0)) - \x_0}{\epsilon}
    = \lim_{\epsilon \downarrow 0}\frac{g(\epsilon) - \x_0}{\epsilon}
    = \frac{g(\lambda^\prime) - \x_0}{\lambda^\prime} = \bd.
\end{equation}
\qed \end{proof}

We will also need the following lemma to prove Theorem \ref{existence-new}. So far, we have shown that equal normal cones at $g(\lambda)$ and $g(\lambda^\prime)$ imply linear curve between these (Lemma \ref{equivalence}). There exists some $\delta >0$ such that normal cones up to $g(\lambda)$ $(\lambda<\delta)$ do not change around $\x_0$ (Lemma \ref{constant normal cone}), and projections form a line from $\x_0$ to $g(\delta)$ (Corollary \ref{normal cone}). We next show the converse: if projections do form a line emanating from $\x_0$ up to some $g(\theta)$, then the normal cones up to $g(\lambda)$ $(\lambda<\theta)$ must also be the same. (This means that $\theta \geq \delta$.)

\begin{lemma}\label{projection forms a line} Let $P \subseteq \mathbb{R}^n$ be a polytope defined using $m$ facet inequalities (e.g., as in \eqref{polytope}). Let $\x_0\in P$ and we are given $\nabla f(\x_0) \in \mathbb{R}^n$. Let $g(\lambda) = \Pi_P(\x_0 - \lambda \nabla f(\x_0))$ be the parametric projections curve. Suppose the projections curve is linear from $\x_0$ up to $g(\delta)$ for some $\delta \geq 0$, i.e.:
\begin{equation*}
    g(\lambda) = \Pi_P(\x_0 - \lambda \nabla f(\x_0)) = \x_0 + \lambda \mathbf{d} \quad \text{for all $\lambda \in [0,\delta]$},
\end{equation*}
for some direction $\bd \in \mathbb{R}^n$. Then, $N_P(g(\lambda)) = N_P(g(\lambda^\prime)) \subseteq N_P(\x_0)$, for all $0<\lambda<\lambda^\prime < \delta$.
\end{lemma}
\begin{proof}
Let $I$ and $J$ denote the index-set of active and inactive constraints at $\x_0$ respectively. We will show that $N_P(g(\lambda)) = N_P(g(\lambda^\prime)) \subseteq N_P(\x_0)$ for all $0<\lambda<\lambda^\prime < \delta$. Our first claim is that since $\lambda^\prime<\delta$, inactive constraints at $\x_0$ must remain inactive (claim (a)), and second, we use the fact that the projection is linear to show that the active constraints are maintained at all $\lambda, \lambda^\prime \in (0, \delta)$ (claim (b)). Now, fix $\lambda,\lambda^\prime \in (0,\delta)$ arbitrarily such that $\lambda^\prime > \lambda$.

\begin{itemize}
    \item[(a)] {\bf Inactive constraints remain inactive:} We show that $\A_Jg(\lambda) < \mathbf{b}_J$ and $\A_Jg(\lambda^\prime) < \mathbf{b}_J$ (component-wise). Since $\x_0 + \delta \bd \in P$,
\begin{equation*}
    \A_J g(\delta) = \A_J (\x_0 + \delta\bd) \leq \mathbf{b}_{J}
\end{equation*}
which implies that $\A_J \bd \leq \frac{\mathbf{b}_{J} - \A_J \x_0}{\delta}$. Now, for any $\lambda < \delta$, we have
\begin{equation*}
    \A_J g(\lambda) = \A_J (\x_0 + \lambda\bd) \leq \A_J\x_0 + \lambda\frac{\mathbf{b}_{J} - \A_J \x_0}{\delta} = \left( 1 -\frac{\lambda}{\delta} \right)\A_J\x_0 + \mathbf{b}_{J} \frac{\lambda}{\delta} < \mathbf{b}_{J}.
\end{equation*}
where the last (strict) inequality follows from the fact that we are taking a convex combination. This shows $\A_Jg(\lambda) < \mathbf{b}_J$ (component-wise) for all $\lambda \in (0,\delta)$. This implies that $N_P(g(\lambda)) \subseteq N_P(\x_0)$ for all $\lambda \in (0,\delta)$.

    \item[(b)] {\bf Active constraints are maintained:} We show that  active constraints at $g(\lambda)$ and $g(\lambda^\prime)$ are the same. Since we know $A_J g(\lambda) < b_J$, $A_J g(\lambda^\prime) < b_J$, we need to check the constraints in the index set $I$, the set of active constraints at $\x_0$. Consider any $i \in I$. Since $\innerprod{\mathbf{a}_i}{\x_0} = b_i$ and $\x_0 + \delta \bd \in P$ $(\delta>0)$, we know that $\innerprod{\mathbf{a}_i}{\bd} \leq 0$. If $\innerprod{\mathbf{a}_i}{\bd} = 0$, then since $g(\lambda) = \x_0 + \lambda \mathbf{d}$, we see that $\innerprod{\mathbf{a}_i}{g(\lambda)} = b_i$ for all $\lambda \in [0,\delta]$. So the constraint corresponding to $\mathbf{a}_i$ is active at both $g(\lambda)$ and $g( \lambda^\prime)$. On the other hand, if $\innerprod{\mathbf{a}_i}{\bd} < 0$, then this constraint must become inactive at $g(\lambda)$, for any $\lambda>0$, i.e., we have
\begin{equation*}
    \innerprod{\mathbf{a}_i}{g(\lambda)} = \innerprod{\mathbf{a}_i}{\x_0 + \lambda \bd} < b_i,
\end{equation*}
and therefore, any constraint in $I$ inactive at $g(\lambda)$ must also be inactive at $g(\lambda^\prime)$.
\end{itemize}
We have thus shown that the set of active constraints are the same, i.e. $N_P(g(\lambda)) = N_P(g(\lambda^\prime))\subseteq N_P(\x_0)$, for all $\lambda, \lambda^\prime \in (0, \delta)$.

\qed \end{proof}

So far, we have shown that equal normal cones at $g(\lambda)$ and $g(\lambda^\prime)$ imply linear curve between these (Lemma \ref{equivalence}). There exists some $\delta >0$ such that normal cones up to $g(\lambda)$ $(\lambda<\delta)$ do not change around $\x_0$ (Lemma \ref{constant normal cone}), and projections form a line from $\x_0$ to $g(\delta)$ (Corollary \ref{normal cone}). We have also shown the converse: if projections do form a line emanating from $\x_0$ up to some $g(\theta)$, then the normal cones up to $g(\lambda)$ $(0<\lambda<\theta)$ must also be the same and a subset of normal cone at $\x_0$. We now show that the maximum value of $\theta$ and $\delta$ is the same, and corresponds to the maximum step-size in the directional derivative of $\mathbf{w} = \nabla f(\x_0)$ at $\x_0$. These properties together give us Theorem \ref{existence-new}.

We are now ready to prove the following:
\existencenew*

\begin{proof}
We now put everything together to complete the proof of Theorem \ref{existence-new}.

\textit{Claim.} We first claim that:
\begin{equation} \label{claim theorem 2}
    g(\lambda) = \x_0 + \lambda \bd_{\x_0}^\Pi \quad \text{for all $\lambda \in [0,\lambda_1^{-}]$},
\end{equation}
which, in particular, means that $\x_1 = g(\lambda_1^{-}) = \x_0 + \lambda_1^{-} \bd_{\x_0}^\Pi$, using the definition of $\x_1$.

\begin{itemize}
\item[\textit{Pf. }] We know using Corollary \ref{normal cone} that $\exists \delta>0$ such that $g(\lambda) = \x_0 + \lambda \bd_{\x_0}^\Pi$ for all $\lambda \in [0,\delta)$. Hence, to prove the claim, we have to show $g(\lambda^\prime) = \x_0 + \lambda^\prime \bd_{\x_0}^\Pi$ for all $\lambda^\prime \in [\delta,\lambda_1^{-}]$. Using \eqref{directional}, we know that
\begin{equation*}
  \x_0 + \lambda^\prime \bd_{\x_0}^\Pi = \x_0 + \frac{\lambda^\prime}{\lambda}(g(\lambda) - \x_0) \quad \text{for any $\lambda \in (0,\delta)$.}
\end{equation*}
Then, since $\x_0 + \frac{\lambda^\prime}{\lambda}(g(\lambda) - \x_0) \in P$ by definition of $\lambda_1^{-}$ and  $\lambda^\prime > \lambda$, using Lemma \ref{affine-hull} we have $g(\lambda^\prime)  = \x_0 + \frac{\lambda^\prime}{\lambda}(g(\lambda) - \x_0) = \x_0 + \lambda^\prime \bd_{\x_0}^\Pi$. The claim now follows since $\lambda^\prime$ was arbitrary.
\end{itemize}

We can now complete the proof of the theorem as follows.

\begin{itemize}
    \item [Case $(i)$] Since, $g(\lambda) = \x_0 + \lambda \bd_{\x_0}^\Pi$ for all $\lambda \in [0,\lambda_1^{-}]$, it follows from Lemma \ref{projection forms a line} that $N_P(g(\lambda)) = N_P(g(\lambda^\prime)) \subseteq N_P(\x_0)$ for all $0<\lambda<\lambda^\prime < \lambda_1^{-}$. This shows that $(i)$ in Theorem \ref{existence-new} holds.
    \item [Case $(ii)$]
   Note that $I(g(\lambda)) \subseteq I(\x_0)$ for any $\lambda\in [0, \lambda_1^{-})$ by property $(i)$. Therefore, for any $i \in I(g(\lambda))$, we have
\begin{align*}
    \innerprod{\mathbf{a}_i}{g(\lambda)} =\innerprod{\mathbf{a}_i}{\x_0 + \lambda \bd_{\x_0}^\Pi} = b_i &\implies \innerprod{\mathbf{a}_i}{\bd_{\x_0}^\Pi} = 0\\ &\implies \innerprod{\mathbf{a}_i}{\x_1} = \innerprod{\mathbf{a}_i}{\x_0 + \lambda_1^{-} {\bd_{\x_0}^\Pi}} = b_i,
\end{align*}
and so the constraint corresponding to $\mathbf{a}_i$ (which is active at $g( \lambda)$) is also active at $\x_1$. We have thus shown that $N_P(g(\lambda)) \subseteq N_P(\x_1)$ for all $\lambda \in (0,\lambda_1^{-})$.

We will now show that this containment is strict, i.e. there is at least one constraint that is active at $\x_1$ but is not active at $g(\lambda)$ for all $\lambda \in (0,\lambda_1^{-})$. Note that since $\bd_{\x_0}^\Pi$ is a feasible direction at $\x_0$, we have $\innerprod{\mathbf{a}_i}{\bd_{\x_0}^\Pi} \leq 0$ for all {$i \in I(\x_0)$}. Thus, it follows that the maximum step size in which we can move along $\bd_{\x_0}^\Pi$ is given by
\begin{equation} \label{max lambda}
    \lambda_1^{-} = \min_{\substack{j \in J:\\ \innerprod{\mathbf{a}_j}{\bd_{\x_0}^\Pi} > 0}} \frac{b_j - \innerprod{\mathbf{a}_j}{\x_0}}{\innerprod{\mathbf{a}_j}{\bd_{\x_0}^\Pi}},
\end{equation}
where the feasible set of the above problem is non-empty, since otherwise this would imply that $\bd_{\x_0}^\Pi$ is a recessive direction (i.e. direction of unboundedness), contradicting the fact that $P$ is a polytope. Let $j^*$ be any optimal index to the optimization problem in \eqref{max lambda}, where $\innerprod{\mathbf{a}_{j^*}}{\x_1} = b_{j^*}$. Now, for any $\lambda \in (0,\lambda_1^{-})$
\begin{align*}
        \innerprod{\mathbf{a}_{j^*}}{g(\lambda)} &= \innerprod{\mathbf{a}_{j^*}}{\x_0 + \lambda \bd_{\x_0}^\Pi} \\
        &< \innerprod{\mathbf{a}_{j^*}}{\x_0 + \lambda_1^{-} \bd_{\x_0}^\Pi}  &(\text{choice of $\lambda$ and $\innerprod{\mathbf{a}_{j^*}}{\bd_{\x_0}^\Pi} >0$})\\
        &= b_{j^*},
\end{align*}
implying that the constraint $\mathbf{a}_{j^*}$ is not active at $g(\lambda)$. Thus, we have $N_P(g(\lambda)) \subset N_P(\x_1)$ for all $\lambda \in (0,\lambda_1^{-})$, which shows property $(ii)$ in Theorem \ref{existence-new}.
\end{itemize}

\qed \end{proof}

\subsection{Proof of Theorem \ref{invariance}}

To prove this theorem we first claim that the first linear segment of the projection curve starting at the $i-1^\text{th}$ breakpoint $\x_{i-1}$ with respect to any vector $\mathbf{w}$ is the same as the $i^\text{th}$ piecewise linear segment of the projection curve starting from $\x_0$ with respect to $\mathbf{w}$. Suppose $\mathbf{w} = \nabla f(\x_0)$, then the invariance property we would like to specifically show is:

\begin{lemma}[Invariance of projections] \label{invariance of proj}
Let $P \subseteq \mathbb{R}^n$ be a polytope. Let $\x_{0} \in P$ and $\nabla f(\x_0) \in \mathbb{R}^n$ be given. Further, let $\x_{i-1} \in P$ be the $i$th breakpoint in the projections curve $g(\lambda) = \Pi_{P}(\x_0 -\lambda \nabla f(\x_0))$, with $\x_{i-1}=\x_0$ for $i=1$. Let $g(\lambda) = \Pi_P(\x_0 - \lambda \nabla f(\x_0))$ be the parametric projections curve. Then we claim the following invariance property of  of orthogonal projections:
\begin{equation} \label{invaraint equation}
  \tilde{g}(\lambda) := \Pi_P(\x_{i-1} - (\lambda - \lambda_{i-1}^{+}) \nabla f(\x_0)) = g(\lambda) \quad \text{for $\lambda \in [\lambda_{i-1}^{+}, \lambda_{i}^{-}]$}.
\end{equation}
\end{lemma}

\begin{proof}
Fix a non-negative scalar ${\lambda} \in [\lambda_{i-1}^{+}, \lambda_{i}^{-}]$ and suppose for a contradiction that $\tilde{g}({\lambda}) = \mathbf{z}$ and $g({\lambda}) = \mathbf{y}$ where $\mathbf{z} \neq\mathbf{y}$. Then, since $\mathbf{z}$ is not the projection $g(\lambda) = \Pi_{P}(\x_0 - \lambda \nabla f(\x_0))$, we know there exists $\tilde{\mathbf{z}}\in P$:
\begin{align}
    &\innerprod{\x_0- \lambda \nabla f(\x_0) - \mathbf{z}}{\tilde{\mathbf{z}} - \mathbf{z}} > 0\\
    \Rightarrow &\innerprod{\x_0- \lambda_{i-1}^{+} \nabla f(\x_0) - \x_{i-1}}{\tilde{\mathbf{z}} - \mathbf{z}} + \innerprod{\x_{i-1}  - (\lambda - \lambda_{i-1}^{+}) \nabla f(\x_0) - \mathbf{z}}{\tilde{\mathbf{z}} - \mathbf{z}} > 0\nonumber\\
    \Rightarrow &\innerprod{\x_0- \lambda_{i-1}^{+} \nabla f(\x_0) - \x_{i-1}}{\tilde{\mathbf{z}} - \mathbf{z}} > 0 \label{eq-31}\\
    \Rightarrow & \innerprod{\x_0- \lambda_{i-1}^{+} \nabla f(\x_0) - \x_{i-1}}{\tilde{\mathbf{z}} - \x_{i-1}} + \innerprod{\x_0- \lambda_{i-1}^{+} \nabla f(\x_0) - \x_{i-1}}{\x_{i-1} - \mathbf{z}} > 0, \nonumber\\
    \Rightarrow & \innerprod{\x_0- \lambda_{i-1}^{+} \nabla f(\x_0) - \x_{i-1}}{\x_{i-1} - \mathbf{z}} > 0,\label{eq-32}
\end{align}

where \eqref{eq-31} follows by first-order optimality at $\mathbf{z}$, and \eqref{eq-32} follows by first-order optimality at $\mathbf{\x_{i-1}}$. Using Theorem \ref{existence-new} with the projections curve starting at $\x_{i-1}$ with parameter $\theta = (\lambda - \lambda_{i-1}^{+})$, we have
\begin{equation}\label{invariant equation 2}
    \tilde{g}(\theta + \lambda_{i-1}^+) := \Pi_P(\x_{i-1} - \theta \nabla f(\x_0)) = \x_{i-1} + \theta \bd_{\x_{i-1}}^\Pi(\nabla f(\x_0)), \text{ for all } \theta \in [0, \lambda_{i}^{-}-\lambda_{i-1}^+],
\end{equation}
 where recall that $\bd_{\x_{i-1}}^\Pi (\nabla f(\x_0))$ is the directional derivative at $\x_{i-1}$ with respect to the direction given by $\nabla f(\mathbf{x}_0)$:
\begin{align*}
    \bd_{\x_{i-1}}^\Pi (\nabla f(\x_0)) &= \lim_{\epsilon \downarrow 0} \frac{\Pi_p(\x_{i-1} - \epsilon \nabla f(\mathbf{x}_0)) - \x_{i-1}}{\epsilon}.
\end{align*}
 Thus, using this fact in \eqref{invariant equation 2}, we have
\begin{align*}
    &\innerprod{\x_0- \lambda_{i-1}^{+} \nabla f(\x_0) - \x_{i-1}}{\x_{i-1} - \mathbf{z}} = \innerprod{\x_0- \lambda_{i-1}^{+} \nabla f(\x_0) - \x_{i-1}}{\x_{i-1} - \tilde{g}(\lambda)}\\
    & \quad =\innerprod{\x_0- \lambda_{i-1}^{+} \nabla f(\x_0) - \x_{i-1}}{{-}(\lambda - \lambda_{i-1}^{+}) \bd_{\x_{i-1}}^\Pi (\nabla f(\x_0))} > 0 ~~\text{for } \lambda>\lambda_{i-1}^+\\
    & \quad \Rightarrow \innerprod{\x_0- \lambda_{i-1}^{+} \nabla f(\x_0) - \x_{i-1}}{\bd_{\x_{i-1}}^\Pi (\nabla f(\x_0))}
    {<} 0
\end{align*}
This gives a contradiction since $\innerprod{\x_0- \lambda_{i-1}^{+} \nabla f(\x_0) - \x_{i-1}}{\bd_{\x_{i-1}}^\Pi (\nabla f(\x_0)} = 0$ by the definition of $\lambda_{i-1}^+$ and $\bd_{\x_{i-1}}^\Pi (\nabla f(\x_0))$.

\qed \end{proof}

\invariance*

\begin{proof}
To prove this theorem, we first consider the case when $\bd_{\x_{i-1}}^\Pi(\nabla f(\x_0)) \neq \mathbf{0}$. In Lemma \ref{invariance of proj} (equations \eqref{invaraint equation} and \eqref{invariant equation 2}), we showed that $\tilde{g}(\lambda) =  \x_{i-1} + (\lambda - \lambda_{i-1}^{+}) \bd_{\x_{i-1}}^\Pi (\nabla f(\x_0)) = g(\lambda)$ for $\lambda \in [\lambda_{i-1}^{+}, \lambda_{i}^{-}]$. This shows that the projections curve is linear between $\lambda_{i-1}^{+}$ and $\lambda_{i}^{-}$. Moreover, using Theorem \ref{existence-new} with characterization in \eqref{invariant equation 2}, we immediately have that $\x_i = g(\lambda_i^{-}) = \x_{i-1} + (\lambda_i^- - \lambda_{i-1}^+)\bd_{\x_{i-1}}^\Pi (\nabla f(\x_0))$ and  $N_P(g(\lambda)) = N_P(g(\lambda^\prime)) \subseteq N_P(\x_{i-1})$, for all $ \lambda_{i-1}^{+} <\lambda< \lambda^\prime < \lambda_{i}^{-}$.

\textit{Claim:} {\bf Drop in normal cone:} If $ \lambda_{i-1}^{-} < \lambda_{i-1}^{+}$, then we further claim that this containment has to be strict, i.e., $N_P(g(\lambda)) \subset N_P(\x_{i-1})$ for $\lambda \in (\lambda_{i-1}^{+}, \lambda_{i}^{-})$.

\begin{itemize}[leftmargin=15pt]
    \item[{\it Pf.}] Suppose for a contradiction that $N_P(g(\lambda)) = N_P(\x_{i-1})$ for some $\lambda_{i-1}^{+} <\lambda < \lambda_{i}^{-}$.

    Using Lemma \ref{equivalence} (linearity of projections), we know that $g(\lambda_{i-1}^{+}) = \delta g(\lambda_{i-1}^{-}) + (1 - \delta) g(\tilde{\lambda})$ for $\delta = \frac{\lambda_{i-1}^+ - \lambda_{i-1}^-}{\lambda_i^- - \lambda_{i-1}^-} \in (0,1)$. But this is a contradiction since $g(\lambda_{i-1}^+) = g(\lambda_{i-1}^-) = \x_{i-1}$ and $g(\tilde{\lambda}) \neq \x_{i-1}$ as $\bd_{\x_{i-1}}^{\Pi}(\nabla f(\x_0)) \neq \mathbf{0}$.
\end{itemize}

This shows that properties $(i)$ and $(ii)$ hold. Moreover, property $(iii)$ immediately holds using $(ii)$ in Theorem \ref{existence-new} with $(\lambda - \lambda_{i-1}^{+})$ in place $\lambda$ and $g(\lambda_{i-1}^{+})$ in place of $\x_0$.

Now, suppose that $\bd_{\x_{i-1}}^\Pi(\nabla f(\x_0)) =\mathbf{0}$. Therefore, it follows that $-\nabla f(\x_{0}) \in N_P(\x_{i-1})$, i.e. $\innerprod{-\nabla f(x_0)}{\mathbf{z} - \x_{i-1}} \leq 0$ for all $\mathbf{z} \in P$. We will now show that this implies that $g(\lambda) = \x_{i-1}$ for all $\lambda \geq \lambda_{i-1}^{+}$, so that $\x_{i-1}$ is indeed endpoint of the curve. Using the first-order optimality condition of $ g(\lambda_{i-1}^{+}) = \x_{i-1}$ we have
\begin{align*}
    \innerprod{\x_0- \lambda_{i-1}^{+} \nabla f(\x_0) - \x_{i-1}}{\mathbf{z} - \x_{i-1}} \leq 0 \quad \forall \mathbf{z} \in P.
\end{align*}
Using the fact that $\innerprod{\nabla f(x_0)}{\mathbf{z} - \x_{i-1}} \leq 0$ for all $\mathbf{z} \in P$ and $\lambda \geq \lambda_{i-1}^{+}$, we get
\begin{align*}
    \innerprod{\x_0-\lambda \nabla f(\x_0) - \x_{i-1}}{\mathbf{z} - \x_{i-1}} \leq 0 \quad \forall \mathbf{z} \in P.
\end{align*}
so that $\x_{i-1}$ satisfies the first-order optimality condition for $g(\lambda)$. This completes the proof.
\qed \end{proof}

\iffalse
Moreover, $\bd_{\x_{i-1}}^\Pi(\nabla f(\x_0)) =\mathbf{0}$, it follows that From \eqref{directional} with the projections curve starting at $\x_{i-1}$, we know that $\mathbf{d}_{\mathbf{x}}^\Pi = \frac{\Pi_P(\x_{i-1} - \epsilon \nabla f(\x_0)) -\x_{i-1}}{\epsilon}$ for $\epsilon > 0$ sufficiently small. Hence, the assumption that $\bd_{\x_{i-1}}^\Pi(\nabla f(\x_0)) =\mathbf{0}$ implies that $\Pi_P(\x_{i-1} - \epsilon \nabla f(\x_0)) = \x_{i-1}$. Using the first-order optimality of $\Pi_P(\x_{i-1} - \epsilon \nabla f(\x_0))$, this implies that
\fi

This proof gives a constructive approach for computing the different linear segments of $g(\lambda)$, where given a current breakpoint $\x_{i-1}$, the next segment of the curve is obtained by computing the directional derivative at $\x_{i-1}$ with respect to the direction given by $\nabla f(\mathbf{x}_0)$.

\subsection{Proof of Theorem \ref{breakpoints}}

\breakpoints*

\begin{proof}
Fix $\mathbf{x} \in P$ and consider the procedure $\textsc{Trace}(\x, \nabla f(\x))$. The fact that $\textsc{Trace}(\x, \nabla f(\x))$ correctly traces the curve $g(\lambda) = \Pi_P(\mathbf{x} - \lambda \nabla f(\mathbf{x}))$ follows from the constructive proof given for Theorem \ref{invariance}. Moreover, upon termination there are two things that can happen: (i) the line-search evaluates to a step-size that is not maximal in one of the segments of $g(\lambda)$, (ii) we reach the end point of the curve $\mathbf{v}^* = \lim_{\lambda \to \infty} g(\lambda)$ (as defined in Theorem \ref{FW limit}). At this point, we know that $-\nabla f(\x) \in N_P(\mathbf{v}^*)$. Recall that for any $\x \in P$, we can compute the directional derivative using a single projection:
\begin{equation*}
   \bd_{\x}^\Pi = \frac{\Pi_P(\x - \epsilon \nabla f(\x)) - \x}{\epsilon},
\end{equation*}
where $\epsilon$ is sufficiently small. Thus, when recomputing the directional derivative in the subsequent iteration:
\begin{equation*}
   \frac{\Pi_P(\mathbf{v}^* - \epsilon \nabla f(\x)) - \mathbf{v}^*}{\epsilon} = \frac{\mathbf{v}^* - \mathbf{v}^*}{\epsilon} = \mathbf{0},
\end{equation*}
where $\epsilon$ is again sufficiently small. The second equality above follows from the definition of $\mathbf{v}^*$ and Lemma \ref{basecase}. This proves the correctness of the termination criterion given in Algorithm \ref{alg: tracing PW proj}.

Once the curve leaves the interior of a face, it can no longer visit the face again. This is because equivalence of normal cones at two projections implies the projections curve is linear between the two points (Lemma \ref{equivalence}). Therefore, the number of breakpoints can be at most the number of faces, i.e.,  $O(2^m)$.

\qed \end{proof}

config: arxiv


TITLE: Show that $\arg\frac{z-1}{z+1} = \frac{\pi}{2}$ when $\operatorname{Im} z > 0$ for $|z| = 1$
QUESTION [2 upvotes]: I've been trying to prove the statement above for sometime and I feel like I am close. I was wondering if I could get some help with my ideas, to see if they are even close.
I have that $\arg \frac{z-1}{z+1} = \arg z-1 - \arg z+1$.
Also if we let $z = x + iy$, then clearly $z-1 = x-1 + iy$ and $z+1 = x+1 - iy$, from this we can see that $\operatorname{Im}z-1 = \operatorname{Im} z+1$.
Suppose $\arg z-1 = \beta$, $\arg z+1 = \theta$. I'm pretty sure the statement above implies that $\cos(\beta - \frac \pi 2) = \sin \theta$. And $\cos\theta_1 = \sin\theta_2$ for when $\theta_1 = \theta_2 = \frac{\pi}{4}$ so $\beta = \frac{3\pi}{4}$ and $\theta = \frac{\pi}{4}$ and this $\beta - \theta = \arg z-1 - \arg z+1 = \frac{\pi}{2}$.
If this is the correct logic at all I really need to fill in some holes, if not can I please have some hints at the right path to take.

REPLY [2 votes]: $$w=\dfrac{z-1}{z+1}=\dfrac{z-1}{z+1}\dfrac{\overline{z}+1}{\overline{z}+1}=i\dfrac{2{\bf Im\,}z}{|z+1|^2}$$
which shows
$${\bf Re\,}w=0~~~,~~~{\bf Im\,}w=\dfrac{2{\bf Im\,}z}{|z+1|^2}>0$$
thus
$\color{blue}{\arg w = \dfrac{\pi}{2}}$.


TITLE: Convergence of characteristic functions to $1$ on a neighborhood of $0$ and weak convergence
QUESTION [4 upvotes]: Prove the following statement:
$ X_n \Rightarrow 0 $ (convergence in distribution) if and only if $ (\exists\; \epsilon>0: |t|<\epsilon) \;\; \phi_n(t) \rightarrow 1  $, where $\phi_n(t)$ is the characteristic function of the random variable $X_n$.
We could write $X_n \rightarrow 0 $ in probability since convergence in probability to a constant and convergence in distribution to a constant are the same concept.
I guess Lévy's continuity theorem implies the 'only if' part.
Thank you very much for your help in advance!

REPLY [7 votes]: If $X_n\to 0$ in distribution, then any $\varepsilon$ does the job.
The converse is harder. Here it is the proof of Levy's continuity theorem which will be used rather than the result in itself. Denoting by $\varphi_n$ the characteristic function of $X_n$ and $\mu_n$ its distribution, we indeed have the equality
$$\tag{1}\varepsilon^{-1}\int_{-\varepsilon}^\varepsilon(1-\varphi_n(t))\mathrm dt=2\int_\Omega\left(1-\frac{\sin(x\varepsilon)}{x\varepsilon}\right)\mathrm d\mu_n(x)$$
which admits the lower bound
$$\tag{2}2\int_{\{|x|\geqslant 2/\varepsilon\}}\left(1-\frac1{|\varepsilon x|}\right)\mathrm d\mu_n(x)\geqslant \mu\{|X_n|\geqslant 2/\varepsilon\}.$$
The LHS in (1) goes to $0$ as $n$ goes to infinity because of the assumption and dominated convergence. Hence, by (2),
$$\tag{3}\lim_{n\to\infty}\mu\{|X_n|\geqslant 2/\varepsilon\}=0.$$
This gives in particular tightness of the sequence $(X_n)_{n\geqslant 1}$. Now we have to prove that the only limit we can have for a subsequence is necessarily $0$.
Assume that a subsequence $(Y_k)_{k\geqslant 1}$ of $(X_n)_{n\geqslant 1}$ converges in distribution to some $Y$. Then $\varphi_Y(t)=1$ if $|t|\lt \varepsilon$ and $Y$ is bounded. Indeed, we take $t_0$ a continuity point of the cumulative distribution function of $|Y|$ such that $t_0\geqslant 2/\varepsilon$. Then by (3),
$$0=\lim_{n\to \infty}\mu\{|X_n|\gt t_0\}=\mu\{|Y|\gt t_0\}.$$
The characteristic function is then analytic, hence equal to $1$ on the whole real line.


TITLE: Show that T is a not a topology on X
QUESTION [0 upvotes]: Let $X=\{a, b, c, d, e\}$ and $T_2=\{X,\emptyset, \{a\},\{c,d\}, \{a,c,e\}, \{b,c,d\}\}$.
I know that $T_2$ is not a topology on X as the union of two members of $T_2$ does not belong to $T_2$, but is it also because of the intersection. For example, $ \{c,d\} \cap \{a, c, e\}=\{c\}$ which is not a member of $T_2$. I just want to make sure I fully understand how to prove that $T_2$ is or is not a topology on X.

REPLY [0 votes]: Yes, exhibiting two sets in $T_2$ whose intersection is not an set in $T_2$ proves that it doesn't define the open sets of a topology, since the collection of open sets of a topology is closed under finite intersections.
(Friendly advice: this is the kind of question (checking against definitions) you must get comfortable and confident answering on your own. It will just slow down your learning otherwise, and also going over a proposed answer and checking it carefully helps you to learn the topic better.)


TITLE: 'Simple' capacitor problem
QUESTION [6 upvotes]: I posted this question because I have a problem in grasping the connection between force on a charge and voltage potential equilibrium. So the problem is the following: we have a charged capacitor disconnected from the battery. If a negative capacitor plate is divided into two pieces but still connected to each other with a wire and we do the same to the positive plate, the charge should be equally distributed. Now, if we decide to bring one half of the negative plate closer to the half part of the positive plate we changed potential but as far as the charge on the plate isn't moving the far negative plate-half and the closer negative plate-half should equally act on the positive pieces as the electric field is uniform and not dependent on distance between plates. There shouldn't be any difference in attraction between all plates. Now, a current should flow through the wire when one part of the capacitor is brought closer as the voltage is different but on the other hand it shouldn't if we take that the electric field on the charge between plates doesn't change with distance (in an ideal case)?

REPLY [0 votes]: If I understand correctly, the argument you're making is this. You know that in situations A and B, the fields between the top and bottom capacitors aren't going to be the same: that's what is meant by "current must flow". The charges will redistribute, because you know what the steady state in situation A is, and you know what the steady state in situation B is, and so you know that there must be some kind of redistribution. This is what quantumwave's answer is saying.
However, the paradox is that if you could freeze the charges in place, and move the top capacitor plates closer together, then as we go from situation A to B, the electric field acting on the unequal charges in the top capacitor plates hasn't changed, and neither has it changed on the charges in the bottom plates, and so there is no force to pull extra charges from the bottom to the top plates.
I can think of three possible arguments to explain what's happening here.

In order for the two plates to be brought closer together, you need to move them. This means they will have a non-zero velocity as we move from situations A to B. Therefore, there will be magnetic effects, and you can't use the results for the electrostatic steady state distribution of the charges on the capacitor plates. Although you can make this velocity $v$ as small as you like (quasi-static), the non-static field effects will be of the same order of magnitude as $v$, and so these could cause redistribution of the charges at a rate of order $v$, and if you integrate the non-static charge redistribution over the whole path, it will sum up to the required change of charge.
I find the above argument not so convincing, as in theory, we could fix the electrical charges in place during the transition from A to B. For example, we could cut the wire, then bring the top plates closer together, and then reconnect the wire afterwards. In other words, there must still be a path from the non-equilibrium situation B to the steady state.

The more convincing argument is that because of the introduction of the conducting wire between the bottom plates and the top plates, the charges in the wire and at the connection between the wire and the plates are not at equilibrium, so they will start moving, which will "kick-start" the motion of the charges towards equilibrium.

Finally, another line of argument might be that it's caused by the edge effects of the capacitor.

I would like to be give more details, by explaining exactly how the wires modify the electric field, but it's probably going to be quite complicated. I thought it might be interesting to study a toy model, where the plates are all parallel: you put down a capacitor at $z = 0$, then another at $z = z_0$, connect the plates by a vertical wire at $x = y = 0$, and then to connect the topmost plate to the bottommost plate, you make the whole of space loop along the $z$ axis, either by repeating the pattern, or by modifying the topology of the space. Unfortunately I don't have time to work through it, but if somebody else would like to give it some thought, that would be great.


TITLE: Can i define an inner product so my basis will be orthogonal?
QUESTION [1 upvotes]: Can every basis of a finite dinensional vector space be orthogonal with respect to some inner product? If no, than why?

REPLY [3 votes]: At least for a finite-dimensional vector space, the answer is "yes".
Given a basis $b_1, \ldots, b_n$, if you have two vectors $v$ and $w$, define their inner product as follows:

Write each in terms of the basis:
$$
v = x_1 b_1 + \ldots + x_n b_n \\
w = y_1 b_1 + \ldots + y_n b_n
$$
Compute the inner product as $x_1y_1 + \ldots + x_n y_n$.

I leave it to you to check that this is, indeed, an inner product, and that under this product the basis is orthonormal.

REPLY [1 votes]: Sure.  Here's why. To calculate the inner product of any two vectors, write each as a linear combination of the basis vectors and use the ordinary formula.
That will define an inner product, and the basis you started with is orthonomrmal.
This all works because the basis gives you a linear transformation that maps the (finite dimensional) vector space bijectively to $\mathbb{R}^n$ and you use the standard inner product there.

REPLY [1 votes]: Yes, that's true for finite dimensional vector spaces.
Let $K$ be $\mathbb{R}$ or $\mathbb{C}$ and let $V$ be a finite dimensional $K$-vector space. If $B=\{v_1,\cdots,v_n\}$ is a basis for $V$, consider $T\colon V\to K^n$ given by $T(v_i)=e_i$ (here $\{e_1,\cdots,e_n\}$ is the canonical basis for $K^n$). Clearly $T$ is an isomorphism.
Besides, we can define an inner product in $V$ by the formula: for $u,v\in V$,
$$\langle u,v\rangle_T = \langle T(u), T(v)\rangle$$
(Show this is in fact an inner product)
With such construction, $(V,\langle\cdot,\cdot\rangle_T)$ has $B$ as an orthonormal basis.


TITLE: time dependence of temperature equalization
QUESTION [2 upvotes]: Suppose you have two thermodynamical systems $X_1$ and $X_2$ (for example water and air) with different temperatures ($T_1 > T_2$). Now put them into thermal contact. Is there a formula which describes, how $T_1$ and $T_2$ changes with time?

REPLY [3 votes]: In a simple heat conduction theory (no convection) the corresponding time is determined with the lowest eigenvalue of the Sturm-Liouville problem: $\Delta T(t) = A\cdot e^{-t/\tau}$ (regular regime), see, for example, my article.
EDIT: For any time $t > 0$ the temperature difference is a series like
$\Delta T(t) = \sum_{n=0}^\infty A_n \cdot e^{-t/\tau_n}$
$\tau_{n+1} < \tau_n$, for example, $\tau_n \propto \frac{1}{\pi^2(n+1)^2}$.
When $t >> \tau_1$, the fast decaying exponentials $e^{-t/\tau_n}$ are small with respect to the slowest one $e^{-t/\tau_0}$ so only one term remains in this sum. The latter regime is called a regular regime of the heat exchange. For certain one-layer 1D systems $\tau \propto \frac{\rho c L^2}{\kappa \pi^2(n+1)^2}$ Here $\kappa$  is the heat conductivity, $\rho$  is the material density, $c$  is the specific heat capacity, and $L$  is the layer thickness (exact $n$-dependence  is determined with the boundary conditions).