src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
author Manuel Eberl <eberlm@in.tum.de>
Thu, 25 Aug 2016 15:50:43 +0200
changeset 63721 492bb53c3420
parent 63680 6e1e8b5abbfa
child 63886 685fb01256af
permissions -rw-r--r--
More analysis lemmas
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
     1
(*  Author:     John Harrison
60428
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
     2
    Author:     Robert Himmelmann, TU Muenchen (Translation from HOL light); proofs reworked by LCP
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
     3
*)
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
     4
63594
bd218a9320b5 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63593
diff changeset
     5
section \<open>Henstock-Kurzweil gauge integration in many dimensions.\<close>
bd218a9320b5 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63593
diff changeset
     6
bd218a9320b5 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63593
diff changeset
     7
theory Henstock_Kurzweil_Integration
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 40513
diff changeset
     8
imports
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 40513
diff changeset
     9
  Derivative
61243
44b2d133063e exchange uniform limit and integral
immler
parents: 61222
diff changeset
    10
  Uniform_Limit
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 40513
diff changeset
    11
  "~~/src/HOL/Library/Indicator_Function"
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
    12
begin
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
    13
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
    14
lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
    15
  scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44176
diff changeset
    16
  scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36899
diff changeset
    17
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    18
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60396
diff changeset
    19
subsection \<open>Sundries\<close>
36243
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
    20
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
    21
lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
    22
lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
    23
lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
    24
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
    25
declare norm_triangle_ineq4[intro]
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
    26
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
    27
lemma simple_image: "{f x |x . x \<in> s} = f ` s"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
    28
  by blast
36243
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
    29
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
    30
lemma linear_simps:
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
    31
  assumes "bounded_linear f"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
    32
  shows
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
    33
    "f (a + b) = f a + f b"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
    34
    "f (a - b) = f a - f b"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
    35
    "f 0 = 0"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
    36
    "f (- a) = - f a"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
    37
    "f (s *\<^sub>R v) = s *\<^sub>R (f v)"
53600
8fda7ad57466 make 'linear' into a sublocale of 'bounded_linear';
huffman
parents: 53597
diff changeset
    38
proof -
8fda7ad57466 make 'linear' into a sublocale of 'bounded_linear';
huffman
parents: 53597
diff changeset
    39
  interpret f: bounded_linear f by fact
8fda7ad57466 make 'linear' into a sublocale of 'bounded_linear';
huffman
parents: 53597
diff changeset
    40
  show "f (a + b) = f a + f b" by (rule f.add)
8fda7ad57466 make 'linear' into a sublocale of 'bounded_linear';
huffman
parents: 53597
diff changeset
    41
  show "f (a - b) = f a - f b" by (rule f.diff)
8fda7ad57466 make 'linear' into a sublocale of 'bounded_linear';
huffman
parents: 53597
diff changeset
    42
  show "f 0 = 0" by (rule f.zero)
8fda7ad57466 make 'linear' into a sublocale of 'bounded_linear';
huffman
parents: 53597
diff changeset
    43
  show "f (- a) = - f a" by (rule f.minus)
8fda7ad57466 make 'linear' into a sublocale of 'bounded_linear';
huffman
parents: 53597
diff changeset
    44
  show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scaleR)
8fda7ad57466 make 'linear' into a sublocale of 'bounded_linear';
huffman
parents: 53597
diff changeset
    45
qed
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    46
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    47
lemma bounded_linearI:
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    48
  assumes "\<And>x y. f (x + y) = f x + f y"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
    49
    and "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
    50
    and "\<And>x. norm (f x) \<le> norm x * K"
36243
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
    51
  shows "bounded_linear f"
53600
8fda7ad57466 make 'linear' into a sublocale of 'bounded_linear';
huffman
parents: 53597
diff changeset
    52
  using assms by (rule bounded_linear_intro) (* FIXME: duplicate *)
51348
011c97ba3b3d move lemma Inf to usage point
hoelzl
parents: 50945
diff changeset
    53
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
    54
lemma bounded_linear_component [intro]: "bounded_linear (\<lambda>x::'a::euclidean_space. x \<bullet> k)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
    55
  by (rule bounded_linear_inner_left)
36243
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
    56
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
    57
lemma transitive_stepwise_lt_eq:
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
    58
  assumes "(\<And>x y z::nat. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z)"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
    59
  shows "((\<forall>m. \<forall>n>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n)))"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
    60
  (is "?l = ?r")
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
    61
proof safe
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    62
  assume ?r
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    63
  fix n m :: nat
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    64
  assume "m < n"
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    65
  then show "R m n"
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    66
  proof (induct n arbitrary: m)
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
    67
    case 0
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
    68
    then show ?case by auto
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
    69
  next
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    70
    case (Suc n)
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
    71
    show ?case
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    72
    proof (cases "m < n")
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    73
      case True
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    74
      show ?thesis
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    75
        apply (rule assms[OF Suc(1)[OF True]])
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60396
diff changeset
    76
        using \<open>?r\<close>
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
    77
        apply auto
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    78
        done
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    79
    next
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    80
      case False
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
    81
      then have "m = n"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
    82
        using Suc(2) by auto
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
    83
      then show ?thesis
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60396
diff changeset
    84
        using \<open>?r\<close> by auto
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    85
    qed
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
    86
  qed
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    87
qed auto
36243
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
    88
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
    89
lemma transitive_stepwise_gt:
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
    90
  assumes "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" "\<And>n. R n (Suc n)"
36243
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
    91
  shows "\<forall>n>m. R m n"
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    92
proof -
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    93
  have "\<forall>m. \<forall>n>m. R m n"
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    94
    apply (subst transitive_stepwise_lt_eq)
60384
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
    95
    apply (blast intro: assms)+
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    96
    done
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
    97
  then show ?thesis by auto
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
    98
qed
36243
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
    99
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   100
lemma transitive_stepwise_le_eq:
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   101
  assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   102
  shows "(\<forall>m. \<forall>n\<ge>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n))"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   103
  (is "?l = ?r")
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   104
proof safe
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   105
  assume ?r
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   106
  fix m n :: nat
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   107
  assume "m \<le> n"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   108
  then show "R m n"
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   109
  proof (induct n arbitrary: m)
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   110
    case 0
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   111
    with assms show ?case by auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   112
  next
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   113
    case (Suc n)
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   114
    show ?case
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   115
    proof (cases "m \<le> n")
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   116
      case True
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60396
diff changeset
   117
      with Suc.hyps \<open>\<forall>n. R n (Suc n)\<close> assms show ?thesis
60384
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
   118
        by blast
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   119
    next
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   120
      case False
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   121
      then have "m = Suc n"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   122
        using Suc(2) by auto
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   123
      then show ?thesis
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   124
        using assms(1) by auto
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   125
    qed
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   126
  qed
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   127
qed auto
36243
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   128
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   129
lemma transitive_stepwise_le:
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   130
  assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   131
    and "\<And>n. R n (Suc n)"
36243
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   132
  shows "\<forall>n\<ge>m. R m n"
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   133
proof -
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   134
  have "\<forall>m. \<forall>n\<ge>m. R m n"
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   135
    apply (subst transitive_stepwise_le_eq)
60384
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
   136
    apply (blast intro: assms)+
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   137
    done
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   138
  then show ?thesis by auto
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   139
qed
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   140
36243
027ae62681be Translated remaining theorems about integration from HOL light.
himmelma
parents: 36081
diff changeset
   141
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60396
diff changeset
   142
subsection \<open>Some useful lemmas about intervals.\<close>
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   143
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   144
lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   145
  using nonempty_Basis
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   146
  by (fastforce simp add: set_eq_iff mem_box)
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   147
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   148
lemma interior_subset_union_intervals:
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   149
  assumes "i = cbox a b"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   150
    and "j = cbox c d"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   151
    and "interior j \<noteq> {}"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   152
    and "i \<subseteq> j \<union> s"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   153
    and "interior i \<inter> interior j = {}"
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   154
  shows "interior i \<subseteq> interior s"
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   155
proof -
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   156
  have "box a b \<inter> cbox c d = {}"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   157
     using inter_interval_mixed_eq_empty[of c d a b] and assms(3,5)
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   158
     unfolding assms(1,2) interior_cbox by auto
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   159
  moreover
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   160
  have "box a b \<subseteq> cbox c d \<union> s"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   161
    apply (rule order_trans,rule box_subset_cbox)
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   162
    using assms(4) unfolding assms(1,2)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   163
    apply auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   164
    done
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   165
  ultimately
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   166
  show ?thesis
