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

section \<open>Binary Predicates Restricted to Elements of a Given Set\<close>

theory Restricted_Predicates
imports Main
begin

text \<open>
  A subset \<open>C\<close> of \<open>A\<close> is a \emph{chain} on \<open>A\<close> (w.r.t.\ \<open>P\<close>)
  iff for all pairs of elements of \<open>C\<close>, one is less than or equal
  to the other one.
\<close>
abbreviation "chain_on P C A \<equiv> pred_on.chain A P C"
lemmas chain_on_def = pred_on.chain_def

lemma chain_on_subset:
  "A \<subseteq> B \<Longrightarrow> chain_on P C A \<Longrightarrow> chain_on P C B"
by (force simp: chain_on_def)

lemma chain_on_imp_subset:
  "chain_on P C A \<Longrightarrow> C \<subseteq> A"
by (simp add: chain_on_def)

lemma subchain_on:
  assumes "C \<subseteq> D" and "chain_on P D A"
  shows "chain_on P C A"
using assms by (auto simp: chain_on_def)

definition restrict_to :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" where
  "restrict_to P A = (\<lambda>x y. x \<in> A \<and> y \<in> A \<and> P x y)"

definition reflp_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
  "reflp_on P A \<longleftrightarrow> (\<forall>a\<in>A. P a a)"

definition transp_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
  "transp_on P A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. P x y \<and> P y z \<longrightarrow> P x z)"

definition total_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
  "total_on P A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x = y \<or> P x y \<or> P y x)"

abbreviation "strict P \<equiv> \<lambda>x y. P x y \<and> \<not> (P y x)"

abbreviation "incomparable P \<equiv> \<lambda>x y. \<not> P x y \<and> \<not> P y x"

abbreviation "antichain_on P f A \<equiv> \<forall>(i::nat) j. f i \<in> A \<and> (i < j \<longrightarrow> incomparable P (f i) (f j))"

lemma strict_reflclp_conv [simp]:
  "strict (P\<^sup>=\<^sup>=) = strict P" by auto

lemma reflp_onI [Pure.intro]:
  "(\<And>a. a \<in> A \<Longrightarrow> P a a) \<Longrightarrow> reflp_on P A"
  unfolding reflp_on_def by blast

lemma transp_onI [Pure.intro]:
  "(\<And>x y z. \<lbrakk>x \<in> A; y \<in> A; z \<in> A; P x y; P y z\<rbrakk> \<Longrightarrow> P x z) \<Longrightarrow> transp_on P A"
  unfolding transp_on_def by blast

lemma total_onI [Pure.intro]:
  "(\<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x = y \<or> P x y \<or> P y x) \<Longrightarrow> total_on P A"
  unfolding total_on_def by blast

lemma reflp_on_reflclp_simp [simp]:
  assumes "reflp_on P A" and "a \<in> A" and "b \<in> A"
  shows "P\<^sup>=\<^sup>= a b = P a b"
  using assms by (auto simp: reflp_on_def)

lemma reflp_on_reflclp:
  "reflp_on (P\<^sup>=\<^sup>=) A"
  by (auto simp: reflp_on_def)

lemma reflp_on_converse_simp [simp]:
  "reflp_on P\<inverse>\<inverse> A \<longleftrightarrow> reflp_on P A"
  by (auto simp: reflp_on_def)

lemma transp_on_converse:
  "transp_on P A \<Longrightarrow> transp_on P\<inverse>\<inverse> A"
  unfolding transp_on_def by blast

lemma transp_on_converse_simp [simp]:
  "transp_on P\<inverse>\<inverse> A \<longleftrightarrow> transp_on P A"
  unfolding transp_on_def by blast

lemma transp_on_reflclp:
  "transp_on P A \<Longrightarrow> transp_on P\<^sup>=\<^sup>= A"
  unfolding transp_on_def by blast

lemma transp_on_strict:
  "transp_on P A \<Longrightarrow> transp_on (strict P) A"
  unfolding transp_on_def by blast

lemma reflp_on_subset:
  "A \<subseteq> B \<Longrightarrow> reflp_on P B \<Longrightarrow> reflp_on P A"
  by (auto simp: reflp_on_def)

lemma transp_on_subset:
  "A \<subseteq> B \<Longrightarrow> transp_on P B \<Longrightarrow> transp_on P A"
  by (auto simp: transp_on_def)

definition wfp_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
where
  "wfp_on P A \<longleftrightarrow> \<not> (\<exists>f. \<forall>i. f i \<in> A \<and> P (f (Suc i)) (f i))"

definition inductive_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
  "inductive_on P A \<longleftrightarrow> (\<forall>Q. (\<forall>y\<in>A. (\<forall>x\<in>A. P x y \<longrightarrow> Q x) \<longrightarrow> Q y) \<longrightarrow> (\<forall>x\<in>A. Q x))"

lemma inductive_onI [Pure.intro]:
  assumes "\<And>Q x. \<lbrakk>x \<in> A; (\<And>y. \<lbrakk>y \<in> A; \<And>x. \<lbrakk>x \<in> A; P x y\<rbrakk> \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> Q y)\<rbrakk> \<Longrightarrow>  Q x"
  shows "inductive_on P A"
  using assms unfolding inductive_on_def by metis

text \<open>
  If @{term P} is well-founded on @{term A} then every non-empty subset @{term Q} of @{term A} has a
  minimal element @{term z} w.r.t. @{term P}, i.e., all elements that are @{term P}-smaller than
  @{term z} are not in @{term Q}.
\<close>
lemma wfp_on_imp_minimal:
  assumes "wfp_on P A"
  shows "\<forall>Q x. x \<in> Q \<and> Q \<subseteq> A \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. P y z \<longrightarrow> y \<notin> Q)"
proof (rule ccontr)
  assume "\<not> ?thesis"
  then obtain Q x where *: "x \<in> Q" "Q \<subseteq> A"
    and "\<forall>z. \<exists>y. z \<in> Q \<longrightarrow> P y z \<and> y \<in> Q" by metis
  from choice [OF this(3)] obtain f
    where **: "\<forall>x\<in>Q. P (f x) x \<and> f x \<in> Q" by blast
  let ?S = "\<lambda>i. (f ^^ i) x"
  have ***: "\<forall>i. ?S i \<in> Q"
  proof
    fix i show "?S i \<in> Q" by (induct i) (auto simp: * **)
  qed
  then have "\<forall>i. ?S i \<in> A" using * by blast
  moreover have "\<forall>i. P (?S (Suc i)) (?S i)"
  proof
    fix i show "P (?S (Suc i)) (?S i)"
      by (induct i) (auto simp: * ** ***)
  qed
  ultimately have "\<forall>i. ?S i \<in> A \<and> P (?S (Suc i)) (?S i)" by blast
  with assms(1) show False
    unfolding wfp_on_def by fast
qed

lemma minimal_imp_inductive_on:
  assumes "\<forall>Q x. x \<in> Q \<and> Q \<subseteq> A \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. P y z \<longrightarrow> y \<notin> Q)"
  shows "inductive_on P A"
proof (rule ccontr)
  assume "\<not> ?thesis"
  then obtain Q x
    where *: "\<forall>y\<in>A. (\<forall>x\<in>A. P x y \<longrightarrow> Q x) \<longrightarrow> Q y"
    and **: "x \<in> A" "\<not> Q x"
    by (auto simp: inductive_on_def)
  let ?Q = "{x\<in>A. \<not> Q x}"
  from ** have "x \<in> ?Q" by auto
  moreover have "?Q \<subseteq> A" by auto
  ultimately obtain z where "z \<in> ?Q"
    and min: "\<forall>y. P y z \<longrightarrow> y \<notin> ?Q"
    using assms [THEN spec [of _ ?Q], THEN spec [of _ x]] by blast
  from \<open>z \<in> ?Q\<close> have "z \<in> A" and "\<not> Q z" by auto
  with * obtain y where "y \<in> A" and "P y z" and "\<not> Q y" by auto
  then have "y \<in> ?Q" by auto
  with \<open>P y z\<close> and min show False by auto
qed

lemmas wfp_on_imp_inductive_on =
  wfp_on_imp_minimal [THEN minimal_imp_inductive_on]

lemma inductive_on_induct [consumes 2, case_names less, induct pred: inductive_on]:
  assumes "inductive_on P A" and "x \<in> A"
    and "\<And>y. \<lbrakk> y \<in> A; \<And>x. \<lbrakk> x \<in> A; P x y \<rbrakk> \<Longrightarrow> Q x \<rbrakk> \<Longrightarrow> Q y"
  shows "Q x"
  using assms unfolding inductive_on_def by metis

lemma inductive_on_imp_wfp_on:
  assumes "inductive_on P A"
  shows "wfp_on P A"
proof -
  let ?Q = "\<lambda>x. \<not> (\<exists>f. f 0 = x \<and> (\<forall>i. f i \<in> A \<and> P (f (Suc i)) (f i)))"
  { fix x assume "x \<in> A"
    with assms have "?Q x"
    proof (induct rule: inductive_on_induct)
      fix y assume "y \<in> A" and IH: "\<And>x. x \<in> A \<Longrightarrow> P x y \<Longrightarrow> ?Q x"
      show "?Q y"
      proof (rule ccontr)
        assume "\<not> ?Q y"
        then obtain f where *: "f 0 = y"
          "\<forall>i. f i \<in> A \<and> P (f (Suc i)) (f i)" by auto
        then have "P (f (Suc 0)) (f 0)" and "f (Suc 0) \<in> A" by auto
        with IH and * have "?Q (f (Suc 0))" by auto
        with * show False by auto
      qed
    qed }
  then show ?thesis unfolding wfp_on_def by blast
qed

definition antisymp_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
  "antisymp_on P A \<longleftrightarrow> (\<forall>a\<in>A. \<forall>b\<in>A. P a b \<and> P b a \<longrightarrow> a = b)"

lemma antisymp_onI [Pure.intro]:
  "(\<And>a b. \<lbrakk>a \<in> A; b \<in> A; P a b; P b a\<rbrakk> \<Longrightarrow> a = b) \<Longrightarrow> antisymp_on P A"
  by (auto simp: antisymp_on_def)

lemma antisymp_on_reflclp [simp]:
  "antisymp_on P\<^sup>=\<^sup>= A = antisymp_on P A"
  by (auto simp: antisymp_on_def)

