# HG changeset patch # User paulson # Date 1503662461 -3600 # Node ID 29d684ce23258101574999e7419e0e9555709cf3 # Parent 678774070c9b6423d172c1dc893c981c3c404df2 unscrambling of integrable_alt diff -r 678774070c9b -r 29d684ce2325 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Aug 25 11:10:03 2017 +0100 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Aug 25 13:01:01 2017 +0100 @@ -5061,80 +5061,67 @@ next let ?F = "\x. if x \ s then f x else 0" assume rhs: ?r - note as = conjunctD2[OF this,rule_format] let ?cube = "\n. cbox (\i\Basis. - real n *\<^sub>R i::'n) (\i\Basis. real n *\<^sub>R i)" - have "Cauchy (\n. integral (?cube n) (\x. if x \ s then f x else 0))" - proof (unfold Cauchy_def, safe, goal_cases) - case (1 e) + have "Cauchy (\n. integral (?cube n) ?F)" + unfolding Cauchy_def + proof (intro allI impI) + fix e::real + assume "e > 0" with rhs obtain B where "0 < B" and B: "\a b c d. ball 0 B \ cbox a b \ ball 0 B \ cbox c d \ norm (integral (cbox a b) ?F - integral (cbox c d) ?F) < e" by blast obtain N where N: "B \ real N" using real_arch_simple by blast - { - fix n - assume n: "n \ N" + have "ball 0 B \ ?cube n" if n: "n \ N" for n + proof - have "sum (op *\<^sub>R (- real n)) Basis \ i \ x \ i \ x \ i \ sum (op *\<^sub>R (real n)) Basis \ i" if "norm x < B" "i \ Basis" for x i::'n using Basis_le_norm[of i x] n N that by (auto simp add: field_simps sum_negf) - then have "ball 0 B \ ?cube n" + then show ?thesis by (auto simp: mem_box dist_norm) - } - then show ?case + qed + then show "\M. \m\M. \n\M. dist (integral (?cube m) ?F) (integral (?cube n) ?F) < e" by (fastforce simp add: dist_norm intro!: B) qed - from this[unfolded convergent_eq_Cauchy[symmetric]] guess i .. - note i = this[THEN LIMSEQ_D] - - show ?l unfolding integrable_on_def has_integral_alt'[of f] - apply (rule_tac x=i in exI) - apply safe - apply (rule as(1)[unfolded integrable_on_def]) - proof goal_cases - case (1 e) - then have *: "e/2 > 0" by auto - from i[OF this] guess N..note N =this[rule_format] - from as(2)[OF *] guess B..note B=conjunctD2[OF this,rule_format] + then obtain i where i: "(\n. integral (?cube n) ?F) \ i" + using convergent_eq_Cauchy by blast + have "\B>0. \a b. ball 0 B \ cbox a b \ norm (integral (cbox a b) ?F - i) < e" + if "e > 0" for e + proof - + have *: "e/2 > 0" using that by auto + then obtain N where N: "\n. N \ n \ norm (i - integral (?cube n) ?F) < e / 2" + using i[THEN LIMSEQ_D, simplified norm_minus_commute] by meson + obtain B where "0 < B" + and B: "\a b c d. \ball 0 B \ cbox a b; ball 0 B \ cbox c d\ \ + norm (integral (cbox a b) ?F - integral (cbox c d) ?F) < e / 2" + using rhs * by meson let ?B = "max (real N) B" - show ?case - apply (rule_tac x="?B" in exI) - proof safe + show ?thesis + proof (intro exI conjI allI impI) show "0 < ?B" - using B(1) by auto + using \B > 0\ by auto fix a b :: 'n - assume ab: "ball 0 ?B \ cbox a b" - from real_arch_simple[of ?B] guess n..note n=this - show "norm (integral (cbox a b) (\x. if x \ s then f x else 0) - i) < e" - apply (rule norm_triangle_half_l) - apply (rule B(2)) - defer - apply (subst norm_minus_commute) - apply (rule N[of n]) - proof safe - show "N \ n" - using n by auto + assume "ball 0 ?B \ cbox a b" + moreover obtain n where n: "max (real N) B \ real n" + using real_arch_simple by blast + moreover have "ball 0 B \ ?cube n" + proof fix x :: 'n assume x: "x \ ball 0 B" - then have "x \ ball 0 ?B" - by auto - then show "x \ cbox a b" - using ab by blast - show "x \ ?cube n" - using x - unfolding mem_box mem_ball dist_norm - apply - - proof (rule, goal_cases) - case (1 i) - then show ?case - using Basis_le_norm[of i x] \i \ Basis\ - using n - by (auto simp add: field_simps sum_negf) - qed - qed + have "\norm (0 - x) < B; i \ Basis\ + \ sum (op *\<^sub>R (-n)) Basis \ i\ x \ i \ x \ i \ sum (op *\<^sub>R n) Basis \ i" for i + using Basis_le_norm[of i x] n by (auto simp add: field_simps sum_negf) + then show "x \ ?cube n" + using x by (auto simp: mem_box dist_norm) + qed + ultimately show "norm (integral (cbox a b) ?F - i) < e" + using norm_triangle_half_l [OF B N] by force qed qed + then show ?l unfolding integrable_on_def has_integral_alt'[of f] + using rhs by blast qed lemma integrable_altD: