Theory MonConv
subsection ‹Monotone Convergence \label{sec:monconv}›
theory MonConv
imports Complex_Main
begin
text ‹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" and "wenzelax"›} ‹ord› of ordered
types like this.
@{prop "mon_conv u f ≡ (∀n. u n ≤ u (Suc n)) ∧ Sup (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]}
›
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" ("_↑_" [60,61] 60)
overloading
mon_conv_real ≡ "mon_conv :: _ ⇒ real ⇒ bool"
mon_conv_real_fun ≡ "mon_conv :: _ ⇒ ('a ⇒ real) ⇒ bool"
mon_conv_set ≡ "mon_conv :: _ ⇒ 'a set ⇒ bool"
begin
definition "x↑(y::real) ≡ (∀n. x n ≤ x (Suc n)) ∧ x ⇢ y"
definition "u↑(f::'a ⇒ real) ≡ (∀n. u n ≤ u (Suc n)) ∧ (∀w. (λn. u n w) ⇢ f w)"
definition "A↑(B::'a set) ≡ (∀n. A n ≤ A (Suc n)) ∧ B = (⋃n. A n)"
end
theorem realfun_mon_conv_iff: "(u↑f) = (∀w. (λn. u n w)↑((f w)::real))"
by (auto simp add: mon_conv_real_def mon_conv_real_fun_def le_fun_def)
text ‹The long arrow signifies convergence of real sequences as
defined in the theory ‹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.›
lemma assumes mon_conv: "x↑(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: mon_conv_real_def)
finally show ?case .
qed
lemma limseq_shift_iff: "(λm. x (m+i)) ⇢ y = x ⇢ y"
proof (induct i)
case 0 show ?case by simp
next
case (Suc n)
also have "(λm. x (m + n)) ⇢ y = (λm. x (Suc m + n)) ⇢ y"
by (rule filterlim_sequentially_Suc[THEN sym])
also have "… = (λm. x (m + Suc n)) ⇢ y"
by simp
finally show ?case .
qed
theorem assumes mon_conv: "x↑(y::real)"
shows real_mon_conv_le: "x i ≤ y"
proof -
from mon_conv have "(λm. x (m+i)) ⇢ y"
by (simp add: mon_conv_real_def 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]])
qed
theorem assumes mon_conv: "x↑(y::('a ⇒ real))"
shows realfun_mon_conv_le: "x i ≤ y"
proof -
{fix w
from mon_conv have "(λi. x i w)↑(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)
qed
lemma assumes mon_conv: "x↑(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"
proof -
from mon_conv have aux: "⋀r. r > 0 ⟹ ∃n. ∀m. n ≤ m ⟶ ¦x m - y¦ < r"
unfolding mon_conv_real_def lim_sequentially 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 blast
qed
theorem real_mon_conv_times:
assumes xy: "x↑(y::real)" and nn: "0≤z"
shows "(λm. z*x m)↑(z*y)"
proof -
from assms have "⋀n. z*x n ≤ z*x (Suc n)"
by (simp add: mon_conv_real_def mult_left_mono)
also from xy have "(λm. z*x m)⇢(z*y)"
by (simp add: mon_conv_real_def tendsto_const tendsto_mult)
ultimately show ?thesis by (simp add: mon_conv_real_def)
qed
theorem realfun_mon_conv_times:
assumes xy: "x↑(y::'a⇒real)" and nn: "0≤z"
shows "(λm w. z*x m w)↑(λw. z*y w)"
proof -
from assms have "⋀w. (λm. z*x m w)↑(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↑(y::real)" and ab: "a↑(b::real)"
shows "(λm. x m + a m)↑(y + b)"
proof -
{ fix n
from assms have "x n ≤ x (Suc n)" and "a n ≤ a (Suc n)"
by (simp_all add: mon_conv_real_def)
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: mon_conv_real_def tendsto_add)
ultimately show ?thesis by (simp add: mon_conv_real_def)
qed
theorem realfun_mon_conv_add:
assumes xy: "x↑(y::'a⇒real)" and ab: "a↑(b::'a ⇒ real)"
shows "(λm w. x m w + a m w)↑(λw. y w + b w)"
proof -
from assms have "⋀w. (λm. x m w + a m w)↑(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↑l ∧ l≤x"
proof -
from incseq_convergent[of c x] mon bound
obtain l where "c ⇢ l" "∀i. c i ≤ l"
by (auto simp: incseq_Suc_iff)
moreover
with bound have "l ≤ x"
by (intro LIMSEQ_le_const2) auto
ultimately show ?thesis
by (auto simp: mon_conv_real_def mon)
qed
theorem real_mon_conv_dom:
assumes xy: "x↑(y::real)" and mon: "⋀n. c n ≤ c (Suc n)"
and dom: "c ≤ x"
shows "∃l. c↑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)
qed
text‹\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↑l ∧ l≤x"
proof
define r where "r t = (SOME l. (λn. c n t)↑l ∧ l≤x t)" for 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)↑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)↑r t ∧ r t≤x t" by (simp add: r_def)
}
thus "c↑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 ‹real_mon_conv_outgrow›, a lemma that will be used for a
monotonicity proof of the integral of simple functions later on.›
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 ↑ (⋃i. A i)"
proof (unfold mon_conv_set_def)
{ fix n
have "mk_mon A n ⊆ mk_mon A (Suc n)"
by auto
}
also
have "(⋃i. mk_mon A i) = (⋃i. A i)"
proof
{ fix i x
assume "x ∈ mk_mon A i"
hence "∃j. x ∈ A j"
by (induct i) auto
hence "x ∈ (⋃i. A i)"
by simp
}
thus "(⋃i. mk_mon A i) ⊆ (⋃i. A i)"
by auto
{ fix i
have "A i ⊆ mk_mon A i"
by (induct i) auto
}
thus "(⋃i. A i) ⊆ (⋃i. mk_mon A i)"
by auto
qed
ultimately show "(∀n. mk_mon A n ⊆ mk_mon A (Suc n)) ∧ ⋃(A ` UNIV) = (⋃n. mk_mon A n)"
by simp
qed
end