definition qo_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
  "qo_on P A \<longleftrightarrow> reflp_on P A \<and> transp_on P A"

definition irreflp_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
  "irreflp_on P A \<longleftrightarrow> (\<forall>a\<in>A. \<not> P a a)"

definition po_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
  "po_on P A \<longleftrightarrow> (irreflp_on P A \<and> transp_on P A)"

lemma po_onI [Pure.intro]:
  "\<lbrakk>irreflp_on P A; transp_on P A\<rbrakk> \<Longrightarrow> po_on P A"
  by (auto simp: po_on_def)

lemma irreflp_onI [Pure.intro]:
  "(\<And>a. a \<in> A \<Longrightarrow> \<not> P a a) \<Longrightarrow> irreflp_on P A"
  unfolding irreflp_on_def by blast

lemma irreflp_on_converse:
  "irreflp_on P A \<Longrightarrow> irreflp_on P\<inverse>\<inverse> A"
  unfolding irreflp_on_def by blast

lemma irreflp_on_converse_simp [simp]:
  "irreflp_on P\<inverse>\<inverse> A \<longleftrightarrow> irreflp_on P A"
  by (auto simp: irreflp_on_def)

lemma po_on_converse_simp [simp]:
  "po_on P\<inverse>\<inverse> A \<longleftrightarrow> po_on P A"
  by (simp add: po_on_def)

lemma po_on_imp_qo_on:
  "po_on P A \<Longrightarrow> qo_on (P\<^sup>=\<^sup>=) A"
  unfolding po_on_def qo_on_def
  by (metis reflp_on_reflclp transp_on_reflclp)

lemma po_on_imp_irreflp_on:
  "po_on P A \<Longrightarrow> irreflp_on P A"
  by (auto simp: po_on_def)

lemma po_on_imp_transp_on:
  "po_on P A \<Longrightarrow> transp_on P A"
  by (auto simp: po_on_def)

lemma irreflp_on_subset:
  assumes "A \<subseteq> B" and "irreflp_on P B"
  shows "irreflp_on P A"
  using assms by (auto simp: irreflp_on_def)

lemma po_on_subset:
  assumes "A \<subseteq> B" and "po_on P B"
  shows "po_on P A"
  using transp_on_subset and irreflp_on_subset and assms
  unfolding po_on_def by blast

lemma transp_on_irreflp_on_imp_antisymp_on:
  assumes "transp_on P A" and "irreflp_on P A"
  shows "antisymp_on (P\<^sup>=\<^sup>=) A"
proof
  fix a b assume "a \<in> A"
    and "b \<in> A" and "P\<^sup>=\<^sup>= a b" and "P\<^sup>=\<^sup>= b a"
  show "a = b"
  proof (rule ccontr)
    assume "a \<noteq> b"
    with \<open>P\<^sup>=\<^sup>= a b\<close> and \<open>P\<^sup>=\<^sup>= b a\<close> have "P a b" and "P b a" by auto
    with \<open>transp_on P A\<close> and \<open>a \<in> A\<close> and \<open>b \<in> A\<close> have "P a a" unfolding transp_on_def by blast
    with \<open>irreflp_on P A\<close> and \<open>a \<in> A\<close> show False unfolding irreflp_on_def by blast
  qed
qed

lemma po_on_imp_antisymp_on:
  assumes "po_on P A"
  shows "antisymp_on P A"
using transp_on_irreflp_on_imp_antisymp_on [of P A] and assms by (auto simp: po_on_def)

lemma strict_reflclp [simp]:
  assumes "x \<in> A" and "y \<in> A"
    and "transp_on P A" and "irreflp_on P A"
  shows "strict (P\<^sup>=\<^sup>=) x y = P x y"
  using assms unfolding transp_on_def irreflp_on_def
  by blast

lemma qo_on_imp_reflp_on:
  "qo_on P A \<Longrightarrow> reflp_on P A"
  by (auto simp: qo_on_def)

lemma qo_on_imp_transp_on:
  "qo_on P A \<Longrightarrow> transp_on P A"
  by (auto simp: qo_on_def)

lemma qo_on_subset:
  "A \<subseteq> B \<Longrightarrow> qo_on P B \<Longrightarrow> qo_on P A"
  unfolding qo_on_def
  using reflp_on_subset
    and transp_on_subset by blast

text \<open>
  Quasi-orders are instances of the @{class preorder} class.
\<close>
lemma qo_on_UNIV_conv:
  "qo_on P UNIV \<longleftrightarrow> class.preorder P (strict P)" (is "?lhs = ?rhs")
proof
  assume "?lhs" then show "?rhs"
    unfolding qo_on_def class.preorder_def
    using qo_on_imp_reflp_on [of P UNIV]
      and qo_on_imp_transp_on [of P UNIV]
    by (auto simp: reflp_on_def) (unfold transp_on_def, blast)
next
  assume "?rhs" then show "?lhs"
    unfolding class.preorder_def
    by (auto simp: qo_on_def reflp_on_def transp_on_def)
qed

lemma wfp_on_iff_inductive_on:
  "wfp_on P A \<longleftrightarrow> inductive_on P A"
  by (blast intro: inductive_on_imp_wfp_on wfp_on_imp_inductive_on)

lemma wfp_on_iff_minimal:
  "wfp_on P A \<longleftrightarrow> (\<forall>Q x.
     x \<in> Q \<and> Q \<subseteq> A \<longrightarrow>
     (\<exists>z\<in>Q. \<forall>y. P y z \<longrightarrow> y \<notin> Q))"
  using wfp_on_imp_minimal [of P A]
    and minimal_imp_inductive_on [of A P]
    and inductive_on_imp_wfp_on [of P A]
    by blast

text \<open>
  Every non-empty well-founded set @{term A} has a minimal element, i.e., an element that is not
  greater than any other element.
\<close>
lemma wfp_on_imp_has_min_elt:
  assumes "wfp_on P A" and "A \<noteq> {}"
  shows "\<exists>x\<in>A. \<forall>y\<in>A. \<not> P y x"
  using assms unfolding wfp_on_iff_minimal by force

lemma wfp_on_induct [consumes 2, case_names less, induct pred: wfp_on]:
  assumes "wfp_on P A" and "x \<in> A"
    and "\<And>y. \<lbrakk> y \<in> A; \<And>x. \<lbrakk> x \<in> A; P x y \<rbrakk> \<Longrightarrow> Q x \<rbrakk> \<Longrightarrow> Q y"
  shows "Q x"
  using assms and inductive_on_induct [of P A x]
  unfolding wfp_on_iff_inductive_on by blast

lemma wfp_on_UNIV [simp]:
  "wfp_on P UNIV \<longleftrightarrow> wfP P"
  unfolding wfp_on_iff_inductive_on inductive_on_def wfP_def wf_def by force

subsection \<open>Measures on Sets (Instead of Full Types)\<close>

definition
  inv_image_betw ::
    "('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"
where
  "inv_image_betw P f A B = (\<lambda>x y. x \<in> A \<and> y \<in> A \<and> f x \<in> B \<and> f y \<in> B \<and> P (f x) (f y))"

definition
  measure_on :: "('a \<Rightarrow> nat) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
where
  "measure_on f A = inv_image_betw (<) f A UNIV"

lemma in_inv_image_betw [simp]:
  "inv_image_betw P f A B x y \<longleftrightarrow> x \<in> A \<and> y \<in> A \<and> f x \<in> B \<and> f y \<in> B \<and> P (f x) (f y)"
  by (auto simp: inv_image_betw_def)

lemma in_measure_on [simp, code_unfold]:
  "measure_on f A x y \<longleftrightarrow> x \<in> A \<and> y \<in> A \<and> f x < f y"
  by (simp add: measure_on_def)

lemma wfp_on_inv_image_betw [simp, intro!]:
  assumes "wfp_on P B"
  shows "wfp_on (inv_image_betw P f A B) A" (is "wfp_on ?P A")
proof (rule ccontr)
  assume "\<not> ?thesis"
  then obtain g where "\<forall>i. g i \<in> A \<and> ?P (g (Suc i)) (g i)" by (auto simp: wfp_on_def)
  with assms show False by (auto simp: wfp_on_def)
qed

lemma wfp_less:
  "wfp_on (<) (UNIV :: nat set)"
  using wf_less by (auto simp: wfP_def)

lemma wfp_on_measure_on [iff]:
  "wfp_on (measure_on f A) A"
  unfolding measure_on_def
  by (rule wfp_less [THEN wfp_on_inv_image_betw])

lemma wfp_on_mono:
  "A \<subseteq> B \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> P x y \<Longrightarrow> Q x y) \<Longrightarrow> wfp_on Q B \<Longrightarrow> wfp_on P A"
  unfolding wfp_on_def by (metis subsetD)

lemma wfp_on_subset:
  "A \<subseteq> B \<Longrightarrow> wfp_on P B \<Longrightarrow> wfp_on P A"
  using wfp_on_mono by blast

lemma restrict_to_iff [iff]:
  "restrict_to P A x y \<longleftrightarrow> x \<in> A \<and> y \<in> A \<and> P x y"
  by (simp add: restrict_to_def)

lemma wfp_on_restrict_to [simp]:
  "wfp_on (restrict_to P A) A = wfp_on P A"
  by (auto simp: wfp_on_def)

lemma irreflp_on_strict [simp, intro]:
  "irreflp_on (strict P) A"
  by (auto simp: irreflp_on_def)

lemma transp_on_map':
  assumes "transp_on Q B"
    and "g ` A \<subseteq> B"
    and "h ` A \<subseteq> B"
    and "\<And>x. x \<in> A \<Longrightarrow> Q\<^sup>=\<^sup>= (h x) (g x)"
  shows "transp_on (\<lambda>x y. Q (g x) (h y)) A"
  using assms unfolding transp_on_def
  by auto (metis imageI subsetD)

lemma transp_on_map:
  assumes "transp_on Q B"
    and "h ` A \<subseteq> B"
  shows "transp_on (\<lambda>x y. Q (h x) (h y)) A"
  using transp_on_map' [of Q B h A h, simplified, OF assms] by blast

lemma irreflp_on_map:
  assumes "irreflp_on Q B"
    and "h ` A \<subseteq> B"
  shows "irreflp_on (\<lambda>x y. Q (h x) (h y)) A"
  using assms unfolding irreflp_on_def by auto

