# Theory MonConv

Up to index of Isabelle/HOL/Integration

theory MonConv
imports Complex_Main
`header {*Monotone Convergence*}theory MonConvimports Complex_Mainbegintext {* A sensible requirement for an integral operator is that it be  ``well-behaved'' with respect to limit functions. To become just a  little more  precise, it is expected that the limit operator may be interchanged  with the integral operator under conditions that are as weak as  possible. To this  end, the notion of monotone convergence is introduced and later  applied in the definition of the integral.   In fact, we distinguish three types of monotone convergence here:  There are converging sequences of real numbers, real functions and  sets. Monotone convergence could even be defined more generally for  any type in the axiomatic type class\footnote{For the concept of axiomatic type  classes, see \cite{Nipkow93,wenzelax}} @{text ord} of ordered  types like this.  @{prop "mon_conv u f ≡ (∀n. u n ≤ u (Suc n)) ∧ isLub UNIV (range u)  f"}  However, this employs the general concept of a least upper bound.  For the special types we have in mind, the more specific  limit --- respective union --- operators are available, combined with many theorems  about their properties. For the type of real- (or rather ordered-) valued functions,  the less-or-equal relation is defined pointwise.  @{thm le_fun_def [no_vars]}  *}(*monotone convergence*) text {*Now the foundations are laid for the definition of monotone  convergence. To express the similarity of the different types of  convergence, a single overloaded operator is used.*}consts  mon_conv:: "(nat => 'a) => 'a::ord => bool" ("_\<up>_" [60,61] 60) defs (overloaded)  real_mon_conv: "x\<up>(y::real) ≡ (∀n. x n ≤ x (Suc n)) ∧ x ----> y"  realfun_mon_conv:   "u\<up>(f::'a => real) ≡ (∀n. u n ≤ u (Suc n)) ∧  (∀w. (λn. u n w) ----> f w)"  set_mon_conv: "A\<up>(B::'a set) ≡ (∀n. A n ≤ A (Suc n)) ∧ B = (\<Union>n. A n)"theorem realfun_mon_conv_iff: "(u\<up>f) = (∀w. (λn. u n w)\<up>((f w)::real))"  by (auto simp add: real_mon_conv realfun_mon_conv le_fun_def)text {* The long arrow signifies convergence of real sequences as  defined in the theory @{text SEQ} \cite{Fleuriot:2000:MNR}. Monotone convergence  for real functions is simply pointwise monotone convergence.  Quite a few properties of these definitions will be necessary later,  and they are listed now, giving only few select proofs. *}     (*This theorem, too, could be proved just the same for any ord  Type!*)lemma assumes mon_conv: "x\<up>(y::real)"  shows mon_conv_mon: "(x i) ≤ (x (m+i))"(*<*)proof (induct m)  case 0   show ?case by simp  next  case (Suc n)  also   from mon_conv have "x (n+i) ≤ x (Suc n+i)"     by (simp add: real_mon_conv)                finally show ?case .qed(*>*)lemma limseq_shift_iff: "(λm. x (m+i)) ----> y = x ----> y"(*<*)proof (induct i)  case 0 show ?case by simpnext   case (Suc n)  also have "(λm. x (m + n)) ----> y = (λm. x (Suc m + n)) ----> y"    by (rule LIMSEQ_Suc_iff[THEN sym])    also have "… = (λm. x (m + Suc n)) ----> y"    by simp  finally show ?case .qed(*>*)    (*This, too, could be established in general*)theorem assumes mon_conv: "x\<up>(y::real)"  shows real_mon_conv_le: "x i ≤ y"proof -  from mon_conv have "(λm. x (m+i)) ----> y"     by (simp add: real_mon_conv limseq_shift_iff)  also from mon_conv have "∀m≥0. x i ≤ x (m+i)" by (simp add: mon_conv_mon)  ultimately show ?thesis by (rule LIMSEQ_le_const[OF _ exI[where x=0]])qedtheorem assumes mon_conv: "x\<up>(y::('a => real))"  shows realfun_mon_conv_le: "x i ≤ y"proof -  {fix w    from mon_conv have "(λi. x i w)\<up>(y w)"       by (simp add: realfun_mon_conv_iff)        hence "x i w ≤ y w"       by (rule real_mon_conv_le)  }  thus ?thesis by (simp add: le_fun_def)qedlemma assumes mon_conv: "x\<up>(y::real)"  and less: "z < y"  shows real_mon_conv_outgrow: "∃n. ∀m. n ≤ m --> z < x m"proof -  from less have less': "0 < y-z"     by simp                  have "∃n.∀m. n ≤ m --> ¦x m + - y¦ < y-z"  unfolding diff_minus [symmetric]  proof -    from mon_conv have aux: "!!r. r > 0 ==> ∃n. ∀m. n ≤ m --> ¦x m - y¦ < r"    unfolding real_mon_conv LIMSEQ_def dist_real_def by auto    with less' show "∃n. ∀m. n ≤ m --> ¦x m - y¦ < y - z" by auto  qed  also  { fix m     from mon_conv have "x m ≤ y"       by (rule real_mon_conv_le)      hence "¦x m + - y¦ = y - x m"       by arith                        also assume "¦x m + - y¦ < y-z"    ultimately have "z < x m"       by arith                  }  ultimately show ?thesis     by blastqedtheorem real_mon_conv_times:   assumes xy: "x\<up>(y::real)" and nn: "0≤z"  shows "(λm. z*x m)\<up>(z*y)"(*<*)proof -  from assms have "!!n. z*x n ≤ z*x (Suc n)"    by (simp add: real_mon_conv mult_left_mono)  also from xy have "(λm. z*x m)---->(z*y)"    by (simp add: real_mon_conv tendsto_const tendsto_mult)  ultimately show ?thesis by (simp add: real_mon_conv)qed(*>*)theorem realfun_mon_conv_times:   assumes xy: "x\<up>(y::'a=>real)" and nn: "0≤z"  shows "(λm w. z*x m w)\<up>(λw. z*y w)"(*<*)proof -  from assms have "!!w. (λm. z*x m w)\<up>(z*y w)"    by (simp add: realfun_mon_conv_iff real_mon_conv_times)  thus ?thesis by (auto simp add: realfun_mon_conv_iff)qed(*>*)theorem real_mon_conv_add:   assumes xy: "x\<up>(y::real)" and ab: "a\<up>(b::real)"  shows "(λm. x m + a m)\<up>(y + b)" (*<*)proof -   { fix n    from assms have "x n ≤ x (Suc n)" and "a n ≤ a (Suc n)"      by (simp_all add: real_mon_conv)    hence "x n + a n ≤ x (Suc n) + a (Suc n)"      by simp  }  also from assms have "(λm. x m + a m)---->(y + b)" by (simp add: real_mon_conv tendsto_add)  ultimately show ?thesis by (simp add: real_mon_conv)qed(*>*)theorem realfun_mon_conv_add:  assumes xy: "x\<up>(y::'a=>real)" and ab: "a\<up>(b::'a => real)"  shows "(λm w. x m w + a m w)\<up>(λw. y w + b w)"(*<*)proof -  from assms have "!!w. (λm. x m w + a m w)\<up>(y w + b w)"    by (simp add: realfun_mon_conv_iff real_mon_conv_add)  thus ?thesis by (auto simp add: realfun_mon_conv_iff)qed(*>*)theorem real_mon_conv_bound:  assumes mon: "!!n. c n ≤ c (Suc n)"  and bound: "!!n. c n ≤ (x::real)"  shows "∃l. c\<up>l ∧ l≤x"proof -  from mon have m2: "∀n. c n ≤ c (Suc n)"     by simp                                   also   def g ≡ "(λn::nat. x)"  hence "∀n. g(Suc n) ≤ g(n)"     by simp                       moreover     -- {*This is like \$\isacommand{also}\$ but lacks the transitivity step.*}    from bound have "∀n. c n ≤ g(n)"     by (simp add: g_def)                 ultimately have   "∃l m. l ≤ m ∧ ((∀n. c n ≤ l) ∧ c----> l) ∧     (∀n. m ≤ g n) ∧ (g ----> m)"    by (rule lemma_nest)  then obtain l m where lm: "l ≤ m" and conv: "c ----> l"     and gm: "g ----> m"     by fast               from gm g_def have "m=x"     by (simp add: tendsto_const LIMSEQ_unique)  with lm conv m2 show ?thesis     by (auto simp add: real_mon_conv) qedtheorem real_mon_conv_dom:  assumes xy: "x\<up>(y::real)" and mon: "!!n. c n ≤ c (Suc n)"  and dom: "c ≤ x"  shows "∃l. c\<up>l ∧ l≤y"proof -  from dom have "!!n. c n ≤ x n" by (simp add: le_fun_def)  also from xy have "!!n. x n ≤ y" by (simp add: real_mon_conv_le)  also note mon   ultimately show ?thesis by (simp add: real_mon_conv_bound) qedtext{*\newpage*}theorem realfun_mon_conv_bound:  assumes mon: "!!n. c n ≤ c (Suc n)"  and bound: "!!n. c n ≤ (x::'a => real)"  shows "∃l. c\<up>l ∧ l≤x"(*<*)proof   def r ≡ "λt. SOME l. (λn. c n t)\<up>l ∧ l≤x t"  { fix t    from mon have m2: "!!n. c n t ≤ c (Suc n) t" by (simp add: le_fun_def)    also     from bound have "!!n. c n t ≤ x t" by (simp add: le_fun_def)        ultimately have "∃l. (λn. c n t)\<up>l ∧ l≤x t" (is "∃l. ?P l")       by (rule real_mon_conv_bound)     hence "?P (SOME l. ?P l)" by (rule someI_ex)    hence "(λn. c n t)\<up>r t ∧ r t≤x t" by (simp add: r_def)  }    thus "c\<up>r ∧ r ≤ x" by (simp add: realfun_mon_conv_iff le_fun_def)qed (*>*)  text {*This brings the theory to an end. Notice how the definition of the limit of a  real sequence is visible in the proof to @{text  real_mon_conv_outgrow}, a lemma that will be used for a  monotonicity proof of the integral of simple functions later on.*}(*<*)  (*Another set construction. Needed in ImportPredSet, but Set is shadowed beyond   reconstruction there.  Before making disjoint, we first need an ascending series of sets*)primrec mk_mon::"(nat => 'a set) => nat => 'a set"where  "mk_mon A 0 = A 0"| "mk_mon A (Suc n) = A (Suc n) ∪ mk_mon A n"lemma "mk_mon A \<up> (\<Union>i. A i)"proof (unfold set_mon_conv)  { fix n    have "mk_mon A n ⊆ mk_mon A (Suc n)"      by auto  }  also  have "(\<Union>i. mk_mon A i) = (\<Union>i. A i)"  proof     { fix i x      assume "x ∈ mk_mon A i"      hence "∃j. x ∈ A j"        by (induct i) auto      hence "x ∈ (\<Union>i. A i)"        by simp    }    thus "(\<Union>i. mk_mon A i) ⊆ (\<Union>i. A i)"      by auto        { fix i       have "A i ⊆ mk_mon A i"        by (induct i) auto    }    thus "(\<Union>i. A i) ⊆ (\<Union>i. mk_mon A i)"      by auto  qed  ultimately show "(∀n. mk_mon A n ⊆ mk_mon A (Suc n)) ∧ UNION UNIV A = (\<Union>n. mk_mon A n)"    by simpqed(*>*)  end`