60384
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
   167
    unfolding assms interior_cbox
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
   168
      by auto (metis IntI UnE empty_iff interior_maximal open_box subsetCE subsetI)
49675
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   169
qed
d9c2fb37d92a tuned proofs;
wenzelm
parents: 49197
diff changeset
   170
63595
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   171
lemma interior_Union_subset_cbox:
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   172
  assumes "finite f"
63595
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   173
  assumes f: "\<And>s. s \<in> f \<Longrightarrow> \<exists>a b. s = cbox a b" "\<And>s. s \<in> f \<Longrightarrow> interior s \<subseteq> t"
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   174
    and t: "closed t"
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   175
  shows "interior (\<Union>f) \<subseteq> t"
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   176
proof -
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   177
  have [simp]: "s \<in> f \<Longrightarrow> closed s" for s
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   178
    using f by auto
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   179
  define E where "E = {s\<in>f. interior s = {}}"
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   180
  then have "finite E" "E \<subseteq> {s\<in>f. interior s = {}}"
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   181
    using \<open>finite f\<close> by auto
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   182
  then have "interior (\<Union>f) = interior (\<Union>(f - E))"
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   183
  proof (induction E rule: finite_subset_induct')
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   184
    case (insert s f')
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   185
    have "interior (\<Union>(f - insert s f') \<union> s) = interior (\<Union>(f - insert s f'))"
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   186
      using insert.hyps \<open>finite f\<close> by (intro interior_closed_Un_empty_interior) auto
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   187
    also have "\<Union>(f - insert s f') \<union> s = \<Union>(f - f')"
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   188
      using insert.hyps by auto
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   189
    finally show ?case
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   190
      by (simp add: insert.IH)
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   191
  qed simp
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   192
  also have "\<dots> \<subseteq> \<Union>(f - E)"
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   193
    by (rule interior_subset)
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   194
  also have "\<dots> \<subseteq> t"
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   195
  proof (rule Union_least)
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   196
    fix s assume "s \<in> f - E"
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   197
    with f[of s] obtain a b where s: "s \<in> f" "s = cbox a b" "box a b \<noteq> {}"
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   198
      by (fastforce simp: E_def)
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   199
    have "closure (interior s) \<subseteq> closure t"
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   200
      by (intro closure_mono f \<open>s \<in> f\<close>)
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   201
    with s \<open>closed t\<close> show "s \<subseteq> t"
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   202
      by (simp add: closure_box)
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   203
  qed
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   204
  finally show ?thesis .
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   205
qed
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   206
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   207
lemma inter_interior_unions_intervals:
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   208
    "finite f \<Longrightarrow> open s \<Longrightarrow> \<forall>t\<in>f. \<exists>a b. t = cbox a b \<Longrightarrow> \<forall>t\<in>f. s \<inter> (interior t) = {} \<Longrightarrow> s \<inter> interior (\<Union>f) = {}"
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   209
  using interior_Union_subset_cbox[of f "UNIV - s"] by auto
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60396
diff changeset
   210
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60396
diff changeset
   211
subsection \<open>Bounds on intervals where they exist.\<close>
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   212
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   213
definition interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   214
  where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   215
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   216
definition interval_lowerbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   217
   where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   218
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   219
lemma interval_upperbound[simp]:
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   220
  "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   221
    interval_upperbound (cbox a b) = (b::'a::euclidean_space)"
62343
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 62207
diff changeset
   222
  unfolding interval_upperbound_def euclidean_representation_setsum cbox_def
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   223
  by (safe intro!: cSup_eq) auto
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   224
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   225
lemma interval_lowerbound[simp]:
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   226
  "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   227
    interval_lowerbound (cbox a b) = (a::'a::euclidean_space)"
62343
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 62207
diff changeset
   228
  unfolding interval_lowerbound_def euclidean_representation_setsum cbox_def
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   229
  by (safe intro!: cInf_eq) auto
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   230
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   231
lemmas interval_bounds = interval_upperbound interval_lowerbound
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   232
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   233
lemma
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   234
  fixes X::"real set"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   235
  shows interval_upperbound_real[simp]: "interval_upperbound X = Sup X"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   236
    and interval_lowerbound_real[simp]: "interval_lowerbound X = Inf X"
62343
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 62207
diff changeset
   237
  by (auto simp: interval_upperbound_def interval_lowerbound_def)
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   238
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   239
lemma interval_bounds'[simp]:
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   240
  assumes "cbox a b \<noteq> {}"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   241
  shows "interval_upperbound (cbox a b) = b"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   242
    and "interval_lowerbound (cbox a b) = a"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   243
  using assms unfolding box_ne_empty by auto
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   244
59425
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   245
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   246
lemma interval_upperbound_Times:
59425
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   247
  assumes "A \<noteq> {}" and "B \<noteq> {}"
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   248
  shows "interval_upperbound (A \<times> B) = (interval_upperbound A, interval_upperbound B)"
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   249
proof-
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   250
  from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   251
  have "(\<Sum>i\<in>Basis. (SUP x:A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x:A. x \<bullet> i) *\<^sub>R i)"
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   252
      by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   253
  moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   254
  have "(\<Sum>i\<in>Basis. (SUP x:A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x:B. x \<bullet> i) *\<^sub>R i)"
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   255
      by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   256
  ultimately show ?thesis unfolding interval_upperbound_def
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   257
      by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod)
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   258
qed
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   259
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   260
lemma interval_lowerbound_Times:
59425
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   261
  assumes "A \<noteq> {}" and "B \<noteq> {}"
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   262
  shows "interval_lowerbound (A \<times> B) = (interval_lowerbound A, interval_lowerbound B)"
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   263
proof-
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   264
  from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   265
  have "(\<Sum>i\<in>Basis. (INF x:A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x:A. x \<bullet> i) *\<^sub>R i)"
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   266
      by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   267
  moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   268
  have "(\<Sum>i\<in>Basis. (INF x:A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x:B. x \<bullet> i) *\<^sub>R i)"
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   269
      by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   270
  ultimately show ?thesis unfolding interval_lowerbound_def
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   271
      by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod)
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   272
qed
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   273
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60396
diff changeset
   274
subsection \<open>Content (length, area, volume...) of an interval.\<close>
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   275
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   276
definition "content (s::('a::euclidean_space) set) =
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   277
  (if s = {} then 0 else (\<Prod>i\<in>Basis. (interval_upperbound s)\<bullet>i - (interval_lowerbound s)\<bullet>i))"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   278
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   279
lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   280
  unfolding box_eq_empty unfolding not_ex not_less by auto
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   281
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   282
lemma content_cbox:
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   283
  fixes a :: "'a::euclidean_space"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   284
  assumes "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   285
  shows "content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   286
  using interval_not_empty[OF assms]
54777
1a2da44c8e7d remove redundant constants
immler
parents: 54776
diff changeset
   287
  unfolding content_def
60384
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
   288
  by auto
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   289
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   290
lemma content_cbox':
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   291
  fixes a :: "'a::euclidean_space"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   292
  assumes "cbox a b \<noteq> {}"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   293
  shows "content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
60384
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
   294
    using assms box_ne_empty(1) content_cbox by blast
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   295
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   296
lemma content_real: "a \<le> b \<Longrightarrow> content {a..b} = b - a"
62343
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 62207
diff changeset
   297
  by (auto simp: interval_upperbound_def interval_lowerbound_def content_def)
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   298
61945
1135b8de26c3 more symbols;
wenzelm
parents: 61915
diff changeset
   299
lemma abs_eq_content: "\<bar>y - x\<bar> = (if x\<le>y then content {x .. y} else content {y..x})"
61204
3e491e34a62e new lemmas and movement of lemmas into place
paulson
parents: 61167
diff changeset
   300
  by (auto simp: content_real)
3e491e34a62e new lemmas and movement of lemmas into place
paulson
parents: 61167
diff changeset
   301
50104
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 49996
diff changeset
   302
lemma content_singleton[simp]: "content {a} = 0"
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 49996
diff changeset
   303
proof -
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   304
  have "content (cbox a a) = 0"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   305
    by (subst content_cbox) (auto simp: ex_in_conv)
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   306
  then show ?thesis by (simp add: cbox_sing)
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   307
qed
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   308
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   309
lemma content_unit[iff]: "content(cbox 0 (One::'a::euclidean_space)) = 1"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   310
 proof -
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   311
   have *: "\<forall>i\<in>Basis. (0::'a)\<bullet>i \<le> (One::'a)\<bullet>i"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   312
    by auto
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   313
  have "0 \<in> cbox 0 (One::'a)"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   314
    unfolding mem_box by auto
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   315
  then show ?thesis
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 57129
diff changeset
   316
     unfolding content_def interval_bounds[OF *] using setprod.neutral_const by auto
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   317
 qed
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   318
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   319
lemma content_pos_le[intro]:
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   320
  fixes a::"'a::euclidean_space"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   321
  shows "0 \<le> content (cbox a b)"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   322
proof (cases "cbox a b = {}")
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   323
  case False
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   324
  then have *: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   325
    unfolding box_ne_empty .
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   326
  have "0 \<le> (\<Prod>i\<in>Basis. interval_upperbound (cbox a b) \<bullet> i - interval_lowerbound (cbox a b) \<bullet> i)"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   327
    apply (rule setprod_nonneg)
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   328
    unfolding interval_bounds[OF *]
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   329
    using *
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   330
    apply auto
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   331
    done
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   332
  also have "\<dots> = content (cbox a b)" using False by (simp add: content_def)
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   333
  finally show ?thesis .
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   334
qed (simp add: content_def)
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   335
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   336
corollary content_nonneg [simp]:
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   337
  fixes a::"'a::euclidean_space"
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   338
  shows "~ content (cbox a b) < 0"
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   339
using not_le by blast
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   340
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   341
lemma content_pos_lt:
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   342
  fixes a :: "'a::euclidean_space"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   343
  assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   344
  shows "0 < content (cbox a b)"
54777
1a2da44c8e7d remove redundant constants
immler
parents: 54776
diff changeset
   345
  using assms
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   346
  by (auto simp: content_def box_eq_empty intro!: setprod_pos)
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   347
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   348
lemma content_eq_0:
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   349
  "content (cbox a b) = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i)"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   350
  by (auto simp: content_def box_eq_empty intro!: setprod_pos bexI)
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   351
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   352
lemma cond_cases: "(P \<Longrightarrow> Q x) \<Longrightarrow> (\<not> P \<Longrightarrow> Q y) \<Longrightarrow> Q (if P then x else y)"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   353
  by auto
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   354
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   355
lemma content_cbox_cases:
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   356
  "content (cbox a (b::'a::euclidean_space)) =
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   357
    (if \<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i then setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis else 0)"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   358
  by (auto simp: not_le content_eq_0 intro: less_imp_le content_cbox)
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   359
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   360
lemma content_eq_0_interior: "content (cbox a b) = 0 \<longleftrightarrow> interior(cbox a b) = {}"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   361
  unfolding content_eq_0 interior_cbox box_eq_empty
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   362
  by auto
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   363
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   364
lemma content_pos_lt_eq:
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   365
  "0 < content (cbox a (b::'a::euclidean_space)) \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
60394
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
   366
proof (rule iffI)
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   367
  assume "0 < content (cbox a b)"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   368
  then have "content (cbox a b) \<noteq> 0" by auto
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   369
  then show "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   370
    unfolding content_eq_0 not_ex not_le by fastforce
60394
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
   371
next
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
   372
  assume "\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i"
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
   373
  then show "0 < content (cbox a b)"
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
   374
    by (metis content_pos_lt)
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   375
qed
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   376
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   377
lemma content_empty [simp]: "content {} = 0"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   378
  unfolding content_def by auto
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   379
60762
bf0c76ccee8d new material for multivariate analysis, etc.
paulson
parents: 60621
diff changeset
   380
lemma content_real_if [simp]: "content {a..b} = (if a \<le> b then b - a else 0)"
bf0c76ccee8d new material for multivariate analysis, etc.
paulson
parents: 60621
diff changeset
   381
  by (simp add: content_real)
bf0c76ccee8d new material for multivariate analysis, etc.
paulson
parents: 60621
diff changeset
   382
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   383
lemma content_subset:
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   384
  assumes "cbox a b \<subseteq> cbox c d"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   385
  shows "content (cbox a b) \<le> content (cbox c d)"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   386
proof (cases "cbox a b = {}")
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   387
  case True
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   388
  then show ?thesis
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   389
    using content_pos_le[of c d] by auto
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   390
next
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   391
  case False
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   392
  then have ab_ne: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   393
    unfolding box_ne_empty by auto
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   394
  then have ab_ab: "a\<in>cbox a b" "b\<in>cbox a b"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   395
    unfolding mem_box by auto
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   396
  have "cbox c d \<noteq> {}" using assms False by auto
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   397
  then have cd_ne: "\<forall>i\<in>Basis. c \<bullet> i \<le> d \<bullet> i"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   398
    using assms unfolding box_ne_empty by auto
60394
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
   399
  have "\<And>i. i \<in> Basis \<Longrightarrow> 0 \<le> b \<bullet> i - a \<bullet> i"
61762
d50b993b4fb9 Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents: 61736
diff changeset
   400
    using ab_ne by auto
60394
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
   401
  moreover
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
   402
  have "\<And>i. i \<in> Basis \<Longrightarrow> b \<bullet> i - a \<bullet> i \<le> d \<bullet> i - c \<bullet> i"
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
   403
    using assms[unfolded subset_eq mem_box,rule_format,OF ab_ab(2)]
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
   404
          assms[unfolded subset_eq mem_box,rule_format,OF ab_ab(1)]
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
   405
      by (metis diff_mono)
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
   406
  ultimately show ?thesis
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
   407
    unfolding content_def interval_bounds[OF ab_ne] interval_bounds[OF cd_ne]
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60396
diff changeset
   408
    by (simp add: setprod_mono if_not_P[OF False] if_not_P[OF \<open>cbox c d \<noteq> {}\<close>])
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   409
qed
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   410
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   411
lemma content_lt_nz: "0 < content (cbox a b) \<longleftrightarrow> content (cbox a b) \<noteq> 0"
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44522
diff changeset
   412
  unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastforce
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   413
59425
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   414
lemma content_times[simp]: "content (A \<times> B) = content A * content B"
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   415
proof (cases "A \<times> B = {}")
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   416
  let ?ub1 = "interval_upperbound" and ?lb1 = "interval_lowerbound"
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   417
  let ?ub2 = "interval_upperbound" and ?lb2 = "interval_lowerbound"
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   418
  assume nonempty: "A \<times> B \<noteq> {}"
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   419
  hence "content (A \<times> B) = (\<Prod>i\<in>Basis. (?ub1 A, ?ub2 B) \<bullet> i - (?lb1 A, ?lb2 B) \<bullet> i)"
59425
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   420
      unfolding content_def by (simp add: interval_upperbound_Times interval_lowerbound_Times)
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   421
  also have "... = content A * content B" unfolding content_def using nonempty
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   422
    apply (subst Basis_prod_def, subst setprod.union_disjoint, force, force, force, simp)
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   423
    apply (subst (1 2) setprod.reindex, auto intro: inj_onI)
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   424
    done
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   425
  finally show ?thesis .
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   426
qed (auto simp: content_def)
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 58877
diff changeset
   427
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   428
lemma content_Pair: "content (cbox (a,c) (b,d)) = content (cbox a b) * content (cbox c d)"
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   429
  by (simp add: cbox_Pair_eq)
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   430
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   431
lemma content_cbox_pair_eq0_D:
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   432
   "content (cbox (a,c) (b,d)) = 0 \<Longrightarrow> content (cbox a b) = 0 \<or> content (cbox c d) = 0"
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   433
  by (simp add: content_Pair)
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   434
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   435
lemma content_eq_0_gen:
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   436
  fixes s :: "'a::euclidean_space set"
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   437
  assumes "bounded s"
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   438
  shows "content s = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. \<exists>v. \<forall>x \<in> s. x \<bullet> i = v)"  (is "_ = ?rhs")
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   439
proof safe
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   440
  assume "content s = 0" then show ?rhs
62390
842917225d56 more canonical names
nipkow
parents: 62343
diff changeset
   441
    apply (clarsimp simp: ex_in_conv content_def split: if_split_asm)
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   442
    apply (rule_tac x=a in bexI)
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   443
    apply (rule_tac x="interval_lowerbound s \<bullet> a" in exI)
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   444
    apply (clarsimp simp: interval_upperbound_def interval_lowerbound_def)
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   445
    apply (drule cSUP_eq_cINF_D)
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   446
    apply (auto simp: bounded_inner_imp_bdd_above [OF assms]  bounded_inner_imp_bdd_below [OF assms])
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   447
    done
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   448
next
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   449
  fix i a
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   450
  assume "i \<in> Basis" "\<forall>x\<in>s. x \<bullet> i = a"
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   451
  then show "content s = 0"
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   452
    apply (clarsimp simp: content_def)
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   453
    apply (rule_tac x=i in bexI)
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   454
    apply (auto simp: interval_upperbound_def interval_lowerbound_def)
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   455
    done
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   456
qed
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   457
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   458
lemma content_0_subset_gen:
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   459
  fixes a :: "'a::euclidean_space"
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   460
  assumes "content t = 0" "s \<subseteq> t" "bounded t" shows "content s = 0"
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   461
proof -
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   462
  have "bounded s"
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   463
    using assms by (metis bounded_subset)
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   464
  then show ?thesis
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   465
    using assms
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   466
    by (auto simp: content_eq_0_gen)
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   467
qed
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   468
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   469
lemma content_0_subset: "\<lbrakk>content(cbox a b) = 0; s \<subseteq> cbox a b\<rbrakk> \<Longrightarrow> content s = 0"
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   470
  by (simp add: content_0_subset_gen bounded_cbox)
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
   471
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   472
63593
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   473
lemma interval_split:
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   474
  fixes a :: "'a::euclidean_space"
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   475
  assumes "k \<in> Basis"
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   476
  shows
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   477
    "cbox a b \<inter> {x. x\<bullet>k \<le> c} = cbox a (\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) c else b\<bullet>i) *\<^sub>R i)"
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   478
    "cbox a b \<inter> {x. x\<bullet>k \<ge> c} = cbox (\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) c else a\<bullet>i) *\<^sub>R i) b"
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   479
  apply (rule_tac[!] set_eqI)
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   480
  unfolding Int_iff mem_box mem_Collect_eq
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   481
  using assms
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   482
  apply auto
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   483
  done
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   484
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   485
lemma content_split:
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   486
  fixes a :: "'a::euclidean_space"
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   487
  assumes "k \<in> Basis"
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   488
  shows "content (cbox a b) = content(cbox a b \<inter> {x. x\<bullet>k \<le> c}) + content(cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   489
proof cases
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   490
  note simps = interval_split[OF assms] content_cbox_cases
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   491
  have *: "Basis = insert k (Basis - {k})" "\<And>x. finite (Basis-{x})" "\<And>x. x\<notin>Basis-{x}"
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   492
    using assms by auto
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   493
  have *: "\<And>X Y Z. (\<Prod>i\<in>Basis. Z i (if i = k then X else Y i)) = Z k X * (\<Prod>i\<in>Basis-{k}. Z i (Y i))"
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   494
    "(\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i) = (\<Prod>i\<in>Basis-{k}. b\<bullet>i - a\<bullet>i) * (b\<bullet>k - a\<bullet>k)"
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   495
    apply (subst *(1))
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   496
    defer
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   497
    apply (subst *(1))
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   498
    unfolding setprod.insert[OF *(2-)]
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   499
    apply auto
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   500
    done
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   501
  assume as: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   502
  moreover
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   503
  have "\<And>x. min (b \<bullet> k) c = max (a \<bullet> k) c \<Longrightarrow>
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   504
    x * (b\<bullet>k - a\<bullet>k) = x * (max (a \<bullet> k) c - a \<bullet> k) + x * (b \<bullet> k - max (a \<bullet> k) c)"
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   505
    by  (auto simp add: field_simps)
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   506
  moreover
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   507
  have **: "(\<Prod>i\<in>Basis. ((\<Sum>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i) *\<^sub>R i) \<bullet> i - a \<bullet> i)) =
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   508
      (\<Prod>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i) - a \<bullet> i)"
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   509
    "(\<Prod>i\<in>Basis. b \<bullet> i - ((\<Sum>i\<in>Basis. (if i = k then max (a \<bullet> k) c else a \<bullet> i) *\<^sub>R i) \<bullet> i)) =
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   510
      (\<Prod>i\<in>Basis. b \<bullet> i - (if i = k then max (a \<bullet> k) c else a \<bullet> i))"
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   511
    by (auto intro!: setprod.cong)
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   512
  have "\<not> a \<bullet> k \<le> c \<Longrightarrow> \<not> c \<le> b \<bullet> k \<Longrightarrow> False"
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   513
    unfolding not_le
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   514
    using as[unfolded ,rule_format,of k] assms
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   515
    by auto
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   516
  ultimately show ?thesis
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   517
    using assms
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   518
    unfolding simps **
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   519
    unfolding *(1)[of "\<lambda>i x. b\<bullet>i - x"] *(1)[of "\<lambda>i x. x - a\<bullet>i"]
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   520
    unfolding *(2)
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   521
    by auto
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   522
next
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   523
  assume "\<not> (\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   524
  then have "cbox a b = {}"
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   525
    unfolding box_eq_empty by (auto simp: not_le)
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   526
  then show ?thesis
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   527
    by (auto simp: not_le)
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   528
qed
bbcb05504fdc HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents: 63540
diff changeset
   529
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60396
diff changeset
   530
subsection \<open>The notion of a gauge --- simply an open set containing the point.\<close>
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   531
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   532
definition "gauge d \<longleftrightarrow> (\<forall>x. x \<in> d x \<and> open (d x))"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   533
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   534
lemma gaugeI:
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   535
  assumes "\<And>x. x \<in> g x"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   536
    and "\<And>x. open (g x)"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   537
  shows "gauge g"
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   538
  using assms unfolding gauge_def by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   539
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   540
lemma gaugeD[dest]:
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   541
  assumes "gauge d"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   542
  shows "x \<in> d x"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   543
    and "open (d x)"
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   544
  using assms unfolding gauge_def by auto
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   545
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   546
lemma gauge_ball_dependent: "\<forall>x. 0 < e x \<Longrightarrow> gauge (\<lambda>x. ball x (e x))"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   547
  unfolding gauge_def by auto
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   548
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   549
lemma gauge_ball[intro]: "0 < e \<Longrightarrow> gauge (\<lambda>x. ball x e)"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   550
  unfolding gauge_def by auto
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   551
60466
7bd794d7c86b fixing more proofs
paulson <lp15@cam.ac.uk>
parents: 60463
diff changeset
   552
lemma gauge_trivial[intro!]: "gauge (\<lambda>x. ball x 1)"
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   553
  by (rule gauge_ball) auto
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   554
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   555
lemma gauge_inter[intro]: "gauge d1 \<Longrightarrow> gauge d2 \<Longrightarrow> gauge (\<lambda>x. d1 x \<inter> d2 x)"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   556
  unfolding gauge_def by auto
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   557
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   558
lemma gauge_inters:
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   559
  assumes "finite s"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   560
    and "\<forall>d\<in>s. gauge (f d)"
60585
48fdff264eb2 tuned whitespace;
wenzelm
parents: 60492
diff changeset
   561
  shows "gauge (\<lambda>x. \<Inter>{f d x | d. d \<in> s})"
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   562
proof -
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   563
  have *: "\<And>x. {f d x |d. d \<in> s} = (\<lambda>d. f d x) ` s"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   564
    by auto
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   565
  show ?thesis
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   566
    unfolding gauge_def unfolding *
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   567
    using assms unfolding Ball_def Inter_iff mem_Collect_eq gauge_def by auto
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   568
qed
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   569
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   570
lemma gauge_existence_lemma:
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   571
  "(\<forall>x. \<exists>d :: real. p x \<longrightarrow> 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. p x \<longrightarrow> q d x)"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   572
  by (metis zero_less_one)
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   573
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   574
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60396
diff changeset
   575
subsection \<open>Divisions.\<close>
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   576
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   577
definition division_of (infixl "division'_of" 40)
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   578
where
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   579
  "s division_of i \<longleftrightarrow>
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   580
    finite s \<and>
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   581
    (\<forall>k\<in>s. k \<subseteq> i \<and> k \<noteq> {} \<and> (\<exists>a b. k = cbox a b)) \<and>
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   582
    (\<forall>k1\<in>s. \<forall>k2\<in>s. k1 \<noteq> k2 \<longrightarrow> interior(k1) \<inter> interior(k2) = {}) \<and>
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   583
    (\<Union>s = i)"
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   584
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   585
lemma division_ofD[dest]:
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   586
  assumes "s division_of i"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   587
  shows "finite s"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   588
    and "\<And>k. k \<in> s \<Longrightarrow> k \<subseteq> i"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   589
    and "\<And>k. k \<in> s \<Longrightarrow> k \<noteq> {}"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   590
    and "\<And>k. k \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   591
    and "\<And>k1 k2. k1 \<in> s \<Longrightarrow> k2 \<in> s \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   592
    and "\<Union>s = i"
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   593
  using assms unfolding division_of_def by auto
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   594
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   595
lemma division_ofI:
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   596
  assumes "finite s"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   597
    and "\<And>k. k \<in> s \<Longrightarrow> k \<subseteq> i"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   598
    and "\<And>k. k \<in> s \<Longrightarrow> k \<noteq> {}"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   599
    and "\<And>k. k \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   600
    and "\<And>k1 k2. k1 \<in> s \<Longrightarrow> k2 \<in> s \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   601
    and "\<Union>s = i"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   602
  shows "s division_of i"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   603
  using assms unfolding division_of_def by auto
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   604
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   605
lemma division_of_finite: "s division_of i \<Longrightarrow> finite s"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   606
  unfolding division_of_def by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   607
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   608
lemma division_of_self[intro]: "cbox a b \<noteq> {} \<Longrightarrow> {cbox a b} division_of (cbox a b)"
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   609
  unfolding division_of_def by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   610
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   611
lemma division_of_trivial[simp]: "s division_of {} \<longleftrightarrow> s = {}"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   612
  unfolding division_of_def by auto
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   613
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   614
lemma division_of_sing[simp]:
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   615
  "s division_of cbox a (a::'a::euclidean_space) \<longleftrightarrow> s = {cbox a a}"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   616
  (is "?l = ?r")
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   617
proof
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   618
  assume ?r
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   619
  moreover
60384
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
   620
  { fix k
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
   621
    assume "s = {{a}}" "k\<in>s"
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
   622
    then have "\<exists>x y. k = cbox x y"
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   623
      apply (rule_tac x=a in exI)+
60384
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
   624
      apply (force simp: cbox_sing)
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   625
      done
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   626
  }
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   627
  ultimately show ?l
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   628
    unfolding division_of_def cbox_sing by auto
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   629
next
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   630
  assume ?l
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   631
  note * = conjunctD4[OF this[unfolded division_of_def cbox_sing]]
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   632
  {
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   633
    fix x
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   634
    assume x: "x \<in> s" have "x = {a}"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   635
      using *(2)[rule_format,OF x] by auto
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   636
  }
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   637
  moreover have "s \<noteq> {}"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   638
    using *(4) by auto
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   639
  ultimately show ?r
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   640
    unfolding cbox_sing by auto
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   641
qed
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   642
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   643
lemma elementary_empty: obtains p where "p division_of {}"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   644
  unfolding division_of_trivial by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   645
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   646
lemma elementary_interval: obtains p where "p division_of (cbox a b)"
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   647
  by (metis division_of_trivial division_of_self)
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   648
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   649
lemma division_contains: "s division_of i \<Longrightarrow> \<forall>x\<in>i. \<exists>k\<in>s. x \<in> k"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   650
  unfolding division_of_def by auto
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   651
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   652
lemma forall_in_division:
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   653
  "d division_of i \<Longrightarrow> (\<forall>x\<in>d. P x) \<longleftrightarrow> (\<forall>a b. cbox a b \<in> d \<longrightarrow> P (cbox a b))"
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44522
diff changeset
   654
  unfolding division_of_def by fastforce
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   655
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   656
lemma division_of_subset:
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   657
  assumes "p division_of (\<Union>p)"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   658
    and "q \<subseteq> p"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   659
  shows "q division_of (\<Union>q)"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   660
proof (rule division_ofI)
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   661
  note * = division_ofD[OF assms(1)]
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   662
  show "finite q"
60384
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
   663
    using "*"(1) assms(2) infinite_super by auto
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   664
  {
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   665
    fix k
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   666
    assume "k \<in> q"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   667
    then have kp: "k \<in> p"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   668
      using assms(2) by auto
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   669
    show "k \<subseteq> \<Union>q"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60396
diff changeset
   670
      using \<open>k \<in> q\<close> by auto
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   671
    show "\<exists>a b. k = cbox a b"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   672
      using *(4)[OF kp] by auto
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   673
    show "k \<noteq> {}"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   674
      using *(3)[OF kp] by auto
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   675
  }
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   676
  fix k1 k2
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   677
  assume "k1 \<in> q" "k2 \<in> q" "k1 \<noteq> k2"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   678
  then have **: "k1 \<in> p" "k2 \<in> p" "k1 \<noteq> k2"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   679
    using assms(2) by auto
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   680
  show "interior k1 \<inter> interior k2 = {}"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   681
    using *(5)[OF **] by auto
49698
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   682
qed auto
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   683
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   684
lemma division_of_union_self[intro]: "p division_of s \<Longrightarrow> p division_of (\<Union>p)"
f68e237e8c10 tuned proofs;
wenzelm
parents: 49675
diff changeset
   685
  unfolding division_of_def by auto
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   686
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   687
lemma division_of_content_0:
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   688
  assumes "content (cbox a b) = 0" "d division_of (cbox a b)"
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   689
  shows "\<forall>k\<in>d. content k = 0"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   690
  unfolding forall_in_division[OF assms(2)]
60384
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
   691
  by (metis antisym_conv assms content_pos_le content_subset division_ofD(2))
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   692
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   693
lemma division_inter:
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   694
  fixes s1 s2 :: "'a::euclidean_space set"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   695
  assumes "p1 division_of s1"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   696
    and "p2 division_of s2"
63595
aca2659ebba7 clean up prove for inter_interior_unions_intervals
hoelzl
parents: 63594
diff changeset
   697
  shows "{k1 \<inter> k2 | k1 k2. k1 \<in> p1 \<and> k2 \<in> p2 \<and> k1 \<inter> k2 \<noteq> {}} division_of (s1 \<inter> s2)"
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   698
  (is "?A' division_of _")
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   699
proof -
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   700
  let ?A = "{s. s \<in>  (\<lambda>(k1,k2). k1 \<inter> k2) ` (p1 \<times> p2) \<and> s \<noteq> {}}"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   701
  have *: "?A' = ?A" by auto
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   702
  show ?thesis
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   703
    unfolding *
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   704
  proof (rule division_ofI)
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   705
    have "?A \<subseteq> (\<lambda>(x, y). x \<inter> y) ` (p1 \<times> p2)"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   706
      by auto
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   707
    moreover have "finite (p1 \<times> p2)"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   708
      using assms unfolding division_of_def by auto
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   709
    ultimately show "finite ?A" by auto
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   710
    have *: "\<And>s. \<Union>{x\<in>s. x \<noteq> {}} = \<Union>s"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   711
      by auto
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   712
    show "\<Union>?A = s1 \<inter> s2"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   713
      apply (rule set_eqI)
62343
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 62207
diff changeset
   714
      unfolding * and UN_iff
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   715
      using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)]
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   716
      apply auto
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   717
      done
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   718
    {
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   719
      fix k
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   720
      assume "k \<in> ?A"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   721
      then obtain k1 k2 where k: "k = k1 \<inter> k2" "k1 \<in> p1" "k2 \<in> p2" "k \<noteq> {}"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   722
        by auto
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   723
      then show "k \<noteq> {}"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   724
        by auto
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   725
      show "k \<subseteq> s1 \<inter> s2"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   726
        using division_ofD(2)[OF assms(1) k(2)] and division_ofD(2)[OF assms(2) k(3)]
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   727
        unfolding k by auto
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   728
      obtain a1 b1 where k1: "k1 = cbox a1 b1"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   729
        using division_ofD(4)[OF assms(1) k(2)] by blast
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   730
      obtain a2 b2 where k2: "k2 = cbox a2 b2"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   731
        using division_ofD(4)[OF assms(2) k(3)] by blast
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   732
      show "\<exists>a b. k = cbox a b"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   733
        unfolding k k1 k2 unfolding inter_interval by auto
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   734
    }
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   735
    fix k1 k2
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   736
    assume "k1 \<in> ?A"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   737
    then obtain x1 y1 where k1: "k1 = x1 \<inter> y1" "x1 \<in> p1" "y1 \<in> p2" "k1 \<noteq> {}"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   738
      by auto
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   739
    assume "k2 \<in> ?A"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   740
    then obtain x2 y2 where k2: "k2 = x2 \<inter> y2" "x2 \<in> p1" "y2 \<in> p2" "k2 \<noteq> {}"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   741
      by auto
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   742
    assume "k1 \<noteq> k2"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   743
    then have th: "x1 \<noteq> x2 \<or> y1 \<noteq> y2"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   744
      unfolding k1 k2 by auto
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   745
    have *: "interior x1 \<inter> interior x2 = {} \<or> interior y1 \<inter> interior y2 = {} \<Longrightarrow>
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   746
      interior (x1 \<inter> y1) \<subseteq> interior x1 \<Longrightarrow> interior (x1 \<inter> y1) \<subseteq> interior y1 \<Longrightarrow>
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   747
      interior (x2 \<inter> y2) \<subseteq> interior x2 \<Longrightarrow> interior (x2 \<inter> y2) \<subseteq> interior y2 \<Longrightarrow>
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   748
      interior (x1 \<inter> y1) \<inter> interior (x2 \<inter> y2) = {}" by auto
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   749
    show "interior k1 \<inter> interior k2 = {}"
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   750
      unfolding k1 k2
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   751
      apply (rule *)