lemma po_on_map:
  assumes "po_on Q B"
    and "h ` A \<subseteq> B"
  shows "po_on (\<lambda>x y. Q (h x) (h y)) A"
  using assms and transp_on_map and irreflp_on_map
  unfolding po_on_def by auto

lemma chain_transp_on_less:
  assumes "\<forall>i. f i \<in> A \<and> P (f i) (f (Suc i))" and "transp_on P A" and "i < j"
  shows "P (f i) (f j)"
using \<open>i < j\<close>
proof (induct j)
  case 0 then show ?case by simp
next
  case (Suc j)
  show ?case
  proof (cases "i = j")
    case True
    with Suc show ?thesis using assms(1) by simp
  next
    case False
    with Suc have "P (f i) (f j)" by force
    moreover from assms have "P (f j) (f (Suc j))" by auto
    ultimately show ?thesis using assms(1, 2) unfolding transp_on_def by blast
  qed
qed

lemma wfp_on_imp_irreflp_on:
  assumes "wfp_on P A"
  shows "irreflp_on P A"
proof
  fix x
  assume "x \<in> A"
  show "\<not> P x x"
  proof
    let ?f = "\<lambda>_. x"
    assume "P x x"
    then have "\<forall>i. P (?f (Suc i)) (?f i)" by blast
    with \<open>x \<in> A\<close> have "\<not> wfp_on P A" by (auto simp: wfp_on_def)
    with assms show False by contradiction
  qed
qed

inductive
  accessible_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool"
  for P and A
where
  accessible_onI [Pure.intro]:
    "\<lbrakk>x \<in> A; \<And>y. \<lbrakk>y \<in> A; P y x\<rbrakk> \<Longrightarrow> accessible_on P A y\<rbrakk> \<Longrightarrow> accessible_on P A x"

lemma accessible_on_imp_mem:
  assumes "accessible_on P A a"
  shows "a \<in> A"
  using assms by (induct) auto

lemma accessible_on_induct [consumes 1, induct pred: accessible_on]:
  assumes *: "accessible_on P A a"
    and IH: "\<And>x. \<lbrakk>accessible_on P A x; \<And>y. \<lbrakk>y \<in> A; P y x\<rbrakk> \<Longrightarrow> Q y\<rbrakk> \<Longrightarrow> Q x"
  shows "Q a"
  by (rule * [THEN accessible_on.induct]) (auto intro: IH accessible_onI)

lemma accessible_on_downward:
  "accessible_on P A b \<Longrightarrow> a \<in> A \<Longrightarrow> P a b \<Longrightarrow> accessible_on P A a"
  by (cases rule: accessible_on.cases) fast

lemma accessible_on_restrict_to_downwards:
  assumes "(restrict_to P A)\<^sup>+\<^sup>+ a b" and "accessible_on P A b"
  shows "accessible_on P A a"
  using assms by (induct) (auto dest: accessible_on_imp_mem accessible_on_downward)

lemma accessible_on_imp_inductive_on:
  assumes "\<forall>x\<in>A. accessible_on P A x"
  shows "inductive_on P A"
proof
  fix Q x
  assume "x \<in> A"
    and *: "\<And>y. \<lbrakk>y \<in> A; \<And>x. \<lbrakk>x \<in> A; P x y\<rbrakk> \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> Q y"
  with assms have "accessible_on P A x" by auto
  then show "Q x"
  proof (induct)
    case (1 z)
    then have "z \<in> A" by (blast dest: accessible_on_imp_mem)
    show ?case by (rule *) fact+
  qed
qed

lemmas accessible_on_imp_wfp_on = accessible_on_imp_inductive_on [THEN inductive_on_imp_wfp_on]

lemma wfp_on_tranclp_imp_wfp_on:
  assumes "wfp_on (P\<^sup>+\<^sup>+) A"
  shows "wfp_on P A"
  by (rule ccontr) (insert assms, auto simp: wfp_on_def)

lemma inductive_on_imp_accessible_on:
  assumes "inductive_on P A"
  shows "\<forall>x\<in>A. accessible_on P A x"
proof
  fix x
  assume "x \<in> A"
  with assms show "accessible_on P A x"
    by (induct) (auto intro: accessible_onI)
qed

lemma inductive_on_accessible_on_conv:
  "inductive_on P A \<longleftrightarrow> (\<forall>x\<in>A. accessible_on P A x)"
  using inductive_on_imp_accessible_on
    and accessible_on_imp_inductive_on
    by blast

lemmas wfp_on_imp_accessible_on =
  wfp_on_imp_inductive_on [THEN inductive_on_imp_accessible_on]

lemma wfp_on_accessible_on_iff:
  "wfp_on P A \<longleftrightarrow> (\<forall>x\<in>A. accessible_on P A x)"
  by (blast dest: wfp_on_imp_accessible_on accessible_on_imp_wfp_on)

lemma accessible_on_tranclp:
  assumes "accessible_on P A x"
  shows "accessible_on ((restrict_to P A)\<^sup>+\<^sup>+) A x"
    (is "accessible_on ?P A x")
  using assms
proof (induct)
  case (1 x)
  then have "x \<in> A" by (blast dest: accessible_on_imp_mem)
  then show ?case
  proof (rule accessible_onI)
    fix y
    assume "y \<in> A"
    assume "?P y x"
    then show "accessible_on ?P A y"
    proof (cases)
      assume "restrict_to P A y x"
      with 1 and \<open>y \<in> A\<close> show ?thesis by blast
    next
      fix z
      assume "?P y z" and "restrict_to P A z x"
      with 1 have "accessible_on ?P A z" by (auto simp: restrict_to_def)
      from accessible_on_downward [OF this \<open>y \<in> A\<close> \<open>?P y z\<close>]
        show ?thesis .
    qed
  qed
qed

lemma wfp_on_restrict_to_tranclp:
  assumes "wfp_on P A"
  shows "wfp_on ((restrict_to P A)\<^sup>+\<^sup>+) A"
  using wfp_on_imp_accessible_on [OF assms]
    and accessible_on_tranclp [of P A]
    and accessible_on_imp_wfp_on [of A "(restrict_to P A)\<^sup>+\<^sup>+"]
    by blast

lemma wfp_on_restrict_to_tranclp':
  assumes "wfp_on (restrict_to P A)\<^sup>+\<^sup>+ A"
  shows "wfp_on P A"
  by (rule ccontr) (insert assms, auto simp: wfp_on_def)

lemma wfp_on_restrict_to_tranclp_wfp_on_conv:
  "wfp_on (restrict_to P A)\<^sup>+\<^sup>+ A \<longleftrightarrow> wfp_on P A"
  using wfp_on_restrict_to_tranclp [of P A]
    and wfp_on_restrict_to_tranclp' [of P A]
    by blast

lemma tranclp_idemp [simp]:
  "(P\<^sup>+\<^sup>+)\<^sup>+\<^sup>+ = P\<^sup>+\<^sup>+" (is "?l = ?r")
proof (intro ext)
  fix x y
  show "?l x y = ?r x y"
  proof
    assume "?l x y" then show "?r x y" by (induct) auto
  next
    assume "?r x y" then show "?l x y" by (induct) auto
  qed
qed

(*TODO: move the following 3 lemmas to Transitive_Closure?*)
lemma stepfun_imp_tranclp:
  assumes "f 0 = x" and "f (Suc n) = z"
    and "\<forall>i\<le>n. P (f i) (f (Suc i))"
  shows "P\<^sup>+\<^sup>+ x z"
  using assms
  by (induct n arbitrary: x z)
     (auto intro: tranclp.trancl_into_trancl)

lemma tranclp_imp_stepfun:
  assumes "P\<^sup>+\<^sup>+ x z"
  shows "\<exists>f n. f 0 = x \<and> f (Suc n) = z \<and> (\<forall>i\<le>n. P (f i) (f (Suc i)))"
    (is "\<exists>f n. ?P x z f n")
  using assms
proof (induct rule: tranclp_induct)
  case (base y)
  let ?f = "(\<lambda>_. y)(0 := x)"
  have "?f 0 = x" and "?f (Suc 0) = y" by auto
  moreover have "\<forall>i\<le>0. P (?f i) (?f (Suc i))"
    using base by auto
  ultimately show ?case by blast
next
  case (step y z)
  then obtain f n where IH: "?P x y f n" by blast
  then have *: "\<forall>i\<le>n. P (f i) (f (Suc i))"
    and [simp]: "f 0 = x" "f (Suc n) = y"
    by auto
  let ?n = "Suc n"
  let ?f = "f(Suc ?n := z)"
  have "?f 0 = x" and "?f (Suc ?n) = z" by auto
  moreover have "\<forall>i\<le>?n. P (?f i) (?f (Suc i))"
    using \<open>P y z\<close> and * by auto
  ultimately show ?case by blast
qed

lemma tranclp_stepfun_conv:
  "P\<^sup>+\<^sup>+ x y \<longleftrightarrow> (\<exists>f n. f 0 = x \<and> f (Suc n) = y \<and> (\<forall>i\<le>n. P (f i) (f (Suc i))))"
  using tranclp_imp_stepfun and stepfun_imp_tranclp by metis

subsection \<open>Facts About Predecessor Sets\<close>

lemma qo_on_predecessor_subset_conv':
  assumes "qo_on P A" and "B \<subseteq> A" and "C \<subseteq> A"
  shows "{x\<in>A. \<exists>y\<in>B. P x y} \<subseteq> {x\<in>A. \<exists>y\<in>C. P x y} \<longleftrightarrow> (\<forall>x\<in>B. \<exists>y\<in>C. P x y)"
  using assms
  by (auto simp: subset_eq qo_on_def reflp_on_def, unfold transp_on_def) metis+

lemma qo_on_predecessor_subset_conv:
  "\<lbrakk>qo_on P A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> {z\<in>A. P z x} \<subseteq> {z\<in>A. P z y} \<longleftrightarrow> P x y"
  using qo_on_predecessor_subset_conv' [of P A "{x}" "{y}"] by simp

lemma po_on_predecessors_eq_conv:
  assumes "po_on P A" and "x \<in> A" and "y \<in> A"
  shows "{z\<in>A. P\<^sup>=\<^sup>= z x} = {z\<in>A. P\<^sup>=\<^sup>= z y} \<longleftrightarrow> x = y"
  using assms(2-)
    and reflp_on_reflclp [of P A]
    and po_on_imp_antisymp_on [OF \<open>po_on P A\<close>]
    unfolding antisymp_on_def reflp_on_def
    by blast

lemma restrict_to_rtranclp:
  assumes "transp_on P A"
    and "x \<in> A" and "y \<in> A"
  shows "(restrict_to P A)\<^sup>*\<^sup>* x y \<longleftrightarrow> P\<^sup>=\<^sup>= x y"
proof -
  { assume "(restrict_to P A)\<^sup>*\<^sup>* x y"
    then have "P\<^sup>=\<^sup>= x y" using assms
      by (induct) (auto, unfold transp_on_def, blast) }
  with assms show ?thesis by auto
qed

lemma reflp_on_restrict_to_rtranclp:
  assumes "reflp_on P A" and "transp_on P A"
    and "x \<in> A" and "y \<in> A"
  shows "(restrict_to P A)\<^sup>*\<^sup>* x y \<longleftrightarrow> P x y"
  unfolding restrict_to_rtranclp [OF assms(2-)]
  unfolding reflp_on_reflclp_simp [OF assms(1, 3-)] ..

end

subset_name: curated


TITLE: $a, b, c \in \mathbb{N}$ such that prime $a + b + 1 > c + 1$. If $k_n = (n + 1)$, then $k_1\dots k_c | (k_{b + 1} - k_a) \dots (k_{b+c} - k_a)$
QUESTION [1 upvotes]: I have natural numbers $a, b, c$ such that $a + b + 1$ is a prime greater than $c + 1$. I need to prove that if $k_n = n(n + 1)$, $(k_{b + 1} - k_a)(k_{b+2} - k_a)\dots(k_{b + c} - k_a)$ is divisible by $k_1k_2\dots k_c$. I have no idea where to begin on this, and have just managed to simplify the divisor to $c!(c+1)!$
Could I please get some help? A hint would be preferred.

REPLY [0 votes]: Hint: $k_{b+i}-k_a = (b+a+i+1)(b-a+i)$


TITLE: Lean4 Exercise: Double negation implies law of excluded middle
QUESTION [4 upvotes]: Been trying to do this exercise from Section 3 of the tutorial for hours and I cannot get it to check. Here's my best attempt below (theorem dne provided by the book):
variable (p : Prop)

open Classical

theorem dne (h : ¬¬p) : p :=
  Or.elim (em p)
  (fun (hp : p) => hp)
  (fun (hnp: ¬p) => absurd hnp h)

theorem step (h : ¬(p ∨ ¬ p)) : ¬p :=
  fun (hp : p) => h (Or.intro_left (¬p) (hp))

theorem exclmid : p ∨ ¬p :=
  dne (
    fun (h : ¬(p ∨ ¬p)) =>
    h (Or.intro_right (p) (step h))
  )

When I type-check my 'step' lemma, I get that it says "∀ (p : Prop), ¬(p ∨ ¬p) → ¬p". I thought that I can give 'step' something of type ¬(p ∨ ¬p) and it will return something of type ¬p, but when I check it on specific examples it doesn't do that.
I've tried a lot of other attempts but I don't get helpful feedback from the editor, so I'm not sure where it's going wrong (like below).
theorem excmid : p ∨ ¬p :=
  dne (
    fun (h : ¬ (p ∨ ¬p)) : False =>
    fun (h2 : p ∨ ¬p) : False =>
    have np : ¬p := fun (hp : p) => h2 (Or.intro_left (¬p) (hp))
    h h2 (Or.intro_right p np)
  )

Any help would be appreciated.

REPLY [3 votes]: TLDR: Supply the argument p ∨ ¬ p to both dne and p to step, or use implicit arguments.

You are almost there!
The variable command
The variable (p : Prop) command can be a bit confusing.  At first it looks like it is saying "for this whole section, just fix p to be a Prop", but the problem is what do you do with definitions and theorems which use this p?  How do you use them inside this section (when variable (p : Prop) is in scope) and how do you use them outside this section (when variable (p : Prop) is no longer in scope!)?  Lean simplifies this (compared to say Coq modules) and instead variable (p : Prop) actually just means "for this whole section, any theorem or definition which uses p gets (p : Prop) automatically added to its assumptions in the signature".  When you use the theorem you have to supply a value for this p argument.
To make it more clear, here are four solutions (with an interlude on solving term proofs in Lean):
Solution 1
Instead of variable (p : Prop) we can just write (p : Prop) explicitly:
open Classical

theorem dne (p : Prop) (h : ¬¬p) : p :=
  Or.elim (em p)
  (fun (hp : p) => hp)
  (fun (hnp: ¬p) => absurd hnp h)

theorem step (p : Prop) (h : ¬(p ∨ ¬ p)) : ¬p :=
  fun (hp : p) => h (Or.intro_left (¬p) (hp))

theorem exclmid (p : Prop) : p ∨ ¬p :=
  dne (p ∨ ¬p) (
    fun (h : ¬(p ∨ ¬p)) =>
    h (Or.intro_right (p) (step p h))
  )

Here we supply the proposition p ∨ ¬p to dne and p to step as the first argument.
Solution 2
In your MWE, we have variable (p : Prop).  Nonetheless, we still have to explicitly supply that argument to both dne and step:
variable (p : Prop)

open Classical

theorem dne (h : ¬¬p) : p :=
  Or.elim (em p)
  (fun (hp : p) => hp)
  (fun (hnp: ¬p) => absurd hnp h)

theorem step (h : ¬(p ∨ ¬ p)) : ¬p :=
  fun (hp : p) => h (Or.intro_left (¬p) (hp))

theorem exclmid : p ∨ ¬p :=
  dne (p ∨ ¬p) (
    fun (h : ¬(p ∨ ¬p)) =>
    h (Or.intro_right (p) (step p h))
  )

Lean errors
Note, if you don't supply the p argument to step, then Lean does give fairly helpful errors
(but of course error messages can always be improved!).
application type mismatch
  step h
argument
  h
has type
  ¬(p ∨ ¬p) : Prop
but is expected to have type
  Prop : Type

This is saying that your first argument to step is wrong.  You should be putting a Prop in the first argument slot, not a proof of ¬(p ∨ ¬p).  When you print step, you get:
theorem step : ∀ (p : Prop), ¬(p ∨ ¬p) → ¬p :=
fun p h hp => h (Or.intro_left (¬p) hp)

You see the first argument comes from ∀ (p : Prop).
Using holes (_) to solve term proofs
Here is some advice to solving term proofs in Lean.  The most helpful tool in making term proofs is holes, i.e. the underscore character.  (Note, tactic proofs, which you will cover later are even easier!) You correctly noticed that your proof needs to start with dne.  So we start with the template:
theorem exclmid : p ∨ ¬p :=
  dne _ _

Why two underscores?  Zero, one, and three underscores give an error at dne, while two underscores only puts the error at the underscore, so we know that is the correct number of arguments to dne.  Next, we hover over the two underscores.  The first, says:
p: Prop
⊢ Prop

The second says:
p: Prop
⊢ ¬¬(p ∨ ¬p)

So the first must be a Prop and the second a proof of ¬¬(p ∨ ¬p).  But these are not independent.  The Prop in the first actually is linked to the proof in the second.  So the only possible value for the first is p ∨ ¬p.  Lean therefore automatically puts the p ∨ ¬p in for you when you do the first _.
A good way to solve a term proof is just to use this trick over and over again until you solved the theorem.  So next you can start to fill the proof of ¬¬(p ∨ ¬p) in by replacing the second underscore with (fun h => _).  Again, Lean will tell you both the type of h and the expected type of the new hole.
Solution 3: Implicit arguments
Notice that Lean is smart enough to know that the first argument to dne is p ∨ ¬p and to step is p.  So one could have just written, say, step _ h in the examples above.  Better however, would be to mark (p : Prop) as implicit in the theorems themselves.  This can be done with either variable {p : Prop} or theorem step {p : Prop} (h : ¬(p ∨ ¬ p)) : ¬p.  Now we don't have to supply that annoying first argument and the proof you wrote goes through as is!
variable {p : Prop}

open Classical

theorem dne (h : ¬¬p) : p :=
  Or.elim (em p)
  (fun (hp : p) => hp)
  (fun (hnp: ¬p) => absurd hnp h)

theorem step (h : ¬(p ∨ ¬ p)) : ¬p :=
  fun (hp : p) => h (Or.intro_left (¬p) (hp))

theorem exclmid : p ∨ ¬p :=
  dne (
    fun (h : ¬(p ∨ ¬p)) =>
    h (Or.intro_right (p) (step h))
  )

Solution 4: Lean 4 magic
Finally, Lean 4 offers a bit of magic.  If a variable like p in a definition or theorem, is just one symbol and its type (Prop in this case) can be inferred from the rest of the theorem, then it is automatically added as an implicit argument to the theorem signature. In this case {p : Prop} is added automatically to the theorem signature.  That means all we have to do is take your MWE and remove the variable line!
open Classical

theorem dne (h : ¬¬p) : p :=
  Or.elim (em p)
  (fun (hp : p) => hp)
  (fun (hnp: ¬p) => absurd hnp h)

theorem step (h : ¬(p ∨ ¬ p)) : ¬p :=
  fun (hp : p) => h (Or.intro_left (¬p) (hp))

theorem exclmid : p ∨ ¬p :=
  dne (
    fun (h : ¬(p ∨ ¬p)) =>
    h (Or.intro_right (p) (step h))
  )

Magic!


TITLE: About generalized Minkowski inequality
QUESTION [5 upvotes]: For which functions $f:\mathbb{R}^+ \to \mathbb{R}^+$ does the inequality
$f^{-1}\left(\sum\limits_{k=1}^n f(x_k+y_k)\right) \leq f^{-1}\left(\sum\limits_{k=1}^n f(x_k)\right) + f^{-1}\left(\sum\limits_{k=1}^n f(y_k)\right)$
hold for any nonnegative real numbers $x_1, \dots, x_n, y_1, \dots, y_n$?
Note that for $f(x)=x^p$, $p \geq 1$, this is the classical Minkowski inequality.
We can assume that $f$ is strictly inreasing to guarantee that $f^{-1}$ exists. Any other natural conditions on $f$ are acceptable. For example: does the above inequality hold for any stricly increasing convex function with $f(0)=0$?

REPLY [5 votes]: The question that you are asking was asked in "On Generalizations of Minkowski's Inequality in the Form of a Triangle Inequality" by F. Mulholland (1949). In that paper, Mulholland established a sufficient condition on $f$, namely that it should satisfy $f(0)=0$, be increasing on $x \ge 0$ and be g-convex, i.e., $\log f(e^x)$ is convex on the reals.
However, Mulholland's condition is not necessary, which seems to have been very recently shown in On functions that solve Mulholland inequality
and on compositions of such functions by M. Petrík (2013)---but given the elementary nature of the question, perhaps the non-necessity of the above g-convexity hypothesis of Mulholland has also previously been observed.


TITLE: If $\chi(g)$ generates a dense subgroup of $\chi(G)$ for all $\chi$ then $g$ generates a dense subgroup of $G$.
QUESTION [1 upvotes]: This question arised from something in Ergodic theory, however this is not necessary to state or answer the question.
Suppose that $G$ is a compact abelian group and $g\in G$.
Are the following two equivalent:

For every continuous character $\chi:G\rightarrow S^1$, $\chi(g)$ generates a dense subgroup of $\chi(G)$.
$g$ generates a dense subgroup of $G$.

Clearly $2$ implies $1$, but I can't figure out whether the opposite holds.
For those who are interested in the connection with ergodic theory. Property $2$ means that $(G,R_g)$ is an ergodic system, and I ask whether this is equivalent to property 1 which means that all the factors $(\chi(G),R_{\chi(g)})$ are ergodic.

REPLY [1 votes]: Short proof: if 2 fails, the group $G/\overline{\langle g\rangle}$ is a nontrivial compact abelian group and hence has a nontrivial continuous character $\chi$. Then $\chi(g)=1$ generates the trivial subgroup, which is not dense in $\chi(G)$, so 1 fails.


TITLE: Finding coefficient of $x^8$
QUESTION [4 upvotes]: There is a question I am having difficult time with. Please help me to find the coefficient of $x^8$ in the polynomial $$(x-1)(x-2)(x-3)........(x-10)$$ I don't even know to start but I think it's related to binomial theorem but again there are no powers here. Any help is appreciated. Thank you.

REPLY [3 votes]: First, we see how we get the powers of $x^8$ thru the traditional method of "expanding out".
To get powers of $x^8$, we will actually multiply 8 $x$'s together with two numbers, e.g.
$x\dots x\cdot (-2)(-3)=6x^8$
So this boils down to finding all the sums of products of two distinct numbers, i.e. $1\times 2+1\times3+\dots+9\times 10$.
First we find out what is $1(2)+1(3)+1(4)+\dots+1(10)$. Surely, it is 54. One other way to write it is $(1+2+\dots+10)-1=54$
Next, we find the product of two distinct numbers, containing 2, i.e.:
$2(2)+2(3)+2(4)+\dots+2(10)$. This is $2(1+3+\dots+10)=2(1+2+\dots+10)-2^2$.
The shortcut to this is to observe that the sum is actually:
$(1+2+\dots+10)(1+2+\dots+10)-(1^2+2^2+\dots+10^2)=55(55)-385=2640$
Note that we have double counted: for instance $1\times 2$ and $2\times 1$ are counted twice.
So dividing by 2 gives 1320 as desired.


TITLE: How to find the optimal lines?
QUESTION [1 upvotes]: Does anyone know anyway or any algorithm that can exactly and/or
numerically find lines $\left\{ l_{i}\right\} _{i=1}^{n_{k}+2}$ that maximizes $$\min_{1\le i<j\le n_{k}+2}\text{angle}\left(l_{i},l_{j}\right)$$ in $\mathbb{R}^{n_{k}}$ for some sequence of integers $1<n_{1}<n_{2}\cdots<n_{k}<\cdots?$ Thanks a lot.

REPLY [1 votes]: Bukh and Cox provide exact constructions for the infinite sequence $n_k\equiv 1\bmod 3$. Sloane maintains numerical solutions for $n_k\leq 16$. Computer-assisted proofs of optimality have been obtained for $n_k\leq 6$; see this paper and references therein.
Edit: The Bukh–Cox construction is contained in the proofs of their Lemma 16 and Theorem 3. In what follows, I isolate the construction for convenience. (Throughout, I use their notation whenever possible, so your $n_k$ is replaced by $d$, for example.) Put $k=2$ and $N=\binom{k+1}{2}=3$, and let $A$ denote any $k\times N$ equiangular tight frame. See this survey for general information on these objects, but in this case, we may take
$$ A = \left[\begin{array}{rrr}1&-\frac{1}{2}&-\frac{1}{2}\\0&\frac{\sqrt{3}}{2}&-\frac{\sqrt{3}}{2}\end{array}\right].$$
If we denote the columns of $A$ by $x_1,x_2,x_3$, then notice that each $x_i$ has unit norm and $|\langle x_i,x_j\rangle|=\frac{1}{2}=:\beta$ for every $1\leq i<j\leq 3$. Take
$$ C:=\frac{1}{\beta}(A^\top A-I)+I. $$
Then the diagonal entries of $C$ are $1$ and the off-diagonal entries of $C$ are $\pm1$. One may further show that $\lambda:=\lambda_\mathrm{max}(C)=\frac{1}{\beta}(\frac{N}{k}-1)+1$. Since $d\equiv -k\bmod N$ by assumption, we have $b:=\frac{d+k}{N}\in\mathbb{N}$. Put $\epsilon=\frac{1}{b\lambda-1}$ and consider the matrix $G:=(1+\epsilon)I-\epsilon(C\otimes J)$, where $I$ is the identity matrix of size $Nb=d+k$ and $J$ is the all-ones matrix of size $b$. One may show that $G$ is positive semidefinite with rank at most $d$, and so $G=XX^\top$ for some $X\in\mathbb{R}^{d\times (d+k)}$. The columns of $X$ are unit vectors that achieve equality in the Bukh–Cox bound (i.e., Theorem 2(a)). It follows that the lines they span maximize the minimum interior angle.


text:
\begin{document}

\title{Wireless Power Transfer Under Kullback-Leibler Distribution Uncertainty: A Mathematical Framework}

\author{Ioannis Krikidis,~\IEEEmembership{Fellow,~IEEE}
\thanks{This work has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (Grant agreement No. 819819).}
\thanks{I. Krikidis is with the Department of Electrical and Computer Engineering, Faculty of Engineering, University of Cyprus, Nicosia 1678 (E-mail: {\sf krikidis@ucy.ac.cy}).}}

\maketitle
\vspace{-0.8cm}
\begin{abstract}
In this letter, we study the performance of a wireless power transfer system under  energy harvesting distribution uncertainty. The uncertainty captures practical nonidealities of the rectification process and is modelled as the maximum Kullback-Leibler distance of the actual distribution from a nominal distribution. The case where symmetrized divergence is considered for the statistical distance between distributions is also considered. By formulating a convex optimization problem, we investigate a mathematical framework that provides closed form expressions for the minimum average harvested energy (the worst performance) and the associated statistical distribution. Theoretical results show that the energy harvesting performance is significantly degraded as the level of the uncertainty increases.
\end{abstract}
\vspace{-0.6cm}
\begin{keywords}
Wireless power transfer, uncertainty, Kullback-Leibler divergence, average energy harvested.
\end{keywords}

\vspace{-0.1cm}
\section{Introduction}

\IEEEPARstart{W}{ireless} power transfer (WPT) is a new technology which allows low-power devices to harvest energy from dedicated/ambient radio-frequency signals. From the seminal work in \cite{RUI2}, where the authors introduced the principles of WPT and the basic network architectures, WPT has attracted a lot of attention from both academia and industry. Recent studies take into account the nonlinearity of the rectification circuit and study WPT from information theory, signal-processing and/or networking perspective \cite{CLE}.

One of the most fundamental questions in WPT is the modelling of the energy harvesting (EH) process. To address this question, several deterministic models have been proposed in the literature by trading off simplicity and accuracy. From the initial linear model which has been used in \cite{RUI2}, the piece-wise linear model captures (in a simple way) the three operation regions of the rectification circuit \cite{LOP}. On the other hand, more sophisticated parametric nonlinear functions (e.g., sigmoidal \cite{BOS}, fractional \cite{CHE}, etc.) have been proposed, where the parameters are tuned by using real data and curve fitting tools. Although these harvesting models try to approximate the behaviour of the circuit from a communication theory perspective, they neglect important practical phenomena e.g., antenna mismatching, parasitic effects, RC filter etc \cite{PAN}. Therefore, these deterministic models are associated with specific operation points of the rectification circuit and are not able to capture its general behaviour.  To make these models more accurate and enhance their practical interest, they should be extended by capturing uncertainty; for systems with low computation/processing capabilities (e.g.,  WPT), this uncertainty can be modelled by a partial knowledge of the EH statistical distribution (including wireless channel and EH process) \cite{LAP}.

A fundamental model for communication under channel distribution uncertainty is the compound channel \cite[Sec. III]{LAP}, where the transmitter knows that the (unknown) channel distribution is within a given Kullback-Leibler (KL) divergence (uncertainty) from a nominal distribution. In this case, the Shannon capacity is associated to a class of fading distributions  rather than a specific distribution. The work in \cite{CHA} studies the compound outage probability of a communication system under KL fading distribution uncertainty and identifies two fundamental operation regimes. The same mathematical framework is used in \cite{CHA2} to study the ergodic compound capacity of a multiple-input multiple-output system with incomplete channel state information and in \cite{CHA3} to design the optimal control of a stochastic system. The work in \cite{BIG}  extends this framework for more general objective functions and investigates the robustness of modulation and coding schemes in body-area networks.

