text:
section \<open>\<open>Extra_General\<close> -- General missing things\<close>

theory Extra_General
  imports
    "HOL-Library.Cardinality"
    "HOL-Analysis.Elementary_Topology"
    "HOL-Analysis.Uniform_Limit"
    "HOL-Library.Set_Algebras"
    "HOL-Types_To_Sets.Types_To_Sets"
    "HOL-Library.Complex_Order"
    "HOL-Analysis.Infinite_Sum"
begin

subsection \<open>Misc\<close>

lemma reals_zero_comparable:
  fixes x::complex
  assumes "x\<in>\<real>"
  shows "x \<le> 0 \<or> x \<ge> 0"
  using assms unfolding complex_is_real_iff_compare0 by assumption

lemma unique_choice: "\<forall>x. \<exists>!y. Q x y \<Longrightarrow> \<exists>!f. \<forall>x. Q x (f x)"
  apply (auto intro!: choice ext) by metis

lemma sum_single:
  assumes "finite A"
  assumes "\<And>j. j \<noteq> i \<Longrightarrow> j\<in>A \<Longrightarrow> f j = 0"
  shows "sum f A = (if i\<in>A then f i else 0)"
  apply (subst sum.mono_neutral_cong_right[where S=\<open>A \<inter> {i}\<close> and h=f])
  using assms by auto

lemma image_set_plus:
  assumes \<open>linear U\<close>
  shows \<open>U ` (A + B) = U ` A + U ` B\<close>
  unfolding image_def set_plus_def
  using assms by (force simp: linear_add)

consts heterogenous_identity :: \<open>'a \<Rightarrow> 'b\<close>
overloading heterogenous_identity_id \<equiv> "heterogenous_identity :: 'a \<Rightarrow> 'a" begin
definition heterogenous_identity_def[simp]: \<open>heterogenous_identity_id = id\<close>
end

lemma L2_set_mono2:
  assumes a1: "finite L" and a2: "K \<le> L"
  shows "L2_set f K \<le> L2_set f L"
proof-
  have "(\<Sum>i\<in>K. (f i)\<^sup>2) \<le> (\<Sum>i\<in>L. (f i)\<^sup>2)"
  proof (rule sum_mono2)
    show "finite L"
      using a1.
    show "K \<subseteq> L"
      using a2.
    show "0 \<le> (f b)\<^sup>2"
      if "b \<in> L - K"
      for b :: 'a
      using that
      by simp
  qed
  hence "sqrt (\<Sum>i\<in>K. (f i)\<^sup>2) \<le> sqrt (\<Sum>i\<in>L. (f i)\<^sup>2)"
    by (rule real_sqrt_le_mono)
  thus ?thesis
    unfolding L2_set_def.
qed

lemma Sup_real_close:
  fixes e :: real
  assumes "0 < e"
    and S: "bdd_above S" "S \<noteq> {}"
  shows "\<exists>x\<in>S. Sup S - e < x"
proof -
  have \<open>Sup (ereal ` S) \<noteq> \<infinity>\<close>
    by (metis assms(2) bdd_above_def ereal_less_eq(3) less_SUP_iff less_ereal.simps(4) not_le)
  moreover have \<open>Sup (ereal ` S) \<noteq> -\<infinity>\<close>
    by (simp add: SUP_eq_iff assms(3))
  ultimately have Sup_bdd: \<open>\<bar>Sup (ereal ` S)\<bar> \<noteq> \<infinity>\<close>
    by auto
  then have \<open>\<exists>x'\<in>ereal ` S. Sup (ereal ` S) - ereal e < x'\<close>
    apply (rule_tac Sup_ereal_close)
    using assms by auto
  then obtain x where \<open>x \<in> S\<close> and Sup_x: \<open>Sup (ereal ` S) - ereal e < ereal x\<close>
    by auto
  have \<open>Sup (ereal ` S) = ereal (Sup S)\<close>
    using Sup_bdd by (rule ereal_Sup[symmetric])
  with Sup_x have \<open>ereal (Sup S - e) < ereal x\<close>
    by auto
  then have \<open>Sup S - e < x\<close>
    by auto
  with \<open>x \<in> S\<close> show ?thesis
    by auto
qed

text \<open>Improved version of @{attribute internalize_sort}: It is not necessary to specify the sort of the type variable.\<close>
attribute_setup internalize_sort' = \<open>let
fun find_tvar thm v = let
  val tvars = Term.add_tvars (Thm.prop_of thm) []
  val tv = case find_first (fn (n,sort) => n=v) tvars of
              SOME tv => tv | NONE => raise THM ("Type variable " ^ string_of_indexname v ^ " not found", 0, [thm])
in
TVar tv
end

fun internalize_sort_attr (tvar:indexname) =
  Thm.rule_attribute [] (fn context => fn thm =>
    (snd (Internalize_Sort.internalize_sort (Thm.ctyp_of (Context.proof_of context) (find_tvar thm tvar)) thm)));
in
  Scan.lift Args.var >> internalize_sort_attr
end\<close>
  "internalize a sort"

subsection \<open>Not singleton\<close>

class not_singleton =
  assumes not_singleton_card: "\<exists>x y. x \<noteq> y"