60384
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
   752
      using assms division_ofD(5) k1 k2(2) k2(3) th apply auto
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   753
      done
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   754
  qed
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   755
qed
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   756
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   757
lemma division_inter_1:
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   758
  assumes "d division_of i"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   759
    and "cbox a (b::'a::euclidean_space) \<subseteq> i"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   760
  shows "{cbox a b \<inter> k | k. k \<in> d \<and> cbox a b \<inter> k \<noteq> {}} division_of (cbox a b)"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   761
proof (cases "cbox a b = {}")
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   762
  case True
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   763
  show ?thesis
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   764
    unfolding True and division_of_trivial by auto
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   765
next
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   766
  case False
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   767
  have *: "cbox a b \<inter> i = cbox a b" using assms(2) by auto
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   768
  show ?thesis
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   769
    using division_inter[OF division_of_self[OF False] assms(1)]
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   770
    unfolding * by auto
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   771
qed
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   772
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   773
lemma elementary_inter:
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   774
  fixes s t :: "'a::euclidean_space set"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   775
  assumes "p1 division_of s"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   776
    and "p2 division_of t"
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   777
  shows "\<exists>p. p division_of (s \<inter> t)"
60384
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
   778
using assms division_inter by blast
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   779
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   780
lemma elementary_inters:
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   781
  assumes "finite f"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   782
    and "f \<noteq> {}"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   783
    and "\<forall>s\<in>f. \<exists>p. p division_of (s::('a::euclidean_space) set)"