The objective of our work is to propose a mathematical framework that integrates an EH distribution uncertainty in WPT systems. Inspired by the fundamental concept of compound channel \cite{CHA,BIG}, we study the minimum average harvested energy for a basic point-to-point link when the actual EH distribution is within a certain KL uncertainty from a nominal distribution. By formulating a convex optimization problem with respect to the actual distribution, we admit a general closed-form  solution via the evaluation of the Karush-Kuhn-Tucker (KKT) optimality conditions. We study the regular KL divergence metric and its asymmetric counterpart  ($\mathcal{D}_{\text{KL}}(f_0||f)$ and $\mathcal{D}_{\text{KL}}(f||f_0)$) as well as the symmetrized divergence. We demonstrate that the EH performance (average harvested energy) significantly decreases as the uncertainty distance increases. Simplified closed-form expressions are derived for the linear EH model with Rayleigh fading, where the nominal distribution is exponential. The case where the class/type of the actual EH distribution is known at the transmitter is also discussed and simple expressions are proposed. The proposed mathematical framework is general and can be used as a basis to systematically study WPT applications.

\vspace{-0.29cm}
\section{Average harvested energy under uncertainty}\label{sec2}

We study a fundamental point-to-point link consisting of one transmitter that transmits energy signals to a single receiver.  Due to the wireless channel and the practical nonidealities of the rectenna circuit \cite{PAN}, the energy harvested becomes a random variable with a nominal distribution $f_0(x)\geq 0$ and an unknown true distribution $f(x)\geq 0$. According to the principles of compound channel \cite{LAP}, we assume that this nominal distribution is within a KL divergence $\mathcal{D}_{\text{KL}}(f_0||f)\leq d$ from the actual distribution, where $\mathcal{D}_{\text{KL}}(f||g)=\int f(x)\log \frac{f(x)}{g(x)}dx$ denotes the KL distance between the distributions $f(x)$ and $g(x)$, and $d$ is the maximum KL divergence; both $f_0(x)$ and $d$ are known at the transmitter through an appropriate training/estimation process and feedback channel\footnote{The nominal distribution $f_0(x)$ refers to the selected model, while the parameter $d$ represents prior knowledge of the approximate behaviour of the distribution and highly depends on the size/quality of the available data, the estimation mechanism \cite{MCK} (e.g., dynamics perturbations, hypothesis test, etc.) as well as the technical capabilities of  the communication and WPT infrastructure (i.e., computational resources, feedback channel, rectenna circuit, etc.) \cite{CHA,CHA2}.}. It is worth noting that the parameters $f_0(x)$ and $d$ determine the EH uncertainty; they are considered constant for the whole communication and independent on the transmit parameters. If the performance of the WPT system is characterized by the average harvested energy, the worst case scenario is captured by the following optimization problem
\vspace{-0.1cm}
\begin{align}
&(P1)\;\;\min_f \int x f(x)dx \\
&\;\;\;\;\;\;\;\;\;\;\text{s. t.}\; \mathcal{D}_{\text{KL}}(f_0||f)\leq d,\;\;\;\int f(x)dx=1. \label{co1}
\end{align}
The solution of the optimization problem (P1) gives the minimum energy that can be harvested, when there is KL uncertainty for the EH distribution. This is an important information for the design of a WPT system with critical quality of service constraints (e.g., design a robust transmission strategy that ensures a minimum average harvested energy for all possible cases; for the whole set of uncertainty). If $\mathcal{E}=\int x f(x)dx$ denotes the solution to (P1), the following theorem gives the associated actual distribution.
\vspace{-0.2cm}
\begin{theorem}\label{th1}
The actual distribution that achieves the minimum average harvested energy is $f(x)=\frac{1}{q(\mu^*)}\frac{f_0(x)}{x+\mu^*}$, where $\mu^*$ is the solution of the ($1$- dimensional) equation $\int f_0(x) \log[q(\mu)(x+\mu)]dx=d$ and $q(\mu)=\int \frac{f_0(x)}{x+\mu}dx$.
\end{theorem}
\begin{proof}
The proof is given in Appendix \ref{ap1}.
\end{proof}
We now consider the performance of the system for two asymptotic cases i.e., $d=0$ and $d\rightarrow \infty$. For the case where $d=0$, there is not distribution uncertainty and thus $f(x)=f_0(x)$ and $\mathcal{E}_0=\int x f_0(x)dx$ (expectation of the nominal distribution). On the other hand, for the case $d\rightarrow \infty$, we have $\int f_0(x) \log[q(\mu)(x+\mu^*)]dx\rightarrow \infty$ which after simple manipulations\footnote{We have $\int f_0(x)\log q(\mu^*)+\int f_0(x)\log(x+\mu^*)\leq \log q(\mu^*) +\mathcal{E}_0+\mu^*$, where we used the basic inequality $\log(x)\leq x$; since $\mu^*$ and $\mathcal{E}_0$ are finite, we have $q(\mu^*)\rightarrow \infty$.} gives $\mu^*\rightarrow 0$, $q(\mu^*)\rightarrow \infty$ and thus $\mathcal{E}\rightarrow 0$. In the following discussion, we apply Theorem \ref{th1} for the case where the nominal distribution is exponential\footnote{The exponential distribution is used for the sake of simplicity to introduce the proposed mathematical framework. It also refers to a linear/piece-wise linear EH model with Rayleigh channel fading.}.

\noindent {\it Special Case (Exponential distribution):} For the case where the nominal distribution is exponential i.e., $f_0(x)=\lambda_0 \exp(-\lambda_0 x)$, we have
\begin{align}
&f(x)=\frac{1}{q(\mu^*)}\frac{\lambda_0\exp(-\lambda_0 x)}{x+\mu^*}=\frac{\exp(-\lambda_0(x+\mu^*))}{E_1(\lambda_0 \mu^*)(x+\mu^*)}, \\
&q(\mu^*)=\int_0^{\infty}\frac{\lambda_0\exp(-\lambda_0 x)}{x+\mu^*}dx=\lambda_0 \exp(\lambda_0 \mu^*)E_1(\lambda_0 \mu^*), \label{q1} \\
\mathcal{E}&=\int_{0}^{\infty}xf(x)dx=\frac{1}{\lambda_0  \exp(\lambda_0 \mu^*)E_1(\lambda_0 \mu^*)}-\mu^*, \label{q2}
\end{align}
where \eqref{q1}, \eqref{q2} employ the expressions in \cite[3.352.4]{GRA}, \cite[3.353.5]{GRA}, respectively, and $E_1(x)=\int_{x}^{\infty}\frac{\exp(-t)}{t}dt$ is the exponential integral \cite{GRA}. The parameter $\mu^*$ is the solution of the simplified equation $q(\mu)/\lambda_0 +\log (\mu q(\mu))=d$. We can also calculate the cumulative density function (CDF) of the distribution, which is useful for the evaluation of the energy outage probability. Specifically, the CDF of the actual distribution is equal to \cite[3.352.1]{GRA}
\begin{align}
F(x)=\!\mathbb{P}(X\leq x)=\!\!\int_{0}^{x}\!\!f(x)dx=\!1\!-\!\frac{E_1(\lambda_0(x+\mu^*))}{E_1(\lambda_0 \mu^*)}.
\end{align}

\vspace{-0.5cm}
\subsection{KL divergence asymmetry}

One of the main properties of the KL divergence is that is not symmetric i.e., $\mathcal{D}_{\text{KL}}(f||g) \neq \mathcal{D}_{\text{KL}}(g||f)$. Here, we replace the KL constraint in \eqref{co1} with $\mathcal{D}_{\text{KL}}(f||f_0)\leq d$ i.e.,
\begin{align}
&(P2)\;\;\min_f \int x f(x)dx \\
&\;\;\;\;\;\;\;\;\;\;\text{s. t.}\; \mathcal{D}_{\text{KL}}(f||f_0)\leq d,\;\;\;\int f(x)dx=1. \label{co2}
\end{align}
By using a similar mathematical framework with the formulation in (P1), we state the following theorem.
\begin{theorem}\label{th2}
The actual distribution that achieves the minimum average harvested energy is $f(x)=\frac{\exp(-x/s^*)f_0(x)}{\int \exp(-x/s^*)f_0(x)dx}$, where the variable $s^*$ is given numerically by solving the ($1$-dimensional) equation in \eqref{s1}.
\end{theorem}
\begin{proof}
The proof is given in Appendix \ref{ap2}.
\end{proof}
By using similar arguments with the problem (P1), we can see that $f(x)=f_0(x)$ when $d=0$; the case $d\rightarrow \infty$ will be discussed bellow for a specific example of nominal distribution.

\noindent {\it Special Case (Exponential distribution):} For the case where $f_0(x)=\lambda_0 \exp(-\lambda_0 x)$, we have $f(x)=(1/s^*+\lambda_0) \exp(-x(1/s^*+\lambda_0))$, which shows that the actual distribution is also exponential with parameter $(1/s^*+\lambda_0)$. In addition, we have $\zeta(s^*)=\frac{\lambda_0}{(\lambda_0+1/s^*)^2}$, $\psi_1(s^*)=\frac{\lambda_0}{(\lambda_0+1/s^*)}$ and thus $\mathcal{E}=\frac{\zeta(s^*)}{\psi_1(s^*)}=\frac{s^*}{1+s^* \lambda_0}$; $s^*$ is the solution of the simplified nonlinear equation $\xi(s)=d$ where $\xi(s)=s\log \frac{Z(s)}{\lambda_0}-\frac{1}{Z(s)}$ and $Z(s)=\frac{1}{s}+\lambda_0$ with $s \in (0, \infty)$.

To study the asymptotic performance, we can see that the function $\xi(s)$ is increasing ($\xi'(s)\geq 0$) in the interval $(0, \overline{s}^*)$ and decreasing  ($\xi'(s)\leq 0$) in the interval $(\overline{s}^*, \infty)$, where $\xi'(s)=\log\left(1+\frac{1}{\lambda_0 s}\right)-\frac{2+\lambda_0 s}{(\lambda_0 s+1)^2}$, and $\xi'(\overline{s}^*)=0$. Therefore, for $d\geq \xi'(s)$ we have $\mathcal{E}=\frac{\overline{s}^*}{1+\overline{s}^*\lambda_0}$; for $d\rightarrow 0$, we have $\lim_{s\rightarrow \infty}\xi(s)\rightarrow 0$ and thus $s^*\rightarrow \infty$ which gives $\mathcal{E}=1/\lambda_0$. This is the basic difference between the two KL divergence metrics; $\mathcal{D}_{\text{KL}}(f||f_0)$ converges to a nonzero constant floor, while $\mathcal{D}_{\text{KL}}(f_0||f)$ asymptotically converges to zero.

