text:
theory Transfer_Euclidean_Space_Vector
imports
  "../Refinement/Refine_Vector_List"
  Transfer_ODE
begin

type_synonym 'n rvec = "(real, 'n) vec"
type_synonym 'n vec1 = "(real, 'n) vec \<times> ((real, 'n) vec, 'n) vec" \<comment> \<open>vector with C1 information\<close>
type_synonym 'a c1_info = "'a \<times> ('a \<Rightarrow>\<^sub>L 'a)"
type_synonym 'n eucl1 = "'n rvec c1_info" \<comment> \<open>abstract C1 information\<close>

subsection \<open>Casting function\<close>

definition "cast = eucl_of_list o list_of_eucl"

lemma cast_eqI: "cast x = y" if "list_of_eucl x = list_of_eucl y"
  using that by (auto simp: cast_def)

lemma cast_eqI2: "cast (x::'a) = (y::'b)"
  if "x = cast y" and "DIM('a::executable_euclidean_space) = DIM('b::executable_euclidean_space)"
  apply (rule cast_eqI)
  using that
  by (auto intro!: nth_equalityI simp: cast_def)

lemma cast_Basis_list_nth[simp]: "cast (Basis_list ! i::'a) = (Basis_list ! i::'b)"
  if "DIM('a::executable_euclidean_space) = DIM('b::executable_euclidean_space)" "i < DIM('b)"
  apply (rule cast_eqI)
  using that
  by (auto simp: inner_Basis nth_eq_iff_index_eq intro!: nth_equalityI)

lemma cast_inner[simp]:
  "cast x \<bullet> (cast y::'b) = x \<bullet> (y::'a)"
  if "DIM('a::executable_euclidean_space) = DIM('b::executable_euclidean_space)"
  using that
  by (subst (2) euclidean_inner)
     (auto simp: cast_def eucl_of_list_inner_eq inner_lv_rel_def sum_Basis_sum_nth_Basis_list
      sum_list_sum_nth atLeast0LessThan)

lemma cast_inner_Basis_list_nth[simp]:
  "cast x \<bullet> (Basis_list::'a list) ! i = x \<bullet> (Basis_list::'b list) ! i"
  if "DIM('a::executable_euclidean_space) = DIM('b::executable_euclidean_space)" "i < DIM('b)"
  using that
  by (auto simp: cast_def eucl_of_list_inner)

lemma cast_eucl_of_list[simp]:
  "cast (eucl_of_list xs::'a) = (eucl_of_list xs::'b)"
  if "DIM('a::executable_euclidean_space) = DIM('b::executable_euclidean_space)" "length xs = DIM('b)"
  using that
  by (auto simp: intro!: euclidean_eqI[where 'a='b])
     (auto simp: cast_def eucl_of_list_inner dest!: in_Basis_index_Basis_list)

lemma norm_cast[simp]: "norm (cast x::'a) = norm (x::'b)"
  if "DIM('a::executable_euclidean_space) = DIM('b::executable_euclidean_space)"
  unfolding norm_conv_dist
  apply (subst (1 2) euclidean_dist_l2)
  using that
  apply (auto simp: L2_set_def sum_Basis_sum_nth_Basis_list  cong: sum.cong)
  apply (subst sum.cong[OF refl])
   apply (subst cast_inner_Basis_list_nth)
     apply auto
  done

lemma linear_cast: "linear (cast::'a\<Rightarrow>'b)"
  if "DIM('a::executable_euclidean_space) = DIM('b::executable_euclidean_space)"
  apply standard
  using that
  by (auto simp: inner_simps intro!: cast_eqI nth_equalityI exI[where x=1])

lemma bounded_linear_cast: "bounded_linear (cast::'a\<Rightarrow>'b)"
  if "DIM('a::executable_euclidean_space) = DIM('b::executable_euclidean_space)"
  apply standard
  using that
  by (auto simp: inner_simps intro!: cast_eqI nth_equalityI exI[where x=1])

lemmas [bounded_linear_intros] = bounded_linear_compose[OF bounded_linear_cast]

lemma cast_id[simp]: "cast i = i"
  by (simp add: cast_eqI)

definition cast_bl where "cast_bl f = Blinfun (cast o blinfun_apply f o cast)"

lemma cast_bl_rep: "cast_bl (f::'a \<Rightarrow>\<^sub>L 'b) x = (cast (f (cast (x::'c)))::'d)"
  if [bounded_linear_intros]:
    "DIM('c::executable_euclidean_space) = DIM('a::executable_euclidean_space)"
     "DIM('b::executable_euclidean_space) = DIM('d::executable_euclidean_space)"
  unfolding cast_bl_def o_def
  apply (subst bounded_linear_Blinfun_apply)
   apply (rule bounded_linear_intros)+
  apply auto
  done

definition "cast_eucl1 x = (cast (fst x), cast_bl (snd x))"

definition [simp]: "op_cast_image = (`) cast"
definition [simp]: "op_cast_eucl1_image = (`) cast_eucl1"
context includes autoref_syntax begin
lemma [autoref_op_pat_def]:
  "(`) cast \<equiv> OP op_cast_image"
  "(`) cast_eucl1 \<equiv> OP op_cast_eucl1_image"
  by auto
end

lemma cast_idem[simp]:
  "cast (cast (x::'c)::'b) = (cast x::'a)"
  if "DIM('a::executable_euclidean_space) = DIM('c::executable_euclidean_space)"
    "DIM('b::executable_euclidean_space) = DIM('c)"
  using that
  by (auto simp: cast_def intro!: )

lemma cast_bl_idem[simp]:
  "cast_bl (cast_bl (x::'c\<Rightarrow>\<^sub>L'c)::'b\<Rightarrow>\<^sub>L'b) = (cast_bl x::'a\<Rightarrow>\<^sub>L'a)"
  if "DIM('a::executable_euclidean_space) = DIM('c::executable_euclidean_space)"
    "DIM('b::executable_euclidean_space) = DIM('c)"
  using that
  by (auto simp: cast_bl_rep o_def intro!: blinfun_eqI)

lemma cast_eucl1_idem[simp]:
  "cast_eucl1 (cast_eucl1 (x::'c c1_info)::'b c1_info) = (cast_eucl1 x::'a c1_info)"
  if "DIM('a::executable_euclidean_space) = DIM('c::executable_euclidean_space)"
    "DIM('b::executable_euclidean_space) = DIM('c)"
  using that
  by (auto simp: cast_def cast_eucl1_def intro!: )

lemma linear_cast_bl:
  "linear (cast_bl::('a \<Rightarrow>\<^sub>L'b) \<Rightarrow> ('c \<Rightarrow>\<^sub>L 'd))"
  if "DIM('c::executable_euclidean_space) = DIM('a::executable_euclidean_space)"
     "DIM('b::executable_euclidean_space) = DIM('d::executable_euclidean_space)"
  by standard
    (auto intro!: blinfun_eqI
      simp: cast_bl_rep that blinfun.bilinear_simps linear_cast linear_add linear.scaleR)
lemma norm_cast_bl_le: "norm ((cast_bl::('a \<Rightarrow>\<^sub>L'b) \<Rightarrow> ('c \<Rightarrow>\<^sub>L 'd)) x) \<le> norm x"
  if "DIM('c::executable_euclidean_space) = DIM('a::executable_euclidean_space)"
  "DIM('b::executable_euclidean_space) = DIM('d::executable_euclidean_space)"
  apply (rule norm_blinfun_bound)
  using that
   apply (auto simp: cast_bl_rep)
  apply (rule norm_blinfun[THEN order_trans])
  apply auto
  done

lemma norm_cast_bl_idem[simp]: "cast_bl ((cast_bl::('a \<Rightarrow>\<^sub>L'b) \<Rightarrow> ('c \<Rightarrow>\<^sub>L 'd)) x) = x"
  if "DIM('c::executable_euclidean_space) = DIM('a::executable_euclidean_space)"
     "DIM('b::executable_euclidean_space) = DIM('d::executable_euclidean_space)"
  by (auto intro!: blinfun_eqI simp: that cast_bl_rep)

lemma norm_cast_bl[simp]: "norm ((cast_bl::('a \<Rightarrow>\<^sub>L'b) \<Rightarrow> ('c \<Rightarrow>\<^sub>L 'd)) x) = norm x"
  if "DIM('c::executable_euclidean_space) = DIM('a::executable_euclidean_space)"
     "DIM('b::executable_euclidean_space) = DIM('d::executable_euclidean_space)"
proof (rule antisym)
  show "norm ((cast_bl::('a \<Rightarrow>\<^sub>L'b) \<Rightarrow> ('c \<Rightarrow>\<^sub>L 'd)) x) \<le> norm x"
    by (rule norm_cast_bl_le; fact)
  have "norm x = norm ((cast_bl::('c \<Rightarrow>\<^sub>L'd) \<Rightarrow> ('a \<Rightarrow>\<^sub>L 'b)) ((cast_bl::('a \<Rightarrow>\<^sub>L'b) \<Rightarrow> ('c \<Rightarrow>\<^sub>L 'd)) x))"
    by (simp add: that)
  also note norm_cast_bl_le[OF that, of "cast_bl x"]
  finally show "norm x \<le> norm ((cast_bl::('a \<Rightarrow>\<^sub>L'b) \<Rightarrow> ('c \<Rightarrow>\<^sub>L 'd)) x)"
    apply (rule order_trans)
     defer
     apply (rule norm_cast_bl_le)
    using that by auto
qed

lemma bounded_linear_cast_bl:
  "bounded_linear (cast_bl::('a \<Rightarrow>\<^sub>L'b) \<Rightarrow> ('c \<Rightarrow>\<^sub>L 'd))"
  if "DIM('c::executable_euclidean_space) = DIM('a::executable_euclidean_space)"
     "DIM('b::executable_euclidean_space) = DIM('d::executable_euclidean_space)"
  by standard
    (auto intro!: blinfun_eqI exI[where x=1]
      simp: cast_bl_rep that blinfun.bilinear_simps linear_cast linear_add linear.scaleR)

lemma cast_bl_has_derivative[derivative_intros]:
  "((\<lambda>a. (cast_bl::('a \<Rightarrow>\<^sub>L'b) \<Rightarrow> ('c \<Rightarrow>\<^sub>L 'd)) (g a)) has_derivative (\<lambda>x. (cast_bl::('a \<Rightarrow>\<^sub>L'b) \<Rightarrow> ('c \<Rightarrow>\<^sub>L 'd)) (g' x))) (at x within X)"
  if "(g has_derivative g') (at x within X)"
     "DIM('c::executable_euclidean_space) = DIM('a::executable_euclidean_space)"
     "DIM('b::executable_euclidean_space) = DIM('d::executable_euclidean_space)"
  apply (rule has_derivative_compose[of g _ _ _ cast_bl, THEN has_derivative_eq_rhs])
    defer apply (rule bounded_linear_imp_has_derivative)
    apply (rule bounded_linear_cast_bl)
  using that
     apply auto
  done

lemma cast_bl_has_vector_derivative[derivative_intros]:
  "((\<lambda>a. (cast_bl::('a \<Rightarrow>\<^sub>L'b) \<Rightarrow> ('c \<Rightarrow>\<^sub>L 'd)) (g a)) has_vector_derivative cast_bl g') (at x within X)"
  if "(g has_vector_derivative g') (at x within X)"
  "DIM('c::executable_euclidean_space) = DIM('a::executable_euclidean_space)"
  "DIM('b::executable_euclidean_space) = DIM('d::executable_euclidean_space)"
  using that
  by (auto simp: has_vector_derivative_def blinfun.bilinear_simps cast_bl_rep linear.scaleR
      linear_cast_bl
      intro!: cast_bl_has_derivative derivative_eq_intros ext blinfun_eqI)

lemma cast_bl_has_vderiv_on:
  "((\<lambda>a. (cast_bl::('a \<Rightarrow>\<^sub>L'b) \<Rightarrow> ('c \<Rightarrow>\<^sub>L 'd)) (g a)) has_vderiv_on vd) X"
  if "(g has_vderiv_on g') X" "\<And>t. t \<in> X \<Longrightarrow> vd t = cast_bl (g' t)"
  "DIM('c::executable_euclidean_space) = DIM('a::executable_euclidean_space)"
  "DIM('b::executable_euclidean_space) = DIM('d::executable_euclidean_space)"
  using that
  by (auto simp: has_vderiv_on_def intro!: derivative_eq_intros)

lemma cast_bl_compose:
  "(cast_bl::('a \<Rightarrow>\<^sub>L'b) \<Rightarrow> ('c \<Rightarrow>\<^sub>L 'd)) (g  o\<^sub>L h) =
    ((cast_bl:: 'e \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'f \<Rightarrow>\<^sub>L 'd) g o\<^sub>L (cast_bl:: 'a \<Rightarrow>\<^sub>L 'e \<Rightarrow> 'c \<Rightarrow>\<^sub>L 'f) h)"
  if "DIM('c::executable_euclidean_space) = DIM('a::executable_euclidean_space)"
  "DIM('b::executable_euclidean_space) = DIM('d::executable_euclidean_space)"
  "DIM('e::executable_euclidean_space) = DIM('f::executable_euclidean_space)"
  by (auto intro!: blinfun_eqI simp: cast_bl_rep that)

locale transfer_eucl_vec =
  fixes a::"'a::executable_euclidean_space" and n::"'n::enum"
  assumes dim[simp]: "DIM('a) = CARD('n)"
begin

context includes lifting_syntax begin

subsection \<open>Transfer from euclidean space to vector\<close>

definition "rel_ve (x::(real, 'n)vec) (y::'a) \<longleftrightarrow> list_of_eucl x = list_of_eucl y"

lemma [transfer_rule]: "bi_total rel_ve"
  apply (auto intro!: bi_totalI left_totalI right_totalI simp: rel_ve_def intro!: )
  subgoal for x by (auto intro!: exI[where x="eucl_of_list (list_of_eucl x)"] nth_equalityI simp: dim)
  subgoal for x by (auto intro!: exI[where x="eucl_of_list (list_of_eucl x)"] nth_equalityI simp: dim)
  done

lemma [transfer_rule]: "bi_unique rel_ve"
  by (auto intro!: bi_uniqueI left_uniqueI right_uniqueI simp: rel_ve_def )
    (metis eucl_of_list_list_of_eucl)+

text \<open>@{const Inf} is underspecified\<close>
text \<open>@{const Sup} is underspecified\<close>

lemma inf_transfer[transfer_rule]:
  "(rel_ve ===> rel_ve ===> rel_ve) inf inf"
  by (auto simp: rel_ve_def nth_eq_iff_index inner_Basis_inf_left
      list_of_eucl_eq_iff intro!: rel_funI)

lemma sup_transfer[transfer_rule]:
  "(rel_ve ===> rel_ve ===> rel_ve) sup sup"
  by (auto simp: rel_ve_def nth_eq_iff_index inner_Basis_sup_left
      list_of_eucl_eq_iff intro!: rel_funI)

lemma abs_transfer[transfer_rule]:
  "(rel_ve ===> rel_ve) abs abs"
  by (auto simp: rel_ve_def nth_eq_iff_index inner_Basis_sup_left abs_inner
      list_of_eucl_eq_iff intro!: rel_funI)

lemma less_eq_transfer[transfer_rule]:
  "(rel_ve ===> rel_ve ===> (=)) less_eq less_eq"
  by (auto simp: rel_ve_def nth_eq_iff_index eucl_le_Basis_list_iff[where 'a='a]
      eucl_le_Basis_list_iff[where 'a="'n rvec"]
      list_of_eucl_eq_iff intro!: rel_funI )

lemma scaleR_transfer[transfer_rule]:
  "((=) ===> rel_ve ===> rel_ve) scaleR scaleR"
  by (auto simp: rel_ve_def algebra_simps nth_eq_iff_index
      list_of_eucl_eq_iff intro!: rel_funI)

lemma Basis_transfer[transfer_rule]:
  "(rel_set rel_ve) Basis Basis"
  apply (rule rel_setI)
  subgoal for x by (auto simp: rel_ve_def list_of_eucl_eq_iff inner_Basis nth_eq_iff_index
        intro!: bexI[where x="Basis_list ! index Basis_list x"])
  subgoal for x by (auto simp: rel_ve_def list_of_eucl_eq_iff inner_Basis nth_eq_iff_index
        intro!: bexI[where x="Basis_list ! index Basis_list x"])
  done

lemma zero_transfer[transfer_rule]:
  "rel_ve 0 0"
  by (auto simp: rel_ve_def algebra_simps nth_eq_iff_index
      list_of_eucl_eq_iff intro!: rel_funI)

lemma uminus_transfer[transfer_rule]:
  "(rel_ve ===> rel_ve) uminus uminus"
  by (auto simp: rel_ve_def algebra_simps nth_eq_iff_index
      list_of_eucl_eq_iff intro!: rel_funI)

lemma plus_transfer[transfer_rule]:
  "(rel_ve ===> rel_ve ===> rel_ve) (+) (+)"
  by (auto simp: rel_ve_def algebra_simps nth_eq_iff_index
      list_of_eucl_eq_iff intro!: rel_funI)

lemma minus_transfer[transfer_rule]:
  "(rel_ve ===> rel_ve ===> rel_ve) (-) (-)"
  by (auto simp: rel_ve_def algebra_simps nth_eq_iff_index
      list_of_eucl_eq_iff intro!: rel_funI)

lemma Basis_list_transfer[transfer_rule]:
  "(list_all2 rel_ve) Basis_list Basis_list"
  by (auto simp: list_all2_iff in_set_zip rel_ve_def inner_Basis
      nth_eq_iff_index intro!: nth_equalityI)

lemma eucl_down_transfer[transfer_rule]:
  "((=) ===> rel_ve ===> rel_ve) eucl_down eucl_down"
  unfolding eucl_down_def
  by (auto simp: rel_ve_def algebra_simps nth_eq_iff_index
      list_of_eucl_eq_iff intro!: rel_funI)

lemma eucl_truncate_up_transfer[transfer_rule]:
  "((=) ===> rel_ve ===> rel_ve) eucl_truncate_up eucl_truncate_up"
  by (auto simp: rel_ve_def algebra_simps nth_eq_iff_index
      list_of_eucl_eq_iff intro!: rel_funI)

lemma eucl_truncate_down_transfer[transfer_rule]:
  "((=) ===> rel_ve ===> rel_ve) eucl_truncate_down eucl_truncate_down"
  by (auto simp: rel_ve_def algebra_simps nth_eq_iff_index
      list_of_eucl_eq_iff intro!: rel_funI)

lemma inner_transfer[transfer_rule]:
  "(rel_ve ===> rel_ve ===> (=)) inner inner"
  apply (subst euclidean_inner[where 'a="'a", abs_def])
  apply (subst euclidean_inner[where 'a="'n rvec", abs_def])
  by (auto simp: rel_ve_def algebra_simps nth_eq_iff_index inner_simps nth_eq_iff_index
      sum_Basis_sum_nth_Basis_list list_of_eucl_eq_iff intro!: rel_funI)

lemma rel_ve_cast: "rel_ve (x::'n rvec) (y::'a) \<longleftrightarrow> x = cast y"
  apply (auto simp: rel_ve_def cast_def intro!: rel_funI)
  by (metis eucl_of_list_list_of_eucl)

lemma rel_ve_cast': "rel_ve (x::'n rvec) (y::'a) \<longleftrightarrow> cast x = y"
  by (auto simp: rel_ve_def cast_def)

lemma cast_transfer[transfer_rule]: "(rel_ve ===> (=)) (\<lambda>x. x) cast"
  by (auto simp: rel_ve_cast)

lemma cast_transfer'[transfer_rule]: "((=) ===> rel_ve) (\<lambda>x. x) cast"
  by (auto simp: rel_ve_cast')

lemma bounded_linear_cast: "bounded_linear (cast::'a \<Rightarrow> 'n rvec)"
  by transfer (rule bounded_linear_ident)

lemma bounded_linear_cast': "bounded_linear (cast::'n rvec \<Rightarrow> 'a)"
  by transfer (rule bounded_linear_ident)

context includes blinfun.lifting begin

lemmas [simp] = cast_bl_rep

lemma eucl_of_list_transfer[transfer_rule]: "(list_all2 (=) ===> rel_ve) eucl_of_list eucl_of_list"
  unfolding eucl_of_list_def
  by transfer_prover

lemma list_of_eucl_transfer[transfer_rule]: "(rel_ve ===> list_all2 (=)) list_of_eucl list_of_eucl"
  unfolding list_of_eucl_def
  by transfer_prover

lemma blinfun_of_matrix_transfer[transfer_rule]:
  "((rel_ve ===> rel_ve ===> (=)) ===> (rel_blinfun rel_ve rel_ve)) blinfun_of_matrix blinfun_of_matrix"
  apply (rule rel_funI)
  apply transfer
  apply (rule rel_funI)
  unfolding rel_blinfun_def
  unfolding sum_Basis_sum_nth_Basis_list
  apply simp
  unfolding rel_ve_def list_of_eucl_eq_iff inner_sum_left
  apply simp
  apply (intro allI impI sum.cong refl)
  apply (rule arg_cong2[where f="(*)"])
  subgoal for a b c d e f g
    apply (rule arg_cong2[where f="(*)"])
    subgoal by simp
    apply (drule rel_funD[where x="Basis_list ! f"]) defer
     apply (drule rel_funD[where x="Basis_list ! g"]) defer
      apply assumption
    subgoal
      by (clarsimp simp: inner_Basis)
        (metis Basis_list_transfer dim index_Basis_list_nth length_Basis_list list_all2_lengthD)
    subgoal
      by (clarsimp simp: inner_Basis)
        (metis Basis_list_transfer dim index_Basis_list_nth length_Basis_list list_all2_lengthD)
    done
  subgoal for a b c d e f g
    apply (clarsimp simp: inner_Basis)
    by (metis (full_types, opaque_lifting) Basis_list_transfer dim index_Basis_list_nth length_Basis_list
        list_all2_conv_all_nth)
  done

lemma transfer_cast[transfer_rule]: "(rel_ve ===> rel_ve) (\<lambda>x. x) cast"
  by (auto simp:)

end

end

end

lemma
  assumes [simp]: "DIM('a::executable_euclidean_space) = CARD('n::enum)"
  shows cast_cast[simp]: "cast (cast x::'n rvec) = (x::'a)" "cast (cast y::'a) = (y::'n rvec)"
  by (auto simp: cast_def cast_def)

lifting_update blinfun.lifting
lifting_forget blinfun.lifting

locale transfer_eucl_vec_ll_on_open = transfer_eucl_vec a n + ll_on_open T f X
  for a::"'a::executable_euclidean_space" and n::"'n::enum" and T f and X::"'a set" +
  fixes vf vX
  defines "vf \<equiv> \<lambda>t x::'n rvec. cast (f t (cast x))::'n rvec"
  defines "vX \<equiv> cast ` X::'n rvec set"
begin

lemma transfer_X[transfer_rule]: "rel_set rel_ve vX X"
  and transfer_f[transfer_rule]: "(rel_fun (=) (rel_fun rel_ve rel_ve)) vf f"
  by (auto simp: rel_ve_cast cast_eqI vX_def vf_def intro!: rel_setI rel_funI)

sublocale v: ll_on_open T vf vX
  by (rule ll_on_open_axioms[untransferred])

context includes lifting_syntax begin

lemma transfer_csols[transfer_rule]:
  "((=) ===> rel_ve ===> rel_set (rel_prod ((=) ===> rel_ve) (=))) v.csols csols"
  unfolding csols_def v.csols_def
  by transfer_prover

lemma transfer_existence_ivl[transfer_rule]:
  "((=) ===> rel_ve ===> rel_set (=)) v.existence_ivl existence_ivl"
  unfolding existence_ivl_def v.existence_ivl_def
  by transfer_prover

lemma cast_v_flow_cast_eq:
  assumes "t \<in> existence_ivl t0 x0"
  shows "cast (v.flow t0 (cast x0) t) = flow t0 x0 t"
  apply (rule equals_flowI[OF _ _ order_refl])
  subgoal
    apply (rule existence_ivl_initial_time)
    using assms mem_existence_ivl_iv_defined(1) apply blast
    using assms mem_existence_ivl_iv_defined(2) by blast
  subgoal by (rule is_interval_existence_ivl)
  subgoal
    apply (rule solves_odeI)
    subgoal using assms
     by (transfer) (rule v.flow_has_vderiv_on[OF v.mem_existence_ivl_iv_defined])
   subgoal using assms
     by transfer (rule v.flow_in_domain)
   done
  subgoal
    using mem_existence_ivl_iv_defined[OF assms]
    apply (auto simp: )
    apply (subst v.flow_initial_time)
    subgoal by simp
    subgoal by transfer
    subgoal by transfer simp
    done
  subgoal by fact
  done

lemma transfer_flow[transfer_rule]:
  "((=) ===> rel_ve ===> (=) ===> rel_ve) v.flow flow"
  apply (auto intro!: rel_funI simp: rel_ve_cast)
  subgoal for t0 x0 t
    apply (cases "t \<in> existence_ivl t0 (cast x0)")
    subgoal by (simp add: cast_eqI cast_v_flow_cast_eq[symmetric])
    subgoal
      apply (subst v.flow_def) apply (subst flow_def)
      apply (auto simp: cast_eqI)
      subgoal by transfer simp
      subgoal by transfer simp
      done
    done
  done

end

end

locale transfer_c1_on_open_euclidean = transfer_eucl_vec a n + c1_on_open_euclidean f f' X
  for a::"'a::executable_euclidean_space" and n::"'n::enum" and f f' and X::"'a set" +
  fixes vf and vf'::"'n rvec \<Rightarrow> 'n rvec \<Rightarrow>\<^sub>L 'n rvec" and vX
  defines "vf \<equiv> \<lambda>x::'n rvec. cast (f (cast x))::'n rvec"
  defines  vf'_def: "vf' \<equiv> \<lambda>x. cast_bl (f' (cast x))"
  defines "vX \<equiv> cast ` X::'n rvec set"
begin

context includes lifting_syntax begin

lemma transfer_X[transfer_rule]: "rel_set rel_ve vX X"
  and transfer_f[transfer_rule]: "(rel_fun rel_ve rel_ve) vf f"
  by (auto simp: rel_ve_cast vX_def vf_def cast_eqI intro!: rel_setI rel_funI)

lemma transfer_f'[transfer_rule]: "(rel_ve ===> (rel_blinfun rel_ve rel_ve)) vf' f'"
  by (auto intro!: rel_funI simp: cast_eqI rel_blinfun_def rel_ve_cast vf'_def)

end

sublocale v: c1_on_open_euclidean vf vf' vX
  unfolding c1_on_open_euclidean_def
  by (rule c1_on_open_axioms[unfolded c1_on_open_euclidean_def, untransferred])

context includes lifting_syntax begin

lemma transfer_csols[transfer_rule]:
  "((=) ===> rel_ve ===> rel_set (rel_prod ((=) ===> rel_ve) (=))) v.csols csols"
  unfolding csols_def v.csols_def
  by transfer_prover

lemma transfer_existence_ivl[transfer_rule]:
  "((=) ===> rel_ve ===> rel_set (=)) v.existence_ivl existence_ivl"
  unfolding existence_ivl_def v.existence_ivl_def
  by transfer_prover

lemma transfer_existence_ivl0[transfer_rule]:
  "(rel_ve ===> rel_set (=)) v.existence_ivl0 existence_ivl0"
proof -
  interpret ll: transfer_eucl_vec_ll_on_open a n UNIV "\<lambda>_. f" X "\<lambda>_. vf" vX
    by unfold_locales (auto simp: vf_def)
  show ?thesis
    unfolding existence_ivl0_def v.existence_ivl0_def
    by transfer_prover
qed

lemma transfer_flow0[transfer_rule]:
  "(rel_ve ===> (=) ===> rel_ve) v.flow0 flow0"
proof -
  interpret ll: transfer_eucl_vec_ll_on_open a n UNIV "\<lambda>_. f" X "\<lambda>_. vf" vX
    by unfold_locales (auto simp: vf_def)
  show ?thesis
    unfolding flow0_def v.flow0_def
    by transfer_prover
qed

lemma cast_v_Dflow_cast_eq:
  assumes "t \<in> existence_ivl0 x0"
  shows "cast_bl (v.Dflow (cast x0) t) = Dflow x0 t"
proof -
  have "x0 \<in> X"
    using assms mem_existence_ivl_iv_defined(1) by blast
  have "0 \<in> existence_ivl0 x0"
    apply (rule existence_ivl_initial_time)
    apply simp
    apply fact
    done
  show ?thesis
  unfolding Dflow_def
  apply (rule mvar.equals_flowI[OF _ _ order_refl])
  subgoal
    apply (rule mvar.existence_ivl_initial_time)
     apply fact
    apply blast
    done
  subgoal by (rule mvar.is_interval_existence_ivl)
  subgoal
    apply (rule solves_odeI)
    subgoal
    proof -
      have *: "mvar.existence_ivl x0 0 1\<^sub>L = (v.mvar.existence_ivl (cast x0) 0 1\<^sub>L)"
        apply (subst mvar_existence_ivl_eq_existence_ivl, fact)
        apply (subst v.mvar_existence_ivl_eq_existence_ivl)
        subgoal using \<open>0 \<in> existence_ivl0 x0\<close> by (transfer)
        subgoal by transfer simp
        done
      have D: "(v.Dflow (cast x0) has_vderiv_on (\<lambda>t. v.vareq (cast x0) t o\<^sub>L v.mvar.flow (cast x0) 0 1\<^sub>L t))
        (mvar.existence_ivl x0 0 1\<^sub>L)"
        unfolding * v.Dflow_def
        apply (rule v.mvar.flow_has_vderiv_on[of 0 "cast x0" "1\<^sub>L"])
        subgoal using \<open>0 \<in> existence_ivl0 x0\<close> by (transfer)
        subgoal by transfer simp
        done
      have vareq_transfer: "vareq x0 x = cast_bl (v.vareq (cast x0) x)"
        if "x \<in> mvar.existence_ivl x0 0 1\<^sub>L"
        for x
        using that
        apply (subst (asm) mvar_existence_ivl_eq_existence_ivl)
        using \<open>0 \<in> existence_ivl0 x0\<close> apply simp
        unfolding vareq_def v.vareq_def
        apply (auto simp: blinfun_ext)
        apply transfer
        apply simp
        done
      show ?thesis
        apply (rule cast_bl_has_vderiv_on)
           apply (rule D)
          apply (simp_all add: v.Dflow_def blinfun_compose_assoc vareq_transfer)
        apply (subst cast_bl_compose)
           apply (auto simp: cast_bl_compose)
        done
    qed
    subgoal by simp
    done
  subgoal
    unfolding Dflow_def[symmetric]
    apply (subst Dflow_zero)
     apply fact
    apply (subst v.Dflow_zero)
    subgoal using \<open>x0 \<in> X\<close> by transfer simp
    subgoal by (auto simp: blinfun_ext)
    done
  subgoal
    by (subst mvar_existence_ivl_eq_existence_ivl; fact)
  done
qed

lemma transfer_Dflow[transfer_rule]:
  "(rel_ve ===> (=) ===> rel_blinfun rel_ve rel_ve) v.Dflow Dflow"
  apply (auto intro!: rel_funI simp: rel_ve_cast rel_blinfun_def)
  subgoal for x0 t d
    apply (cases "t \<in> mvar.existence_ivl (cast x0) 0 1\<^sub>L")
    subgoal
      apply (subst cast_v_Dflow_cast_eq[symmetric])
      using mvar.existence_ivl_subset[of "cast x0" 0 id_blinfun]
      by auto
    subgoal premises prems
    proof -
      have x0: "x0 \<notin> X \<longleftrightarrow> cast x0 \<notin> vX"
        by transfer simp
      have mvars: "mvar.existence_ivl x0 0 1\<^sub>L = v.mvar.existence_ivl (cast x0) 0 1\<^sub>L"
        apply (cases "cast x0 \<in> X")
        subgoal
          apply (subst mvar_existence_ivl_eq_existence_ivl)
           apply simp
          apply (subst v.mvar_existence_ivl_eq_existence_ivl)
           apply simp
           apply transfer apply simp
          apply transfer apply simp
          done
        subgoal premises prems
        proof -
          have "mvar.existence_ivl (cast x0) 0 1\<^sub>L = {}"
            apply (subst mvar.existence_ivl_empty_iff)
            using prems
            by simp
          moreover have "v.mvar.existence_ivl (cast x0) 0 1\<^sub>L = {}"
            apply (subst v.mvar.existence_ivl_empty_iff)
            using prems
            apply simp
            apply transfer apply simp
            done
          ultimately show ?thesis
            apply simp
            using \<open>mvar.existence_ivl (cast x0) 0 1\<^sub>L = {}\<close> \<open>v.mvar.existence_ivl (cast x0) 0 1\<^sub>L = {}\<close> by auto
        qed
        done
      show ?thesis
        using prems
        apply (subst v.Dflow_def) apply (subst Dflow_def)
        apply (subst v.mvar.flow_def) apply (subst mvar.flow_def)
        unfolding mvars
        apply (auto simp: blinfun.bilinear_simps)
        using mvars apply blast
        subgoal premises apply transfer by simp
        done
    qed
    done
  done

lemma returns_to_transfer[transfer_rule]:
  "(rel_set rel_ve ===> rel_ve ===> (=)) v.returns_to returns_to"
  unfolding returns_to_def v.returns_to_def
  by transfer_prover

lemma return_time_transfer[transfer_rule]:
  "(rel_set rel_ve ===> rel_ve ===> (=)) v.return_time return_time"
  unfolding return_time_def v.return_time_def
  by transfer_prover

lemma poincare_map_transfer[transfer_rule]:
  "(rel_set rel_ve ===> rel_ve ===> rel_ve) v.poincare_map poincare_map"
  unfolding v.poincare_map_def poincare_map_def
  by transfer_prover

lemma poincare_mapsto_transfer[transfer_rule]:
  "(rel_set rel_ve
   ===> rel_set (rel_prod rel_ve (rel_blinfun rel_ve rel_ve))
   ===> rel_set rel_ve
   ===> rel_set rel_ve
   ===> rel_set (rel_prod rel_ve (rel_blinfun rel_ve rel_ve))
   ===> (=)) v.poincare_mapsto poincare_mapsto"
  unfolding poincare_mapsto_def v.poincare_mapsto_def
    has_derivative_within differentiable_def
  by transfer_prover

lemma flowsto_transfer[transfer_rule]:
  "(rel_set (rel_prod rel_ve (rel_blinfun rel_ve rel_ve))
   ===> rel_set (=)
   ===> rel_set (rel_prod rel_ve (rel_blinfun rel_ve rel_ve))
   ===> rel_set (rel_prod rel_ve (rel_blinfun rel_ve rel_ve))
   ===> (=)) v.flowsto flowsto"
  unfolding flowsto_def v.flowsto_def
  by transfer_prover

end

end

end

subset_name: curated


TITLE: Are Semiprimitive (Jacobson Semisimple, J-Semisimple) Rings Dedekind Finite?
QUESTION [3 upvotes]: Unfortunately there exists some ambiguity in the term semisimple. We have the common notion of semisimple, that of Artinian semisimple, and the less common one, that of Jacobson semisimple (not less common as in this object is less common, but less common as in it's referred to as simply "semisimple" less often). I encountered a problem which asked to show that a semisimple ring is Dedekind finite. This is fine if we have the common definition as then the ring is by definition Artinian and the whole thing follows from there:
If $ab=1$ then we can look at $bR\supset b^2R \supset \ldots$ and by DCC we have that $b^nR=b^{n+1}R$ so $b^n=b^{n+1}r$ and multiplying by $a^n$ on the left we get $1=br$ and of course $a=abr=r$ so $ba=1$.
However, if by chance the problem had intended the less common usage, prove that a semiprimitive $R$ is Dedekind finite, I'm not sure how to do this, and consequently I'm not sure if it's true or not. A semiprimitive ring is one in which the Jacobson radical is trivial (hence the other names). This makes using theorems like $R$ is Dedekind finite iff $R/J(R)$ is Dedekind finite useless. Does anyone have a counterexample or proof of this? Or a reference? Thanks so much!

REPLY [3 votes]: No, semiprimitive rings are not necessarily Dedekind finite. You can find examples like this at the Database of Ring Theory.
The canonical example of a ring in which there exists $a,b$ such that $ab=1$ but $ba\neq 1$ is the ring of linear transformations of an infinite dimensional vector space, where the transformations are written on the left side of vectors. It has Jacobson radical zero. Actually more is true: it is right primitive and von Neumann regular, both of which imply it has Jacobson radical zero.


TITLE: Ridge regression objective function gradient
QUESTION [1 upvotes]: Considering ridge regression problem with given objective function as:
$$f (W) = \|XW - Y\|_F^2 + \lambda \|W\|_F^2$$
Having convex and twice differentiable function results into:
$$\nabla f (W) = 2 \lambda W + 2X^T(XW - Y)$$
And finding its roots. My question is: why is the gradient of $\|XW - Y\|_F^2$ equal to $2X^T(XW - Y)$?

REPLY [0 votes]: Rewrite
$$||XW-Y||^2_2 = \left[XW-Y\right]^T\left[XW-Y\right]=\left[W^TX^T-Y^T\right]\left[XW-Y\right]=W^TX^TXW-Y^TXW-W^TX^TY+Y^TY$$
Hence, the total derivative on the right-hand side gives
$$dW^TX^TXW+W^TX^TXdW-2dW^TX^TY=2dW^T\left[X^TXW-X^TY \right]=dW^T\left[2X^T(XW-Y) \right].$$
The expression in the bracket is the gradient of the initial expression with respect to $W$. Note, that I used the fact that the transpose of a scalar is a scalar.


TITLE: application of the theorem of implicit functions
QUESTION [1 upvotes]: 1.Solve the equation $f(x,y,z):= x^{4}+2x\cos(y) + \sin (z) = 0$ in a neighbourhood of $p=(0,0,0)$ for z in the form : $z=g(x,y)$
  2. Give the maximal domain for $g$ and the neighbourhood of $p$ and
  3.calculate the differential of $g$. Check the connection between the theorem of implicit function for the differential of $g$ and the differential of $f$.

I solve like this:

$z= \arcsin(-x^{4}-2x\cos(y)$ ,
we can see that the maximal domain must be : $Do_{x}=[-1,1]$ and $Do_{y}=[\frac{1}{2}(3\pi) , \frac{1}{2}(7\pi)]$  . How does one calculate the neighbourhood of $p$?
$\displaystyle Dg(x,y)= \begin{pmatrix} \frac{-2(2x^{3}+\cos(y))}{(1-(x^{4}+2x\cos(y))^{2})^{1/2}} & \frac{2x\sin(y)}{(1-(x^{4}+2x\cos(y))^{1/2}} \end{pmatrix}$

how can I show the connection, if put $Df(x,y,g(x,y))$ then i get $0$ and that is not even invertible.
Thanks for any efforts to explain.

REPLY [1 votes]: Ad 1: $g(x,y)=\arcsin\bigl(-x^4-2x\cos (y)\bigr)$ is correct.
Ad 2: One has to determine the maximal connected set in the $(x,y)$-plane  containing $(0,0)$, on which the auxiliary function
$$h(x,y):=-x^4-2x\cos(y)$$
has an absolute value $<1$. To this end I drew the curves $h(x,y)=-1$, $h(x,y)=0$,  and $h(x,y)=1$ with the help of Mathematica. Here is the result:
contour http://www.math.ethz.ch/~blatter/contourplot.jpg
The domain you are looking for is the infinite wavy strip going vertically upwards, minus the holes.
Ad 3: You computed correctly the gradient $\nabla g(x,y)$. It's coordinates are the coefficients of the differential $dg$, when expressed as a linear combination of the coordinate differentials: $dg=g_x\ dx+g_y\ dy$.
There is no connection between the differential $df=f_x\ dx+f_y\ dy+ f_z\ dz$ and the differential $dg$ in variable terms, because these differentials live in completely different spaces. If, however, you are given a point $p$ on the surface $S$ defined by the equation $f(x,y,z)=0$ then there is a relation between the differentials $df(p)$ and $dg(p')$, where $p'$ denotes the point $p$ projected onto the $(x,y)$-plane. This relation is best viewed in terms of partial derivatives, namely
$$g_x(p')=-{f_x(p)\over f_z(p)}\ ,\qquad g_y(p')=-{f_y(p)\over f_z(p)}\ .$$
You can easily check that for $p=(0,0,0)$, $p'=(0,0)$ everything is o.k.


TITLE: Does the complex logarithm have a primitive on $\operatorname{Re}z >0$
QUESTION [1 upvotes]: If $\log:\mathbb{C} \setminus(-\infty,0]\rightarrow \mathbb{C}$ is the principal branch of the complex logarithm, does it then have a primitive on $\{z \in \mathbb{C} : \operatorname{Re}z >0$}?
Can someone help me with this question?

REPLY [1 votes]: Yes, of course: the region is simply connected and the logarithm is holomorphic over it.
An antiderivative is $f(z)=z\log z-z$.


TITLE: 1-form $\theta=y_{1}dx^1+y_2dx^2$ conjugate momenta
QUESTION [1 upvotes]: I'm considering on cotangent bundle of a two-dimensional variety where in canonical coordinates $(x^i,y_i)$ is defined in the 1-form
$$\theta=y_{1}dx^1+y_2dx^2$$
let new coordinate:
$$x^1=q^1\cosh(q^2)$$
$$x^2=q^1\sinh(q^2)$$
I have to determinate:
1) the conjugate momenta $(p_{\alpha})$ concerning to $(q^{\alpha})$
2) the components of $\theta(q^{\alpha},p_{\alpha})$.
I think I can replace:
$$dx^1=\cosh(q^2)dq^1+q^1\sinh(q^2)dq^2$$
$$dx^2=\sinh(q^2)dq^1+q^1\cosh(q^2)dq^2$$
Unfortunately I know the definition of conjugate momenta  only in Hamiltonian mechanics $p_{\mu}=\frac{\partial L}{\partial u^{\mu}}$ and I do not know how  to go on here.
 I looked for a definition but I did not find it.

REPLY [2 votes]: In Hamiltonian mechanics, the conjugate momenta are the cotangent vectors. When the tautological one-form $\theta$ is written as $$\theta=\sum_i y_idx_i$$ in canonical coordinates $(x^i,y_i)$, the canonical momenta are precisely $y_i$.
You may refer to equation $(4)$ of the following answer on a physics stackexchange post to see how conjugate momenta transforms between coordinates: https://physics.stackexchange.com/questions/176555/momentum-is-a-cotangent-vector/176578#176578 . Remember that there is a hidden summation over all $i$ on the right-hand-side of that equation.
The $q^i$ in that answer corresponds to $x^i$ in your question; the $p_i$ in that answer corresponds to $y_i$ in your question; the $q'^j$ in that answer corresponds to $q^j$ in your question; the $p_j'$ in that question corresponds to $p_j$ in your question.


TITLE: Proof Strategies on P versus BPP
QUESTION [7 upvotes]: Typically to show $P=NP$, one has to show an NP complete problem has a polynomial time solution and to show $P\neq NP$, has to show an NP complete problem has superpolynomial lower bound. These are broadly the general techniques.
For showing $P=BPP$ or $P\neq BPP$ what strategies can be used or used? It is not like there is one problem in BPP that can either be shown to be derandomized or not be derandomized that solves the question.

REPLY [7 votes]: Although there aren't any problems known to be $\mathsf{BPP}$-complete (and Sipser gave an oracle relative to which $\mathsf{BPP}$ doesn't have complete problems), one topic to look at here is pseudorandom generators. The existence of a good enough pseudorandom generator implies $\mathsf{BPP} = \mathsf{P}$. This isn't $\mathsf{BPP}$-complete, but it does have the feature that a single algorithm could show $\mathsf{BPP}=\mathsf{P}$.
Also, although not $\mathsf{BPP}$-complete, Polynomial Identity Testing is a good single problem in $\mathsf{BPP}$ to focus on derandomizing. Many problems in $\mathsf{BPP}$ are actually in $\mathsf{RP}$ or $\mathsf{coRP}$, often due to the Schwarz-Zippel Lemma (in fact, there are apparently very few known candidates that are known to be in $\mathsf{BPP}$ but not in $\mathsf{RP} \cup \mathsf{coRP}$, see this related question), so derandomizing PIT would derandomize a whole bunch of problems. Furthermore, derandomizing PIT is known to imply strong lower bounds on $\mathsf{NEXP}$.


TITLE: Carter Subgroups and Projectors
QUESTION [0 upvotes]: R. Carter prooved that in finite soluble groups $G$ Carter subgroups $C$ exist and that they are conjugated. Furthermore they are exactly the nilpotent projectors: For every normal subgroup $N$ of $G$ the factor group $CN/N$ is maximal nilpotent in $G/N$.
My question is whether in non-finite soluble groups Carter subgroups (if they exist) are nilpotent projectors.
They are maximal nilpotent also in the infinte case and also for non-solvable groups.

REPLY [1 votes]: There are different definitions of Carter subgroups in infinite groups. Thus the Carter subgroups of a generalized soluble group are the
locally nilpotent abnormal subgroups (see, for example, Journal of Algebra
Volume 297, Issue 1, 1 March 2006, Pages 273-291, Abnormal subgroups and Carter subgroups in some classes of infinite groups L.A.KurdachenkoaJ.Otal J,A.Russoc, G.Vincenzid.). See also L. A.  Kurdachenko and  I. Ya.  Subbotin.  Abnormal subgroups and Carter subgroups in some infinite groups,  Algebra and Discrete Mathematics,  Number 1.  (2005).  pp.  63 – 77, and
L.  A.  Kurdachenko,  J.  Otal,  I.  Ya.  Subbotin.  Abnormal,  pronormal,  contranormal,  and Carter subgroups in some generalized minimax groups,  Communications in Algebra,  Volume 33,  Number 12 (2005), 4595 – 4616.


TITLE: Limit sequence sets
QUESTION [4 upvotes]: In my measure theory book I came across the following definition:
Let $(A_n)_{n\ge1}$ be a sequence of subsets of some set $X$. Define:
$\limsup_{n\to\infty} A_n:=\bigcap_{n\ge1}\bigcup_{k\ge n}A_k$
$\liminf_{n\to\infty} A_n:=\bigcup_{n\ge1}\bigcap_{k\ge n}A_k$
Call the sequence convergent if $\limsup_{n\to\infty} A_n=\liminf_{n\to\infty} A_n$ , in which case we define $\lim_{n\to\infty} A_n:=\limsup_{n\to\infty} A_n$
My question is, does this notion of convergence correspond to some sort of metric on the set of subsets of $X$, or is it completely unrelated to the usual concept of a limit? Thanks

REPLY [0 votes]: I agree with @Marek's answer that we do not really need to look at it topologically at all (there is a general notion of convergence spaces, e.g.). There is however one context where it does correspond to a metric convergence: the so-called Hausdorff metric on the hyperspace of a compact metric space (which is the set of non-empty closed subsets of that space, a topological analogue of a powerset). IIRC, your notion of convergence and the one induced by the Hausdorff metric coincide. But the set-theoretic one is much more general.
Also, I seem to recall that if we consider $\mathcal{P}(X)$ to be topologized like $\{0,1\}^X$, identifying a set and its characteristic function, and using the product topology, we get this notion of convergence as well. http://en.wikipedia.org/wiki/Limit_superior_and_limit_inferior seems to confirm this.


TITLE: Relative distance to prime numbers
QUESTION [0 upvotes]: Let $p_{n,1}$ be the next biggest prime for $n \in \mathbb{N}$, $p_{n,2}$ the next biggest but one and so on. (e.g. $p_{4,1} = 5$, $p_{4,2} = 7$, ...)
Are there $n,m \in \mathbb{N}, n\neq m$ so that
$$p_{n,j}-n=p_{m,j}-m$$
for each $j\in\mathbb{N}$?

REPLY [1 votes]: There are prime gaps of arbitrary size (e.g. $k!+2,...,k!+k$ are all composite). If there were such a pair $m,n$ it would mean that the pattern of prime gaps repeats with a period of $|m-n|$, so arbitrarily large prime gaps would not be possible.


TITLE: Geometric interpretations of the quotient rule and reciprocal rule.
QUESTION [4 upvotes]: I have been reviewing basic calculus by working through Gilbert Strang's book "Calculus". My full time job is as a programmer, but I tutor calculus on the side. Professor Strang has kindly made the pdfs of the book, solutions manual, and study guide available for free https://ocw.mit.edu/resources/res-18-001-calculus-online-textbook-spring-2005/textbook/
I understand his 'regular' proofs of the reciprocal rule,
$$\frac{d}{{dx}}\left( {\frac{1}{{v\left( x \right)}}} \right) = \frac{{ - dv/dx}}{{{v^2}}}$$
and the quotient rule,
$$\frac{d}{{dx}}\left( {\frac{{u\left( x \right)}}{{v\left( x \right)}}} \right) = \frac{{v\frac{{du}}{{dx}} - u\frac{{dv}}{{dx}}}}{{{v^2}}}$$
however... I'm struggling to understand what appears to be his informal geometric derivation of both of these rules from figure 2.14, pg  74:

I know how to derive that $\frac{1}{{v + \Delta v}} - \frac{1}{v}$ is equal to $\frac{{ - \Delta v}}{{v\left( {v + \Delta v} \right)}}$, and that $\frac{{u + \Delta u}}{{v + \Delta v}} - \frac{u}{v} = \frac{{v\Delta u - u\Delta v}}{{v\left( {v + \Delta v} \right)}}$. I also know how to get from those equalities to the reciprocal rule and quotient rule. I just have not been able to figure out an intuitive way to understand the reciprocal rule and quotient rule geometrically from figure 2.14.
I found a way to use figure 2.14 and geometry to derive $\frac{1}{{v + \Delta v}} - \frac{1}{v} = \frac{{ - \Delta v}}{{v\left( {v + \Delta v} \right)}}$ and
$\frac{{ - \Delta v}}{{v\left( {v + \Delta v} \right)}}$. I couldn't think of a geometric way to derive $\frac{{u + \Delta u}}{{v + \Delta v}} - \frac{u}{v} = \frac{{v\Delta u - u\Delta v}}{{v\left( {v + \Delta v} \right)}}$.
Basically, the best I was able to do for the numerator of the difference quotient for the reciprocal rule from figure 2.14 was show that a geometric derivation of that equation is consistent with the algebraic definition.
Here's the best I could come up with, using a modified version of figure 2.14 that I made in paint:

For the reciprocal rule (left side of the and its top equation).
$$\text{Area}_{red - triangle} = \frac{{\Delta v}}{2}$$
$$\text{Area}_{blue - triangle} = \frac{v}{2}$$
$$\text{Area}_{red - triangle} + \text{Area}_{blue - triangle} = \frac{{v + \Delta v}}{2}$$
$$v + \Delta v = 2\left( {\text{Area}_{red - triangle}} + \text{Area}_{blue - triangle} \right)$$
$$v = 2\text{Area}_{blue - triangle}$$
$$\frac{1}{{v + \Delta v}} = \frac{1}{{2\left( {Are{a_{red - triangle}} + Are{a_{blue - triangle}}} \right)}}$$
$$\frac{1}{v} = \frac{1}{{2\text{Area}_{blue - triangle}}}$$
$$\frac{1}{{v + \Delta v}} = \frac{1}{{2\left( {Are{a_{red - triangle}} + Are{a_{blue - triangle}}} \right)}}$$
$$\frac{1}{{v + \Delta v}} - \frac{1}{v} = \frac{1}{2}\left( {\frac{{ - Are{a_{red - triangle}}}}{{\left( {Are{a_{red - triangle}} + Are{a_{blue - triangle}}} \right)Are{a_{blue - triangle}}}}} \right)$$
$$\frac{1}{{v + \Delta v}} - \frac{1}{v} = \frac{1}{2}\left[ {\frac{{ - \frac{{\Delta v}}{2}}}{{\left( {\frac{{v + \Delta v}}{2}} \right)\frac{v}{2}}}} \right] = \frac{{ - \Delta v}}{{\left( {v + \Delta v} \right)\frac{v}{2}}}$$
From there... I know how to derive the reciprocal rule... taking the limit of the difference quotient as $\Delta x \rightarrow 0$
Basically seems like circular reasoning... I assume that Professor Strang included the figure to give students an intuitive, geometric feel of the quotient rule and reciprocal rule, considering that Professor Strang's informal geometric derivation of the product rule is intuitive (also... why include figure 2.14 at all if it isn't meant to help readers gain an intuitive grasp of the reciprocal and quotient rules). The pdf of his textbook is in black and white, which makes figure 2.13 on page 72 difficult to read. Here is a re-creation of figure 2.13 that I put together using paint:

And the product rule plus an informal proof of it:
If $u = u(x)$ and $v = v(x)$ (assuming u and v are differentiable functions of x):
$$\frac{d}{{dx}}\left( {uv} \right) = u\frac{{dv}}{{dx}} + v\frac{{du}}{{dx}}$$
Informal 'proof':
$$\frac{d}{{dx}}\left( {uv} \right) = \mathop {\lim }\limits_{h \to 0} \frac{{u\left( {x + h} \right)v\left( {x + h} \right) - u\left( x \right)v(x)}}{h}$$
As $h \to 0$,$\Delta u \to 0{\text{ and }}\Delta v \to h$
From 'Calculus' by Gilbert Strang:

The important change in area are the two strips $u \Delta v$ and $v \Delta u$. The corner area $\Delta u \Delta v$ is much smaller. When we divide by $\Delta x$ (h), the strips give $u \frac{\Delta v}{\Delta x}$ and $v \frac{\Delta u}{\Delta x}$. The corner gives $\Delta u \frac{Delta v}{\Delta x}$, which approaches zero. The extra area comes from the whole side strip.

I would greatly appreciate it if someone could help me figure out a better way to interpret figure 2.14. I know it isn't really essential for me to have an intuitive feel of the quotient rule or the reciprocal rule, however it drives me pretty crazy if I can't figure something out.

REPLY [3 votes]: I don't know if this is great.
$v = \frac {1}{u}$

The two rectangles are equal area.
$u(-dv) = (v-dv) du\\
dv(du - u=) = \frac {1}{u} du\\
dv = -\frac {1}{u(u-du)}\ du$
Next
$v = \frac {a}{u}$

$uv = a\\
(u + du)(v+dv) = (a+da)\\
u\ dv + v\ du + dv\ du = da\\
dv(u + du) = da - \frac {a}{u}\ du\\
dv(u + du) = \frac {u\ da - a\ du}{u}\\
dv = \frac {u\ da - a\ du}{u(u + du)}$


TITLE: bayesian hyperpriors central limit theorem analogy
QUESTION [1 upvotes]: Let's say I have some distribution F, and then put a prior on a parameter of that distribution by using some prior distribution P1. Then let's say I put a hyperprior on that hyperparamter by using a distribution P2. To be concrete, think of a beta-binomial model.
But then let's say we continue putting priors on the parameters and on those parameters, etc. in the limit that we go to infinitely many levels of priors. Are there any kinds of theorems, etc. or interesting results related to doing this many times? In particular is there any kind of central limit theorem analogy such that if I repeat this toward infinitely many times, having hyperhyperhyper---hyperpriors on things, that I would end up getting some kind of limiting distribution for F?

REPLY [1 votes]: Practically speaking, putting deeper and deeper layers in the hierarchy doesn't do much good, because the data tend to have little to say about the deeper levels.
Adding a few more hyperpriors could change the amount of data needed to get good estimates from 100s to 10000s very quickly.
Never-the-less, putting a hyper prior on a parameter is just placing a mixture distribution on the distribution below it, for example, in the setting:
\begin{equation}
\begin{split}
Y | \mu_1 & \sim N(\mu_1,\sigma^2_1)\\
\mu_1 & \sim N(\mu_2,\sigma^2_2)
\end{split}
\end{equation}
You can see $\int_{-\infty}^\infty P[Y|\mu_1]P[\mu_1]d\mu_1 = P[Y]$ is still just a distribution on $Y$; one with some of the responsibility of specifying $\mu_1$ removed, but nevertheless still just a sampling distribution on the data.
One thing to note is that in this setting the exact distribution for $Y$ after integrating out $\mu_1$ is $N(\mu_2,\sigma_1^2+\sigma_2^2)$. So, for example, if you specified a hierarchical model like:
\begin{equation}
\begin{split}
Y | \mu_1 & \sim N(\mu_1,\sigma^2_1)\\
\mu_1 | \mu_2 & \sim N(\mu_2,\sigma^2_2)\\
\mu_2 | \mu_3 & \sim N(\mu_3,\sigma^2_3)\\
& ...\\
\mu_{n-1} | \mu_n & \sim N(\mu_n,\sigma^2_n)\\
\end{split}
\end{equation}
The scenario you just described is happening, and the marginal distribution of $Y$ is:
\begin{equation}
Y \sim N(\mu_n, \sum_{i=1}^n \sigma^2_i)
\end{equation}
So in essence, placing multiple hyper-priors in deeper and deeper sequence just increasingly "mixes" your base distribution into a more diffuse one.


TITLE: A 4x4 matrix representation of SU(3)?
QUESTION [5 upvotes]: Is it possible to find a representation of the infinitesimal generators of the special unitary group SU(3) that contains 4 by 4 matrices, by say taking a Kronecker product of its irreducible representation(s) with itself?
I know this is possible for SU(2), where one can express the three 4 by 4 matrices spanning the unit quaternion group in terms of some of the generators of SU(4), which are 4 by 4 matrices as well.
I am trying to do the same for SU(3). This question is motivated by the investigation of higher dimensional gauge theories. Thanks.

REPLY [1 votes]: As noted by the accepted answer and the comments, the answer is no.
Note, we can prove this without using Young Tableaux: we can check the possible dimensions as noted in Jyrki's comment above by directly using the known dimension formula for $SU(3)$:

The irreducible representations are indexed by a pair of non-negative
  integers $(m_1,m_2)$ and the dimension of the irreducible
  representation is given by
\begin{align}
\dim(V_{m_1,m_2}) = \frac{1}{2}(m_1+1)(m_2+1)(m_1+m_2+2)
\end{align}

One checks that there is no pair of non-negative integers that gives $\dim(V_{m_1,m_2})=4$ by testing the first few (and only) possibilities directly.


TITLE: Homemade Spectrometer
QUESTION [7 upvotes]: Recently I have had ideas of how to build a spectroscope, but I'm not sure if it will work. As can be seen in the diagram, the experiment is simple: it consists of a laser that generates the light that passes over a gas in a closed tube sample and the light goes straight into a prism which, according to one of the most basic laws of physics, decompose light. If you can share your thoughts about my project, if it will work, if it is efficient or other issues, I appreciate it. Felipe

REPLY [0 votes]: The experiment could work if only the gas inside the spectre would be thin enough to let the light through. If the gas is thick then it wold block some of the light making it flicker.


TITLE: if $U\cup W=V$ then $U=V$ or $W=V$
QUESTION [0 upvotes]: Let $U,W$ two subspaces in $V$. Assuming that $U\cup W = V$, show that: $U=V$ or $W=V$.

So, by definition of union:
$$U \cup W = \left\{ {u + w|u \in U,w \in W} \right\}$$

How to proceed?
And a technical issue: Is $U \cup W$ equivalent to $U + W$?

EDIT:

Consider the following scenario (Following @Learner approach):
$U = V \backslash \{x\}$ and $W = V \backslash \{y\}$.
$U\cup W = V$, but none of the subspaces is equal to $V$.
Where is the error?

REPLY [3 votes]: You can show more generally that $U\cup W$ can only be a vector space if one of $U,W$ is contained in the other, in which case the union is of course the latter (larger) of the two subspaces. To prove this, suppose to the contrary that neither of $U,W$ is contained in the other; choose $u\in U\setminus W$ and $w\in W\setminus U$, and prove that $u+w\notin U\cup W$ for a contradiction.


TITLE: Why particles are going clockwise in most synchrotrons?
QUESTION [1 upvotes]: First I'm sorry for my poor choice of words, I'm not into physics so I'm lacking of appropriate words.
I'm doing some personal research on synchrotrons, synchrotron radiation and all that stuff. It appears that on many synchrotron I looked at, particles in the storage ring are going clockwise. I know that ESRF, Diamond and SOLEIL are going clockwise.
I think there is only at SPRing-8 and SESAME they're going counter-clockwise.
My point is, is there a reason for this ? Interests of going clockwise vs counter-clockwise ?
Thanks,

REPLY [2 votes]: No fundamental reasons. In fact a number of colliders operate simultaneously with beams in both directions. At the design stage the choice might be driven by civil engineering constraints for instance for the positioning of the  injector.
It is also interesting to note that in existing machines the beam direction can be switched by changing the polarity of the ring or by injecting antiparticles. Clearly at a light source all the light lines will then point in the wrong direction, and/or if a collimation system is present, it may not effectively absorb secondary showers.
The fact that a (booster) ring or a linac can be reversed depends on what kind of accelerating cavities are employed. If travelling waves cavities are in place this will be impossible, but if they use standing waves there is no problem. An example of such booster ring is the CERN PS, which during LEP times was used to accelerate both $e^+$ and $e^-$ alternatively. The Fermilab main injector ring accelerated both protons and antiprotons for the Tevatron. Concerning linac, proposals for recirculating linear accelerator (RLA) in "dogbone" configuration (with particles entering from both sides) were made as a part of the neutrino factory and muon collider.


TITLE: Sturm-Liouville and Continuity
QUESTION [1 upvotes]: If you have a differential equation
$$ y'' + R(x)y' + (Q(x) + \lambda P(x))y = 0$$ on some interval $(a,b)$ why must the coefficient functions be continuous on this interval? My guess is that if you are trying to solve the equation for some $y(x)$ valid on $(a,b)$, you don't really want to be multiplying that solution by functions that aren't continuous since you want a valid solution $y(x)$ for all $x \in (a,b)$.
Next, if we multiply the above second order differential equation by the integrating factor
$$ r(x) = e^{\int R(x)dx}$$
and use the product rule to simplify we get
$$(r(x)y')' + (q(x) + \lambda p(x)) = 0$$
where $q(x) = Q(x)e^{\int R(x)dx}$ and $p(x) = P(x)e^{\int R(x)dx}$. This is Sturm-Liouville form.
Why must $p, q, r,$ and $r'$ be continuous on $(a,b)$. My guess is the same the above response. My book also specifies that $r(x) > 0$ and $p(x) > 0$. Why are these conditions necessary? I'd guess that if $r=0$ then we lose the second order part of the differential equation. If $p = 0$ then we lose the $\lambda$ part of the equation. But why can't they be negative?

REPLY [2 votes]: The usual theorems on existence and uniqueness of solutions for an equation
$$
y''=f(x,y,y')
$$
require $f$ to be continuous. When the equation is
$$
y'' = -R(x)y' - (Q(x) - \lambda P(x))y
$$
this means that you want $P$, $Q$ and $R$ continuous.
Also, in general you want your solution to be $C^2$, which means that the right hand side must be continuous.
Without the continuity condition, the definition of solution and the results of existence and uniqueness of solution are more complicated. Consider for instance the equation $y'=p(x)y$ where $p(x)=0$ if $x<0$, $p(x)=1$ if $x\ge0$. The solution is
$$
y(x)=\begin{cases} C & x<0,\\ C\,e^x & x\ge0,\end{cases}
$$
which is not differentiable at $x=0$ unless $C=0$. So, in what sense does $y$ satisfy the equation at $x=0$?


TITLE: What's the posterior for mutivariate lognormal with covar known?
QUESTION [2 upvotes]: I know the univariate case but not the multivariate case.
Suppose we have a multivariate lognormal dist:
$$ \boldsymbol{X} \sim \text{lognormal }(\boldsymbol{\mu}, \boldsymbol{\Sigma}) $$
where $\boldsymbol{\Sigma}$ is known and we have a multivariate Normal as the prior:
$$ \boldsymbol{\mu} \sim \mathcal{N}(\boldsymbol{\theta}, \boldsymbol{\Delta}) $$
Then what's the posterior with observation $\boldsymbol{x_0}$?

REPLY [2 votes]: If you observe $\boldsymbol{X}$, you've got the same information as if you've observed $\log\boldsymbol{X}$.  So that reduces it to a normal distribution with a normal prior on the mean.