A couple of new results
authorpaulson <lp15@cam.ac.uk>
Mon Apr 09 17:20:58 2018 +0100 (17 months ago)
changeset 679708c012a49293a
parent 67969 83c8cafdebe8
child 67971 e9f66b35d636
A couple of new results
src/HOL/Analysis/Determinants.thy
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Computational_Algebra/Formal_Power_Series.thy
     1.1 --- a/src/HOL/Analysis/Determinants.thy	Mon Apr 09 15:20:11 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Determinants.thy	Mon Apr 09 17:20:58 2018 +0100
     1.3 @@ -197,7 +197,7 @@
     1.4    by (simp add: det_diagonal mat_def)
     1.5  
     1.6  lemma det_0 [simp]: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0"
     1.7 -  by (simp add: det_def prod_zero)
     1.8 +  by (simp add: det_def prod_zero power_0_left)
     1.9  
    1.10  lemma det_permute_rows:
    1.11    fixes A :: "'a::comm_ring_1^'n^'n"
    1.12 @@ -815,20 +815,16 @@
    1.13        apply (simp only: ab_left_minus add.assoc[symmetric])
    1.14        apply simp
    1.15        done
    1.16 -    from c ci
    1.17      have thr0: "- row i A = sum (\<lambda>j. (1/ c i) *s (c j *s row j A)) (?U - {i})"
    1.18 -      unfolding sum.remove[OF fU iU] sum_cmul
    1.19 -      apply -
    1.20        apply (rule vector_mul_lcancel_imp[OF ci])
    1.21 -      apply (auto simp add: field_simps)
    1.22 -      unfolding *
    1.23 -      apply rule
    1.24 +      using c ci  unfolding sum.remove[OF fU iU] sum_cmul
    1.25 +      apply (auto simp add: field_simps *)
    1.26        done
    1.27      have thr: "- row i A \<in> span {row j A| j. j \<noteq> i}"
    1.28        unfolding thr0
    1.29        apply (rule span_sum)
    1.30        apply simp
    1.31 -      apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+
    1.32 +      apply (rule span_mul [where 'a="real^'n"])
    1.33        apply (rule span_superset)
    1.34        apply auto
    1.35        done
    1.36 @@ -869,7 +865,7 @@
    1.37    have thd0: "det (\<chi> i. if i = k then row k A + (\<Sum>i \<in> ?Uk. x $ i *s row i A) else row i A) = det A"
    1.38      apply (rule det_row_span)
    1.39      apply (rule span_sum)
    1.40 -    apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+
    1.41 +    apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])
    1.42      apply (rule span_superset)
    1.43      apply auto
    1.44      done
     2.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Apr 09 15:20:11 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Apr 09 17:20:58 2018 +0100
     2.3 @@ -1289,7 +1289,8 @@
     2.4        have "prj1 (vf X - uf X) ^ DIM('M) = (\<Prod>i::'M \<in> Basis. prj1 (vf X - uf X))"
     2.5          by (rule prod_constant [symmetric])
     2.6        also have "\<dots> = (\<Prod>i\<in>Basis. vf X \<bullet> i - uf X \<bullet> i)"
     2.7 -        using prj1_idem [OF \<open>X \<in> \<D>\<close>] by (auto simp: algebra_simps intro: prod.cong)
     2.8 +        apply (rule prod.cong [OF refl])
     2.9 +        by (simp add: \<open>X \<in> \<D>\<close> inner_diff_left prj1_idem)
    2.10        finally have prj1_eq: "prj1 (vf X - uf X) ^ DIM('M) = (\<Prod>i\<in>Basis. vf X \<bullet> i - uf X \<bullet> i)" .
    2.11        have "uf X \<in> cbox (uf X) (vf X)" "vf X \<in> cbox (uf X) (vf X)"
    2.12          using uvz [OF \<open>X \<in> \<D>\<close>] by (force simp: mem_box)+
     3.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Apr 09 15:20:11 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Apr 09 17:20:58 2018 +0100
     3.3 @@ -660,12 +660,18 @@
     3.4  lemma integrable_cmul: "f integrable_on S \<Longrightarrow> (\<lambda>x. c *\<^sub>R f(x)) integrable_on S"
     3.5    unfolding integrable_on_def by(auto intro: has_integral_cmul)
     3.6  
     3.7 -lemma integrable_on_cmult_iff:
     3.8 +lemma integrable_on_scaleR_iff [simp]:
     3.9 +  fixes c :: real
    3.10 +  assumes "c \<noteq> 0"
    3.11 +  shows "(\<lambda>x. c *\<^sub>R f x) integrable_on S \<longleftrightarrow> f integrable_on S"
    3.12 +  using integrable_cmul[of "\<lambda>x. c *\<^sub>R f x" S "1 / c"] integrable_cmul[of f S c] \<open>c \<noteq> 0\<close>
    3.13 +  by auto
    3.14 +
    3.15 +lemma integrable_on_cmult_iff [simp]:
    3.16    fixes c :: real
    3.17    assumes "c \<noteq> 0"
    3.18    shows "(\<lambda>x. c * f x) integrable_on S \<longleftrightarrow> f integrable_on S"
    3.19 -  using integrable_cmul[of "\<lambda>x. c * f x" S "1 / c"] integrable_cmul[of f S c] \<open>c \<noteq> 0\<close>
    3.20 -  by auto
    3.21 +  using integrable_on_scaleR_iff [of c f] assms by simp
    3.22  
    3.23  lemma integrable_on_cmult_left:
    3.24    assumes "f integrable_on S"
    3.25 @@ -676,6 +682,9 @@
    3.26  lemma integrable_neg: "f integrable_on S \<Longrightarrow> (\<lambda>x. -f(x)) integrable_on S"
    3.27    unfolding integrable_on_def by(auto intro: has_integral_neg)
    3.28  
    3.29 +lemma integrable_neg_iff: "(\<lambda>x. -f(x)) integrable_on S \<longleftrightarrow> f integrable_on S"
    3.30 +  using integrable_neg by fastforce
    3.31 +
    3.32  lemma integrable_diff:
    3.33    "f integrable_on S \<Longrightarrow> g integrable_on S \<Longrightarrow> (\<lambda>x. f x - g x) integrable_on S"
    3.34    unfolding integrable_on_def by(auto intro: has_integral_diff)
    3.35 @@ -2295,20 +2304,20 @@
    3.36    using assms negligible_subset by force
    3.37  
    3.38  lemma negligible_Un:
    3.39 -  assumes "negligible s"
    3.40 -    and "negligible t"
    3.41 -  shows "negligible (s \<union> t)"
    3.42 -  unfolding negligible_def
    3.43 -proof (safe, goal_cases)
    3.44 -  case (1 a b)
    3.45 -  note assms[unfolded negligible_def,rule_format,of a b]
    3.46 -  then show ?case
    3.47 -    apply (subst has_integral_spike_eq[OF assms(2)])
    3.48 -    defer
    3.49 -    apply assumption
    3.50 -    unfolding indicator_def
    3.51 -    apply auto
    3.52 -    done
    3.53 +  assumes "negligible S" and T: "negligible T"
    3.54 +  shows "negligible (S \<union> T)"
    3.55 +proof -
    3.56 +  have "(indicat_real (S \<union> T) has_integral 0) (cbox a b)"
    3.57 +    if S0: "(indicat_real S has_integral 0) (cbox a b)" 
    3.58 +      and  "(indicat_real T has_integral 0) (cbox a b)" for a b
    3.59 +  proof (subst has_integral_spike_eq[OF T])
    3.60 +    show "indicat_real S x = indicat_real (S \<union> T) x" if "x \<in> cbox a b - T" for x
    3.61 +      by (metis Diff_iff Un_iff indicator_def that)
    3.62 +    show "(indicat_real S has_integral 0) (cbox a b)"
    3.63 +      by (simp add: S0)
    3.64 +  qed
    3.65 +  with assms show ?thesis
    3.66 +    unfolding negligible_def by blast
    3.67  qed
    3.68  
    3.69  lemma negligible_Un_eq[simp]: "negligible (s \<union> t) \<longleftrightarrow> negligible s \<and> negligible t"
    3.70 @@ -3430,7 +3439,7 @@
    3.71        by (simp add: inner_simps field_simps)
    3.72      ultimately show ?thesis using False
    3.73        by (simp add: image_affinity_cbox content_cbox'
    3.74 -        prod.distrib[symmetric] prod_constant[symmetric] inner_diff_left)
    3.75 +        prod.distrib[symmetric] prod_constant[symmetric] inner_diff_left del: prod_constant)
    3.76    qed
    3.77  qed
    3.78  
    3.79 @@ -5235,19 +5244,21 @@
    3.80  
    3.81  lemma has_integral_Un:
    3.82    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
    3.83 -  assumes f: "(f has_integral i) s" "(f has_integral j) t"
    3.84 -    and neg: "negligible (s \<inter> t)"
    3.85 -  shows "(f has_integral (i + j)) (s \<union> t)"
    3.86 -proof -
    3.87 -  note * = has_integral_restrict_UNIV[symmetric, of f]
    3.88 -  show ?thesis
    3.89 -    unfolding *
    3.90 -    apply (rule has_integral_spike[OF assms(3)])
    3.91 -    defer
    3.92 -    apply (rule has_integral_add[OF f[unfolded *]])
    3.93 -    apply auto
    3.94 -    done
    3.95 -qed
    3.96 +  assumes f: "(f has_integral i) S" "(f has_integral j) T"
    3.97 +    and neg: "negligible (S \<inter> T)"
    3.98 +  shows "(f has_integral (i + j)) (S \<union> T)"
    3.99 +  unfolding has_integral_restrict_UNIV[symmetric, of f]
   3.100 +proof (rule has_integral_spike[OF neg])
   3.101 +  let ?f = "\<lambda>x. (if x \<in> S then f x else 0) + (if x \<in> T then f x else 0)"
   3.102 +  show "(?f has_integral i + j) UNIV"
   3.103 +    by (simp add: f has_integral_add)
   3.104 +qed auto
   3.105 +
   3.106 +lemma integral_Un [simp]:
   3.107 +  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   3.108 +  assumes "f integrable_on S" "f integrable_on T" "negligible (S \<inter> T)"
   3.109 +  shows "integral (S \<union> T) f = integral S f + integral T f"
   3.110 +  using has_integral_Un by (simp add: has_integral_Un assms integrable_integral integral_unique)
   3.111  
   3.112  lemma integrable_Un:
   3.113    fixes f :: "'a::euclidean_space \<Rightarrow> 'b :: banach"
     4.1 --- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Mon Apr 09 15:20:11 2018 +0100
     4.2 +++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Mon Apr 09 17:20:58 2018 +0100
     4.3 @@ -3434,10 +3434,12 @@
     4.4    then show ?thesis by simp
     4.5  next
     4.6    case (Suc m)
     4.7 -  have th0: "a^n = prod (\<lambda>k. a) {0..m}" "(a oo c) ^ n = prod (\<lambda>k. a oo c) {0..m}"
     4.8 +  have "(\<Prod>n = 0..m. a) oo c = (\<Prod>n = 0..m. a oo c)"
     4.9 +    using c0 fps_compose_prod_distrib by blast
    4.10 +  moreover have th0: "a^n = prod (\<lambda>k. a) {0..m}" "(a oo c) ^ n = prod (\<lambda>k. a oo c) {0..m}"
    4.11      by (simp_all add: prod_constant Suc)
    4.12 -  then show ?thesis
    4.13 -    by (simp add: fps_compose_prod_distrib[OF c0])
    4.14 +  ultimately show ?thesis
    4.15 +    by presburger
    4.16  qed
    4.17  
    4.18  lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)"