\vspace{-0.3cm}
\subsection{Symmetrized divergence}\label{sd}

The symmetrized divergence is another statistical distance metric, which in contrast to the KL divergence metrics, it satisfies the property of symmetry \cite{MOU}. Specifically, the symmetrized divergence is defined as
\begin{align}
\mathcal{D}_{\text{SYM}}(f_0, f)=\frac{1}{2}\big[\mathcal{D}_{\text{KL}}(f_0||f)+\mathcal{D}_{\text{KL}}(f||f_0) \big],
\end{align}
and it can be seen that $\mathcal{D}_{\text{SYM}}(f_0, f)=\mathcal{D}_{\text{SYM}}(f, f_0)$; we note that $\mathcal{D}_{\text{SYM}}$ might not satisfy the triangle inequality and therefore it is not an actual distance. In this case, the original optimization problem is formulated as follows
\begin{align}
&(P3)\;\;\min_f \int x f(x)dx \\
&\;\;\;\;\;\;\;\;\;\;\text{s. t.}\; \mathcal{D}_{\text{SYM}}(f_0, f)\leq d,\;\;\;\int f(x)dx=1. \label{co3}
\end{align}
The optimization problem (P3) is also convex since the symmetrized divergence is a convex statistical metric. In the following theorem, we provide the actual distribution that solves (P3) as a function of the nominal distribution.
\begin{theorem}\label{th3}
The actual distribution that achieves the minimum average harvested energy is $f(x)=\frac{f_0(x)}{W_0 \left(\exp \left(\frac{2(x+\mu^*)}{s^*} \right) \right)}$, where the parameters $s^*>0$, $\mu^*$ are computed numerically by solving the (two-dimensional) system of equations in \eqref{x1}, \eqref{x2}.
\end{theorem}
\begin{proof}
The proof is given in Appendix \ref{ap3}.
\end{proof}

\vspace{-0.3cm}
\subsection{Known class/type of the true distribution- case studies}

Here, we assume that although there is uncertainty for the distribution $f(x)$, we know the exact class/type of the unknown distribution. This assumption can be supported by a more strict distribution estimation process, which provides the type of the distribution in addition to the maximum statistical distance $d$; this case has mainly theoretical interest and allows to further investigate the impact of the divergence between the selected and the true model on the system performance. The following discussion refers to two specific case studies.