lemma not_singleton_existence[simp]:
  \<open>\<exists> x::('a::not_singleton). x \<noteq> t\<close>
  using not_singleton_card[where ?'a = 'a] by (metis (full_types))

lemma UNIV_not_singleton[simp]: "(UNIV::_::not_singleton set) \<noteq> {x}"
  using not_singleton_existence[of x] by blast

lemma UNIV_not_singleton_converse:
  assumes"\<And>x::'a. UNIV \<noteq> {x}"
  shows "\<exists>x::'a. \<exists>y. x \<noteq> y"
  using assms
  by fastforce

subclass (in card2) not_singleton
  apply standard using two_le_card
  by (meson card_2_iff' obtain_subset_with_card_n)

subclass (in perfect_space) not_singleton
  apply intro_classes
  by (metis (mono_tags) Collect_cong Collect_mem_eq UNIV_I local.UNIV_not_singleton local.not_open_singleton local.open_subopen)

lemma class_not_singletonI_monoid_add:
  assumes "(UNIV::'a set) \<noteq> {0}"
  shows "class.not_singleton TYPE('a::monoid_add)"
proof intro_classes
  let ?univ = "UNIV :: 'a set"
  from assms obtain x::'a where "x \<noteq> 0"
    by auto
  thus "\<exists>x y :: 'a. x \<noteq> y"
    by auto
qed

lemma not_singleton_vs_CARD_1:
  assumes \<open>\<not> class.not_singleton TYPE('a)\<close>
  shows \<open>class.CARD_1 TYPE('a)\<close>
  using assms unfolding class.not_singleton_def class.CARD_1_def
  by (metis (full_types) One_nat_def UNIV_I card.empty card.insert empty_iff equalityI finite.intros(1) insert_iff subsetI)

subsection \<open>\<^class>\<open>CARD_1\<close>\<close>

context CARD_1 begin

lemma everything_the_same[simp]: "(x::'a)=y"
  by (metis (full_types) UNIV_I card_1_singletonE empty_iff insert_iff local.CARD_1)

lemma CARD_1_UNIV: "UNIV = {x::'a}"
  by (metis (full_types) UNIV_I card_1_singletonE local.CARD_1 singletonD)

lemma CARD_1_ext: "x (a::'a) = y b \<Longrightarrow> x = y"
proof (rule ext)
  show "x t = y t"
    if "x a = y b"
    for t :: 'a
    using that  apply (subst (asm) everything_the_same[where x=a])
    apply (subst (asm) everything_the_same[where x=b])
    by simp
qed

end

instance unit :: CARD_1
  apply standard by auto

instance prod :: (CARD_1, CARD_1) CARD_1
  apply intro_classes
  by (simp add: CARD_1)

instance "fun" :: (CARD_1, CARD_1) CARD_1
  apply intro_classes
  by (auto simp add: card_fun CARD_1)

lemma enum_CARD_1: "(Enum.enum :: 'a::{CARD_1,enum} list) = [a]"
proof -
  let ?enum = "Enum.enum :: 'a::{CARD_1,enum} list"
  have "length ?enum = 1"
    apply (subst card_UNIV_length_enum[symmetric])
    by (rule CARD_1)
  then obtain b where "?enum = [b]"
    apply atomize_elim
    apply (cases ?enum, auto)
    by (metis length_0_conv length_Cons nat.inject)
  thus "?enum = [a]"
    by (subst everything_the_same[of _ b], simp)
qed

subsection \<open>Topology\<close>

lemma cauchy_filter_metricI:
  fixes F :: "'a::metric_space filter"
  assumes "\<And>e. e>0 \<Longrightarrow> \<exists>P. eventually P F \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> dist x y < e)"
  shows "cauchy_filter F"
proof (unfold cauchy_filter_def le_filter_def, auto)
  fix P :: "'a \<times> 'a \<Rightarrow> bool"
  assume "eventually P uniformity"
  then obtain e where e: "e > 0" and P: "dist x y < e \<Longrightarrow> P (x, y)" for x y
    unfolding eventually_uniformity_metric by auto

  obtain P' where evP': "eventually P' F" and P'_dist: "P' x \<and> P' y \<Longrightarrow> dist x y < e" for x y
    apply atomize_elim using assms e by auto

  from evP' P'_dist P
  show "eventually P (F \<times>\<^sub>F F)"
    unfolding eventually_uniformity_metric eventually_prod_filter eventually_filtermap by metis
qed

lemma cauchy_filter_metric_filtermapI:
  fixes F :: "'a filter" and f :: "'a\<Rightarrow>'b::metric_space"
  assumes "\<And>e. e>0 \<Longrightarrow> \<exists>P. eventually P F \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> dist (f x) (f y) < e)"
  shows "cauchy_filter (filtermap f F)"
proof (rule cauchy_filter_metricI)
  fix e :: real assume e: "e > 0"
  with assms obtain P where evP: "eventually P F" and dist: "P x \<and> P y \<Longrightarrow> dist (f x) (f y) < e" for x y
    by atomize_elim auto
  define P' where "P' y = (\<exists>x. P x \<and> y = f x)" for y
  have "eventually P' (filtermap f F)"
    unfolding eventually_filtermap P'_def
    using evP
    by (smt eventually_mono)
  moreover have "P' x \<and> P' y \<longrightarrow> dist x y < e" for x y
    unfolding P'_def using dist by metis
  ultimately show "\<exists>P. eventually P (filtermap f F) \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> dist x y < e)"
    by auto
qed

lemma tendsto_add_const_iff:
  \<comment> \<open>This is a generalization of \<open>Limits.tendsto_add_const_iff\<close>,
      the only difference is that the sort here is more general.\<close>
  "((\<lambda>x. c + f x :: 'a::topological_group_add) \<longlongrightarrow> c + d) F \<longleftrightarrow> (f \<longlongrightarrow> d) F"
  using tendsto_add[OF tendsto_const[of c], of f d]
    and tendsto_add[OF tendsto_const[of "-c"], of "\<lambda>x. c + f x" "c + d"] by auto

lemma finite_subsets_at_top_minus:
  assumes "A\<subseteq>B"
  shows "finite_subsets_at_top (B - A) \<le> filtermap (\<lambda>F. F - A) (finite_subsets_at_top B)"
proof (rule filter_leI)
  fix P assume "eventually P (filtermap (\<lambda>F. F - A) (finite_subsets_at_top B))"
  then obtain X where "finite X" and "X \<subseteq> B"
    and P: "finite Y \<and> X \<subseteq> Y \<and> Y \<subseteq> B \<longrightarrow> P (Y - A)" for Y
    unfolding eventually_filtermap eventually_finite_subsets_at_top by auto

  hence "finite (X-A)" and "X-A \<subseteq> B - A"
    by auto
  moreover have "finite Y \<and> X-A \<subseteq> Y \<and> Y \<subseteq> B - A \<longrightarrow> P Y" for Y
    using P[where Y="Y\<union>X"] \<open>finite X\<close> \<open>X \<subseteq> B\<close>
    by (metis Diff_subset Int_Diff Un_Diff finite_Un inf.orderE le_sup_iff sup.orderE sup_ge2)
  ultimately show "eventually P (finite_subsets_at_top (B - A))"
    unfolding eventually_finite_subsets_at_top by meson
qed

lemma finite_subsets_at_top_inter:
  assumes "A\<subseteq>B"
  shows "filtermap (\<lambda>F. F \<inter> A) (finite_subsets_at_top B) \<le> finite_subsets_at_top A"
proof (rule filter_leI)
  show "eventually P (filtermap (\<lambda>F. F \<inter> A) (finite_subsets_at_top B))"
    if "eventually P (finite_subsets_at_top A)"
    for P :: "'a set \<Rightarrow> bool"
    using that unfolding eventually_filtermap
    unfolding eventually_finite_subsets_at_top
    by (metis Int_subset_iff assms finite_Int inf_le2 subset_trans)
qed

lemma tendsto_principal_singleton:
  shows "(f \<longlongrightarrow> f x) (principal {x})"
  unfolding tendsto_def eventually_principal by simp

lemma complete_singleton:
  "complete {s::'a::uniform_space}"
proof-
  have "F \<le> principal {s} \<Longrightarrow>
         F \<noteq> bot \<Longrightarrow> cauchy_filter F \<Longrightarrow> F \<le> nhds s" for F
    by (metis eventually_nhds eventually_principal le_filter_def singletonD)
  thus ?thesis
    unfolding complete_uniform
    by simp
qed

subsection \<open>Complex numbers\<close>

lemma cmod_Re:
  assumes "x \<ge> 0"
  shows "cmod x = Re x"
  using assms unfolding less_eq_complex_def cmod_def
  by auto

lemma abs_complex_real[simp]: "abs x \<in> \<real>" for x :: complex
  by (simp add: abs_complex_def)

lemma Im_abs[simp]: "Im (abs x) = 0"
  using abs_complex_real complex_is_Real_iff by blast

lemma cnj_x_x: "cnj x * x = (abs x)\<^sup>2"
proof (cases x)
  show "cnj x * x = \<bar>x\<bar>\<^sup>2"
    if "x = Complex x1 x2"
    for x1 :: real
      and x2 :: real
    using that
    by (auto simp: complex_cnj complex_mult abs_complex_def
        complex_norm power2_eq_square complex_of_real_def)
qed

lemma cnj_x_x_geq0[simp]: \<open>cnj x * x \<ge> 0\<close>
  by (simp add: less_eq_complex_def)

subsection \<open>List indices and enum\<close>

fun index_of where
  "index_of x [] = (0::nat)"
| "index_of x (y#ys) = (if x=y then 0 else (index_of x ys + 1))"

definition "enum_idx (x::'a::enum) = index_of x (enum_class.enum :: 'a list)"

lemma index_of_length: "index_of x y \<le> length y"
  apply (induction y) by auto

lemma index_of_correct:
  assumes "x \<in> set y"
  shows "y ! index_of x y = x"
  using assms apply (induction y arbitrary: x)
  by auto

lemma enum_idx_correct:
  "Enum.enum ! enum_idx i = i"
proof-
  have "i \<in> set enum_class.enum"
    using UNIV_enum by blast
  thus ?thesis
    unfolding enum_idx_def
    using index_of_correct by metis
qed

lemma index_of_bound:
  assumes "y \<noteq> []" and "x \<in> set y"
  shows "index_of x y < length y"
  using assms proof(induction y arbitrary: x)
  case Nil
  thus ?case by auto
next
  case (Cons a y)
  show ?case
  proof(cases "a = x")
    case True
    thus ?thesis by auto
  next
    case False
    moreover have "a \<noteq> x \<Longrightarrow> index_of x y < length y"
      using Cons.IH Cons.prems(2) by fastforce
    ultimately show ?thesis by auto
  qed
qed

lemma enum_idx_bound: "enum_idx x < length (Enum.enum :: 'a list)" for x :: "'a::enum"
proof-
  have p1: "False"
    if "(Enum.enum :: 'a list) = []"
  proof-
    have "(UNIV::'a set) = set ([]::'a list)"
      using that UNIV_enum by metis
    also have "\<dots> = {}"
      by blast
    finally have "(UNIV::'a set) = {}".
    thus ?thesis by simp
  qed
  have p2: "x \<in> set (Enum.enum :: 'a list)"
    using UNIV_enum by auto
  moreover have "(enum_class.enum::'a list) \<noteq> []"
    using p2 by auto
  ultimately show ?thesis
    unfolding enum_idx_def
    using index_of_bound [where x = x and y = "(Enum.enum :: 'a list)"]
    by auto
qed

lemma index_of_nth:
  assumes "distinct xs"
  assumes "i < length xs"
  shows "index_of (xs ! i) xs = i"
  using assms
  by (metis gr_implies_not_zero index_of_bound index_of_correct length_0_conv nth_eq_iff_index_eq nth_mem)

lemma enum_idx_enum:
  assumes \<open>i < CARD('a::enum)\<close>
  shows \<open>enum_idx (enum_class.enum ! i :: 'a) = i\<close>
  unfolding enum_idx_def apply (rule index_of_nth)
  using assms by (simp_all add: card_UNIV_length_enum enum_distinct)

subsection \<open>Filtering lists/sets\<close>

lemma map_filter_map: "List.map_filter f (map g l) = List.map_filter (f o g) l"
proof (induction l)
  show "List.map_filter f (map g []) = List.map_filter (f \<circ> g) []"
    by (simp add: map_filter_simps)
  show "List.map_filter f (map g (a # l)) = List.map_filter (f \<circ> g) (a # l)"
    if "List.map_filter f (map g l) = List.map_filter (f \<circ> g) l"
    for a :: 'c
      and l :: "'c list"
    using that  map_filter_simps(1)
    by (metis comp_eq_dest_lhs list.simps(9))
qed

lemma map_filter_Some[simp]: "List.map_filter (\<lambda>x. Some (f x)) l = map f l"
proof (induction l)
  show "List.map_filter (\<lambda>x. Some (f x)) [] = map f []"
    by (simp add: map_filter_simps)
  show "List.map_filter (\<lambda>x. Some (f x)) (a # l) = map f (a # l)"
    if "List.map_filter (\<lambda>x. Some (f x)) l = map f l"
    for a :: 'b
      and l :: "'b list"
    using that by (simp add: map_filter_simps(1))
qed

lemma filter_Un: "Set.filter f (x \<union> y) = Set.filter f x \<union> Set.filter f y"
  unfolding Set.filter_def by auto

lemma Set_filter_unchanged: "Set.filter P X = X" if "\<And>x. x\<in>X \<Longrightarrow> P x" for P and X :: "'z set"
  using that unfolding Set.filter_def by auto

subsection \<open>Maps\<close>

definition "inj_map \<pi> = (\<forall>x y. \<pi> x = \<pi> y \<and> \<pi> x \<noteq> None \<longrightarrow> x = y)"

definition "inv_map \<pi> = (\<lambda>y. if Some y \<in> range \<pi> then Some (inv \<pi> (Some y)) else None)"

lemma inj_map_total[simp]: "inj_map (Some o \<pi>) = inj \<pi>"
  unfolding inj_map_def inj_def by simp

lemma inj_map_Some[simp]: "inj_map Some"
  by (simp add: inj_map_def)

lemma inv_map_total:
  assumes "surj \<pi>"
  shows "inv_map (Some o \<pi>) = Some o inv \<pi>"
proof-
  have "(if Some y \<in> range (\<lambda>x. Some (\<pi> x))
          then Some (SOME x. Some (\<pi> x) = Some y)
          else None) =
         Some (SOME b. \<pi> b = y)"
    if "surj \<pi>"
    for y
    using that by auto
  hence  "surj \<pi> \<Longrightarrow>
    (\<lambda>y. if Some y \<in> range (\<lambda>x. Some (\<pi> x))
         then Some (SOME x. Some (\<pi> x) = Some y) else None) =
    (\<lambda>x. Some (SOME xa. \<pi> xa = x))"
    by (rule ext)
  thus ?thesis
    unfolding inv_map_def o_def inv_def
    using assms by linarith
qed

lemma inj_map_map_comp[simp]:
  assumes a1: "inj_map f" and a2: "inj_map g"
  shows "inj_map (f \<circ>\<^sub>m g)"
  using a1 a2
  unfolding inj_map_def
  by (metis (mono_tags, lifting) map_comp_def option.case_eq_if option.expand)

lemma inj_map_inv_map[simp]: "inj_map (inv_map \<pi>)"
proof (unfold inj_map_def, rule allI, rule allI, rule impI, erule conjE)
  fix x y
  assume same: "inv_map \<pi> x = inv_map \<pi> y"
    and pix_not_None: "inv_map \<pi> x \<noteq> None"
  have x_pi: "Some x \<in> range \<pi>"
    using pix_not_None unfolding inv_map_def apply auto
    by (meson option.distinct(1))
  have y_pi: "Some y \<in> range \<pi>"
    using pix_not_None unfolding same unfolding inv_map_def apply auto
    by (meson option.distinct(1))
  have "inv_map \<pi> x = Some (Hilbert_Choice.inv \<pi> (Some x))"
    unfolding inv_map_def using x_pi by simp
  moreover have "inv_map \<pi> y = Some (Hilbert_Choice.inv \<pi> (Some y))"
    unfolding inv_map_def using y_pi by simp
  ultimately have "Hilbert_Choice.inv \<pi> (Some x) = Hilbert_Choice.inv \<pi> (Some y)"
    using same by simp
  thus "x = y"
    by (meson inv_into_injective option.inject x_pi y_pi)
qed

lemma abs_summable_bdd_above:
  fixes f :: \<open>'a \<Rightarrow> 'b::real_normed_vector\<close>
  shows \<open>f abs_summable_on A \<longleftrightarrow> bdd_above (sum (\<lambda>x. norm (f x)) ` {F. F\<subseteq>A \<and> finite F})\<close>
proof (rule iffI)
  assume \<open>f abs_summable_on A\<close>
  have \<open>(\<Sum>x\<in>F. norm (f x)) = (\<Sum>\<^sub>\<infinity>x\<in>F. norm (f x))\<close> if \<open>finite F\<close> for F
    by (simp add: that)
  also have \<open>(\<Sum>\<^sub>\<infinity>x\<in>F. norm (f x)) \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))\<close> if \<open>F \<subseteq> A\<close> for F
    by (smt (verit) Diff_subset \<open>f abs_summable_on A\<close> infsum_Diff infsum_nonneg norm_ge_zero summable_on_subset_banach that)
  finally show \<open>bdd_above (sum (\<lambda>x. norm (f x)) ` {F. F \<subseteq> A \<and> finite F})\<close>
    by (auto intro!: bdd_aboveI)
next
  assume \<open>bdd_above (sum (\<lambda>x. norm (f x)) ` {F. F\<subseteq>A \<and> finite F})\<close>
  then show \<open>f abs_summable_on A\<close>
    by (simp add: nonneg_bdd_above_summable_on)
qed

lemma infsum_nonneg:
  fixes f :: "'a \<Rightarrow> 'b::{ordered_comm_monoid_add,linorder_topology}"
  assumes "\<And>x. x \<in> M \<Longrightarrow> 0 \<le> f x"
  shows "infsum f M \<ge> 0" (is "?lhs \<ge> _")
  apply (cases \<open>f summable_on M\<close>)
   apply (rule infsum_nonneg)
  using assms by (auto simp add: infsum_not_exists)

lemma abs_summable_product:
  fixes x :: "'a \<Rightarrow> 'b::{real_normed_div_algebra,banach,second_countable_topology}"
  assumes x2_sum: "(\<lambda>i. (x i) * (x i)) abs_summable_on A"
    and y2_sum: "(\<lambda>i. (y i) * (y i)) abs_summable_on A"
  shows "(\<lambda>i. x i * y i) abs_summable_on A"
proof (rule nonneg_bdd_above_summable_on, simp, rule bdd_aboveI2, rename_tac F)
  fix F assume \<open>F \<in> {F. F \<subseteq> A \<and> finite F}\<close>
  then have r1: "finite F" and b4: "F \<subseteq> A"
    by auto

  have a1: "(\<Sum>\<^sub>\<infinity>i\<in>F. norm (x i * x i)) \<le> (\<Sum>\<^sub>\<infinity>i\<in>A. norm (x i * x i))"
    apply (rule infsum_mono_neutral)
    using b4 r1 x2_sum by auto

  have "norm (x i * y i) \<le> norm (x i * x i) + norm (y i * y i)" for i
    unfolding norm_mult
    by (smt mult_left_mono mult_nonneg_nonneg mult_right_mono norm_ge_zero)
  hence "(\<Sum>i\<in>F. norm (x i * y i)) \<le> (\<Sum>i\<in>F. norm (x i * x i) + norm (y i * y i))"
    by (simp add: sum_mono)
  also have "\<dots> = (\<Sum>i\<in>F. norm (x i * x i)) + (\<Sum>i\<in>F. norm (y i * y i))"
    by (simp add: sum.distrib)
  also have "\<dots> = (\<Sum>\<^sub>\<infinity>i\<in>F. norm (x i * x i)) + (\<Sum>\<^sub>\<infinity>i\<in>F. norm (y i * y i))"
    by (simp add: \<open>finite F\<close>)
  also have "\<dots> \<le> (\<Sum>\<^sub>\<infinity>i\<in>A. norm (x i * x i)) + (\<Sum>\<^sub>\<infinity>i\<in>A. norm (y i * y i))"
    by (smt (verit, del_insts) a1 Diff_iff Infinite_Sum.infsum_nonneg assms(2) b4 infsum_def infsum_mono_neutral norm_ge_zero subset_eq)
  finally show \<open>(\<Sum>xa\<in>F. norm (x xa * y xa)) \<le> (\<Sum>\<^sub>\<infinity>i\<in>A. norm (x i * x i)) + (\<Sum>\<^sub>\<infinity>i\<in>A. norm (y i * y i))\<close>
    by simp
qed

end

subset_name: curated


text:
\usepackage{docmute}

\usepackage{enumerate,multirow}
\usepackage{amsmath}
\usepackage{amsthm,amsfonts,amssymb,mathtools,xspace}
\usepackage{tikz}
\usetikzlibrary{decorations.pathreplacing}
\usetikzlibrary{decorations.markings}
\usetikzlibrary{calc}
\usetikzlibrary{shapes.geometric}
\usepackage{etoolbox}
\usepackage{datetime}

\pretolerance=2000

\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{conjecture}[theorem]{Conjecture}
\theoremstyle{definition}
\newtheorem{defn}[theorem]{Definition}
\newtheorem{examples}[theorem]{Examples}
\newtheorem{example}[theorem]{Example}
\newtheorem{remark}[theorem]{Remark}
\newtheorem*{question}{Question}

\newenvironment{pic}[1][]
{\begin{aligned}\begin{tikzpicture}[#1]}
{\end{tikzpicture}\end{aligned}}
\newcommand{\edges}[1][]
{
}

\makeatletter
\def\calign@preamble{
   &\hfil\strut@
    \setboxz@h{\@lign$\m@th\displaystyle{##}$}
    \ifmeasuring@\savefieldlength@\fi
    \set@field
    \hfil
    \tabskip\alignsep@
}
\let\cmeasure@\measure@
\patchcmd\cmeasure@{\divide\@tempcntb\tw@}{}{}{}
\patchcmd\cmeasure@{\divide\@tempcntb\tw@}{}{}{}
\patchcmd\cmeasure@{\ifodd\maxfields@
  \global\advance\maxfields@\@ne
  \fi}{}{}{}
\newenvironment{calign}
{
  \let\align@preamble\calign@preamble
  \let\measure@\cmeasure@
  \align
}
{
  \endalign
}
\makeatother

\makeatletter
\newcommand{\starsection}[1]{
  \removelastskip
  \vskip 3ex\goodbreak
  \refstepcounter{section}
  \noindent
  \begingroup
  \leavevmode\Large\bfseries\raggedright
  \thesection*\quad
  #1
  \par
  \endgroup
  \vskip 2ex\nobreak
  \addcontentsline{toc}{section}{
    \protect\numberline{\thesection*}
    #1}
}
\makeatother

\setcounter{secnumdepth}{2}

\renewcommand\matrix[1]
{\hspace{-1.5pt}\left( \hspace{-2pt} \raisebox{-0pt}{$\begin{array}{@{\extracolsep{-5.5pt}\,}cccc}#1\end{array}$}  \hspace{0pt} \right)\hspace{-1.5pt}}
\newcommand\fmatrix[1]
{\hspace{-1.5pt}\left( \hspace{-2pt} \raisebox{-0pt}{\footnotesize$\begin{array}{@{\extracolsep{-5.5pt}\,}cccc}#1\end{array}$}  \hspace{0pt} \right)\hspace{-1.5pt}}
\newcommand\tinymatrix[1]
{\left( \hspace{-2pt} \renewcommand\thickspace{\kern2pt} \scriptstyle\begin{smallmatrix} #1 \end{smallmatrix} \hspace{-2pt} \right)}
\newcommand\foplus{\!\oplus\!}

\newcommand\ignore[1]{}
\newcommand\superequals[1]{\ensuremath{\stackrel {\makebox[0pt]{\ensuremath{\scriptstyle #1}}}{=}}}
\newcommand\equalref[1]{\superequals{\eqref{#1}}}
\newcommand\equalreftwo[2]{\ensuremath{\stackrel{\makebox[0pt]{\ensuremath{\stackrel{\scriptstyle\eqref{#1}}{\scriptstyle\eqref{#2}}}}}{=}}}

\def\customsubsection{\subsection*}

\pgfdeclarelayer{foreground}
\pgfdeclarelayer{background}
\pgfsetlayers{main,foreground,background}
\tikzset{smallbox/.style={draw, fill=white, minimum height=0.45cm, minimum width=0.45cm, inner sep=-100pt}}

\makeatletter
\pgfkeys{
  /tikz/on layer/.code={
    \pgfonlayer{#1}\begingroup
    \aftergroup\endpgfonlayer
    \aftergroup\endgroup
  },
  /tikz/node on layer/.code={
    \gdef\node@@on@layer{
      \setbox\tikz@tempbox=\hbox\bgroup\pgfonlayer{#1}\unhbox\tikz@tempbox\endpgfonlayer\egroup}
    \aftergroup\node@on@layer
  },
  /tikz/end node on layer/.code={
    \endpgfonlayer\endgroup\endgroup
  }
}
\def\node@on@layer{\aftergroup\node@@on@layer}
\makeatother\def\thickness{0.7pt}
\tikzstyle{oldmorphism}=[minimum width=30pt, minimum height=16pt, draw, font=\small, inner sep=0pt, fill=white, line width=\thickness]
\tikzstyle{cross}=[preaction={draw=white, -, line width=10pt}]

\tikzstyle{braid}=[double=black, line width=3*\thickness, double distance=\thickness, white]
\tikzstyle{string}=[line width=\thickness]
\tikzstyle{scalar}=[circle, inner sep=0pt, minimum width=15pt, draw, line width=\thickness]
\tikzstyle{dot}=[circle, draw=black, fill=black!25, inner sep=.4ex, line width=\thickness, node on layer=foreground]
\tikzstyle{blackdot}=[circle, draw=black, fill=black!100, inner sep=.4ex, line width=\thickness, node on layer=foreground]
\tikzstyle{graydot}=[circle, draw=black, fill=gray!40!white, inner sep=.4ex, line width=\thickness, node on layer=foreground]
\tikzstyle{whitedot}=[circle, draw=black, fill=white, inner sep=.4ex, line width=\thickness, node on layer=foreground]
\tikzstyle{mixedmorphism}=[morphism, minimum width=30pt, minimum height=16pt, draw, font=\small, inner sep=0pt, fill=white, line width=\thickness,rounded corners=1ex]
\tikzstyle{thick}=[line width=\thickness]
\tikzstyle{tiny}=[font=\tiny]

\tikzset{arrow/.style={decoration={
    markings,
    mark=at position #1 with \arrow{thickarrow}},
    postaction=decorate}
}
\tikzset{reverse arrow/.style={decoration={
    markings,
    mark=at position #1 with \arrow{reversethickarrow}},
    postaction=decorate}
}

\newif\ifblack\pgfkeys{/tikz/black/.is if=black}
\newif\ifwedge\pgfkeys{/tikz/wedge/.is if=wedge}
\newif\ifvflip\pgfkeys{/tikz/vflip/.is if=vflip}
\newif\ifhflip\pgfkeys{/tikz/hflip/.is if=hflip}
\newif\ifhvflip\pgfkeys{/tikz/hvflip/.is if=hvflip}
\newif\ifconnectnw\pgfkeys{/tikz/connect nw/.is if=connectnw}
\newif\ifconnectne\pgfkeys{/tikz/connect ne/.is if=connectne}
\newif\ifconnectsw\pgfkeys{/tikz/connect sw/.is if=connectsw}
\newif\ifconnectse\pgfkeys{/tikz/connect se/.is if=connectse}
\newif\ifconnectn\pgfkeys{/tikz/connect n/.is if=connectn}
\newif\ifconnects\pgfkeys{/tikz/connect s/.is if=connects}
\newif\ifconnectnwf\pgfkeys{/tikz/connect nw >/.is if=connectnwf}
\newif\ifconnectnef\pgfkeys{/tikz/connect ne >/.is if=connectnef}
\newif\ifconnectswf\pgfkeys{/tikz/connect sw >/.is if=connectswf}
\newif\ifconnectsef\pgfkeys{/tikz/connect se >/.is if=connectsef}
\newif\ifconnectnf\pgfkeys{/tikz/connect n >/.is if=connectnf}
\newif\ifconnectsf\pgfkeys{/tikz/connect s >/.is if=connectsf}
\newif\ifconnectnwr\pgfkeys{/tikz/connect nw </.is if=connectnwr}
\newif\ifconnectner\pgfkeys{/tikz/connect ne </.is if=connectner}
\newif\ifconnectswr\pgfkeys{/tikz/connect sw </.is if=connectswr}
\newif\ifconnectser\pgfkeys{/tikz/connect se </.is if=connectser}
\newif\ifconnectnr\pgfkeys{/tikz/connect n </.is if=connectnr}
\newif\ifconnectsr\pgfkeys{/tikz/connect s </.is if=connectsr}
\tikzset{keylengthnw/.initial=\connectheight}
\tikzset{keylengthn/.initial =\connectheight}
\tikzset{keylengthne/.initial=\connectheight}
\tikzset{keylengthsw/.initial=\connectheight}
\tikzset{keylengths/.initial =\connectheight}
\tikzset{keylengthse/.initial=\connectheight}
\tikzset{connect nw length/.style={connect nw=true, keylengthnw={#1}}}
\tikzset{connect n length/.style ={connect n =true, keylengthn ={#1}}}
\tikzset{connect ne length/.style={connect ne=true, keylengthne={#1}}}
\tikzset{connect sw length/.style={connect sw=true, keylengthsw={#1}}}
\tikzset{connect s length/.style ={connect s =true, keylengths ={#1}}}
\tikzset{connect se length/.style={connect se=true, keylengthse={#1}}}
\tikzset{connect nw < length/.style={connect nw <=true, keylengthnw={#1}}}
\tikzset{connect n < length/.style ={connect n <=true,  keylengthn ={#1}}}
\tikzset{connect ne < length/.style={connect ne <=true, keylengthne={#1}}}
\tikzset{connect sw < length/.style={connect sw <=true, keylengthnw={#1}}}
\tikzset{connect s < length/.style ={connect s <=true,  keylengths ={#1}}}
\tikzset{connect se < length/.style={connect se <=true, keylengthse={#1}}}
\tikzset{connect nw > length/.style={connect nw >=true, keylengthnw={#1}}}
\tikzset{connect n > length/.style ={connect n >=true,  keylengthn ={#1}}}
\tikzset{connect ne > length/.style={connect ne >=true, keylengthne={#1}}}
\tikzset{connect sw > length/.style={connect sw >=true, keylengthsw={#1}}}
\tikzset{connect s > length/.style ={connect s >=true,  keylengths ={#1}}}
\tikzset{connect se > length/.style={connect se >=true, keylengthse={#1}}}

\newlength\morphismheight
\setlength\morphismheight{0.5cm}
\newlength\minimummorphismwidth
\setlength\minimummorphismwidth{0.1cm}
\newlength\stateheight
\setlength\stateheight{0.4cm}
\newlength\minimumstatewidth
\setlength\minimumstatewidth{0.89cm}
\newlength\connectheight
\setlength\connectheight{0.5cm}
\tikzset{width/.initial=\minimummorphismwidth}

\makeatletter
\pgfarrowsdeclare{thickarrow}{thickarrow}
{
  \pgfutil@tempdima=-0.84pt
  \advance\pgfutil@tempdima by-1.3\pgflinewidth
  \pgfutil@tempdimb=-1.7pt
  \advance\pgfutil@tempdimb by.625\pgflinewidth
  \pgfarrowsleftextend{+\pgfutil@tempdima}
  \pgfarrowsrightextend{+\pgfutil@tempdimb}
}
{
  \pgfmathparse{\pgfgetarrowoptions{thickarrow}}
  \pgfsetlinewidth{1.25 pt}
  \pgfutil@tempdima=0.28pt
  \advance\pgfutil@tempdima by.3\pgflinewidth
  \pgfsetlinewidth{0.8\pgflinewidth}
  \pgfsetdash{}{+0pt}
  \pgfsetroundcap
  \pgfsetroundjoin
  \pgfpathmoveto{\pgfqpoint{-3\pgfutil@tempdima}{4\pgfutil@tempdima}}
  \pgfpathcurveto
  {\pgfqpoint{-2.75\pgfutil@tempdima}{2.5\pgfutil@tempdima}}
  {\pgfqpoint{0pt}{0.25\pgfutil@tempdima}}
  {\pgfqpoint{0.75\pgfutil@tempdima}{0pt}}
  \pgfpathcurveto
  {\pgfqpoint{0pt}{-0.25\pgfutil@tempdima}}
  {\pgfqpoint{-2.75\pgfutil@tempdima}{-2.5\pgfutil@tempdima}}
  {\pgfqpoint{-3\pgfutil@tempdima}{-4\pgfutil@tempdima}}
  \pgfusepathqstroke
}
\pgfarrowsdeclare{reversethickarrow}{reversethickarrow}
{
  \pgfutil@tempdima=-0.84pt
  \advance\pgfutil@tempdima by-1.3\pgflinewidth
  \pgfutil@tempdimb=0.2pt
  \advance\pgfutil@tempdimb by.625\pgflinewidth
  \pgfarrowsleftextend{+\pgfutil@tempdima}
  \pgfarrowsrightextend{+\pgfutil@tempdimb}
}
{
  \pgftransformxscale{-1}
  \pgfmathparse{\pgfgetarrowoptions{thickarrow}}
  \ifpgfmathunitsdeclared
    \pgfmathparse{\pgfmathresult pt}
  \else
    \pgfmathparse{\pgfmathresult*\pgflinewidth}
  \fi
  \let\thickness=\pgfmathresult
  \pgfsetlinewidth{1.25 pt}
  \pgfutil@tempdima=0.28pt
  \advance\pgfutil@tempdima by.3\pgflinewidth
  \pgfsetlinewidth{0.8\pgflinewidth}
  \pgfsetdash{}{+0pt}
  \pgfsetroundcap
  \pgfsetroundjoin
  \pgfpathmoveto{\pgfqpoint{-3\pgfutil@tempdima}{4\pgfutil@tempdima}}
  \pgfpathcurveto
  {\pgfqpoint{-2.75\pgfutil@tempdima}{2.5\pgfutil@tempdima}}
  {\pgfqpoint{0pt}{0.25\pgfutil@tempdima}}
  {\pgfqpoint{0.75\pgfutil@tempdima}{0pt}}
  \pgfpathcurveto
  {\pgfqpoint{0pt}{-0.25\pgfutil@tempdima}}
  {\pgfqpoint{-2.75\pgfutil@tempdima}{-2.5\pgfutil@tempdima}}
  {\pgfqpoint{-3\pgfutil@tempdima}{-4\pgfutil@tempdima}}
  \pgfusepathqstroke
}
\makeatother

\makeatletter
\pgfdeclareshape{ground}
{
    \savedanchor\centerpoint
    {
        \pgf@x=0pt
        \pgf@y=0pt
    }
    \anchor{center}{\centerpoint}
    \anchorborder{\centerpoint}

    \anchor{north}
    {
        \pgf@x=0pt
        \pgf@y=0.5*0.33*\stateheight
    }
    \anchor{south}
    {
        \pgf@x=0pt
        \pgf@y=0pt
    }
    \saveddimen\overallwidth
    {
        \pgfkeysgetvalue{/pgf/minimum width}{\minwidth}
        \pgf@x=\minimumstatewidth
        \ifdim\pgf@x<\minwidth
            \pgf@x=\minwidth
        \fi
    }
    \backgroundpath
    {
        \begin{pgfonlayer}{foreground}
        \pgfsetstrokecolor{black}
        \pgfsetlinewidth{1.25pt}
        \ifhflip
            \pgftransformyscale{-1}
        \fi
        \pgftransformscale{0.5}
        \pgfpathmoveto{\pgfpoint{-0.5*\overallwidth}{0}}
        \pgfpathlineto{\pgfpoint{0.5*\overallwidth}{0}}
        \pgfpathmoveto{\pgfpoint{-0.33*\overallwidth}{0.33*\stateheight}}
        \pgfpathlineto{\pgfpoint{0.33*\overallwidth}{0.33*\stateheight}}
        \pgfpathmoveto{\pgfpoint{-0.16*\overallwidth}{0.66*\stateheight}}
        \pgfpathlineto{\pgfpoint{0.16*\overallwidth}{0.66*\stateheight}}
        \pgfpathmoveto{\pgfpoint{-0.02*\overallwidth}{\stateheight}}
        \pgfpathlineto{\pgfpoint{0.02*\overallwidth}{\stateheight}}
        \pgfusepath{stroke}
        \end{pgfonlayer}
    }
}
\tikzset{forward arrow style/.style={every to/.style, decoration={
    markings,
    mark=at position 0.5 with \arrow{thickarrow}},
    postaction=decorate}}
\tikzset{reverse arrow style/.style={every to/.style, decoration={
    markings,
    mark=at position 0.5 with \arrow{reversethickarrow}},
    postaction=decorate}}
\pgfdeclareshape{morphism}
{
    \savedanchor\centerpoint
    {
        \pgf@x=0pt
        \pgf@y=0pt
    }
    \anchor{center}{\centerpoint}
    \anchorborder{\centerpoint}
    \saveddimen\savedlengthnw
    {
        \pgfkeysgetvalue{/tikz/keylengthnw}{\len}
        \pgf@x=\len
    }
    \saveddimen\savedlengthn
    {
        \pgfkeysgetvalue{/tikz/keylengthn}{\len}
        \pgf@x=\len
    }
    \saveddimen\savedlengthne
    {
        \pgfkeysgetvalue{/tikz/keylengthne}{\len}
        \pgf@x=\len
    }
    \saveddimen\savedlengthsw
    {
        \pgfkeysgetvalue{/tikz/keylengthsw}{\len}
        \pgf@x=\len
    }
    \saveddimen\savedlengths
    {
        \pgfkeysgetvalue{/tikz/keylengths}{\len}
        \pgf@x=\len
    }
    \saveddimen\savedlengthse
    {
        \pgfkeysgetvalue{/tikz/keylengthse}{\len}
        \pgf@x=\len
    }
    \saveddimen\overallwidth
    {
        \pgfkeysgetvalue{/tikz/width}{\minwidth}
        \pgf@x=\wd\pgfnodeparttextbox
        \ifdim\pgf@x<\minwidth
            \pgf@x=\minwidth
        \fi
    }
    \savedanchor{\upperrightcorner}
    {
        \pgf@y=.5\ht\pgfnodeparttextbox
        \advance\pgf@y by -.5\dp\pgfnodeparttextbox
        \pgf@x=.5\wd\pgfnodeparttextbox
    }
    \anchor{north}
    {
        \pgf@x=0pt
        \pgf@y=0.5\morphismheight
    }
    \anchor{north east}
    {
        \pgf@x=\overallwidth
        \multiply \pgf@x by 2
        \divide \pgf@x by 5
        \pgf@y=0.5\morphismheight
    }
    \anchor{east}
    {
        \pgf@x=\overallwidth
        \divide \pgf@x by 2
        \advance \pgf@x by 5pt
        \pgf@y=0pt
    }
    \anchor{west}
    {
        \pgf@x=-\overallwidth
        \divide \pgf@x by 2
        \advance \pgf@x by -5pt
        \pgf@y=0pt
    }
    \anchor{north west}
    {
        \pgf@x=-\overallwidth
        \multiply \pgf@x by 2
        \divide \pgf@x by 5
        \pgf@y=0.5\morphismheight
    }
    \anchor{connect nw}
    {
        \pgf@x=-\overallwidth
        \multiply \pgf@x by 2
        \divide \pgf@x by 5
        \pgf@y=0.5\morphismheight
        \advance\pgf@y by \savedlengthnw
    }
    \anchor{connect ne}
    {
        \pgf@x=\overallwidth
        \multiply \pgf@x by 2
        \divide \pgf@x by 5
        \pgf@y=0.5\morphismheight
        \advance\pgf@y by \savedlengthne
    }
    \anchor{connect sw}
    {
        \pgf@x=-\overallwidth
        \multiply \pgf@x by 2
        \divide \pgf@x by 5
        \pgf@y=-0.5\morphismheight
        \advance\pgf@y by -\savedlengthsw
    }
    \anchor{connect se}
    {
        \pgf@x=\overallwidth
        \multiply \pgf@x by 2
        \divide \pgf@x by 5
        \pgf@y=-0.5\morphismheight
        \advance\pgf@y by -\savedlengthse
    }
    \anchor{connect n}
    {
        \pgf@x=0pt
        \pgf@y=0.5\morphismheight
        \advance\pgf@y by \savedlengthn
    }
    \anchor{connect s}
    {
        \pgf@x=0pt
        \pgf@y=-0.5\morphismheight
        \advance\pgf@y by -\savedlengths
    }
    \anchor{south east}
    {
        \pgf@x=\overallwidth
        \multiply \pgf@x by 2
        \divide \pgf@x by 5
        \pgf@y=-0.5\morphismheight
    }
    \anchor{south west}
    {
        \pgf@x=-\overallwidth
        \multiply \pgf@x by 2
        \divide \pgf@x by 5
        \pgf@y=-0.5\morphismheight
    }
    \anchor{south}
    {
        \pgf@x=0pt
        \pgf@y=-0.5\morphismheight
    }
    \anchor{text}
    {
        \upperrightcorner
        \pgf@x=-\pgf@x
        \pgf@y=-\pgf@y
    }
    \backgroundpath
    {
        \pgfsetstrokecolor{black}
        \pgfsetlinewidth{\thickness}
        \begin{scope}
                \ifhflip
                    \pgftransformyscale{-1}
                \fi
                \ifvflip
                    \pgftransformxscale{-1}
                \fi
                \ifhvflip
                    \pgftransformxscale{-1}
                    \pgftransformyscale{-1}
                \fi
                \pgfpathmoveto{\pgfpoint
                    {-0.5*\overallwidth-5pt}
                    {0.5*\morphismheight}}
                \pgfpathlineto{\pgfpoint
                    {0.5*\overallwidth+5pt}
                    {0.5*\morphismheight}}
                \ifwedge
                    \pgfpathlineto{\pgfpoint
                        {0.5*\overallwidth + 15pt}
                        {-0.5*\morphismheight}}
                \else
                    \pgfpathlineto{\pgfpoint
                        {0.5*\overallwidth + 5pt}
                        {-0.5*\morphismheight}}
                \fi
                \pgfpathlineto{\pgfpoint
                    {-0.5*\overallwidth-5pt}
                    {-0.5*\morphismheight}}
                \pgfpathclose
                \pgfusepath{stroke}
        \end{scope}
        \ifconnectnw
            \pgfpathmoveto{\pgfpoint
                {-0.4*\overallwidth}
                {0.5*\morphismheight}}
            \pgfpathlineto{\pgfpoint
                {-0.4*\overallwidth}
                {0.5*\morphismheight+\savedlengthnw}}
            \pgfusepath{stroke}
        \fi
        \ifconnectne
            \pgfpathmoveto{\pgfpoint
                {0.4*\overallwidth}
                {0.5*\morphismheight}}
            \pgfpathlineto{\pgfpoint
                {0.4*\overallwidth}
                {0.5*\morphismheight+\savedlengthne}}
            \pgfusepath{stroke}
        \fi
        \ifconnectsw
            \pgfpathmoveto{\pgfpoint
                {-0.4*\overallwidth}
                {-0.5*\morphismheight}}
            \pgfpathlineto{\pgfpoint
                {-0.4*\overallwidth}
                {-0.5*\morphismheight-\savedlengthsw}}
            \pgfusepath{stroke}
        \fi
        \ifconnectse
            \pgfpathmoveto{\pgfpoint
                {0.4*\overallwidth}
                {-0.5*\morphismheight}}
            \pgfpathlineto{\pgfpoint
                {0.4*\overallwidth}
                {-0.5*\morphismheight-\savedlengthse}}
            \pgfusepath{stroke}
        \fi
        \ifconnectn
            \pgfpathmoveto{\pgfpoint
                {0pt}
                {0.5*\morphismheight}}
            \pgfpathlineto{\pgfpoint
                {0pt}
                {0.5*\morphismheight+\savedlengthn}}
            \pgfusepath{stroke}
        \fi
        \ifconnects
            \pgfpathmoveto{\pgfpoint
                {0pt}
                {-0.5*\morphismheight}}
            \pgfpathlineto{\pgfpoint
                {0pt}
                {-0.5*\morphismheight-\savedlengths}}
            \pgfusepath{stroke}
        \fi
        \ifconnectnwf
            \draw [forward arrow style] (-0.4*\overallwidth,0.5*\morphismheight)
                to (-0.4*\overallwidth,0.5*\morphismheight+\savedlengthnw);
        \fi
        \ifconnectnef
            \draw [forward arrow style] (0.4*\overallwidth,0.5*\morphismheight)
                to (0.4*\overallwidth,0.5*\morphismheight+\savedlengthne);
        \fi
        \ifconnectswf
            \draw [forward arrow style] (-0.4*\overallwidth,-0.5*\morphismheight-\savedlengthsw)
                to (-0.4*\overallwidth,-0.5*\morphismheight);
        \fi
        \ifconnectsef
            \draw [forward arrow style] (0.4*\overallwidth,-0.5*\morphismheight-\savedlengthse)
                to (0.4*\overallwidth,-0.5*\morphismheight);
        \fi
        \ifconnectnf
            \draw [forward arrow style] (0,0.5*\morphismheight)
                to (0,0.5*\morphismheight+\savedlengthn);
        \fi
        \ifconnectsf
            \draw [forward arrow style] (0,-0.5*\morphismheight-\savedlengths)
                to (0,-0.5*\morphismheight);
        \fi
        \ifconnectnwr
            \draw [reverse arrow style] (-0.4*\overallwidth,0.5*\morphismheight)
                to (-0.4*\overallwidth,0.5*\morphismheight+\savedlengthnw);
        \fi
        \ifconnectner
            \draw [reverse arrow style] (0.4*\overallwidth,0.5*\morphismheight)
                to (0.4*\overallwidth,0.5*\morphismheight+\savedlengthne);
        \fi
        \ifconnectswr
            \draw [reverse arrow style] (-0.4*\overallwidth,-0.5*\morphismheight-\savedlengthsw)
                to (-0.4*\overallwidth,-0.5*\morphismheight);
        \fi
        \ifconnectser
            \draw [reverse arrow style] (0.4*\overallwidth,-0.5*\morphismheight-\savedlengthse)
                to (0.4*\overallwidth,-0.5*\morphismheight);
        \fi
        \ifconnectnr
            \draw [reverse arrow style] (0,0.5*\morphismheight)
                to (0,0.5*\morphismheight+\savedlengthn);
        \fi
        \ifconnectsr
            \draw [reverse arrow style] (0,-0.5*\morphismheight-\savedlengths)
                to (0,-0.5*\morphismheight);
        \fi
    }
}
\pgfdeclareshape{swish right}
{
    \savedanchor\centerpoint
    {
        \pgf@x=0pt
        \pgf@y=0pt
    }
    \anchor{center}{\centerpoint}
    \anchorborder{\centerpoint}
    \anchor{north}
    {
        \pgf@x=\minimummorphismwidth
        \divide\pgf@x by 5
        \pgf@y=\morphismheight
        \divide\pgf@y by 2
        \advance\pgf@y by \connectheight
    }
    \anchor{south}
    {
        \pgf@x=-\minimummorphismwidth
        \divide\pgf@x by 5
        \pgf@y=-\morphismheight
        \divide\pgf@y by 2
        \advance\pgf@y by -\connectheight
    }
    \backgroundpath
    {
        \pgfsetstrokecolor{black}
        \pgfsetlinewidth{\thickness}
        \pgfpathmoveto{\pgfpoint
            {-0.2*\minimummorphismwidth}
            {-0.5*\morphismheight-\connectheight}}
        \pgfpathcurveto
            {\pgfpoint{-0.2*\minimummorphismwidth}{0pt}}
            {\pgfpoint{0.2*\minimummorphismwidth}{0pt}}
            {\pgfpoint
                {0.2*\minimummorphismwidth}
                {0.5*\morphismheight+\connectheight}}
        \pgfusepath{stroke}
    }
}
\pgfdeclareshape{swish left}
{
    \savedanchor\centerpoint
    {
        \pgf@x=0pt
        \pgf@y=0pt
    }
    \anchor{center}{\centerpoint}
    \anchorborder{\centerpoint}
    \anchor{north}
    {
        \pgf@x=-\minimummorphismwidth
        \divide\pgf@x by 5
        \pgf@y=\morphismheight
        \divide\pgf@y by 2
        \advance\pgf@y by \connectheight
    }
    \anchor{south}
    {
        \pgf@x=\minimummorphismwidth
        \divide\pgf@x by 5
        \pgf@y=-\morphismheight
        \divide\pgf@y by 2
        \advance\pgf@y by -\connectheight
    }
    \backgroundpath
    {
        \pgfsetstrokecolor{black}
        \pgfsetlinewidth{\thickness}
        \pgfpathmoveto{\pgfpoint
            {0.2*\minimummorphismwidth}
            {-0.5*\morphismheight-\connectheight}}
        \pgfpathcurveto
            {\pgfpoint{0.2*\minimummorphismwidth}{0pt}}
            {\pgfpoint{-0.2*\minimummorphismwidth}{0pt}}
            {\pgfpoint
                {-0.2*\minimummorphismwidth}
                {0.5*\morphismheight+\connectheight}}
        \pgfusepath{stroke}
    }
}
\pgfdeclareshape{state}
{
    \savedanchor\centerpoint
    {
        \pgf@x=0pt
        \pgf@y=0pt
    }
    \anchor{center}{\centerpoint}
    \anchorborder{\centerpoint}
    \saveddimen\overallwidth
    {
        \pgf@x=3\wd\pgfnodeparttextbox
        \ifdim\pgf@x<\minimumstatewidth
            \pgf@x=\minimumstatewidth
        \fi
    }
    \savedanchor{\upperrightcorner}
    {
        \pgf@x=.5\wd\pgfnodeparttextbox
        \pgf@y=.5\ht\pgfnodeparttextbox
        \advance\pgf@y by -.5\dp\pgfnodeparttextbox
    }
    \anchor{A}
    {
        \pgf@x=-\overallwidth
        \divide\pgf@x by 4
        \pgf@y=0pt
    }
    \anchor{B}
    {
        \pgf@x=\overallwidth
        \divide\pgf@x by 4
        \pgf@y=0pt
    }
    \anchor{text}
    {
        \upperrightcorner
        \pgf@x=-\pgf@x
        \ifhflip
            \pgf@y=-\pgf@y
            \advance\pgf@y by 0.4\stateheight
        \else
            \pgf@y=-\pgf@y
            \advance\pgf@y by -0.4\stateheight
        \fi
    }
    \backgroundpath
    {

        \pgfsetstrokecolor{black}
        \pgfsetlinewidth{\thickness}
        \pgfpathmoveto{\pgfpoint{-0.5*\overallwidth}{0}}
        \pgfpathlineto{\pgfpoint{0.5*\overallwidth}{0}}
        \ifhflip
            \pgfpathlineto{\pgfpoint{0}{\stateheight}}
        \else
            \pgfpathlineto{\pgfpoint{0}{-\stateheight}}
        \fi
        \pgfpathclose
        \ifblack
            \pgfsetfillcolor{black!50}
            \pgfusepath{fill,stroke}
        \else
            \pgfusepath{stroke}
        \fi

    }
}
\makeatother

\newcommand{\tinycomult}[1][dot]{
\smash{\raisebox{-1.8pt}{\hspace{-5pt}\ensuremath{\begin{pic}[scale=0.34,string]
    \node (0) at (0,0) {};
    \node[#1, inner sep=1.5pt] (1) at (0,0.55) {};
    \node (2) at (-0.5,1) {};
    \node (3) at (0.5,1) {};
    \draw (0.center) to (1.center);
    \draw (1.center) to [out=left, in=down, out looseness=1.5] (2.center);
    \draw (1.center) to [out=right, in=down, out looseness=1.5] (3.center);
\end{pic}
}\hspace{-3pt}}}}
\newcommand{\tinycounit}[1][dot]{
\smash{\raisebox{-1.8pt}{\ensuremath{\hspace{-3pt}\begin{pic}[scale=0.34,string]
        \node (0) at (0,0) {};
        \node (1) at (0,1) {};
        \node[#1, inner sep=1.5pt] (d) at (0,0.55) {};
        \draw (0.center) to (d.center);
    \end{pic}
    \hspace{-1pt}}}}}
\newcommand{\tinymult}[1][dot]{
\smash{{\hspace{-5pt}\ensuremath{\begin{aligned}\begin{tikzpicture}[scale=0.36,thick,yscale=-1]
    \node (0) at (0,0) {};
    \node (2) at (-0.5,1) {};
    \node (3) at (0.5,1) {};
    \draw (0.center) to (0,0.55);
    \draw (0,0.55) to [out=left, in=down, out looseness=1.5] (2.center);
    \draw (0,0.55) to [out=right, in=down, out looseness=1.5] (3.center);
    \node[#1, inner sep=1.5pt] (1) at (0,0.55) {};
\end{tikzpicture}\end{aligned}
}\hspace{-3pt}}}}
\newcommand{\tinyunit}[1][dot]{
\smash{{\ensuremath{\hspace{-3pt}\begin{aligned}\begin{tikzpicture}[scale=0.4,thick,yscale=-1]
        \node (0) at (0,0) {};
        \node (1) at (0,1) {};
        \draw (0.center) to (0,0.55);
        \node[#1, inner sep=1.5pt] (d) at (0,0.55) {};
    \end{tikzpicture}\end{aligned}
    \hspace{-1pt}}}}}
\newcommand{\tinyid}{\raisebox{-2pt}{\ensuremath{\hspace{-4pt}\begin{pic}[scale=0.4,string]
        \node (0) at (0,0) {};
        \node (1) at (0,1) {};
        \draw[string] (0.center) to (1.center);
     \end{pic}
     \hspace{-2pt}}}}
\newcommand{\tinyhandle}[1][dot]{\raisebox{-2pt}{\ensuremath{\hspace{-3pt}\begin{pic}[scale=0.4,string]
        \node (0) at (0,0) {};
        \node[dot, inner sep=1.0pt] (1) at (0,0.3) {};
        \node[dot, inner sep=1.0pt] (2) at (0,0.7) {};
        \node (3) at (0,1) {};
        \draw (0.center) to (1.center);
        \draw (2.center) to (3.center);
        \draw[in=180, out=180, looseness=2] (1.center) to (2.center);
        \draw[in=0, out=0, looseness=2] (1.center) to (2.center);
\end{pic}\hspace{-1pt}}}}

\newcommand{\name}[1]{\ensuremath{\ulcorner #1 \urcorner}}
\newcommand{\coname}[1]{\ensuremath{\llcorner #1 \lrcorner}}
\newcommand{\op}{\ensuremath{\mathrm{op}}}
\newcommand{\tuple}[2]{\ensuremath{\left(\begin{smallmatrix} #1\\#2 \end{smallmatrix}\right)}}
\DeclareMathOperator{\Tr}{Tr}
\DeclareMathOperator{\dom}{dom}
\DeclareMathOperator{\cod}{cod}
\newcommand\cat[1]{\ensuremath{\mathbf{#1}}}
\renewcommand\dag{\ensuremath{\dagger}}
\newcommand\lecture[2]{\section{#1}}
\newcommand\id[1][]{\ensuremath{\mathrm{id}_{#1}}}
\def\totimes{{\textstyle \bigotimes}}
\newcommand\sxleftarrow[1]{\xleftarrow{\smash{#1}}}
\newcommand\sxrightarrow[1]{\xrightarrow{\smash{#1}}}
\newcommand\xto[1]{\xrightarrow{#1}}
\newcommand\sxto[1]{\sxrightarrow{#1}}
\renewcommand{\-}[0]{\nobreakdash-\hspace{0pt}}
\DeclareMathOperator{\Ob}{Ob}
\newcommand\ket[1]{\ensuremath{| #1 \rangle}}
\newcommand\bra[1]{\ensuremath{\langle #1 |}}
\newcommand\C{\ensuremath{\mathbb{C}}}
\newcommand{\inprod}[2]{\ensuremath{\langle #1\hspace{0.5pt}|\hspace{0.5pt}#2 \rangle}}
\newcommand{\defined}{\ensuremath{\mathop{\downarrow}}}
\newcommand\Hom{\ensuremath{\textrm{Hom}}}
\newcommand\pdag{{\phantom{\dagger}}}
\DeclareMathOperator{\CP}{CPM}
\DeclareMathOperator{\CPstar}{CP^*}
\newcommand{\proj}{\ensuremath{p}}
\newcommand{\inj}{\ensuremath{i}}
\DeclareMathOperator{\Prob}{Prob}
\newcommand{\ie}{\textit{i.e.}\xspace}
\newcommand{\eg}{\textit{e.g.}\xspace}
\newcommand\ud{\ensuremath{\mathrm{d}}}
\usepackage{color}
\newcommand{\todo}[1]{{\color{red}#1}}

\def\swangle{-145}
\def\seangle{-35}
\def\nwangle{145}
\def\neangle{35}

\def\newyscale{0.8}
\def\newxscale{0.75}

\ignore{
\usepackage{mathtools}
\tikzstyle{dot}=[inner sep=0.7mm,minimum width=0pt,minimum
height=0pt,fill=black,draw=black,shape=circle]
\tikzstyle{black dot}=[dot,fill=black]
\tikzstyle{white dot}=[dot,fill=white]
\tikzstyle{gray dot}=[dot,fill=gray!40!white]
}

config: arxiv


TITLE: Can the total sum of geometric multiplicities be less than n for an nxn matrix?
QUESTION [1 upvotes]: Can the total sum of geometric multiplicities be less than $n$ for an $n \times n$ matrix?
I understand that the algebraic multiplicity bounds the geometric multiplicity, which leads me to think that the sum of the geometric multiplicity cannot be greater than $n$ as there are $n$ eigenvalues but I am unsure if the geometric multiplicity can be less than $n$.

REPLY [1 votes]: Try
$$
\begin{bmatrix}0&1\\0&0\end{bmatrix}.
$$


TITLE: which variable within a simple interest formula influences the greatest amount of interest?
QUESTION [0 upvotes]: this is interesting to me as i am an investor working out which variable, (the principal sum, the terms of months, and the interest rate) is the deciding factor on how to get the most interest from an investment. Any answers or suggestions would be awesome with some explanation please. :)

REPLY [0 votes]: The answer is that it depends on your options. If you have a range of options, you can find which one is optimal, or for a particular interest rate, number of months, and principal investment you can compare a (25)% increase in one of the variables to a (25)% increase in another variable
Let's look at an example.
The total amount of money in the account after $t$ units of time with principal investment $P$ and interest rate $r$ compounded $n$ times per year is:
$A = P(1 + r/n)^{nt}$
Example: $P=40,000$,  $r = .04= 4\%$, monthly compounding $n=12$ over $t=4$ years. A \$40,000 dollar investment is made for 4 years with annual interest rate of 4%. Interest is compounded monthly.
\$46,927.95 is the balance after 4 years. Thus \$6,927.95 interest was earned.
If we change only the interest rate to 5%, the interest gained after 4 years is \$8,835.81.
If we change only the number of years to 5,  the interest gained after 5 years is \$8,839.86.
If we change only the Principal to \$50,000, the interest gained after 4 years is \$8,659.93.
For the particular values I chose, a 25% increase in duration had a similar (.04% difference in interest gained) impact to a 25% increase in interest rate. Both of these had a stronger impact (about 2% difference in interest gained) than changing the principal investment by 25%.


TITLE: How many $m$ such that : $\sum\limits_{k=1}^m \left\lfloor\frac{m}{k}\right\rfloor$ be even?
QUESTION [5 upvotes]: Find how many $m \le 1000$ such that :
$$\sum\limits_{k=1}^m \left\lfloor \frac{m}{k}\right\rfloor$$
be even ( $\lfloor x\rfloor$ is the largest integer smaller than $x$.)
I think that one case is  $\sum\limits_{k=1}^m \left\lfloor \frac{m}{k}\right\rfloor$ is even if for every integer  $k$ ( $ 1 \le k \le m $) $\left\lfloor\frac{m}{k}\right\rfloor$ be even or the number of odd number be even  in $\sum\limits_{k=1}^m \left\lfloor\frac{m}{k}\right\rfloor$. $\big($ $
\sum\limits_{i=1}^n\left\lfloor\frac{n}{i}\right\rfloor=\sum\limits_{i=1}^n d(i)
$
where $d(\ )$ is the divisor function $\big)$

REPLY [2 votes]: Hint, further to the comments
$$\sum\limits_{k=1}^{m} \left \lfloor \frac{m}{k} \right \rfloor=\sum\limits_{k=1}^{m}d(k) \tag{1}$$

$m=1 \Rightarrow \sum\limits_{k=1}^{1} \left \lfloor \frac{1}{k} \right \rfloor=\sum\limits_{k=1}^{1}d(k)=\color{blue}{1}$, i.e. $\color{red}{\{1\}}$ is the only perfect square or $\color{blue}{\left \lfloor \sqrt{1} \right \rfloor=1}$ in total.
$m=2 \Rightarrow \sum\limits_{k=1}^{2} \left \lfloor \frac{2}{k} \right \rfloor=\sum\limits_{k=1}^{2}d(k)=1+2=\color{blue}{3}$, i.e. $\color{red}{\{1\}}$ is the only perfect square or $\color{blue}{\left \lfloor \sqrt{2} \right \rfloor=1}$ in total.
$m=3 \Rightarrow \sum\limits_{k=1}^{3} \left \lfloor \frac{3}{k} \right \rfloor=\sum\limits_{k=1}^{3}d(k)=1+2+2=\color{blue}{5}$, i.e. $\color{red}{\{1\}}$ is the only perfect square or $\color{blue}{\left \lfloor \sqrt{3} \right \rfloor=1}$ in total.
$m=4 \Rightarrow \sum\limits_{k=1}^{4} \left \lfloor \frac{4}{k} \right \rfloor=\sum\limits_{k=1}^{4}d(k)=1+2+2+3=\color{blue}{8}$, i.e. $\color{red}{\{1, 4\}}$ are the only perfect squares or $\color{blue}{\left \lfloor \sqrt{4} \right \rfloor=2}$ in total.
$m=5 \Rightarrow \sum\limits_{k=1}^{5} \left \lfloor \frac{5}{k} \right \rfloor=\sum\limits_{k=1}^{5}d(k)=1+2+2+3+2=\color{blue}{10}$, i.e. $\color{red}{\{1, 4\}}$ are the only perfect squares or $\color{blue}{\left \lfloor \sqrt{5} \right \rfloor=2}$ in total.

Is the pattern visible now? It should be easy to show it by induction.


TITLE: Complex integration along a curve
QUESTION [0 upvotes]: I have to calculate this integral:
$$
\int_C e^z\,dz
$$
where $C$ is the circle $|z - jπ/2| = π/2$ from the point $z = 0$ to the point $z = jπ$.
I know how to calculate these with circles which central point is at $(0,0)$ but I don't know how it works with this.. So I will be very glad if I got any tips or help.
Thanks!

REPLY [0 votes]: Use the complex version of the fundamental theorem of calculus: $F(z) = e^z$ is an anti-derivative of your $f$, so
$$
\int_C e^z\,dz = F(i\pi) - F(0) = -2.
$$


TITLE: If rank$(AB)=0$, then rank$(B)\leq $nullity$(A)$.
QUESTION [1 upvotes]: Intuitively, this is true. But I'm unsure how to prove it. I know that rank$(AB)=0\Rightarrow AB=0$, but how do I use this to show that the rank of $B$ is at most the nullity of $A$?

REPLY [6 votes]: Interpreting the matrices as linear maps, the rank of $B$ is the dimension of the image of $B$, and the nullity of $A$ is the dimension of the kernel of $A$. If $\operatorname{Im}B\subseteq \ker A$ (which is to say, the composition of the two maps is the zero map), then we must have the inequality you're asking for.


TITLE: Is it true that if $H_1$ and $H_2$ are isomorphic cyclic subgroups of $G$, then $G/H_1\cong G/H_2$?
QUESTION [1 upvotes]: I have a question: it is true that if $H_1$ and $H_2$ are cyclic groups that are isomorphic, then $G/H_1$ is isomorphic to $G/H_2$? I know that if I remove the condition "cyclic groups", the given statement is false and there are numerous counterexamples that disprove it, but I don't know if my statement is true and I don't how to create a counterexample or to prove it. If it is true, can you give me a hint about how this can be proven?
For example, I just have shown that $Z_{12}/ \langle 2 \rangle$ is isomorphic to $Z_{12}/Z_6$ which is isomorphic to $Z_3$ (since both $\langle 2 \rangle$ and $Z_6$ are isomorphic). How this can be generalized?

REPLY [0 votes]: $m\mathbb Z\cong n\mathbb Z\cong Z$ for $m\neq n$, but $\mathbb Z/m\mathbb Z\not\cong\mathbb Z/n\mathbb Z$.


TITLE: Companion matrix of bivariate polynomial
QUESTION [8 upvotes]: A polynomial in one variable can be expressed as a companion matrix, of which the eigenvalues are the roots of the polynomial and which can be found by using e.g. QR decomposition or power iteration.
Is there anything like this for multivariate polynomials? To keep things simple: is there a "companion" matrix for quadratic or cubic bivariate polynomial? And is it possible to employ some eigenvalue algorithm for find all of its roots?

REPLY [0 votes]: In general you can't find all of multivariate polynomial roots. You can factor it, but the factorization is in general not unique and you won't be getting just one root per factor. For example $$x^2+y^2 - 1=0$$ has solutions all along the unit circle so that would be an infinite number of roots. But if you have $$x^3+xy^2-x =0$$
of course you can write it as
$$x(x^2+y^2-1)=0$$
which is the selection between a line of $0$ for an $x$ and said circle.


TITLE: Sum of squareroots of primes under Galois action
QUESTION [1 upvotes]: Let $p_1, ..., p_r$ be distinct prime numbers, $L = \mathbb{Q}(\sqrt{p_1}, ..., \sqrt{p_r})$ and $\alpha = \sqrt{p_1} + ... + \sqrt{p_r}$.
Is there any way to proof, that
$$ \{ \sigma(\alpha) \ | \ \sigma \in \text{Gal}(L/\mathbb{Q}) \}$$
is contained in $\mathbb{Q}(\alpha)$ without showing, that $L = \mathbb{Q}(\alpha)$?

REPLY [3 votes]: If the set of $\alpha$'s conjugates in $\mathbb{C}$ is $A=\{\alpha_1= \alpha, \alpha_2, \dots, \alpha_n\}$, it suffices to show that $\mathbb{Q}(A) = \mathbb{Q}(\alpha)$. Since the former is a splitting field, it is Galois, with Galois group $G$.
Now note that if all of $G$'s  subgroups are normal, then, in particular, $\mathbb{Q}(\alpha)$ is normal over $\mathbb{Q}$, therefore it contains all of $\alpha$'s conjugates and the result follows.
Since $L/\mathbb{Q}$ is normal $L$ and contains $\mathbb{Q}(A)$, $G$ is a subgroup of $\text{Gal}(L/\mathbb{Q}) \approx \mathbb{Z}_2^r$, and since $\mathbb{Z}_2^r$ is abelian, all of its subgroups are normal, including those of $G$.
In general, this argument works for any $\alpha \in L$, for example $\alpha = \sqrt{p_1}\sqrt{p_3}+\sqrt{p_2}$.


TITLE: Eigenvalues of large symmetric random tensors
QUESTION [2 upvotes]: I am studying the eigenvalues of large random tensors and realise that very little is known about it. I was wondering what is already known and what could be potential leads to find their limiting distribution.
Random symmetric tensor
Let $\mathbf{T}$ be a real fully symmetric tensor of order $3$ and size $N$. Its components can be represented as $T_{ijk}\in \mathbb{R}$ for all $1\leq i,j,k\leq N$. By symmetric I mean that if I permute any indices the value stays the same:
\begin{equation}
T_{ijk}=T_{ikj}=\dots=T_{jki}
\end{equation}
Eigenvalues
One possible definition of eigenvalues: let $x\in \mathbb{C}^N$ and $\lambda\in\mathbb{C}$ such that:
\begin{equation}
\sum_{jk}^NT_{ijk}x_kx_j=\lambda x_i
\label{eq1}
\end{equation}
with the constraint that $\sum_i x_i^2=1$.
It has been shown (in [1] for example) that for a tensor of order 3 and size $N$ there are $2^{N}-1$ eigenvalues $\lambda$. Perhaps an intuitive idea on why is to see that the eigenvalue equation is composed of $N$ quadratic equations. Each equation possesses two roots, hence $2^N$ possible combinations of solutions, minus the normalisation constraint.
Possible leads
It would be interesting to find the limiting distribution of eigenvalues of random tensors for large $N$. The eigenvalues are real only if their eigenvectors are real. I conjecture that the purely real eigenvalues scale with $\sqrt{N}$ whereas the general eigenvalues scale with $N$. That is to say, I would expect the real eigenvalues to be distributed on a closed non trivial interval when the elements of the tensor have a variance scaled with $1/\sqrt{N}$.
1. Reducing it to a non-linear matrix problem:
We define the matrix $M$ such that: $M_{ij}=\sum_{k}T_{ijk}x_k$. Therefore the eigenvalue problem would boil down to find the eigenvalues of $M$:
\begin{align}
\sum_{jk}^NT_{ijk}x_kx_j&=\lambda x_i\\
\implies \sum_{j}M_{ij}x_j&=\lambda x_i
\end{align}
Where the elements of $M$ now also depend on the eigenvectors.
2. Choosing an appropriate basis to uncouple the equations:
If we fix the index $i$, we can represent $T$ as a collection of $N$ matrices:
${M}^{(1)},{M}^{(2)}\dots{M}^{(N)}$ where $T_{ijk}={M_{jk}}^{(i)}$.
Since $T$ is real and fully symmetric, ${M}^{(i)}$ is also real symmetric $(1\leq i\leq N)$. There will also share some elements in common and not be fully independent from one another. For example $T_{ijk}=T_{kij}\implies M_{ij}^{(1)}=M_{1j}^{(i)}$. So matrix $M^{(1)}$ will be composed of the first column of all the other matrices. What is the relation between the eigenvalues of $M^{(i)}$ and $M^{(j)}$? Are they directly linked to the eigenvalues of $T$?
Here were some of the first ideas that came naturally to my mind. If you know a paper or some ideas on how to tackle this problem this would be very interesting.
[1]: Cartwright, D., & Sturmfels, B. (2013). The number of eigenvalues of a tensor. Linear algebra and its applications, 438(2), 942-952.

REPLY [3 votes]: A productive way to approach this problem has been to focus on the real eigenvalues of the symmetric tensor and identify these with the critical points on the unit sphere of a Kostlan polynomial. In this way Paul Breiding was able to find an exact answer for the expected number of real eigenvalues when the symmetric tensor has a Gaussian distribution.
The generalization of the Wigner semicircle law to real symmetric tensors (tensor GOE) was studied by Razvan Gurau.


TITLE: Meromorphic functions fixing $\mathbb S^1$
QUESTION [0 upvotes]: The following question is similar to this one:

Determine all meromorphic functions $f \colon \Bbb C \to \Bbb C$ that $$
 \vert f(z) \vert = 1 \qquad \forall z \colon \vert z \vert = 1.
$$

Unfortunately I have no idea to tackle this. Sorry for insufficient background.
I guess the Blaschke products would also needed in this question, but the poles and zeros are not "confined", and then the situation might be subtle. Anyway, thanks in advance for any comments and ideas.

REPLY [0 votes]: Note that if $f$ has no zeroes or poles inside the unit circle, $f=\lambda, |\lambda|=1$ by applying the maximum modulus to $f, \frac{1}{f}$.
So let the finite number of zeroes inside the unit disc be $z_1,..z_k$ and the finite number of poles inside the unit disc be $w_1,..w_m$ (all counted with multiplicities so some $z$'s or $w$'s can be equal in between but $z_j \ne w_l$ and either set can be empty - note that $f$ meromorphic means that there are finitely many zeroes and poles within any compact set since the function is not identical zero or infinity given that $|f|=1$ on the unit circle)
But now if $B(z)=\Pi{\frac{z-z_j}{1-\bar z_j z}}$ is the corresponding Blaschke product for zeroes and $B_1(z)=\Pi{\frac{z-w_j}{1-\bar w_j z}}$ is the corresponding Blaschke product for poles (taken as $1$ if the respective set is empty), $|B|=|B_1|=1$ on the unit circle and by construction:
$g(z)=\frac{f(z)B_1(z)}{B(z)}$ is analytic inside the unit disc and has no zeroes as $B$ eliminates them and no poles since $B_1$ eliminates them, while preserving the fact that $|g|=1$ on the unit circle. Hence $g=\lambda$ constant of unit modulus and putting all together:
$f(z)=\lambda\Pi_{1 \le j \le k}{\frac{z-z_j}{1-\bar z_j z}}\Pi_{1 \le l \le m}{\frac{1-\bar w_l z}{z-w_l}}$, where $|\lambda|=1, k,m \ge 0, |z_1|,..|z_k| < 1, |w_1|, ...|w_m| <1, z_j \ne w_l$ but otherwise all arbitrary with the given conditions (so some $z$'s can be equal and same with $w$'s while the respective factors are $1$ if $k=0$ or $m=0$)