60585
48fdff264eb2 tuned whitespace;
wenzelm
parents: 60492
diff changeset
   784
  shows "\<exists>p. p division_of (\<Inter>f)"
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   785
  using assms
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   786
proof (induct f rule: finite_induct)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   787
  case (insert x f)
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   788
  show ?case
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   789
  proof (cases "f = {}")
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   790
    case True
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   791
    then show ?thesis
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   792
      unfolding True using insert by auto
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   793
  next
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   794
    case False
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   795
    obtain p where "p division_of \<Inter>f"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   796
      using insert(3)[OF False insert(5)[unfolded ball_simps,THEN conjunct2]] ..
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   797
    moreover obtain px where "px division_of x"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   798
      using insert(5)[rule_format,OF insertI1] ..
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   799
    ultimately show ?thesis
60384
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
   800
      by (simp add: elementary_inter Inter_insert)
49970
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   801
  qed
ca5ab959c0ae tuned proofs;
wenzelm
parents: 49698
diff changeset
   802
qed auto
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   803
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   804
lemma division_disjoint_union:
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   805
  assumes "p1 division_of s1"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   806
    and "p2 division_of s2"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   807
    and "interior s1 \<inter> interior s2 = {}"
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   808
  shows "(p1 \<union> p2) division_of (s1 \<union> s2)"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   809
proof (rule division_ofI)
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   810
  note d1 = division_ofD[OF assms(1)]
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   811
  note d2 = division_ofD[OF assms(2)]
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   812
  show "finite (p1 \<union> p2)"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   813
    using d1(1) d2(1) by auto
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   814
  show "\<Union>(p1 \<union> p2) = s1 \<union> s2"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   815
    using d1(6) d2(6) by auto
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   816
  {
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   817
    fix k1 k2
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   818
    assume as: "k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   819
    moreover
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   820
    let ?g="interior k1 \<inter> interior k2 = {}"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   821
    {
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   822
      assume as: "k1\<in>p1" "k2\<in>p2"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   823
      have ?g
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   824
        using interior_mono[OF d1(2)[OF as(1)]] interior_mono[OF d2(2)[OF as(2)]]
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   825
        using assms(3) by blast
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   826
    }
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   827
    moreover
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   828
    {
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   829
      assume as: "k1\<in>p2" "k2\<in>p1"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   830
      have ?g
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   831
        using interior_mono[OF d1(2)[OF as(2)]] interior_mono[OF d2(2)[OF as(1)]]
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   832
        using assms(3) by blast
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   833
    }
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   834
    ultimately show ?g
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   835
      using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   836
  }
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   837
  fix k
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   838
  assume k: "k \<in> p1 \<union> p2"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   839
  show "k \<subseteq> s1 \<union> s2"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   840
    using k d1(2) d2(2) by auto
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   841
  show "k \<noteq> {}"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   842
    using k d1(3) d2(3) by auto
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   843
  show "\<exists>a b. k = cbox a b"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   844
    using k d1(4) d2(4) by auto
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   845
qed
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   846
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   847
lemma partial_division_extend_1:
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   848
  fixes a b c d :: "'a::euclidean_space"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   849
  assumes incl: "cbox c d \<subseteq> cbox a b"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   850
    and nonempty: "cbox c d \<noteq> {}"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   851
  obtains p where "p division_of (cbox a b)" "cbox c d \<in> p"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   852
proof
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   853
  let ?B = "\<lambda>f::'a\<Rightarrow>'a \<times> 'a.
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   854
    cbox (\<Sum>i\<in>Basis. (fst (f i) \<bullet> i) *\<^sub>R i) (\<Sum>i\<in>Basis. (snd (f i) \<bullet> i) *\<^sub>R i)"
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 63018
diff changeset
   855
  define p where "p = ?B ` (Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)})"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   856
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   857
  show "cbox c d \<in> p"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   858
    unfolding p_def
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   859
    by (auto simp add: box_eq_empty cbox_def intro!: image_eqI[where x="\<lambda>(i::'a)\<in>Basis. (c, d)"])
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   860
  {
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   861
    fix i :: 'a
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   862
    assume "i \<in> Basis"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   863
    with incl nonempty have "a \<bullet> i \<le> c \<bullet> i" "c \<bullet> i \<le> d \<bullet> i" "d \<bullet> i \<le> b \<bullet> i"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   864
      unfolding box_eq_empty subset_box by (auto simp: not_le)
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   865
  }
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   866
  note ord = this
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   867
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   868
  show "p division_of (cbox a b)"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   869
  proof (rule division_ofI)
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   870
    show "finite p"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   871
      unfolding p_def by (auto intro!: finite_PiE)
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   872
    {
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   873
      fix k
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   874
      assume "k \<in> p"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52141
diff changeset
   875
      then obtain f where f: "f \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" and k: "k = ?B f"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   876
        by (auto simp: p_def)
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   877
      then show "\<exists>a b. k = cbox a b"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   878
        by auto
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   879
      have "k \<subseteq> cbox a b \<and> k \<noteq> {}"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   880
      proof (simp add: k box_eq_empty subset_box not_less, safe)
53374
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53015
diff changeset
   881
        fix i :: 'a
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53015
diff changeset
   882
        assume i: "i \<in> Basis"
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   883
        with f have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   884
          by (auto simp: PiE_iff)
53374
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53015
diff changeset
   885
        with i ord[of i]
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   886
        show "a \<bullet> i \<le> fst (f i) \<bullet> i" "snd (f i) \<bullet> i \<le> b \<bullet> i" "fst (f i) \<bullet> i \<le> snd (f i) \<bullet> i"
54776
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 54775
diff changeset
   887
          by auto
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   888
      qed
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   889
      then show "k \<noteq> {}" "k \<subseteq> cbox a b"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   890
        by auto
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   891
      {
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   892
        fix l
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   893
        assume "l \<in> p"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52141
diff changeset
   894
        then obtain g where g: "g \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" and l: "l = ?B g"
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   895
          by (auto simp: p_def)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   896
        assume "l \<noteq> k"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   897
        have "\<exists>i\<in>Basis. f i \<noteq> g i"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   898
        proof (rule ccontr)
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   899
          assume "\<not> ?thesis"
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   900
          with f g have "f = g"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   901
            by (auto simp: PiE_iff extensional_def intro!: ext)
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60396
diff changeset
   902
          with \<open>l \<noteq> k\<close> show False
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   903
            by (simp add: l k)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   904
        qed
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   905
        then obtain i where *: "i \<in> Basis" "f i \<noteq> g i" ..
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   906
        then have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
60384
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
   907
                  "g i = (a, c) \<or> g i = (c, d) \<or> g i = (d, b)"
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   908
          using f g by (auto simp: PiE_iff)
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   909
        with * ord[of i] show "interior l \<inter> interior k = {}"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   910
          by (auto simp add: l k interior_cbox disjoint_interval intro!: bexI[of _ i])
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   911
      }
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60396
diff changeset
   912
      note \<open>k \<subseteq> cbox a b\<close>
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   913
    }
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   914
    moreover
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   915
    {
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   916
      fix x assume x: "x \<in> cbox a b"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   917
      have "\<forall>i\<in>Basis. \<exists>l. x \<bullet> i \<in> {fst l \<bullet> i .. snd l \<bullet> i} \<and> l \<in> {(a, c), (c, d), (d, b)}"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   918
      proof
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   919
        fix i :: 'a
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   920
        assume "i \<in> Basis"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   921
        with x ord[of i]
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   922
        have "(a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> c \<bullet> i) \<or> (c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i) \<or>
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   923
            (d \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i)"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   924
          by (auto simp: cbox_def)
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   925
        then show "\<exists>l. x \<bullet> i \<in> {fst l \<bullet> i .. snd l \<bullet> i} \<and> l \<in> {(a, c), (c, d), (d, b)}"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   926
          by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   927
      qed
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   928
      then obtain f where
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   929
        f: "\<forall>i\<in>Basis. x \<bullet> i \<in> {fst (f i) \<bullet> i..snd (f i) \<bullet> i} \<and> f i \<in> {(a, c), (c, d), (d, b)}"
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   930
        unfolding bchoice_iff ..
53374
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53015
diff changeset
   931
      moreover from f have "restrict f Basis \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   932
        by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   933
      moreover from f have "x \<in> ?B (restrict f Basis)"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   934
        by (auto simp: mem_box)
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   935
      ultimately have "\<exists>k\<in>p. x \<in> k"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   936
        unfolding p_def by blast
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   937
    }
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   938
    ultimately show "\<Union>p = cbox a b"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   939
      by auto
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   940
  qed
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50348
diff changeset
   941
qed
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
   942
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   943
lemma partial_division_extend_interval:
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   944
  assumes "p division_of (\<Union>p)" "(\<Union>p) \<subseteq> cbox a b"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   945
  obtains q where "p \<subseteq> q" "q division_of cbox a (b::'a::euclidean_space)"
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   946
proof (cases "p = {}")
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   947
  case True
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   948
  obtain q where "q division_of (cbox a b)"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   949
    by (rule elementary_interval)
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
   950
  then show ?thesis
60384
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
   951
    using True that by blast
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   952
next
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   953
  case False
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   954
  note p = division_ofD[OF assms(1)]
60428
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
   955
  have div_cbox: "\<forall>k\<in>p. \<exists>q. q division_of cbox a b \<and> k \<in> q"
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   956
  proof
61165
8020249565fb tuned proofs;
wenzelm
parents: 61076
diff changeset
   957
    fix k
8020249565fb tuned proofs;
wenzelm
parents: 61076
diff changeset
   958
    assume kp: "k \<in> p"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   959
    obtain c d where k: "k = cbox c d"
61165
8020249565fb tuned proofs;
wenzelm
parents: 61076
diff changeset
   960
      using p(4)[OF kp] by blast
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   961
    have *: "cbox c d \<subseteq> cbox a b" "cbox c d \<noteq> {}"
61165
8020249565fb tuned proofs;
wenzelm
parents: 61076
diff changeset
   962
      using p(2,3)[OF kp, unfolded k] using assms(2)
54776
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 54775
diff changeset
   963
      by (blast intro: order.trans)+
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   964
    obtain q where "q division_of cbox a b" "cbox c d \<in> q"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   965
      by (rule partial_division_extend_1[OF *])
61165
8020249565fb tuned proofs;
wenzelm
parents: 61076
diff changeset
   966
    then show "\<exists>q. q division_of cbox a b \<and> k \<in> q"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   967
      unfolding k by auto
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   968
  qed
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   969
  obtain q where q: "\<And>x. x \<in> p \<Longrightarrow> q x division_of cbox a b" "\<And>x. x \<in> p \<Longrightarrow> x \<in> q x"
60428
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
   970
    using bchoice[OF div_cbox] by blast
60394
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
   971
  { fix x
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   972
    assume x: "x \<in> p"
60394
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
   973
    have "q x division_of \<Union>q x"
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   974
      apply (rule division_ofI)
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   975
      using division_ofD[OF q(1)[OF x]]
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   976
      apply auto
60394
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
   977
      done }
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
   978
  then have "\<And>x. x \<in> p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
   979
    by (meson Diff_subset division_of_subset)
60585
48fdff264eb2 tuned whitespace;
wenzelm
parents: 60492
diff changeset
   980
  then have "\<exists>d. d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)"
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   981
    apply -
60394
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
   982
    apply (rule elementary_inters [OF finite_imageI[OF p(1)]])
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
   983
    apply (auto simp: False elementary_inters [OF finite_imageI[OF p(1)]])
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   984
    done
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   985
  then obtain d where d: "d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)" ..
60394
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
   986
  have "d \<union> p division_of cbox a b"
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   987
  proof -
60394
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
   988
    have te: "\<And>s f t. s \<noteq> {} \<Longrightarrow> \<forall>i\<in>s. f i \<union> i = t \<Longrightarrow> t = \<Inter>(f ` s) \<union> \<Union>s" by auto
60428
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
   989
    have cbox_eq: "cbox a b = \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p) \<union> \<Union>p"
60394
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
   990
    proof (rule te[OF False], clarify)
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   991
      fix i
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   992
      assume i: "i \<in> p"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
   993
      show "\<Union>(q i - {i}) \<union> i = cbox a b"
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   994
        using division_ofD(6)[OF q(1)[OF i]] using q(2)[OF i] by auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
   995
    qed
60428
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
   996
    { fix k
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   997
      assume k: "k \<in> p"
60428
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
   998
      have *: "\<And>u t s. t \<inter> s = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<inter> t = {}"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
   999
        by auto
60428
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
  1000
      have "interior (\<Inter>i\<in>p. \<Union>(q i - {i})) \<inter> interior k = {}"
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
  1001
      proof (rule *[OF inter_interior_unions_intervals])
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1002
        note qk=division_ofD[OF q(1)[OF k]]
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1003
        show "finite (q k - {k})" "open (interior k)" "\<forall>t\<in>q k - {k}. \<exists>a b. t = cbox a b"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
  1004
          using qk by auto
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1005
        show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}"
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1006
          using qk(5) using q(2)[OF k] by auto
60428
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
  1007
        show "interior (\<Inter>i\<in>p. \<Union>(q i - {i})) \<subseteq> interior (\<Union>(q k - {k}))"
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
  1008
          apply (rule interior_mono)+
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
  1009
          using k
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
  1010
          apply auto
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
  1011
          done
60428
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
  1012
      qed } note [simp] = this
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
  1013
    show "d \<union> p division_of (cbox a b)"
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
  1014
      unfolding cbox_eq
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
  1015
      apply (rule division_disjoint_union[OF d assms(1)])
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
  1016
      apply (rule inter_interior_unions_intervals)
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
  1017
      apply (rule p open_interior ballI)+
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
  1018
      apply simp_all
60428
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
  1019
      done
60394
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
  1020
  qed
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
  1021
  then show ?thesis
b699cedd04e8 tidying messy proofs
paulson <lp15@cam.ac.uk>
parents: 60384
diff changeset
  1022
    by (meson Un_upper2 that)
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1023
qed
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1024
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1025
lemma elementary_bounded[dest]:
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1026
  fixes s :: "'a::euclidean_space set"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
  1027
  shows "p division_of s \<Longrightarrow> bounded s"
56189
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
  1028
  unfolding division_of_def by (metis bounded_Union bounded_cbox)
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1029
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1030
lemma elementary_subset_cbox:
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1031
  "p division_of s \<Longrightarrow> \<exists>a b. s \<subseteq> cbox a (b::'a::euclidean_space)"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1032
  by (meson elementary_bounded bounded_subset_cbox)
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1033
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1034
lemma division_union_intervals_exists:
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1035
  fixes a b :: "'a::euclidean_space"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1036
  assumes "cbox a b \<noteq> {}"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1037
  obtains p where "(insert (cbox a b) p) division_of (cbox a b \<union> cbox c d)"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1038
proof (cases "cbox c d = {}")
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1039
  case True
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1040
  show ?thesis
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1041
    apply (rule that[of "{}"])
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1042
    unfolding True
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1043
    using assms
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1044
    apply auto
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1045
    done
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1046
next
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1047
  case False
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1048
  show ?thesis
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1049
  proof (cases "cbox a b \<inter> cbox c d = {}")
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1050
    case True
62618
f7f2467ab854 Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
  1051
    then show ?thesis
f7f2467ab854 Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
  1052
      by (metis that False assms division_disjoint_union division_of_self insert_is_Un interior_Int interior_empty)
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1053
  next
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1054
    case False
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1055
    obtain u v where uv: "cbox a b \<inter> cbox c d = cbox u v"
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1056
      unfolding inter_interval by auto
60428
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
  1057
    have uv_sub: "cbox u v \<subseteq> cbox c d" using uv by auto
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1058
    obtain p where "p division_of cbox c d" "cbox u v \<in> p"
60428
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
  1059
      by (rule partial_division_extend_1[OF uv_sub False[unfolded uv]])
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
  1060
    note p = this division_ofD[OF this(1)]
60428
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
  1061
    have "interior (cbox a b \<inter> \<Union>(p - {cbox u v})) = interior(cbox u v \<inter> \<Union>(p - {cbox u v}))"
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
  1062
      apply (rule arg_cong[of _ _ interior])
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
  1063
      using p(8) uv by auto
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
  1064
    also have "\<dots> = {}"
61518
ff12606337e9 new lemmas about topology, etc., for Cauchy integral formula
paulson
parents: 61424
diff changeset
  1065
      unfolding interior_Int
60428
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
  1066
      apply (rule inter_interior_unions_intervals)
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
  1067
      using p(6) p(7)[OF p(2)] p(3)
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
  1068
      apply auto
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
  1069
      done
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
  1070
    finally have [simp]: "interior (cbox a b) \<inter> interior (\<Union>(p - {cbox u v})) = {}" by simp
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
  1071
    have cbe: "cbox a b \<union> cbox c d = cbox a b \<union> \<Union>(p - {cbox u v})"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1072
      using p(8) unfolding uv[symmetric] by auto
62618
f7f2467ab854 Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
  1073
    have "insert (cbox a b) (p - {cbox u v}) division_of cbox a b \<union> \<Union>(p - {cbox u v})"
f7f2467ab854 Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
  1074
    proof -
f7f2467ab854 Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
  1075
      have "{cbox a b} division_of cbox a b"
f7f2467ab854 Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
  1076
        by (simp add: assms division_of_self)
f7f2467ab854 Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
  1077
      then show "insert (cbox a b) (p - {cbox u v}) division_of cbox a b \<union> \<Union>(p - {cbox u v})"
f7f2467ab854 Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
  1078
        by (metis (no_types) Diff_subset \<open>interior (cbox a b) \<inter> interior (\<Union>(p - {cbox u v})) = {}\<close> division_disjoint_union division_of_subset insert_is_Un p(1) p(8))
f7f2467ab854 Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
  1079
    qed
f7f2467ab854 Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
  1080
    with that[of "p - {cbox u v}"] show ?thesis by (simp add: cbe)
50945
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1081
  qed
917e76c53f82 tuned proofs;
wenzelm
parents: 50919
diff changeset
  1082
qed
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents:
diff changeset
  1083
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1084
lemma division_of_unions:
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1085
  assumes "finite f"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
  1086
    and "\<And>p. p \<in> f \<Longrightarrow> p division_of (\<Union>p)"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1087
    and "\<And>k1 k2. k1 \<in> \<Union>f \<Longrightarrow> k2 \<in> \<Union>f \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1088
  shows "\<Union>f division_of \<Union>\<Union>f"
60384
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
  1089
  using assms
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
  1090
  by (auto intro!: division_ofI)
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1091
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1092
lemma elementary_union_interval:
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1093
  fixes a b :: "'a::euclidean_space"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1094
  assumes "p division_of \<Union>p"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1095
  obtains q where "q division_of (cbox a b \<union> \<Union>p)"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1096
proof -
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1097
  note assm = division_ofD[OF assms]
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
  1098
  have lem1: "\<And>f s. \<Union>\<Union>(f ` s) = \<Union>((\<lambda>x. \<Union>(f x)) ` s)"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1099
    by auto
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1100
  have lem2: "\<And>f s. f \<noteq> {} \<Longrightarrow> \<Union>{s \<union> t |t. t \<in> f} = s \<union> \<Union>f"
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1101
    by auto
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1102
  {
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1103
    presume "p = {} \<Longrightarrow> thesis"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1104
      "cbox a b = {} \<Longrightarrow> thesis"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1105
      "cbox a b \<noteq> {} \<Longrightarrow> interior (cbox a b) = {} \<Longrightarrow> thesis"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1106
      "p \<noteq> {} \<Longrightarrow> interior (cbox a b)\<noteq>{} \<Longrightarrow> cbox a b \<noteq> {} \<Longrightarrow> thesis"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1107
    then show thesis by auto
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1108
  next
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1109
    assume as: "p = {}"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1110
    obtain p where "p division_of (cbox a b)"
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
  1111
      by (rule elementary_interval)
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1112
    then show thesis
60384
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
  1113
      using as that by auto
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1114
  next
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1115
    assume as: "cbox a b = {}"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1116
    show thesis
60384
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
  1117
      using as assms that by auto
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1118
  next
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1119
    assume as: "interior (cbox a b) = {}" "cbox a b \<noteq> {}"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1120
    show thesis
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1121
      apply (rule that[of "insert (cbox a b) p"],rule division_ofI)
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1122
      unfolding finite_insert
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1123
      apply (rule assm(1)) unfolding Union_insert
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1124
      using assm(2-4) as
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1125
      apply -
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54411
diff changeset
  1126
      apply (fast dest: assm(5))+
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1127
      done
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1128
  next
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1129
    assume as: "p \<noteq> {}" "interior (cbox a b) \<noteq> {}" "cbox a b \<noteq> {}"
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1130
    have "\<forall>k\<in>p. \<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> k)"
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
  1131
    proof
61165
8020249565fb tuned proofs;
wenzelm
parents: 61076
diff changeset
  1132
      fix k
8020249565fb tuned proofs;
wenzelm
parents: 61076
diff changeset
  1133
      assume kp: "k \<in> p"
8020249565fb tuned proofs;
wenzelm
parents: 61076
diff changeset
  1134
      from assm(4)[OF kp] obtain c d where "k = cbox c d" by blast
8020249565fb tuned proofs;
wenzelm
parents: 61076
diff changeset
  1135
      then show "\<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> k)"
60384
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
  1136
        by (meson as(3) division_union_intervals_exists)
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1137
    qed
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1138
    from bchoice[OF this] obtain q where "\<forall>x\<in>p. insert (cbox a b) (q x) division_of (cbox a b) \<union> x" ..
53408
a67d32e2d26e tuned proofs;
wenzelm
parents: 53399
diff changeset
  1139
    note q = division_ofD[OF this[rule_format]]
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1140
    let ?D = "\<Union>{insert (cbox a b) (q k) | k. k \<in> p}"
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 60585
diff changeset
  1141
    show thesis
60428
5e9de4faef98 fixed several "inside-out" proofs
paulson <lp15@cam.ac.uk>
parents: 60425
diff changeset
  1142
    proof (rule that[OF division_ofI])
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1143
      have *: "{insert (cbox a b) (q k) |k. k \<in> p} = (\<lambda>k. insert (cbox a b) (q k)) ` p"
53399
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1144
        by auto
43b3b3fa6967 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1145
      show "finite ?D"
60384
b33690cad45e Tidied lots of messy proofs
paulson <lp15@cam.ac.uk>
parents: 60180
diff changeset
  1146
        using "*" assm(1) q(1) by auto
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56181
diff changeset
  1147
      show "\<Union>?D = cbox a b \<union> \<Union>p"
53399 <