\noindent {\bf Case study 1} (Exponential distributions): if the nominal and the actual distribution are exponential with parameters $\lambda_0$ and $\lambda_1\geq \lambda_0$, respectively, the KL divergence is written as
\begin{align}
\mathcal{D}_{\text{KL}}(f_0||f)&=\!\int_{0}^{\infty}\!\lambda_0 \exp(-\lambda_0 x)\log \frac{\lambda_0 \exp(-\lambda_0 x)}{\lambda_1 \exp(-\lambda_1 x)}dx \nonumber \\
&= \log \frac{\lambda_0}{\lambda_1}+\frac{\lambda_1-\lambda_0}{\lambda_0}.
\end{align}
In this case, we have $\mathcal{D}_{\text{KL}}(f_0||f)\leq d\Rightarrow \frac{\lambda_1}{\lambda_0}\exp(-\frac{\lambda_1}{\lambda_0})\geq \exp(-d-1)$. Since the function $g(x)=x\exp(-x)$ is monotonically decreasing for $x\geq 1$ (i.e., $g'(x)\leq 0$ with $x\geq1$), the minimum average expected value is achieved at the boundary i.e., $\frac{\lambda_1}{\lambda_0}\exp(-\frac{\lambda_1}{\lambda_0})=\exp(-d-1)$ which gives $\lambda_1^*=\max[-\lambda_0W_0(-\exp(-d-1)),\lambda_0(1+d)]$, where $W_0(\cdot)$ is the principal branch of the LambertW function \cite{GRA}; in a similar way, for the  symmetric case ($\mathcal{D}_{\text{KL}}(f||f_0)$) we have $\lambda_1^*=\max[-\lambda_0/W_0(-\exp(-1-d)),\lambda_0/(1+d)]$.
For the case of the symmetrized divergence, we have $\mathcal{D}_\text{SYM}(f_0,f)=\frac{\lambda_1}{\lambda_0}+\frac{\lambda_0}{\lambda_1}-2$ and therefore $\mathcal{D}_\text{SYM}(f_0,f)\leq d \Rightarrow \lambda_1^2-2\lambda_0 (d+1)\lambda_1+\lambda_0^2\leq 0$ with solution $\lambda_1 \in [\lambda_0(d+1)-\lambda_0\sqrt{d(d+2)},\lambda_0(d+1)+\lambda_0\sqrt{d(d+2)}]$; therefore $\lambda_1^*=\lambda_0(d+1)+\lambda_0\sqrt{d(d+2)}$. For all the cases, the minimum  average harvested energy is equal to $\mathcal{E}=1/\lambda_1^*$.

\noindent {\bf Case study 2} (Uniform distributions): If the nominal and the actual distributions are uniform over the interval $[0,\alpha]$ and $[0,\beta]$ with $\beta\leq \alpha$, respectively, we obtain
$\mathcal{D}_{\text{KL}}(f||f_0) \leq d\Rightarrow \log\frac{\alpha}{\beta} \leq d \Rightarrow \beta\geq \alpha \exp(-d)$,
and therefore the solution of the optimization problem considered is achieved at the boundary i.e., $\mathcal{E}=\frac{\alpha\exp(-d)}{2}$.
As for KL asymmetry and the symmetric divergence, $f_0(x)$ is not dominated by $f(x)$ and thus we have $\mathcal{D}_{\text{KL}}(f_0||f)=\infty$ \cite[Def. 6.1]{MOU}; therefore, these two metrics have not practical interest.

\begin{figure}[t]
\centering
\includegraphics[width=0.8\linewidth]{krikidis_WCL2020-0748_fig1.eps}
\caption{CDF of the actual distribution for different values of $d$; solid-lines and dashed-lines correspond to the KL divergence $\mathcal{D}_{\text{KL}}(f_0||f)$ and $\mathcal{D}_{\text{KL}}(f||f_0)$, respectively; nominal distribution $f_0(x)=\exp(-x)$.}\label{fig0}
\end{figure}

\begin{figure}[t]
\centering
\includegraphics[width=0.75\linewidth]{krikidis_WCL2020-0748_fig2.eps}
\caption{Minimum average energy harvested (worst case performance) versus $d$ with $f_0(x)=\exp(-x)$; for the $\mathcal{D}_{\text{KL}}(f||f_0)$ case,  we have $\xi'(s)=0\Rightarrow \overline{s}^*=0.46$, and $\mathcal{E}=\frac{\overline{s}^*}{1+\lambda_0 \overline{s}^*}=0.31$.}\label{fig1}
\end{figure}

\begin{figure}[t]
\centering
\includegraphics[width=0.85\linewidth]{krikidis_WCL2020-0748_fig3.eps}
\caption{CDF of the actual distribution under symmetrized divergence uncertainty for different values of $d$; nominal distribution $f_0(x)=\exp(-x)$.}\label{fig2}
\end{figure}

\begin{figure}[t]
\centering
\includegraphics[width=0.65\linewidth]{krikidis_WCL2020-0748_fig4.eps}
\caption{Uncertainty with known class of distribution- $\lambda_1/\lambda_0$ versus the distance $d$ for an exponential nominal distribution $f_0(x)=\lambda_0 \exp(-\lambda_0 x)$.}\label{fig3}
\end{figure}

\vspace{-0.3cm}
\section{Numerical results}
Computer simulations are carried-out to validate the proposed mathematical framework. For the sake of simplicity, the numerical results concern a normalized exponential nominal distribution i.e., $f_0(x)=\lambda_0 \exp(-\lambda_0 x)$ with $\lambda_0=1$.

Fig. \ref{fig0} shows the CDF of the actual distribution for different values of $d$ for both KL divergence metrics considered. As it can be seen, a higher KL distance $d$ shifts the CDF curves from right to left and increases the gap between nominal and actual distribution. We can see that the uncertainty significantly affects the harvested energy and an increase of the distance $d$ results in a more conservative EH performance. Another interesting observation is that both KL divergence metrics follow the same behaviour/trend and result in same general conclusions; however, it worth noting that $\mathcal{D}_{\text{KL}}(f||f_0)$ results in a more conservative actual distribution than $\mathcal{D}_{\text{KL}}(f_0||f)$ for low $d$. As the distance $d$ increases, we have the opposite behaviour which is also justified by the asymptotic performance of the two metrics (see Fig. \ref{fig1} for $d=0.5$).

Fig. \ref{fig1} plots the minimum average harvested energy (worst case performance) versus the KL distance $d$ for both considered KL divergence metrics. As it can be seen, the worst performance significantly decreases as the distance $d$ increases. This plot also validates our asymptotic results for high values of $d$ (i.e., $d\rightarrow \infty$) which are discussed in Section \ref{sec2}. It can be seen that swapping the distributions (nominal and true) results in a floor effect; $\mathcal{E}$ asymptotically converges to zero for the metric $\mathcal{D}_{\text{KL}}(f_0||f)$, while $\mathcal{E}$ converges to a constant floor that depends on the KL distance $d$ i.e., $\overline{s}^*/(\lambda \overline{s}^*+1)$ for the metric $\mathcal{D}_{\text{KL}}(f||f_0)$.

In Fig. \ref{fig2}, we show the CDF of the actual distribution for different values of $d$, when statistical distance corresponds to the symmetrized divergence metric. It can be seen that the CDF is shifted towards its left as the distance $d$ increases; therefore the associated energy outage probability increases. This behaviour is inline with the observations in Fig. \ref{fig0}. However, it is worth noting that the symmetrized divergence results in a CDF which is between the CDFs associated with  $\mathcal{D}_{\text{KL}}(f_0||f)$ and $\mathcal{D}_{\text{KL}}(f||f_0)$. Therefore, the symmetrized divergence consists of a balance between the two KL metrics considered. In this figure, we also show the minimum harvested energy (solution to (P3)) by following the theoretical framework in Section \ref{sd}.

Finally, Fig. \ref{fig3} deals with the actual distribution when the class/type of the true distribution is known. Specifically, we assume that nominal/actual distributions are exponential with parameters $\lambda_0$ and $\lambda_1$, respectively, and we plot $\lambda_1/\lambda_0$ versus $d$ for the statistical divergence metrics considered. It can be seen that the difference between the true and the nominal distributions increases as the divergence $d$ increases. In addition, we can see $\mathcal{D}_{\text{KL}}(f_0||f)$ provides a better estimation of $f(x)$ (i.e., $\lambda_1/\lambda_0$ increases linearly with $d$), while  $\mathcal{D}_{\text{KL}}(f||f_0)$ results in an exponential difference.

\vspace{-0.2cm}
\section{Conclusion}

A mathematical framework that integrates EH uncertainty in the current deterministic WPT models has been proposed. By exploiting the notion of the compound channel model, we have studied the worst performance (average harvested energy) when the actual end-to-end distribution is within a given KL/symmetrized maximum statistical distance from a nominal distribution. General closed-form expressions that hold for any nominal distribution as well as simplified expressions that refer to an exponential nominal distribution have been derived. Theoretical results show that distribution uncertainty significantly affects EH performance and therefore its integration to current WPT models is essential for a robust design.

\vspace{-0.1cm}

\appendices
\section{Proof of Theorem \ref{th1}} \label{ap1}
\vspace{-0.1cm}

Since the problem is convex (i.e., linear objective function and convex constraints), KKT conditions are necessary and sufficient for optimality \cite{BOY}. The Lagrangian function of the problem is written as
\begin{align}
&L=\int x f(x) dx \nonumber \\
&\!+\! s \left(\int\!\!\ f_0(x)\log \frac{f_0(x)}{f(x)}dx-d\right)+\mu \left(\int\!\! f(x)dx-1\right),
\end{align}
where $s$ and $\mu$ are the Lagrange multipliers of two constraints.  The associated KKT conditions are given as follows \cite{BOY}
\begin{align}
 x-s\frac{f_0(x)}{f(x)}+\mu=0&, \label{eq1}  \\
\int f(x)dx-1 =0&, \label{eq2} \\
s \left(\int f_0(x)\log \frac{f_0(x)}{f(x)}dx-d \right)=0&, \label{eq3} \\
s\geq 0&.
\end{align}
\noindent From the complementary slackness condition in \eqref{eq3}, for $s>0$ the minimum is achieved at the boundary. In this case, by combining \eqref{eq1} and \eqref{eq2} and after some manipulations, we have
\begin{align}
f(x)=\frac{f_0(x)}{q(\mu^*)(x+\mu^*)},
\end{align}
\vspace{-0.2cm}
where
\vspace{-0.2cm}
\begin{align}
q(\mu)=\int \frac{f_0(x)}{x+\mu}dx,
\end{align}
and $\mu^*$ is the unique solution of the nonlinear equation
\begin{align}
\int f_0(x) \log[q(\mu)(x+\mu)]dx=d,
\end{align}
which can be solved numerically (e.g., Newton-Raphson method).

\vspace{-0.4cm}
\section{proof of Theorem \ref{th2}}\label{ap2}

Since the asymmetric KL divergence is also convex with respect to $f(x)$ \cite{MOU}, the optimization problem remains convex; we formulate the Lagrange function i.e.
\vspace{-0.2cm}
\begin{align}
&L_2=\int x f(x)dx \nonumber \\
&+s \left(\int\! f(x) \log \frac{f(x)}{f_0(x)}dx-d   \right)\!+\!\mu \left(\int\! f(x)dx-1 \!\right).
\end{align}
\vspace{-0.2cm}
The associated KKT conditions \cite{BOY} are written as
\begin{align}
x+s\left(\log\frac{f(x)}{f_0(x)}  \right)+\mu=0&, \\
\int f(x)dx=1&, \\
s\left(\int f(x) \log \frac{f(x)}{f_0(x)}dx-d \right)=0&. \label{d1} \\
s\geq 0&.
\end{align}
For $s>0$, the optimal solution is located at the boundary (complementary slackness in \eqref{d1}); by combining the above equations, we have
\begin{align}
f(x)=\frac{\psi_0(x,s^*)}{\psi_1(s^*)},
\end{align}
where
\begin{align}
&\psi_0(x,s)=\exp(-x/s)f_0(x), \\
&\psi_1(s)=\int \psi_0(x,s)dx, \\
&\zeta(s)=\int x \psi_0(x,s)dx.
\end{align}
The optimal dual variable $s^*$ can be found by solving numerically the following equality
\begin{align}
-\frac{\zeta(s)}{\psi_1(s)}-s\log \psi_1(s)=sd. \label{s1}
\end{align}

\vspace{-0.8cm}
\section{Proof of Theorem \ref{th3}}\label{ap3}

The Lagrangian function for the problem in (P3) is written as
\vspace{-0.5cm}
\begin{align}
&L=\int x f(x)dx \nonumber
\end{align}

\begin{align}
&+\frac{s}{2}\left(\int f_0(x)\log \frac{f_0(x)}{f(x)}dx
+ \int f(x)\log \frac{f(x)}{f_0(x)}dx \right) \nonumber \\
&+\mu \left(\int f(x)dx-1 \right).
\end{align}
By taking the derivative of $L$ with respect of $f(x)$, we employ the KKT conditions
\begin{align}
x-\frac{s}{2}\left(\frac{f_0(x)}{f(x)}+\log \frac{f_0(x)}{f(x)}\right)+\mu =0&, \label{x0} \\
\int f(x)dx=1&, \label{x1} \\
\frac{s}{2}\!\left(\!\int\! f_0(x)\log \frac{f_0(x)}{f(x)}dx\!+\!\!\!\int\!\!\! f(x)\log \frac{f(x)}{f_0(x)}dx\!-d \!\right)=0&, \label{x2} \\
s\geq 0&.
\end{align}
\vspace{-0.1cm}
By solving \eqref{x0} with respect to $f(x)$, we derive an expression of the actual distribution
\begin{align}
f(x)=\frac{f_0(x)}{W_0 \left(\exp \left(\frac{2(x+\mu^*)}{s^*} \right) \right)},
\end{align}
where the optimal dual parameters $s^*$ and $\mu^*$ can be computed numerically by solving a (two-dimensional) nonlinear system of equation that is defined by \eqref{x1} and \eqref{x2}.

config: arxiv


TITLE: Stiff differential equation
QUESTION [0 upvotes]: I'm trying to solve a system of differential equations with Runge-Kutta method. When I use the step size $h=1$ my problem has true answer but when I use the smaller $h$ (for example $h = 0.1$) my answer is very bad. So I think I have a stiff problem. My question is how can  I prove my problem is stiff? I want to know the methods that used for proving stiff problems. Thanks a lot

REPLY [0 votes]: Compute the condition number of the Jacobian of the right side of the ODE at interesting points. If this number is very large, you have a stiff system. Edit: Since that tells you about the direction dependence of the Lipschitz constant. Non-stiff systems have a very low direction dependence.

Direct methods: Step size variation: Try a variety of step sizes $h$, for each $h$ compute the solution for $h$ and $h/2$, the difference between these two is an approximation of the error of the $h$ solution. This should be proportional to $h^p$ where $p$ is the global convergence order of the method. If the system is stiff, this becomes true only for very small step sizes $h$ or never, because then it becomes over-shadowed by rising numerical noise accumulation from the increasing number of steps.
Order variation: Use an adaptive method that has three embedded methods. If I remember correctly, there is a popular RK method that has embedded orders 1-5-6. See if the local errors conform to the theory for moderate Lipschitz constants.


TITLE: How to attack this probability question directly?
QUESTION [1 upvotes]: Below is a example probability question I found in my book. I want to attack this question directly instead of using the complement approach. How do I do that? My book always uses the complement approach, but I want to see how to tackle it head on.
Example Problem:
Mark is taking four final exams next week. His studying was erratic and all scores A, B, C, D, and F are equally likely for each exam. What is the probability that Mark will get at least one A?
Take complements. The complementary event of getting at least one A is getting no As. Since outcomes are equally likely, by the multiplication principle there are $4^4$ exam outcomes with no As (four grade choices for each of four exams). And there are $5^4$ possible outcomes in all. The desired probability is $1−(4^4/5^4)=0.5904$.

REPLY [1 votes]: There's a reason taking complements is often suggested.  But to tackle it head on, as you say, we note that the number of A is a random variable with a binomial distribution of ${\cal Bin}(4, 1/5)$   (Do you know why?)
$$X_A\sim{\cal Bin}(n, p) \iff \mathsf P(X_A=k) = {n\choose k}p^k (1-p)^{n-k}$$
So for this problem, $n=4, p=1/5$ and we want $X_A\geqslant 1$ so we need to evaluate the series:
$$\begin{align}\mathsf P(X_A\geqslant 1) &= \sum_{k=1}^4 \mathsf P(X_A=k) \\ & = {4\choose 1}\frac {4^3}{5^4} + {4\choose 2}\frac {4^2}{5^4} + {4\choose 3}\frac {4}{5^4} + {4\choose 4}\frac {1}{5^4}
\\[4ex]
\mathsf P(X_A\geqslant 1) & = 1-\mathsf P(X=0)
\\ & = 1- {4\choose 0}\frac {4^4} {5^4}
\\ & = \frac{369}{625}
\end{align}$$


TITLE: Prime Ideals in a Localised Ring
QUESTION [1 upvotes]: Let $R$ be a commutative ring, and let $S \subseteq R$ be a multiplicatively closed subset (not containing $0$). Then we construct the localised ring $R [ S^{-1} ]$. I understand that prime ideals in $R [ S^{-1} ]$ correspond to prime ideals in $R$ which do not intersect $S$. Is it always true that if $\mathfrak{q}$ is prime in $R$, then $\mathfrak{q}R[S^{-1}]$ is prime in $R[S^{-1}]$?

REPLY [3 votes]: Either $\mathfrak q$ does not intersect $S$, and then you know that the extension to $S^{-1}R$ is prime, or it intersects $S$ in which case $\mathfrak q(S^{-1}R) = S^{-1}R$ is a very specific non-prime.
Here's an elementary way to prove the first assertion: show that $a/s$ is in $\mathfrak q(S^{-1}R)$ if and only if $a \in \mathfrak q$. You'll need to use that $\mathfrak q$ is prime and that $S \cap \mathfrak q=\varnothing$.