tagged 8 theories for the Analysis manual.
--- a/src/HOL/Analysis/Fashoda_Theorem.thy Sun Oct 21 20:45:01 2018 +0200
+++ b/src/HOL/Analysis/Fashoda_Theorem.thy Sun Oct 21 23:02:52 2018 +0100
@@ -2,15 +2,15 @@
Author: Robert Himmelmann, TU Muenchen (translation from HOL light)
*)
-section \<open>Fashoda meet theorem\<close>
+section%important \<open>Fashoda meet theorem\<close>
theory Fashoda_Theorem
imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
begin
-subsection \<open>Bijections between intervals\<close>
+subsection%important \<open>Bijections between intervals\<close>
-definition interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::euclidean_space"
+definition%important interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::euclidean_space"
where "interval_bij =
(\<lambda>(a, b) (u, v) x. (\<Sum>i\<in>Basis. (u\<bullet>i + (x\<bullet>i - a\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (v\<bullet>i - u\<bullet>i)) *\<^sub>R i))"
@@ -30,14 +30,14 @@
apply (rule, rule continuous_interval_bij)
done
-lemma in_interval_interval_bij:
+lemma%important in_interval_interval_bij:
fixes a b u v x :: "'a::euclidean_space"
assumes "x \<in> cbox a b"
and "cbox u v \<noteq> {}"
shows "interval_bij (a, b) (u, v) x \<in> cbox u v"
apply (simp only: interval_bij_def split_conv mem_box inner_sum_left_Basis cong: ball_cong)
apply safe
-proof -
+proof%unimportant -
fix i :: 'a
assume i: "i \<in> Basis"
have "cbox a b \<noteq> {}"
@@ -70,7 +70,7 @@
using assms by (intro interval_bij_bij) (auto simp: Basis_vec_def inner_axis)
-subsection \<open>Fashoda meet theorem\<close>
+subsection%important \<open>Fashoda meet theorem\<close>
lemma infnorm_2:
fixes x :: "real^2"
@@ -89,7 +89,7 @@
shows "\<bar>x$1\<bar> \<le> 1" and "\<bar>x$2\<bar> \<le> 1"
using assms unfolding infnorm_eq_1_2 by auto
-lemma fashoda_unit:
+lemma%important fashoda_unit:
fixes f g :: "real \<Rightarrow> real^2"
assumes "f ` {-1 .. 1} \<subseteq> cbox (-1) 1"
and "g ` {-1 .. 1} \<subseteq> cbox (-1) 1"
@@ -99,7 +99,7 @@
and "f 1$1 = 1" "g (- 1) $2 = -1"
and "g 1 $2 = 1"
shows "\<exists>s\<in>{-1 .. 1}. \<exists>t\<in>{-1 .. 1}. f s = g t"
-proof (rule ccontr)
+proof%unimportant (rule ccontr)
assume "\<not> ?thesis"
note as = this[unfolded bex_simps,rule_format]
define sqprojection
@@ -256,7 +256,7 @@
qed
qed
-lemma fashoda_unit_path:
+lemma%important fashoda_unit_path:
fixes f g :: "real \<Rightarrow> real^2"
assumes "path f"
and "path g"
@@ -267,7 +267,7 @@
and "(pathstart g)$2 = -1"
and "(pathfinish g)$2 = 1"
obtains z where "z \<in> path_image f" and "z \<in> path_image g"
-proof -
+proof%unimportant -
note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
define iscale where [abs_def]: "iscale z = inverse 2 *\<^sub>R (z + 1)" for z :: real
have isc: "iscale ` {- 1..1} \<subseteq> {0..1}"
@@ -312,7 +312,7 @@
done
qed
-lemma fashoda:
+lemma%important fashoda:
fixes b :: "real^2"
assumes "path f"
and "path g"
@@ -323,7 +323,7 @@
and "(pathstart g)$2 = a$2"
and "(pathfinish g)$2 = b$2"
obtains z where "z \<in> path_image f" and "z \<in> path_image g"
-proof -
+proof%unimportant -
fix P Q S
presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" and "Q \<Longrightarrow> thesis" and "S \<Longrightarrow> thesis"
then show thesis
@@ -470,7 +470,7 @@
qed
-subsection \<open>Some slightly ad hoc lemmas I use below\<close>
+subsection%unimportant \<open>Some slightly ad hoc lemmas I use below\<close>
lemma segment_vertical:
fixes a :: "real^2"
@@ -630,9 +630,9 @@
qed
-subsection \<open>Useful Fashoda corollary pointed out to me by Tom Hales\<close>
+subsection%important \<open>Useful Fashoda corollary pointed out to me by Tom Hales\<close>(*FIXME change title? *)
-lemma fashoda_interlace:
+lemma%important fashoda_interlace:
fixes a :: "real^2"
assumes "path f"
and "path g"
@@ -646,7 +646,7 @@
and "(pathstart g)$1 < (pathfinish f)$1"
and "(pathfinish f)$1 < (pathfinish g)$1"
obtains z where "z \<in> path_image f" and "z \<in> path_image g"
-proof -
+proof%unimportant -
have "cbox a b \<noteq> {}"
using path_image_nonempty[of f] using assms(3) by auto
note ab=this[unfolded interval_eq_empty_cart not_ex forall_2 not_less]
--- a/src/HOL/Analysis/Improper_Integral.thy Sun Oct 21 20:45:01 2018 +0200
+++ b/src/HOL/Analysis/Improper_Integral.thy Sun Oct 21 23:02:52 2018 +0100
@@ -1,15 +1,15 @@
-section\<open>Continuity of the indefinite integral; improper integral theorem\<close>
+section%important \<open>Continuity of the indefinite integral; improper integral theorem\<close>
theory "Improper_Integral"
imports Equivalence_Lebesgue_Henstock_Integration
begin
-subsection\<open>Equiintegrability\<close>
+subsection%important \<open>Equiintegrability\<close>
text\<open>The definition here only really makes sense for an elementary set.
We just use compact intervals in applications below.\<close>
-definition equiintegrable_on (infixr "equiintegrable'_on" 46)
+definition%important equiintegrable_on (infixr "equiintegrable'_on" 46)
where "F equiintegrable_on I \<equiv>
(\<forall>f \<in> F. f integrable_on I) \<and>
(\<forall>e > 0. \<exists>\<gamma>. gauge \<gamma> \<and>
@@ -28,11 +28,11 @@
unfolding equiintegrable_on_def Ball_def
by (erule conj_forward imp_forward all_forward ex_forward | blast)+
-lemma equiintegrable_on_Un:
+lemma%important equiintegrable_on_Un:
assumes "F equiintegrable_on I" "G equiintegrable_on I"
shows "(F \<union> G) equiintegrable_on I"
unfolding equiintegrable_on_def
-proof (intro conjI impI allI)
+proof%unimportant (intro conjI impI allI)
show "\<forall>f\<in>F \<union> G. f integrable_on I"
using assms unfolding equiintegrable_on_def by blast
show "\<exists>\<gamma>. gauge \<gamma> \<and>
@@ -76,12 +76,12 @@
text\<open> Main limit theorem for an equiintegrable sequence.\<close>
-theorem equiintegrable_limit:
+theorem%important equiintegrable_limit:
fixes g :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
assumes feq: "range f equiintegrable_on cbox a b"
and to_g: "\<And>x. x \<in> cbox a b \<Longrightarrow> (\<lambda>n. f n x) \<longlonglongrightarrow> g x"
shows "g integrable_on cbox a b \<and> (\<lambda>n. integral (cbox a b) (f n)) \<longlonglongrightarrow> integral (cbox a b) g"
-proof -
+proof%unimportant -
have "Cauchy (\<lambda>n. integral(cbox a b) (f n))"
proof (clarsimp simp add: Cauchy_def)
fix e::real
@@ -151,10 +151,10 @@
qed
-lemma equiintegrable_reflect:
+lemma%important equiintegrable_reflect:
assumes "F equiintegrable_on cbox a b"
shows "(\<lambda>f. f \<circ> uminus) ` F equiintegrable_on cbox (-b) (-a)"
-proof -
+proof%unimportant -
have "\<exists>\<gamma>. gauge \<gamma> \<and>
(\<forall>f \<D>. f \<in> (\<lambda>f. f \<circ> uminus) ` F \<and> \<D> tagged_division_of cbox (- b) (- a) \<and> \<gamma> fine \<D> \<longrightarrow>
norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral (cbox (- b) (- a)) f) < e)"
@@ -226,7 +226,7 @@
by auto
qed
-subsection\<open>Subinterval restrictions for equiintegrable families\<close>
+subsection%important\<open>Subinterval restrictions for equiintegrable families\<close>
text\<open>First, some technical lemmas about minimizing a "flat" part of a sum over a division.\<close>
@@ -246,13 +246,13 @@
qed
-lemma content_division_lemma1:
+lemma%important content_division_lemma1:
assumes div: "\<D> division_of S" and S: "S \<subseteq> cbox a b" and i: "i \<in> Basis"
and mt: "\<And>K. K \<in> \<D> \<Longrightarrow> content K \<noteq> 0"
and disj: "(\<forall>K \<in> \<D>. K \<inter> {x. x \<bullet> i = a \<bullet> i} \<noteq> {}) \<or> (\<forall>K \<in> \<D>. K \<inter> {x. x \<bullet> i = b \<bullet> i} \<noteq> {})"
shows "(b \<bullet> i - a \<bullet> i) * (\<Sum>K\<in>\<D>. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))
\<le> content(cbox a b)" (is "?lhs \<le> ?rhs")
-proof -
+proof%unimportant -
have "finite \<D>"
using div by blast
define extend where
@@ -409,13 +409,13 @@
qed
-proposition sum_content_area_over_thin_division:
+proposition%important sum_content_area_over_thin_division:
assumes div: "\<D> division_of S" and S: "S \<subseteq> cbox a b" and i: "i \<in> Basis"
and "a \<bullet> i \<le> c" "c \<le> b \<bullet> i"
and nonmt: "\<And>K. K \<in> \<D> \<Longrightarrow> K \<inter> {x. x \<bullet> i = c} \<noteq> {}"
shows "(b \<bullet> i - a \<bullet> i) * (\<Sum>K\<in>\<D>. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))
\<le> 2 * content(cbox a b)"
-proof (cases "content(cbox a b) = 0")
+proof%unimportant (cases "content(cbox a b) = 0")
case True
have "(\<Sum>K\<in>\<D>. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) = 0"
using S div by (force intro!: sum.neutral content_0_subset [OF True])
@@ -609,7 +609,7 @@
-proposition bounded_equiintegral_over_thin_tagged_partial_division:
+proposition%important bounded_equiintegral_over_thin_tagged_partial_division:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes F: "F equiintegrable_on cbox a b" and f: "f \<in> F" and "0 < \<epsilon>"
and norm_f: "\<And>h x. \<lbrakk>h \<in> F; x \<in> cbox a b\<rbrakk> \<Longrightarrow> norm(h x) \<le> norm(f x)"
@@ -617,7 +617,7 @@
"\<And>c i S h. \<lbrakk>c \<in> cbox a b; i \<in> Basis; S tagged_partial_division_of cbox a b;
\<gamma> fine S; h \<in> F; \<And>x K. (x,K) \<in> S \<Longrightarrow> (K \<inter> {x. x \<bullet> i = c \<bullet> i} \<noteq> {})\<rbrakk>
\<Longrightarrow> (\<Sum>(x,K) \<in> S. norm (integral K h)) < \<epsilon>"
-proof (cases "content(cbox a b) = 0")
+proof%unimportant (cases "content(cbox a b) = 0")
case True
show ?thesis
proof
@@ -813,13 +813,13 @@
-proposition equiintegrable_halfspace_restrictions_le:
+proposition%important equiintegrable_halfspace_restrictions_le:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes F: "F equiintegrable_on cbox a b" and f: "f \<in> F"
and norm_f: "\<And>h x. \<lbrakk>h \<in> F; x \<in> cbox a b\<rbrakk> \<Longrightarrow> norm(h x) \<le> norm(f x)"
shows "(\<Union>i \<in> Basis. \<Union>c. \<Union>h \<in> F. {(\<lambda>x. if x \<bullet> i \<le> c then h x else 0)})
equiintegrable_on cbox a b"
-proof (cases "content(cbox a b) = 0")
+proof%unimportant (cases "content(cbox a b) = 0")
case True
then show ?thesis by simp
next
@@ -1172,13 +1172,13 @@
-corollary equiintegrable_halfspace_restrictions_ge:
+corollary%important equiintegrable_halfspace_restrictions_ge:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes F: "F equiintegrable_on cbox a b" and f: "f \<in> F"
and norm_f: "\<And>h x. \<lbrakk>h \<in> F; x \<in> cbox a b\<rbrakk> \<Longrightarrow> norm(h x) \<le> norm(f x)"
shows "(\<Union>i \<in> Basis. \<Union>c. \<Union>h \<in> F. {(\<lambda>x. if x \<bullet> i \<ge> c then h x else 0)})
equiintegrable_on cbox a b"
-proof -
+proof%unimportant -
have *: "(\<Union>i\<in>Basis. \<Union>c. \<Union>h\<in>(\<lambda>f. f \<circ> uminus) ` F. {\<lambda>x. if x \<bullet> i \<le> c then h x else 0})
equiintegrable_on cbox (- b) (- a)"
proof (rule equiintegrable_halfspace_restrictions_le)
@@ -1203,11 +1203,11 @@
qed
-proposition equiintegrable_closed_interval_restrictions:
+proposition%important equiintegrable_closed_interval_restrictions:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes f: "f integrable_on cbox a b"
shows "(\<Union>c d. {(\<lambda>x. if x \<in> cbox c d then f x else 0)}) equiintegrable_on cbox a b"
-proof -
+proof%unimportant -
let ?g = "\<lambda>B c d x. if \<forall>i\<in>B. c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i then f x else 0"
have *: "insert f (\<Union>c d. {?g B c d}) equiintegrable_on cbox a b" if "B \<subseteq> Basis" for B
proof -
@@ -1264,16 +1264,16 @@
-subsection\<open>Continuity of the indefinite integral\<close>
+subsection%important\<open>Continuity of the indefinite integral\<close>
-proposition indefinite_integral_continuous:
+proposition%important indefinite_integral_continuous:
fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
assumes int_f: "f integrable_on cbox a b"
and c: "c \<in> cbox a b" and d: "d \<in> cbox a b" "0 < \<epsilon>"
obtains \<delta> where "0 < \<delta>"
"\<And>c' d'. \<lbrakk>c' \<in> cbox a b; d' \<in> cbox a b; norm(c' - c) \<le> \<delta>; norm(d' - d) \<le> \<delta>\<rbrakk>
\<Longrightarrow> norm(integral(cbox c' d') f - integral(cbox c d) f) < \<epsilon>"
-proof -
+proof%unimportant -
{ assume "\<exists>c' d'. c' \<in> cbox a b \<and> d' \<in> cbox a b \<and> norm(c' - c) \<le> \<delta> \<and> norm(d' - d) \<le> \<delta> \<and>
norm(integral(cbox c' d') f - integral(cbox c d) f) \<ge> \<epsilon>"
(is "\<exists>c' d'. ?\<Phi> c' d' \<delta>") if "0 < \<delta>" for \<delta>
@@ -1358,11 +1358,11 @@
by (meson not_le that)
qed
-corollary indefinite_integral_uniformly_continuous:
+corollary%important indefinite_integral_uniformly_continuous:
fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
assumes "f integrable_on cbox a b"
shows "uniformly_continuous_on (cbox (Pair a a) (Pair b b)) (\<lambda>y. integral (cbox (fst y) (snd y)) f)"
-proof -
+proof%unimportant -
show ?thesis
proof (rule compact_uniformly_continuous, clarsimp simp add: continuous_on_iff)
fix c d and \<epsilon>::real
@@ -1383,11 +1383,11 @@
qed
-corollary bounded_integrals_over_subintervals:
+corollary%important bounded_integrals_over_subintervals:
fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
assumes "f integrable_on cbox a b"
shows "bounded {integral (cbox c d) f |c d. cbox c d \<subseteq> cbox a b}"
-proof -
+proof%unimportant -
have "bounded ((\<lambda>y. integral (cbox (fst y) (snd y)) f) ` cbox (a, a) (b, b))"
(is "bounded ?I")
by (blast intro: bounded_cbox bounded_uniformly_continuous_image indefinite_integral_uniformly_continuous [OF assms])
@@ -1414,7 +1414,7 @@
We only need to assume that the integrals are bounded, and we get absolute integrability,
but we also need a (rather weak) bound assumption on the function.\<close>
-theorem absolutely_integrable_improper:
+theorem%important absolutely_integrable_improper:
fixes f :: "'M::euclidean_space \<Rightarrow> 'N::euclidean_space"
assumes int_f: "\<And>c d. cbox c d \<subseteq> box a b \<Longrightarrow> f integrable_on cbox c d"
and bo: "bounded {integral (cbox c d) f |c d. cbox c d \<subseteq> box a b}"
@@ -1422,7 +1422,7 @@
\<Longrightarrow> \<exists>g. g absolutely_integrable_on cbox a b \<and>
((\<forall>x \<in> cbox a b. f x \<bullet> i \<le> g x) \<or> (\<forall>x \<in> cbox a b. f x \<bullet> i \<ge> g x))"
shows "f absolutely_integrable_on cbox a b"
-proof (cases "content(cbox a b) = 0")
+proof%unimportant (cases "content(cbox a b) = 0")
case True
then show ?thesis
by auto
--- a/src/HOL/Analysis/Interval_Integral.thy Sun Oct 21 20:45:01 2018 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy Sun Oct 21 23:02:52 2018 +0100
@@ -8,11 +8,11 @@
imports Equivalence_Lebesgue_Henstock_Integration
begin
-lemma continuous_on_vector_derivative:
+lemma%important continuous_on_vector_derivative:
"(\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)) \<Longrightarrow> continuous_on S f"
- by (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous)
+ by%unimportant (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous)
-definition "einterval a b = {x. a < ereal x \<and> ereal x < b}"
+definition%important "einterval a b = {x. a < ereal x \<and> ereal x < b}"
lemma einterval_eq[simp]:
shows einterval_eq_Icc: "einterval (ereal a) (ereal b) = {a <..< b}"
@@ -42,11 +42,11 @@
lemma filterlim_sup1: "(LIM x F. f x :> G1) \<Longrightarrow> (LIM x F. f x :> (sup G1 G2))"
unfolding filterlim_def by (auto intro: le_supI1)
-lemma ereal_incseq_approx:
+lemma%important ereal_incseq_approx:
fixes a b :: ereal
assumes "a < b"
obtains X :: "nat \<Rightarrow> real" where "incseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> b"
-proof (cases b)
+proof%unimportant (cases b)
case PInf
with \<open>a < b\<close> have "a = -\<infinity> \<or> (\<exists>r. a = ereal r)"
by (cases a) auto
@@ -78,12 +78,12 @@
(auto simp: real incseq_def intro!: divide_left_mono)
qed (insert \<open>a < b\<close>, auto)
-lemma ereal_decseq_approx:
+lemma%important ereal_decseq_approx:
fixes a b :: ereal
assumes "a < b"
obtains X :: "nat \<Rightarrow> real" where
"decseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> a"
-proof -
+proof%unimportant -
have "-b < -a" using \<open>a < b\<close> by simp
from ereal_incseq_approx[OF this] guess X .
then show thesis
@@ -93,14 +93,14 @@
done
qed
-lemma einterval_Icc_approximation:
+lemma%important einterval_Icc_approximation:
fixes a b :: ereal
assumes "a < b"
obtains u l :: "nat \<Rightarrow> real" where
"einterval a b = (\<Union>i. {l i .. u i})"
"incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
"l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b"
-proof -
+proof%unimportant -
from dense[OF \<open>a < b\<close>] obtain c where "a < c" "c < b" by safe
from ereal_incseq_approx[OF \<open>c < b\<close>] guess u . note u = this
from ereal_decseq_approx[OF \<open>a < c\<close>] guess l . note l = this
@@ -129,7 +129,7 @@
(* TODO: in this definition, it would be more natural if einterval a b included a and b when
they are real. *)
-definition interval_lebesgue_integral :: "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> 'a::{banach, second_countable_topology}" where
+definition%important interval_lebesgue_integral :: "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> 'a::{banach, second_countable_topology}" where
"interval_lebesgue_integral M a b f =
(if a \<le> b then (LINT x:einterval a b|M. f x) else - (LINT x:einterval b a|M. f x))"
@@ -140,7 +140,7 @@
translations
"LINT x=a..b|M. f" == "CONST interval_lebesgue_integral M a b (\<lambda>x. f)"
-definition interval_lebesgue_integrable :: "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> 'a::{banach, second_countable_topology}) \<Rightarrow> bool" where
+definition%important interval_lebesgue_integrable :: "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> 'a::{banach, second_countable_topology}) \<Rightarrow> bool" where
"interval_lebesgue_integrable M a b f =
(if a \<le> b then set_integrable M (einterval a b) f else set_integrable M (einterval b a) f)"
@@ -151,7 +151,7 @@
translations
"LBINT x=a..b. f" == "CONST interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"
-subsection\<open>Basic properties of integration over an interval\<close>
+subsection%important\<open>Basic properties of integration over an interval\<close>
lemma interval_lebesgue_integral_cong:
"a \<le> b \<Longrightarrow> (\<And>x. x \<in> einterval a b \<Longrightarrow> f x = g x) \<Longrightarrow> einterval a b \<in> sets M \<Longrightarrow>
@@ -202,17 +202,17 @@
interval_lebesgue_integrable M a b (\<lambda>x. c * f x)"
by (simp add: interval_lebesgue_integrable_def)
-lemma interval_lebesgue_integrable_mult_left [intro, simp]:
+lemma%important interval_lebesgue_integrable_mult_left [intro, simp]:
fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow>
interval_lebesgue_integrable M a b (\<lambda>x. f x * c)"
- by (simp add: interval_lebesgue_integrable_def)
+ by%unimportant (simp add: interval_lebesgue_integrable_def)
-lemma interval_lebesgue_integrable_divide [intro, simp]:
+lemma%important interval_lebesgue_integrable_divide [intro, simp]:
fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field, second_countable_topology}"
shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow>
interval_lebesgue_integrable M a b (\<lambda>x. f x / c)"
- by (simp add: interval_lebesgue_integrable_def)
+ by%unimportant (simp add: interval_lebesgue_integrable_def)
lemma interval_lebesgue_integral_mult_right [simp]:
fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
@@ -220,11 +220,11 @@
c * interval_lebesgue_integral M a b f"
by (simp add: interval_lebesgue_integral_def)
-lemma interval_lebesgue_integral_mult_left [simp]:
+lemma%important interval_lebesgue_integral_mult_left [simp]:
fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
shows "interval_lebesgue_integral M a b (\<lambda>x. f x * c) =
interval_lebesgue_integral M a b f * c"
- by (simp add: interval_lebesgue_integral_def)
+ by%unimportant (simp add: interval_lebesgue_integral_def)
lemma interval_lebesgue_integral_divide [simp]:
fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field, second_countable_topology}"
@@ -242,11 +242,11 @@
unfolding interval_lebesgue_integral_def
by (auto simp: interval_lebesgue_integral_def set_integral_complex_of_real)
-lemma interval_lebesgue_integral_le_eq:
+lemma%important interval_lebesgue_integral_le_eq:
fixes a b f
assumes "a \<le> b"
shows "interval_lebesgue_integral M a b f = (LINT x : einterval a b | M. f x)"
-using assms by (auto simp: interval_lebesgue_integral_def)
+using%unimportant assms by (auto simp: interval_lebesgue_integral_def)
lemma interval_lebesgue_integral_gt_eq:
fixes a b f
@@ -271,9 +271,9 @@
interval_lebesgue_integrable lborel b a f"
by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integrable_def einterval_same)
-lemma interval_integral_reflect:
+lemma%important interval_integral_reflect:
"(LBINT x=a..b. f x) = (LBINT x=-b..-a. f (-x))"
-proof (induct a b rule: linorder_wlog)
+proof%unimportant (induct a b rule: linorder_wlog)
case (sym a b) then show ?case
by (auto simp: interval_lebesgue_integral_def interval_integrable_endpoints_reverse
split: if_split_asm)
@@ -299,11 +299,11 @@
lemma interval_integral_to_infinity_eq: "(LINT x=ereal a..\<infinity> | M. f x) = (LINT x : {a<..} | M. f x)"
unfolding interval_lebesgue_integral_def by auto
-lemma interval_integrable_to_infinity_eq: "(interval_lebesgue_integrable M a \<infinity> f) =
+lemma%important interval_integrable_to_infinity_eq: "(interval_lebesgue_integrable M a \<infinity> f) =
(set_integrable M {a<..} f)"
- unfolding interval_lebesgue_integrable_def by auto
+ unfolding%unimportant interval_lebesgue_integrable_def by auto
-subsection\<open>Basic properties of integration over an interval wrt lebesgue measure\<close>
+subsection%important\<open>Basic properties of integration over an interval wrt lebesgue measure\<close>
lemma interval_integral_zero [simp]:
fixes a b :: ereal
@@ -317,12 +317,12 @@
unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq
by (auto simp: less_imp_le field_simps measure_def set_integrable_def set_lebesgue_integral_def)
-lemma interval_integral_cong_AE:
+lemma%important interval_integral_cong_AE:
assumes [measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel"
assumes "AE x \<in> einterval (min a b) (max a b) in lborel. f x = g x"
shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g"
using assms
-proof (induct a b rule: linorder_wlog)
+proof%unimportant (induct a b rule: linorder_wlog)
case (sym a b) then show ?case
by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b])
next
@@ -331,11 +331,11 @@
intro!: set_lebesgue_integral_cong_AE)
qed
-lemma interval_integral_cong:
+lemma%important interval_integral_cong:
assumes "\<And>x. x \<in> einterval (min a b) (max a b) \<Longrightarrow> f x = g x"
shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g"
using assms
-proof (induct a b rule: linorder_wlog)
+proof%unimportant (induct a b rule: linorder_wlog)
case (sym a b) then show ?case
by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b])
next
@@ -407,11 +407,11 @@
apply (auto simp: eq anti_eq einterval_iff split: split_indicator)
done
-lemma interval_integral_sum:
+lemma%important interval_integral_sum:
fixes a b c :: ereal
assumes integrable: "interval_lebesgue_integrable lborel (min a (min b c)) (max a (max b c)) f"
shows "(LBINT x=a..b. f x) + (LBINT x=b..c. f x) = (LBINT x=a..c. f x)"
-proof -
+proof%unimportant -
let ?I = "\<lambda>a b. LBINT x=a..b. f x"
{ fix a b c :: ereal assume "interval_lebesgue_integrable lborel a c f" "a \<le> b" "b \<le> c"
then have ord: "a \<le> b" "b \<le> c" "a \<le> c" and f': "set_integrable lborel (einterval a c) f"
@@ -446,11 +446,11 @@
(simp_all add: min_absorb1 min_absorb2 max_absorb1 max_absorb2 field_simps 1 2 3)
qed
-lemma interval_integrable_isCont:
+lemma%important interval_integrable_isCont:
fixes a b and f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
shows "(\<And>x. min a b \<le> x \<Longrightarrow> x \<le> max a b \<Longrightarrow> isCont f x) \<Longrightarrow>
interval_lebesgue_integrable lborel a b f"
-proof (induct a b rule: linorder_wlog)
+proof%unimportant (induct a b rule: linorder_wlog)
case (le a b) then show ?case
unfolding interval_lebesgue_integrable_def set_integrable_def
by (auto simp: interval_lebesgue_integrable_def
@@ -476,9 +476,9 @@
by (subst interval_lebesgue_integral_le_eq, simp) (rule set_borel_integral_eq_integral)
-subsection\<open>General limit approximation arguments\<close>
+subsection%important\<open>General limit approximation arguments\<close>
-lemma interval_integral_Icc_approx_nonneg:
+lemma%important interval_integral_Icc_approx_nonneg:
fixes a b :: ereal
assumes "a < b"
fixes u l :: "nat \<Rightarrow> real"
@@ -493,7 +493,7 @@
shows
"set_integrable lborel (einterval a b) f"
"(LBINT x=a..b. f x) = C"
-proof -
+proof%unimportant -
have 1 [unfolded set_integrable_def]: "\<And>i. set_integrable lborel {l i..u i} f" by (rule f_integrable)
have 2: "AE x in lborel. mono (\<lambda>n. indicator {l n..u n} x *\<^sub>R f x)"
proof -
@@ -534,7 +534,7 @@
by (rule integrable_monotone_convergence[OF 1 2 3 4 5])
qed
-lemma interval_integral_Icc_approx_integrable:
+lemma%important interval_integral_Icc_approx_integrable:
fixes u l :: "nat \<Rightarrow> real" and a b :: ereal
fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
assumes "a < b"
@@ -543,7 +543,7 @@
"l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b"
assumes f_integrable: "set_integrable lborel (einterval a b) f"
shows "(\<lambda>i. LBINT x=l i.. u i. f x) \<longlonglongrightarrow> (LBINT x=a..b. f x)"
-proof -
+proof%unimportant -
have "(\<lambda>i. LBINT x:{l i.. u i}. f x) \<longlonglongrightarrow> (LBINT x:einterval a b. f x)"
unfolding set_lebesgue_integral_def
proof (rule integral_dominated_convergence)
@@ -571,7 +571,7 @@
by (simp add: interval_lebesgue_integral_le_eq[symmetric] interval_integral_Icc less_imp_le)
qed
-subsection\<open>A slightly stronger Fundamental Theorem of Calculus\<close>
+subsection%important\<open>A slightly stronger Fundamental Theorem of Calculus\<close>
text\<open>Three versions: first, for finite intervals, and then two versions for
arbitrary intervals.\<close>
@@ -580,13 +580,13 @@
TODO: make the older versions corollaries of these (using continuous_at_imp_continuous_on, etc.)
*)
-lemma interval_integral_FTC_finite:
+lemma%important interval_integral_FTC_finite:
fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: real
assumes f: "continuous_on {min a b..max a b} f"
assumes F: "\<And>x. min a b \<le> x \<Longrightarrow> x \<le> max a b \<Longrightarrow> (F has_vector_derivative (f x)) (at x within
{min a b..max a b})"
shows "(LBINT x=a..b. f x) = F b - F a"
-proof (cases "a \<le> b")
+proof%unimportant (cases "a \<le> b")
case True
have "(LBINT x=a..b. f x) = (LBINT x. indicat_real {a..b} x *\<^sub>R f x)"
by (simp add: True interval_integral_Icc set_lebesgue_integral_def)
@@ -617,7 +617,7 @@
qed
-lemma interval_integral_FTC_nonneg:
+lemma%important interval_integral_FTC_nonneg:
fixes f F :: "real \<Rightarrow> real" and a b :: ereal
assumes "a < b"
assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV F x :> f x"
@@ -628,7 +628,7 @@
shows
"set_integrable lborel (einterval a b) f"
"(LBINT x=a..b. f x) = B - A"
-proof -
+proof%unimportant -
obtain u l where approx:
"einterval a b = (\<Union>i. {l i .. u i})"
"incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
@@ -669,7 +669,7 @@
by (rule interval_integral_Icc_approx_nonneg [OF \<open>a < b\<close> approx 1 f_nonneg 2 3])
qed
-lemma interval_integral_FTC_integrable:
+lemma%important interval_integral_FTC_integrable:
fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: ereal
assumes "a < b"
assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> (F has_vector_derivative f x) (at x)"
@@ -678,7 +678,7 @@
assumes A: "((F \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)"
assumes B: "((F \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)"
shows "(LBINT x=a..b. f x) = B - A"
-proof -
+proof%unimportant -
obtain u l where approx:
"einterval a b = (\<Union>i. {l i .. u i})"
"incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
@@ -714,14 +714,14 @@
einterval.
*)
-lemma interval_integral_FTC2:
+lemma%important interval_integral_FTC2:
fixes a b c :: real and f :: "real \<Rightarrow> 'a::euclidean_space"
assumes "a \<le> c" "c \<le> b"
and contf: "continuous_on {a..b} f"
fixes x :: real
assumes "a \<le> x" and "x \<le> b"
shows "((\<lambda>u. LBINT y=c..u. f y) has_vector_derivative (f x)) (at x within {a..b})"
-proof -
+proof%unimportant -
let ?F = "(\<lambda>u. LBINT y=a..u. f y)"
have intf: "set_integrable lborel {a..b} f"
by (rule borel_integrable_atLeastAtMost', rule contf)
@@ -746,11 +746,11 @@
qed (insert assms, auto)
qed
-lemma einterval_antiderivative:
+lemma%important einterval_antiderivative:
fixes a b :: ereal and f :: "real \<Rightarrow> 'a::euclidean_space"
assumes "a < b" and contf: "\<And>x :: real. a < x \<Longrightarrow> x < b \<Longrightarrow> isCont f x"
shows "\<exists>F. \<forall>x :: real. a < x \<longrightarrow> x < b \<longrightarrow> (F has_vector_derivative f x) (at x)"
-proof -
+proof%unimportant -
from einterval_nonempty [OF \<open>a < b\<close>] obtain c :: real where [simp]: "a < c" "c < b"
by (auto simp: einterval_def)
let ?F = "(\<lambda>u. LBINT y=c..u. f y)"
@@ -781,19 +781,19 @@
qed
qed
-subsection\<open>The substitution theorem\<close>
+subsection%important\<open>The substitution theorem\<close>
text\<open>Once again, three versions: first, for finite intervals, and then two versions for
arbitrary intervals.\<close>
-lemma interval_integral_substitution_finite:
+lemma%important interval_integral_substitution_finite:
fixes a b :: real and f :: "real \<Rightarrow> 'a::euclidean_space"
assumes "a \<le> b"
and derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_real_derivative (g' x)) (at x within {a..b})"
and contf : "continuous_on (g ` {a..b}) f"
and contg': "continuous_on {a..b} g'"
shows "LBINT x=a..b. g' x *\<^sub>R f (g x) = LBINT y=g a..g b. f y"
-proof-
+proof%unimportant-
have v_derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_vector_derivative (g' x)) (at x within {a..b})"
using derivg unfolding has_field_derivative_iff_has_vector_derivative .
then have contg [simp]: "continuous_on {a..b} g"
@@ -833,7 +833,7 @@
(* TODO: is it possible to lift the assumption here that g' is nonnegative? *)
-lemma interval_integral_substitution_integrable:
+lemma%important interval_integral_substitution_integrable:
fixes f :: "real \<Rightarrow> 'a::euclidean_space" and a b u v :: ereal
assumes "a < b"
and deriv_g: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV g x :> g' x"
@@ -845,7 +845,7 @@
and integrable: "set_integrable lborel (einterval a b) (\<lambda>x. g' x *\<^sub>R f (g x))"
and integrable2: "set_integrable lborel (einterval A B) (\<lambda>x. f x)"
shows "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *\<^sub>R f (g x))"
-proof -
+proof%unimportant -
obtain u l where approx [simp]:
"einterval a b = (\<Union>i. {l i .. u i})"
"incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
@@ -932,7 +932,7 @@
An alternative: make the second one the main one, and then have another lemma
that says that if f is nonnegative and all the other hypotheses hold, then it is integrable. *)
-lemma interval_integral_substitution_nonneg:
+lemma%important interval_integral_substitution_nonneg:
fixes f g g':: "real \<Rightarrow> real" and a b u v :: ereal
assumes "a < b"
and deriv_g: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV g x :> g' x"
@@ -946,7 +946,7 @@
shows
"set_integrable lborel (einterval A B) f"
"(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))"
-proof -
+proof%unimportant -
from einterval_Icc_approximation[OF \<open>a < b\<close>] guess u l . note approx [simp] = this
note less_imp_le [simp]
have aless[simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
@@ -1079,17 +1079,17 @@
translations
"CLBINT x=a..b. f" == "CONST complex_interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"
-lemma interval_integral_norm:
+lemma%important interval_integral_norm:
fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
shows "interval_lebesgue_integrable lborel a b f \<Longrightarrow> a \<le> b \<Longrightarrow>
norm (LBINT t=a..b. f t) \<le> LBINT t=a..b. norm (f t)"
- using integral_norm_bound[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"]
- by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def)
+ using%unimportant integral_norm_bound[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"]
+ by%unimportant (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def)
-lemma interval_integral_norm2:
+lemma%important interval_integral_norm2:
"interval_lebesgue_integrable lborel a b f \<Longrightarrow>
norm (LBINT t=a..b. f t) \<le> \<bar>LBINT t=a..b. norm (f t)\<bar>"
-proof (induct a b rule: linorder_wlog)
+proof%unimportant (induct a b rule: linorder_wlog)
case (sym a b) then show ?case
by (simp add: interval_integral_endpoints_reverse[of a b] interval_integrable_endpoints_reverse[of a b])
next
--- a/src/HOL/Analysis/Radon_Nikodym.thy Sun Oct 21 20:45:01 2018 +0200
+++ b/src/HOL/Analysis/Radon_Nikodym.thy Sun Oct 21 23:02:52 2018 +0100
@@ -2,13 +2,13 @@
Author: Johannes Hölzl, TU München
*)
-section \<open>Radon-Nikod{\'y}m derivative\<close>
+section%important \<open>Radon-Nikod{\'y}m derivative\<close>
theory Radon_Nikodym
imports Bochner_Integration
begin
-definition diff_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
+definition%important diff_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
where
"diff_measure M N = measure_of (space M) (sets M) (\<lambda>A. emeasure M A - emeasure N A)"
@@ -17,12 +17,12 @@
and sets_diff_measure[simp]: "sets (diff_measure M N) = sets M"
by (auto simp: diff_measure_def)
-lemma emeasure_diff_measure:
+lemma%important emeasure_diff_measure:
assumes fin: "finite_measure M" "finite_measure N" and sets_eq: "sets M = sets N"
assumes pos: "\<And>A. A \<in> sets M \<Longrightarrow> emeasure N A \<le> emeasure M A" and A: "A \<in> sets M"
shows "emeasure (diff_measure M N) A = emeasure M A - emeasure N A" (is "_ = ?\<mu> A")
- unfolding diff_measure_def
-proof (rule emeasure_measure_of_sigma)
+ unfolding%unimportant diff_measure_def
+proof%unimportant (rule emeasure_measure_of_sigma)
show "sigma_algebra (space M) (sets M)" ..
show "positive (sets M) ?\<mu>"
using pos by (simp add: positive_def)
@@ -102,9 +102,9 @@
by (meson that)
qed
-lemma (in sigma_finite_measure) Ex_finite_integrable_function:
+lemma%important (in sigma_finite_measure) Ex_finite_integrable_function:
"\<exists>h\<in>borel_measurable M. integral\<^sup>N M h \<noteq> \<infinity> \<and> (\<forall>x\<in>space M. 0 < h x \<and> h x < \<infinity>)"
-proof -
+proof%unimportant -
obtain A :: "nat \<Rightarrow> 'a set" where
range[measurable]: "range A \<subseteq> sets M" and
space: "(\<Union>i. A i) = space M" and
@@ -163,9 +163,9 @@
qed measurable
qed
-subsection "Absolutely continuous"
+subsection%important "Absolutely continuous"
-definition absolutely_continuous :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
+definition%important absolutely_continuous :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
"absolutely_continuous M N \<longleftrightarrow> null_sets M \<subseteq> null_sets N"
lemma absolutely_continuousI_count_space: "absolutely_continuous (count_space A) M"
@@ -183,11 +183,11 @@
"absolutely_continuous M N \<Longrightarrow> A \<in> sets M \<Longrightarrow> emeasure M A = 0 \<Longrightarrow> emeasure N A = 0"
by (auto simp: absolutely_continuous_def null_sets_def)
-lemma absolutely_continuous_AE:
+lemma%important absolutely_continuous_AE:
assumes sets_eq: "sets M' = sets M"
and "absolutely_continuous M M'" "AE x in M. P x"
shows "AE x in M'. P x"
-proof -
+proof%unimportant -
from \<open>AE x in M. P x\<close> obtain N where N: "N \<in> null_sets M" "{x\<in>space M. \<not> P x} \<subseteq> N"
unfolding eventually_ae_filter by auto
show "AE x in M'. P x"
@@ -198,13 +198,14 @@
qed
qed
-subsection "Existence of the Radon-Nikodym derivative"
+subsection%important "Existence of the Radon-Nikodym derivative"
-lemma (in finite_measure) Radon_Nikodym_finite_measure:
+lemma%important
+ (in finite_measure) Radon_Nikodym_finite_measure:
assumes "finite_measure N" and sets_eq[simp]: "sets N = sets M"
assumes "absolutely_continuous M N"
shows "\<exists>f \<in> borel_measurable M. density M f = N"
-proof -
+proof%unimportant -
interpret N: finite_measure N by fact
define G where "G = {g \<in> borel_measurable M. \<forall>A\<in>sets M. (\<integral>\<^sup>+x. g x * indicator A x \<partial>M) \<le> N A}"
have [measurable_dest]: "f \<in> G \<Longrightarrow> f \<in> borel_measurable M"
@@ -383,11 +384,11 @@
qed auto
qed
-lemma (in finite_measure) split_space_into_finite_sets_and_rest:
+lemma%important (in finite_measure) split_space_into_finite_sets_and_rest:
assumes ac: "absolutely_continuous M N" and sets_eq[simp]: "sets N = sets M"
shows "\<exists>B::nat\<Rightarrow>'a set. disjoint_family B \<and> range B \<subseteq> sets M \<and> (\<forall>i. N (B i) \<noteq> \<infinity>) \<and>
(\<forall>A\<in>sets M. A \<inter> (\<Union>i. B i) = {} \<longrightarrow> (emeasure M A = 0 \<and> N A = 0) \<or> (emeasure M A > 0 \<and> N A = \<infinity>))"
-proof -
+proof%unimportant -
let ?Q = "{Q\<in>sets M. N Q \<noteq> \<infinity>}"
let ?a = "SUP Q:?Q. emeasure M Q"
have "{} \<in> ?Q" by auto
@@ -492,10 +493,10 @@
qed
qed
-lemma (in finite_measure) Radon_Nikodym_finite_measure_infinite:
+lemma%important (in finite_measure) Radon_Nikodym_finite_measure_infinite:
assumes "absolutely_continuous M N" and sets_eq: "sets N = sets M"
shows "\<exists>f\<in>borel_measurable M. density M f = N"
-proof -
+proof%unimportant -
from split_space_into_finite_sets_and_rest[OF assms]
obtain Q :: "nat \<Rightarrow> 'a set"
where Q: "disjoint_family Q" "range Q \<subseteq> sets M"
@@ -606,14 +607,14 @@
by (auto intro!: bexI[of _ "\<lambda>x. h x * f x"] simp: density_density_eq)
qed
-subsection \<open>Uniqueness of densities\<close>
+subsection%important \<open>Uniqueness of densities\<close>
-lemma finite_density_unique:
+lemma%important finite_density_unique:
assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
assumes pos: "AE x in M. 0 \<le> f x" "AE x in M. 0 \<le> g x"
and fin: "integral\<^sup>N M f \<noteq> \<infinity>"
shows "density M f = density M g \<longleftrightarrow> (AE x in M. f x = g x)"
-proof (intro iffI ballI)
+proof%unimportant (intro iffI ballI)
fix A assume eq: "AE x in M. f x = g x"
with borel show "density M f = density M g"
by (auto intro: density_cong)
@@ -651,13 +652,13 @@
show "AE x in M. f x = g x" by auto
qed
-lemma (in finite_measure) density_unique_finite_measure:
+lemma%important (in finite_measure) density_unique_finite_measure:
assumes borel: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
assumes pos: "AE x in M. 0 \<le> f x" "AE x in M. 0 \<le> f' x"
assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>\<^sup>+x. f x * indicator A x \<partial>M) = (\<integral>\<^sup>+x. f' x * indicator A x \<partial>M)"
(is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A")
shows "AE x in M. f x = f' x"
-proof -
+proof%unimportant -
let ?D = "\<lambda>f. density M f"
let ?N = "\<lambda>A. ?P f A" and ?N' = "\<lambda>A. ?P f' A"
let ?f = "\<lambda>A x. f x * indicator A x" and ?f' = "\<lambda>A x. f' x * indicator A x"
@@ -763,11 +764,11 @@
shows "density M f = density M f' \<longleftrightarrow> (AE x in M. f x = f' x)"
using density_unique[OF assms] density_cong[OF f f'] by auto
-lemma sigma_finite_density_unique:
+lemma%important sigma_finite_density_unique:
assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
and fin: "sigma_finite_measure (density M f)"
shows "density M f = density M g \<longleftrightarrow> (AE x in M. f x = g x)"
-proof
+proof%unimportant
assume "AE x in M. f x = g x" with borel show "density M f = density M g"
by (auto intro: density_cong)
next
@@ -796,11 +797,11 @@
done
qed
-lemma (in sigma_finite_measure) sigma_finite_iff_density_finite':
+lemma%important (in sigma_finite_measure) sigma_finite_iff_density_finite':
assumes f: "f \<in> borel_measurable M"
shows "sigma_finite_measure (density M f) \<longleftrightarrow> (AE x in M. f x \<noteq> \<infinity>)"
(is "sigma_finite_measure ?N \<longleftrightarrow> _")
-proof
+proof%unimportant
assume "sigma_finite_measure ?N"
then interpret N: sigma_finite_measure ?N .
from N.Ex_finite_integrable_function obtain h where
@@ -886,18 +887,18 @@
by (subst sigma_finite_iff_density_finite')
(auto simp: max_def intro!: measurable_If)
-subsection \<open>Radon-Nikodym derivative\<close>
+subsection%important \<open>Radon-Nikodym derivative\<close>
-definition RN_deriv :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a \<Rightarrow> ennreal" where
+definition%important RN_deriv :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a \<Rightarrow> ennreal" where
"RN_deriv M N =
(if \<exists>f. f \<in> borel_measurable M \<and> density M f = N
then SOME f. f \<in> borel_measurable M \<and> density M f = N
else (\<lambda>_. 0))"
-lemma RN_derivI:
+lemma%important RN_derivI:
assumes "f \<in> borel_measurable M" "density M f = N"
shows "density M (RN_deriv M N) = N"
-proof -
+proof%unimportant -
have *: "\<exists>f. f \<in> borel_measurable M \<and> density M f = N"
using assms by auto
then have "density M (SOME f. f \<in> borel_measurable M \<and> density M f = N) = N"
@@ -924,11 +925,11 @@
"absolutely_continuous M N \<Longrightarrow> sets N = sets M \<Longrightarrow> density M (RN_deriv M N) = N"
by (metis RN_derivI Radon_Nikodym)
-lemma (in sigma_finite_measure) RN_deriv_nn_integral:
+lemma%important (in sigma_finite_measure) RN_deriv_nn_integral:
assumes N: "absolutely_continuous M N" "sets N = sets M"
and f: "f \<in> borel_measurable M"
shows "integral\<^sup>N N f = (\<integral>\<^sup>+x. RN_deriv M N x * f x \<partial>M)"
-proof -
+proof%unimportant -
have "integral\<^sup>N N f = integral\<^sup>N (density M (RN_deriv M N)) f"
using N by (simp add: density_RN_deriv)
also have "\<dots> = (\<integral>\<^sup>+x. RN_deriv M N x * f x \<partial>M)"
@@ -952,14 +953,14 @@
by (intro sigma_finite_density_unique[THEN iffD1] f borel_measurable_RN_deriv
density_RN_deriv_density[symmetric])
-lemma (in sigma_finite_measure) RN_deriv_distr:
+lemma%important (in sigma_finite_measure) RN_deriv_distr:
fixes T :: "'a \<Rightarrow> 'b"
assumes T: "T \<in> measurable M M'" and T': "T' \<in> measurable M' M"
and inv: "\<forall>x\<in>space M. T' (T x) = x"
and ac[simp]: "absolutely_continuous (distr M M' T) (distr N M' T)"
and N: "sets N = sets M"
shows "AE x in M. RN_deriv (distr M M' T) (distr N M' T) (T x) = RN_deriv M N x"
-proof (rule RN_deriv_unique)
+proof%unimportant (rule RN_deriv_unique)
have [simp]: "sets N = sets M" by fact
note sets_eq_imp_space_eq[OF N, simp]
have measurable_N[simp]: "\<And>M'. measurable N M' = measurable M M'" by (auto simp: measurable_def)
@@ -1011,23 +1012,23 @@
by (simp add: comp_def)
qed
-lemma (in sigma_finite_measure) RN_deriv_finite:
+lemma%important (in sigma_finite_measure) RN_deriv_finite:
assumes N: "sigma_finite_measure N" and ac: "absolutely_continuous M N" "sets N = sets M"
shows "AE x in M. RN_deriv M N x \<noteq> \<infinity>"
-proof -
+proof%unimportant -
interpret N: sigma_finite_measure N by fact
from N show ?thesis
using sigma_finite_iff_density_finite[OF borel_measurable_RN_deriv, of N] density_RN_deriv[OF ac]
by simp
qed
-lemma (in sigma_finite_measure)
+lemma%important (in sigma_finite_measure) (* *FIX ME needs name*)
assumes N: "sigma_finite_measure N" and ac: "absolutely_continuous M N" "sets N = sets M"
and f: "f \<in> borel_measurable M"
shows RN_deriv_integrable: "integrable N f \<longleftrightarrow>
integrable M (\<lambda>x. enn2real (RN_deriv M N x) * f x)" (is ?integrable)
and RN_deriv_integral: "integral\<^sup>L N f = (\<integral>x. enn2real (RN_deriv M N x) * f x \<partial>M)" (is ?integral)
-proof -
+proof%unimportant -
note ac(2)[simp] and sets_eq_imp_space_eq[OF ac(2), simp]
interpret N: sigma_finite_measure N by fact
@@ -1053,14 +1054,14 @@
done
qed
-lemma (in sigma_finite_measure) real_RN_deriv:
+lemma%important (in sigma_finite_measure) real_RN_deriv:
assumes "finite_measure N"
assumes ac: "absolutely_continuous M N" "sets N = sets M"
obtains D where "D \<in> borel_measurable M"
and "AE x in M. RN_deriv M N x = ennreal (D x)"
and "AE x in N. 0 < D x"
and "\<And>x. 0 \<le> D x"
-proof
+proof%unimportant
interpret N: finite_measure N by fact
note RN = borel_measurable_RN_deriv density_RN_deriv[OF ac]
--- a/src/HOL/Analysis/Regularity.thy Sun Oct 21 20:45:01 2018 +0200
+++ b/src/HOL/Analysis/Regularity.thy Sun Oct 21 23:02:52 2018 +0100
@@ -4,11 +4,11 @@
section \<open>Regularity of Measures\<close>
-theory Regularity
+theory Regularity (* FIX suggestion to rename to e.g. RegularityMeasures *)
imports Measure_Space Borel_Space
begin
-lemma
+lemma%important (*FIX needs name *)
fixes M::"'a::{second_countable_topology, complete_space} measure"
assumes sb: "sets M = sets borel"
assumes "emeasure M (space M) \<noteq> \<infinity>"
@@ -17,7 +17,7 @@
(SUP K : {K. K \<subseteq> B \<and> compact K}. emeasure M K)" (is "?inner B")
and outer_regular: "emeasure M B =
(INF U : {U. B \<subseteq> U \<and> open U}. emeasure M U)" (is "?outer B")
-proof -
+proof%unimportant -
have Us: "UNIV = space M" by (metis assms(1) sets_eq_imp_space_eq space_borel)
hence sU: "space M = UNIV" by simp
interpret finite_measure M by rule fact
--- a/src/HOL/Analysis/Set_Integral.thy Sun Oct 21 20:45:01 2018 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy Sun Oct 21 23:02:52 2018 +0100
@@ -15,11 +15,11 @@
Notation
*)
-definition "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M"
+definition%important "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M"
-definition "set_integrable M A f \<equiv> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
+definition%important "set_integrable M A f \<equiv> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
-definition "set_lebesgue_integral M A f \<equiv> lebesgue_integral M (\<lambda>x. indicator A x *\<^sub>R f x)"
+definition%important "set_lebesgue_integral M A f \<equiv> lebesgue_integral M (\<lambda>x. indicator A x *\<^sub>R f x)"
syntax
"_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
@@ -319,11 +319,11 @@
using ae by (auto simp: subset_eq split: split_indicator)
qed (use assms in \<open>auto simp: set_borel_measurable_def\<close>)
-lemma set_borel_measurable_subset:
+lemma%important set_borel_measurable_subset:
fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
assumes [measurable]: "set_borel_measurable M A f" "B \<in> sets M" and "B \<subseteq> A"
shows "set_borel_measurable M B f"
-proof -
+proof%unimportant-
have "set_borel_measurable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
using assms unfolding set_borel_measurable_def
using borel_measurable_indicator borel_measurable_scaleR by blast
@@ -360,13 +360,13 @@
finally show ?thesis .
qed
-lemma set_integral_finite_Union:
+lemma%important set_integral_finite_Union:
fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
assumes "finite I" "disjoint_family_on A I"
and "\<And>i. i \<in> I \<Longrightarrow> set_integrable M (A i) f" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
shows "(LINT x:(\<Union>i\<in>I. A i)|M. f x) = (\<Sum>i\<in>I. LINT x:A i|M. f x)"
using assms
-proof induction
+proof%unimportant induction
case (insert x F)
then have "A x \<inter> UNION F A = {}"
by (meson disjoint_family_on_insert)
@@ -410,14 +410,14 @@
qed
(* Proof from Royden Real Analysis, p. 91. *)
-lemma lebesgue_integral_countable_add:
+lemma%important lebesgue_integral_countable_add:
fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
assumes meas[intro]: "\<And>i::nat. A i \<in> sets M"
and disj: "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
and intgbl: "set_integrable M (\<Union>i. A i) f"
shows "LINT x:(\<Union>i. A i)|M. f x = (\<Sum>i. (LINT x:(A i)|M. f x))"
unfolding set_lebesgue_integral_def
-proof (subst integral_suminf[symmetric])
+proof%unimportant (subst integral_suminf[symmetric])
show int_A: "integrable M (\<lambda>x. indicat_real (A i) x *\<^sub>R f x)" for i
using intgbl unfolding set_integrable_def [symmetric]
by (rule set_integrable_subset) auto
@@ -825,12 +825,12 @@
The formalization is more painful as one should jump back and forth between reals and ereals and justify
all the time positivity or integrability (thankfully, measurability is handled more or less automatically).\<close>
-lemma Scheffe_lemma1:
+lemma%important Scheffe_lemma1:
assumes "\<And>n. integrable M (F n)" "integrable M f"
"AE x in M. (\<lambda>n. F n x) \<longlonglongrightarrow> f x"
"limsup (\<lambda>n. \<integral>\<^sup>+ x. norm(F n x) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f x) \<partial>M)"
shows "(\<lambda>n. \<integral>\<^sup>+ x. norm(F n x - f x) \<partial>M) \<longlonglongrightarrow> 0"
-proof -
+proof%unimportant -
have [measurable]: "\<And>n. F n \<in> borel_measurable M" "f \<in> borel_measurable M"
using assms(1) assms(2) by simp_all
define G where "G = (\<lambda>n x. norm(f x) + norm(F n x) - norm(F n x - f x))"
@@ -921,26 +921,26 @@
by (rule tendsto_0_if_Limsup_eq_0_ennreal)
qed
-lemma Scheffe_lemma2:
+lemma%important Scheffe_lemma2:
fixes F::"nat \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}"
assumes "\<And> n::nat. F n \<in> borel_measurable M" "integrable M f"
"AE x in M. (\<lambda>n. F n x) \<longlonglongrightarrow> f x"
"\<And>n. (\<integral>\<^sup>+ x. norm(F n x) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f x) \<partial>M)"
shows "(\<lambda>n. \<integral>\<^sup>+ x. norm(F n x - f x) \<partial>M) \<longlonglongrightarrow> 0"
-proof (rule Scheffe_lemma1)
+proof%unimportant (rule Scheffe_lemma1)
fix n::nat
have "(\<integral>\<^sup>+ x. norm(f x) \<partial>M) < \<infinity>" using assms(2) by (metis has_bochner_integral_implies_finite_norm integrable.cases)
then have "(\<integral>\<^sup>+ x. norm(F n x) \<partial>M) < \<infinity>" using assms(4)[of n] by auto
then show "integrable M (F n)" by (subst integrable_iff_bounded, simp add: assms(1)[of n])
qed (auto simp add: assms Limsup_bounded)
-lemma tendsto_set_lebesgue_integral_at_right:
+lemma%important tendsto_set_lebesgue_integral_at_right:
fixes a b :: real and f :: "real \<Rightarrow> 'a :: {banach,second_countable_topology}"
assumes "a < b" and sets: "\<And>a'. a' \<in> {a<..b} \<Longrightarrow> {a'..b} \<in> sets M"
and "set_integrable M {a<..b} f"
shows "((\<lambda>a'. set_lebesgue_integral M {a'..b} f) \<longlongrightarrow>
set_lebesgue_integral M {a<..b} f) (at_right a)"
-proof (rule tendsto_at_right_sequentially[OF assms(1)], goal_cases)
+proof%unimportant (rule tendsto_at_right_sequentially[OF assms(1)], goal_cases)
case (1 S)
have eq: "(\<Union>n. {S n..b}) = {a<..b}"
proof safe
@@ -961,13 +961,13 @@
The next lemmas relate convergence of integrals over an interval to
improper integrals.
\<close>
-lemma tendsto_set_lebesgue_integral_at_left:
+lemma%important tendsto_set_lebesgue_integral_at_left:
fixes a b :: real and f :: "real \<Rightarrow> 'a :: {banach,second_countable_topology}"
assumes "a < b" and sets: "\<And>b'. b' \<in> {a..<b} \<Longrightarrow> {a..b'} \<in> sets M"
and "set_integrable M {a..<b} f"
shows "((\<lambda>b'. set_lebesgue_integral M {a..b'} f) \<longlongrightarrow>
set_lebesgue_integral M {a..<b} f) (at_left b)"
-proof (rule tendsto_at_left_sequentially[OF assms(1)], goal_cases)
+proof%unimportant (rule tendsto_at_left_sequentially[OF assms(1)], goal_cases)
case (1 S)
have eq: "(\<Union>n. {a..S n}) = {a..<b}"
proof safe
@@ -983,12 +983,12 @@
with eq show ?case by simp
qed
-lemma tendsto_set_lebesgue_integral_at_top:
+lemma%important tendsto_set_lebesgue_integral_at_top:
fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
assumes sets: "\<And>b. b \<ge> a \<Longrightarrow> {a..b} \<in> sets M"
and int: "set_integrable M {a..} f"
shows "((\<lambda>b. set_lebesgue_integral M {a..b} f) \<longlongrightarrow> set_lebesgue_integral M {a..} f) at_top"
-proof (rule tendsto_at_topI_sequentially)
+proof%unimportant (rule tendsto_at_topI_sequentially)
fix X :: "nat \<Rightarrow> real" assume "filterlim X at_top sequentially"
show "(\<lambda>n. set_lebesgue_integral M {a..X n} f) \<longlonglongrightarrow> set_lebesgue_integral M {a..} f"
unfolding set_lebesgue_integral_def
@@ -1020,12 +1020,12 @@
qed
qed
-lemma tendsto_set_lebesgue_integral_at_bot:
+lemma%important tendsto_set_lebesgue_integral_at_bot:
fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
assumes sets: "\<And>a. a \<le> b \<Longrightarrow> {a..b} \<in> sets M"
and int: "set_integrable M {..b} f"
shows "((\<lambda>a. set_lebesgue_integral M {a..b} f) \<longlongrightarrow> set_lebesgue_integral M {..b} f) at_bot"
-proof (rule tendsto_at_botI_sequentially)
+proof%unimportant (rule tendsto_at_botI_sequentially)
fix X :: "nat \<Rightarrow> real" assume "filterlim X at_bot sequentially"
show "(\<lambda>n. set_lebesgue_integral M {X n..b} f) \<longlonglongrightarrow> set_lebesgue_integral M {..b} f"
unfolding set_lebesgue_integral_def
--- a/src/HOL/Analysis/Simplex_Content.thy Sun Oct 21 20:45:01 2018 +0200
+++ b/src/HOL/Analysis/Simplex_Content.thy Sun Oct 21 23:02:52 2018 +0100
@@ -5,7 +5,7 @@
The content of an n-dimensional simplex, including the formula for the content of a
triangle and Heron's formula.
*)
-section \<open>Volume of a simplex\<close>
+section%important \<open>Volume of a simplex\<close>
theory Simplex_Content
imports Change_Of_Vars
begin
@@ -27,13 +27,13 @@
using assms sum_nonneg[of A x] unfolding S_def
by (force simp: sum_delta_notmem algebra_simps)
-lemma emeasure_std_simplex_aux:
+lemma%important emeasure_std_simplex_aux:
fixes t :: real
assumes "finite (A :: 'a set)" "t \<ge> 0"
shows "emeasure (Pi\<^sub>M A (\<lambda>_. lborel))
(S A t \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) = t ^ card A / fact (card A)"
using assms(1,2)
-proof (induction arbitrary: t rule: finite_induct)
+proof%unimportant (induction arbitrary: t rule: finite_induct)
case (empty t)
thus ?case by (simp add: PiM_empty S_def)
next
@@ -111,18 +111,18 @@
finally show ?thesis by (simp only: std_simplex)
qed
-theorem content_std_simplex:
+theorem%important content_std_simplex:
"measure lborel (convex hull (insert 0 Basis :: 'a :: euclidean_space set)) =
1 / fact DIM('a)"
- by (simp add: measure_def emeasure_std_simplex)
+ by%unimportant (simp add: measure_def emeasure_std_simplex)
(* TODO: move to Change_of_Vars *)
-lemma measure_lebesgue_linear_transformation:
+lemma%important measure_lebesgue_linear_transformation:
fixes A :: "(real ^ 'n :: {finite, wellorder}) set"
fixes f :: "_ \<Rightarrow> real ^ 'n :: {finite, wellorder}"
assumes "bounded A" "A \<in> sets lebesgue" "linear f"
shows "measure lebesgue (f ` A) = \<bar>det (matrix f)\<bar> * measure lebesgue A"
-proof -
+proof%unimportant -
from assms have [intro]: "A \<in> lmeasurable"
by (intro bounded_set_imp_lmeasurable) auto
hence [intro]: "f ` A \<in> lmeasurable"
@@ -142,12 +142,12 @@
finally show ?thesis .
qed
-theorem content_simplex:
+theorem%important content_simplex:
fixes X :: "(real ^ 'n :: {finite, wellorder}) set" and f :: "'n :: _ \<Rightarrow> real ^ ('n :: _)"
assumes "finite X" "card X = Suc CARD('n)" and x0: "x0 \<in> X" and bij: "bij_betw f UNIV (X - {x0})"
defines "M \<equiv> (\<chi> i. \<chi> j. f j $ i - x0 $ i)"
shows "content (convex hull X) = \<bar>det M\<bar> / fact (CARD('n))"
-proof -
+proof%unimportant -
define g where "g = (\<lambda>x. M *v x)"
have [simp]: "M *v axis i 1 = f i - x0" for i :: 'n
by (simp add: M_def matrix_vector_mult_basis column_def vec_eq_iff)
@@ -183,11 +183,11 @@
using finite_imp_compact_convex_hull[OF \<open>finite X\<close>] by (auto dest: compact_imp_closed)
qed
-theorem content_triangle:
+theorem%important content_triangle:
fixes A B C :: "real ^ 2"
shows "content (convex hull {A, B, C}) =
\<bar>(C $ 1 - A $ 1) * (B $ 2 - A $ 2) - (B $ 1 - A $ 1) * (C $ 2 - A $ 2)\<bar> / 2"
-proof -
+proof%unimportant -
define M :: "real ^ 2 ^ 2" where "M \<equiv> (\<chi> i. \<chi> j. (if j = 1 then B else C) $ i - A $ i)"
define g where "g = (\<lambda>x. M *v x)"
define std where "std = (convex hull insert 0 Basis :: (real ^ 2) set)"
@@ -227,12 +227,12 @@
by (auto dest!: compact_imp_closed simp: det_2 M_def)
qed
-theorem heron:
+theorem%important heron:
fixes A B C :: "real ^ 2"
defines "a \<equiv> dist B C" and "b \<equiv> dist A C" and "c \<equiv> dist A B"
defines "s \<equiv> (a + b + c) / 2"
shows "content (convex hull {A, B, C}) = sqrt (s * (s - a) * (s - b) * (s - c))"
-proof -
+proof%unimportant -
have [simp]: "(UNIV :: 2 set) = {1, 2}"
using exhaust_2 by auto
have dist_eq: "dist (A :: real ^ 2) B ^ 2 = (A $ 1 - B $ 1) ^ 2 + (A $ 2 - B $ 2) ^ 2"
--- a/src/HOL/Analysis/Tagged_Division.thy Sun Oct 21 20:45:01 2018 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy Sun Oct 21 23:02:52 2018 +0100
@@ -3,8 +3,8 @@
Author: Robert Himmelmann, TU Muenchen (Translation from HOL light); proofs reworked by LCP
*)
-section \<open>Tagged divisions used for the Henstock-Kurzweil gauge integration\<close>
-
+section%important \<open>Tagged divisions used for the Henstock-Kurzweil gauge integration\<close>
+(*FIXME move together with Henstock_Kurzweil_Integration.thy *)
theory Tagged_Division
imports Connected
begin
@@ -31,8 +31,8 @@
scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
-subsection \<open>Sundries\<close>
-
+subsection%unimportant \<open>Sundries\<close>
+(*FIXME restructure this entire section consists of single lemma *)
text\<open>A transitive relation is well-founded if all initial segments are finite.\<close>
lemma wf_finite_segments:
@@ -55,7 +55,7 @@
by (simp add: field_simps)
qed
-subsection \<open>Some useful lemmas about intervals\<close>
+subsection%unimportant \<open>Some useful lemmas about intervals\<close>
lemma interior_subset_union_intervals:
assumes "i = cbox a b"
@@ -130,12 +130,12 @@
lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}"
by (simp add: box_ne_empty)
-subsection \<open>Bounds on intervals where they exist\<close>
+subsection%important \<open>Bounds on intervals where they exist\<close>
-definition interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
+definition%important interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)"
-definition interval_lowerbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
+definition%important interval_lowerbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
lemma interval_upperbound[simp]:
@@ -152,22 +152,22 @@
lemmas interval_bounds = interval_upperbound interval_lowerbound
-lemma
+lemma%important
fixes X::"real set"
shows interval_upperbound_real[simp]: "interval_upperbound X = Sup X"
and interval_lowerbound_real[simp]: "interval_lowerbound X = Inf X"
- by (auto simp: interval_upperbound_def interval_lowerbound_def)
+ by%unimportant (auto simp: interval_upperbound_def interval_lowerbound_def)
-lemma interval_bounds'[simp]:
+lemma%important interval_bounds'[simp]:
assumes "cbox a b \<noteq> {}"
shows "interval_upperbound (cbox a b) = b"
and "interval_lowerbound (cbox a b) = a"
- using assms unfolding box_ne_empty by auto
+ using%unimportant assms unfolding box_ne_empty by auto
-lemma interval_upperbound_Times:
+lemma%important interval_upperbound_Times:
assumes "A \<noteq> {}" and "B \<noteq> {}"
shows "interval_upperbound (A \<times> B) = (interval_upperbound A, interval_upperbound B)"
-proof-
+proof%unimportant-
from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
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)"
by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
@@ -178,10 +178,10 @@
by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
qed
-lemma interval_lowerbound_Times:
+lemma%important interval_lowerbound_Times:
assumes "A \<noteq> {}" and "B \<noteq> {}"
shows "interval_lowerbound (A \<times> B) = (interval_lowerbound A, interval_lowerbound B)"
-proof-
+proof%unimportant-
from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
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)"
by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
@@ -192,9 +192,9 @@
by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
qed
-subsection \<open>The notion of a gauge --- simply an open set containing the point\<close>
+subsection%important \<open>The notion of a gauge --- simply an open set containing the point\<close>
-definition "gauge \<gamma> \<longleftrightarrow> (\<forall>x. x \<in> \<gamma> x \<and> open (\<gamma> x))"
+definition%important "gauge \<gamma> \<longleftrightarrow> (\<forall>x. x \<in> \<gamma> x \<and> open (\<gamma> x))"
lemma gaugeI:
assumes "\<And>x. x \<in> \<gamma> x"
@@ -226,11 +226,11 @@
using equation_minus_iff
by (auto simp: gauge_def surj_def intro!: open_surjective_linear_image linear_uminus)
-lemma gauge_Inter:
+lemma%important gauge_Inter:
assumes "finite S"
and "\<And>u. u\<in>S \<Longrightarrow> gauge (f u)"
shows "gauge (\<lambda>x. \<Inter>{f u x | u. u \<in> S})"
-proof -
+proof%unimportant -
have *: "\<And>x. {f u x |u. u \<in> S} = (\<lambda>u. f u x) ` S"
by auto
show ?thesis
@@ -238,20 +238,20 @@
using assms unfolding Ball_def Inter_iff mem_Collect_eq gauge_def by auto
qed
-lemma gauge_existence_lemma:
+lemma%important gauge_existence_lemma:
"(\<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)"
- by (metis zero_less_one)
+ by%unimportant (metis zero_less_one)
-subsection \<open>Attempt a systematic general set of "offset" results for components\<close>
-
+subsection%unimportant \<open>Attempt a systematic general set of "offset" results for components\<close>
+(*FIXME Restructure *)
lemma gauge_modify:
assumes "(\<forall>S. open S \<longrightarrow> open {x. f(x) \<in> S})" "gauge d"
shows "gauge (\<lambda>x. {y. f y \<in> d (f x)})"
using assms unfolding gauge_def by force
-subsection \<open>Divisions\<close>
+subsection%important \<open>Divisions\<close>
-definition division_of (infixl "division'_of" 40)
+definition%important division_of (infixl "division'_of" 40)
where
"s division_of i \<longleftrightarrow>
finite s \<and>
@@ -605,10 +605,10 @@
qed
qed
-proposition partial_division_extend_interval:
+proposition%important partial_division_extend_interval:
assumes "p division_of (\<Union>p)" "(\<Union>p) \<subseteq> cbox a b"
obtains q where "p \<subseteq> q" "q division_of cbox a (b::'a::euclidean_space)"
-proof (cases "p = {}")
+proof%unimportant (cases "p = {}")
case True
obtain q where "q division_of (cbox a b)"
by (rule elementary_interval)
@@ -687,11 +687,11 @@
"p division_of S \<Longrightarrow> \<exists>a b. S \<subseteq> cbox a (b::'a::euclidean_space)"
by (meson bounded_subset_cbox_symmetric elementary_bounded)
-lemma division_union_intervals_exists:
+lemma%important division_union_intervals_exists:
fixes a b :: "'a::euclidean_space"
assumes "cbox a b \<noteq> {}"
obtains p where "(insert (cbox a b) p) division_of (cbox a b \<union> cbox c d)"
-proof (cases "cbox c d = {}")
+proof%unimportant (cases "cbox c d = {}")
case True
with assms that show ?thesis by force
next
@@ -739,11 +739,11 @@
shows "\<Union>f division_of \<Union>\<Union>f"
using assms by (auto intro!: division_ofI)
-lemma elementary_union_interval:
+lemma%important elementary_union_interval:
fixes a b :: "'a::euclidean_space"
assumes "p division_of \<Union>p"
obtains q where "q division_of (cbox a b \<union> \<Union>p)"
-proof (cases "p = {} \<or> cbox a b = {}")
+proof%unimportant (cases "p = {} \<or> cbox a b = {}")
case True
obtain p where "p division_of (cbox a b)"
by (rule elementary_interval)
@@ -855,11 +855,11 @@
using that by auto
qed
-lemma elementary_union:
+lemma%important elementary_union:
fixes S T :: "'a::euclidean_space set"
assumes "ps division_of S" "pt division_of T"
obtains p where "p division_of (S \<union> T)"
-proof -
+proof%unimportant -
have *: "S \<union> T = \<Union>ps \<union> \<Union>pt"
using assms unfolding division_of_def by auto
show ?thesis
@@ -868,13 +868,13 @@
by (simp add: * that)
qed
-lemma partial_division_extend:
+lemma%important partial_division_extend:
fixes T :: "'a::euclidean_space set"
assumes "p division_of S"
and "q division_of T"
and "S \<subseteq> T"
obtains r where "p \<subseteq> r" and "r division_of T"
-proof -
+proof%unimportant -
note divp = division_ofD[OF assms(1)] and divq = division_ofD[OF assms(2)]
obtain a b where ab: "T \<subseteq> cbox a b"
using elementary_subset_cbox[OF assms(2)] by auto
@@ -931,7 +931,7 @@
qed
-lemma division_split:
+lemma%important division_split:
fixes a :: "'a::euclidean_space"
assumes "p division_of (cbox a b)"
and k: "k\<in>Basis"
@@ -939,7 +939,7 @@
(is "?p1 division_of ?I1")
and "{l \<inter> {x. x\<bullet>k \<ge> c} | l. l \<in> p \<and> l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}} division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
(is "?p2 division_of ?I2")
-proof (rule_tac[!] division_ofI)
+proof%unimportant (rule_tac[!] division_ofI)
note p = division_ofD[OF assms(1)]
show "finite ?p1" "finite ?p2"
using p(1) by auto
@@ -995,9 +995,9 @@
}
qed
-subsection \<open>Tagged (partial) divisions\<close>
+subsection%important \<open>Tagged (partial) divisions\<close>
-definition tagged_partial_division_of (infixr "tagged'_partial'_division'_of" 40)
+definition%important tagged_partial_division_of (infixr "tagged'_partial'_division'_of" 40)
where "s tagged_partial_division_of i \<longleftrightarrow>
finite s \<and>
(\<forall>x K. (x, K) \<in> s \<longrightarrow> x \<in> K \<and> K \<subseteq> i \<and> (\<exists>a b. K = cbox a b)) \<and>
@@ -1014,20 +1014,20 @@
(x2, K2) \<in> s \<Longrightarrow> (x1, K1) \<noteq> (x2, K2) \<Longrightarrow> interior K1 \<inter> interior K2 = {}"
using assms unfolding tagged_partial_division_of_def by blast+
-definition tagged_division_of (infixr "tagged'_division'_of" 40)
+definition%important tagged_division_of (infixr "tagged'_division'_of" 40)
where "s tagged_division_of i \<longleftrightarrow> s tagged_partial_division_of i \<and> (\<Union>{K. \<exists>x. (x,K) \<in> s} = i)"
lemma tagged_division_of_finite: "s tagged_division_of i \<Longrightarrow> finite s"
unfolding tagged_division_of_def tagged_partial_division_of_def by auto
-lemma tagged_division_of:
+lemma%important tagged_division_of:
"s tagged_division_of i \<longleftrightarrow>
finite s \<and>
(\<forall>x K. (x, K) \<in> s \<longrightarrow> x \<in> K \<and> K \<subseteq> i \<and> (\<exists>a b. K = cbox a b)) \<and>
(\<forall>x1 K1 x2 K2. (x1, K1) \<in> s \<and> (x2, K2) \<in> s \<and> (x1, K1) \<noteq> (x2, K2) \<longrightarrow>
interior K1 \<inter> interior K2 = {}) \<and>
(\<Union>{K. \<exists>x. (x,K) \<in> s} = i)"
- unfolding tagged_division_of_def tagged_partial_division_of_def by auto
+ unfolding%unimportant tagged_division_of_def tagged_partial_division_of_def by auto
lemma tagged_division_ofI:
assumes "finite s"
@@ -1052,10 +1052,10 @@
and "(\<Union>{K. \<exists>x. (x,K) \<in> s} = i)"
using assms unfolding tagged_division_of by blast+
-lemma division_of_tagged_division:
+lemma%important division_of_tagged_division:
assumes "s tagged_division_of i"
shows "(snd ` s) division_of i"
-proof (rule division_ofI)
+proof%unimportant (rule division_ofI)
note assm = tagged_division_ofD[OF assms]
show "\<Union>(snd ` s) = i" "finite (snd ` s)"
using assm by auto
@@ -1073,10 +1073,10 @@
using assm(5) k'(2) xk by blast
qed
-lemma partial_division_of_tagged_division:
+lemma%important partial_division_of_tagged_division:
assumes "s tagged_partial_division_of i"
shows "(snd ` s) division_of \<Union>(snd ` s)"
-proof (rule division_ofI)
+proof%unimportant (rule division_ofI)
note assm = tagged_partial_division_ofD[OF assms]
show "finite (snd ` s)" "\<Union>(snd ` s) = \<Union>(snd ` s)"
using assm by auto
@@ -1121,12 +1121,12 @@
unfolding box_real[symmetric]
by (rule tagged_division_of_self)
-lemma tagged_division_Un:
+lemma%important tagged_division_Un:
assumes "p1 tagged_division_of s1"
and "p2 tagged_division_of s2"
and "interior s1 \<inter> interior s2 = {}"
shows "(p1 \<union> p2) tagged_division_of (s1 \<union> s2)"
-proof (rule tagged_division_ofI)
+proof%unimportant (rule tagged_division_ofI)
note p1 = tagged_division_ofD[OF assms(1)]
note p2 = tagged_division_ofD[OF assms(2)]
show "finite (p1 \<union> p2)"
@@ -1149,12 +1149,12 @@
by (metis "*" UnE assms(1) assms(2) inf_sup_aci(1) p2(5) tagged_division_ofD(3) xk xk'(1) xk'(2))
qed
-lemma tagged_division_Union:
+lemma%important tagged_division_Union:
assumes "finite I"
and tag: "\<And>i. i\<in>I \<Longrightarrow> pfn i tagged_division_of i"
and disj: "\<And>i1 i2. \<lbrakk>i1 \<in> I; i2 \<in> I; i1 \<noteq> i2\<rbrakk> \<Longrightarrow> interior(i1) \<inter> interior(i2) = {}"
shows "\<Union>(pfn ` I) tagged_division_of (\<Union>I)"
-proof (rule tagged_division_ofI)
+proof%unimportant (rule tagged_division_ofI)
note assm = tagged_division_ofD[OF tag]
show "finite (\<Union>(pfn ` I))"
using assms by auto
@@ -1229,13 +1229,13 @@
unfolding box_real[symmetric]
by (rule tagged_division_Un_interval)
-lemma tagged_division_split_left_inj:
+lemma%important tagged_division_split_left_inj:
assumes d: "d tagged_division_of i"
and tags: "(x1, K1) \<in> d" "(x2, K2) \<in> d"
and "K1 \<noteq> K2"
and eq: "K1 \<inter> {x. x \<bullet> k \<le> c} = K2 \<inter> {x. x \<bullet> k \<le> c}"
shows "interior (K1 \<inter> {x. x\<bullet>k \<le> c}) = {}"
-proof -
+proof%unimportant -
have "interior (K1 \<inter> K2) = {} \<or> (x2, K2) = (x1, K1)"
using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
then show ?thesis
@@ -1255,11 +1255,11 @@
using eq \<open>K1 \<noteq> K2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
qed
-lemma (in comm_monoid_set) over_tagged_division_lemma:
+lemma%important (in comm_monoid_set) over_tagged_division_lemma:
assumes "p tagged_division_of i"
and "\<And>u v. box u v = {} \<Longrightarrow> d (cbox u v) = \<^bold>1"
shows "F (\<lambda>(_, k). d k) p = F d (snd ` p)"
-proof -
+proof%unimportant -
have *: "(\<lambda>(_ ,k). d k) = d \<circ> snd"
by (simp add: fun_eq_iff)
note assm = tagged_division_ofD[OF assms(1)]
@@ -1286,15 +1286,15 @@
qed
-subsection \<open>Functions closed on boxes: morphisms from boxes to monoids\<close>
+subsection%important \<open>Functions closed on boxes: morphisms from boxes to monoids\<close>
text \<open>This auxiliary structure is used to sum up over the elements of a division. Main theorem is
\<open>operative_division\<close>. Instances for the monoid are @{typ "'a option"}, @{typ real}, and
@{typ bool}.\<close>
-paragraph \<open>Using additivity of lifted function to encode definedness.\<close>
+paragraph%important \<open>Using additivity of lifted function to encode definedness.\<close>
-definition lift_option :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> 'c option"
+definition%important lift_option :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> 'c option"
where
"lift_option f a' b' = Option.bind a' (\<lambda>a. Option.bind b' (\<lambda>b. Some (f a b)))"
@@ -1304,10 +1304,10 @@
"lift_option f a' None = None"
by (auto simp: lift_option_def)
-lemma comm_monoid_lift_option:
+lemma%important comm_monoid_lift_option:
assumes "comm_monoid f z"
shows "comm_monoid (lift_option f) (Some z)"
-proof -
+proof%unimportant -
from assms interpret comm_monoid f z .
show ?thesis
by standard (auto simp: lift_option_def ac_simps split: bind_split)
@@ -1335,15 +1335,15 @@
paragraph \<open>Division points\<close>
-definition "division_points (k::('a::euclidean_space) set) d =
+definition%important "division_points (k::('a::euclidean_space) set) d =
{(j,x). j \<in> Basis \<and> (interval_lowerbound k)\<bullet>j < x \<and> x < (interval_upperbound k)\<bullet>j \<and>
(\<exists>i\<in>d. (interval_lowerbound i)\<bullet>j = x \<or> (interval_upperbound i)\<bullet>j = x)}"
-lemma division_points_finite:
+lemma%important division_points_finite:
fixes i :: "'a::euclidean_space set"
assumes "d division_of i"
shows "finite (division_points i d)"
-proof -
+proof%unimportant -
note assm = division_ofD[OF assms]
let ?M = "\<lambda>j. {(j,x)|x. (interval_lowerbound i)\<bullet>j < x \<and> x < (interval_upperbound i)\<bullet>j \<and>
(\<exists>i\<in>d. (interval_lowerbound i)\<bullet>j = x \<or> (interval_upperbound i)\<bullet>j = x)}"
@@ -1353,7 +1353,7 @@
unfolding * using assm by auto
qed
-lemma division_points_subset:
+lemma%important division_points_subset:
fixes a :: "'a::euclidean_space"
assumes "d division_of (cbox a b)"
and "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i" "a\<bullet>k < c" "c < b\<bullet>k"
@@ -1362,7 +1362,7 @@
division_points (cbox a b) d" (is ?t1)
and "division_points (cbox a b \<inter> {x. x\<bullet>k \<ge> c}) {l \<inter> {x. x\<bullet>k \<ge> c} | l . l \<in> d \<and> ~(l \<inter> {x. x\<bullet>k \<ge> c} = {})} \<subseteq>
division_points (cbox a b) d" (is ?t2)
-proof -
+proof%unimportant -
note assm = division_ofD[OF assms(1)]
have *: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
"\<forall>i\<in>Basis. a\<bullet>i \<le> (\<Sum>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i) *\<^sub>R i) \<bullet> i"
@@ -1423,7 +1423,7 @@
by force
qed
-lemma division_points_psubset:
+lemma%important division_points_psubset:
fixes a :: "'a::euclidean_space"
assumes d: "d division_of (cbox a b)"
and altb: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i" "a\<bullet>k < c" "c < b\<bullet>k"
@@ -1434,7 +1434,7 @@
division_points (cbox a b) d" (is "?D1 \<subset> ?D")
and "division_points (cbox a b \<inter> {x. x\<bullet>k \<ge> c}) {l \<inter> {x. x\<bullet>k \<ge> c} | l. l\<in>d \<and> l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}} \<subset>
division_points (cbox a b) d" (is "?D2 \<subset> ?D")
-proof -
+proof%unimportant -
have ab: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
using altb by (auto intro!:less_imp_le)
obtain u v where l: "l = cbox u v"
@@ -1485,13 +1485,13 @@
using \<open>K1 \<in> \<D>\<close> \<open>K1 \<noteq> K2\<close> by auto
qed
-lemma division_split_right_inj:
+lemma%important division_split_right_inj:
fixes S :: "'a::euclidean_space set"
assumes div: "\<D> division_of S"
and eq: "K1 \<inter> {x::'a. x\<bullet>k \<ge> c} = K2 \<inter> {x. x\<bullet>k \<ge> c}"
and "K1 \<in> \<D>" "K2 \<in> \<D>" "K1 \<noteq> K2"
shows "interior (K1 \<inter> {x. x\<bullet>k \<ge> c}) = {}"
-proof -
+proof%unimportant -
have "interior K2 \<inter> interior {a. a \<bullet> k \<ge> c} = interior K1 \<inter> interior {a. a \<bullet> k \<ge> c}"
by (metis (no_types) eq interior_Int)
moreover have "\<And>A. interior A \<inter> interior K2 = {} \<or> A = K2 \<or> A \<notin> \<D>"
@@ -1515,13 +1515,13 @@
unfolding * ** interval_split[OF assms] by (rule refl)
qed
-lemma division_doublesplit:
+lemma%important division_doublesplit:
fixes a :: "'a::euclidean_space"
assumes "p division_of (cbox a b)"
and k: "k \<in> Basis"
shows "(\<lambda>l. l \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> e}) ` {l\<in>p. l \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> e} \<noteq> {}}
division_of (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> e})"
-proof -
+proof%unimportant -
have *: "\<And>x c. \<bar>x - c\<bar> \<le> e \<longleftrightarrow> x \<ge> c - e \<and> x \<le> c + e"
by auto
have **: "\<And>p q p' q'. p division_of q \<Longrightarrow> p = p' \<Longrightarrow> q = q' \<Longrightarrow> p' division_of q'"
@@ -1560,9 +1560,9 @@
using box_empty_imp [of One "-One"] by simp
qed
-lemma division:
+lemma%important division:
"F g d = g (cbox a b)" if "d division_of (cbox a b)"
-proof -
+proof%unimportant -
define C where [abs_def]: "C = card (division_points (cbox a b) d)"
then show ?thesis
using that proof (induction C arbitrary: a b d rule: less_induct)
@@ -1747,10 +1747,10 @@
qed
qed
-lemma tagged_division:
+lemma%important tagged_division:
assumes "d tagged_division_of (cbox a b)"
shows "F (\<lambda>(_, l). g l) d = g (cbox a b)"
-proof -
+proof%unimportant -
have "F (\<lambda>(_, k). g k) d = F g (snd ` d)"
using assms box_empty_imp by (rule over_tagged_division_lemma)
then show ?thesis
@@ -1828,14 +1828,14 @@
qed
-subsection \<open>Special case of additivity we need for the FTC\<close>
-
-lemma additive_tagged_division_1:
+subsection%important \<open>Special case of additivity we need for the FTC\<close>
+(*fix add explanation here *)
+lemma%important additive_tagged_division_1:
fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
assumes "a \<le> b"
and "p tagged_division_of {a..b}"
shows "sum (\<lambda>(x,k). f(Sup k) - f(Inf k)) p = f b - f a"
-proof -
+proof%unimportant -
let ?f = "(\<lambda>k::(real) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))"
interpret operative_real plus 0 ?f
rewrites "comm_monoid_set.F (+) 0 = sum"
@@ -1856,9 +1856,9 @@
qed
-subsection \<open>Fine-ness of a partition w.r.t. a gauge\<close>
+subsection%important \<open>Fine-ness of a partition w.r.t. a gauge\<close>
-definition fine (infixr "fine" 46)
+definition%important fine (infixr "fine" 46)
where "d fine s \<longleftrightarrow> (\<forall>(x,k) \<in> s. k \<subseteq> d x)"
lemma fineI:
@@ -1881,21 +1881,21 @@
lemma fine_Un: "d fine p1 \<Longrightarrow> d fine p2 \<Longrightarrow> d fine (p1 \<union> p2)"
unfolding fine_def by blast
-lemma fine_Union: "(\<And>p. p \<in> ps \<Longrightarrow> d fine p) \<Longrightarrow> d fine (\<Union>ps)"
+lemma%important fine_Union: "(\<And>p. p \<in> ps \<Longrightarrow> d fine p) \<Longrightarrow> d fine (\<Union>ps)"
unfolding fine_def by auto
-lemma fine_subset: "p \<subseteq> q \<Longrightarrow> d fine q \<Longrightarrow> d fine p"
+lemma%unimportant fine_subset: "p \<subseteq> q \<Longrightarrow> d fine q \<Longrightarrow> d fine p"
unfolding fine_def by blast
-subsection \<open>Some basic combining lemmas\<close>
+subsection%important \<open>Some basic combining lemmas\<close>
-lemma tagged_division_Union_exists:
+lemma%important tagged_division_Union_exists:
assumes "finite I"
and "\<forall>i\<in>I. \<exists>p. p tagged_division_of i \<and> d fine p"
and "\<forall>i1\<in>I. \<forall>i2\<in>I. i1 \<noteq> i2 \<longrightarrow> interior i1 \<inter> interior i2 = {}"
and "\<Union>I = i"
obtains p where "p tagged_division_of i" and "d fine p"
-proof -
+proof%unimportant -
obtain pfn where pfn:
"\<And>x. x \<in> I \<Longrightarrow> pfn x tagged_division_of x"
"\<And>x. x \<in> I \<Longrightarrow> d fine pfn x"
@@ -1905,25 +1905,25 @@
using assms(1) assms(3) assms(4) pfn(1) tagged_division_Union apply force
by (metis (mono_tags, lifting) fine_Union imageE pfn(2))
qed
-
+(* FIXME structure here, do not have one lemma in each subsection *)
-subsection \<open>The set we're concerned with must be closed\<close>
+subsection%unimportant \<open>The set we're concerned with must be closed\<close>
lemma division_of_closed:
fixes i :: "'n::euclidean_space set"
shows "s division_of i \<Longrightarrow> closed i"
unfolding division_of_def by fastforce
-subsection \<open>General bisection principle for intervals; might be useful elsewhere\<close>
+subsection%important \<open>General bisection principle for intervals; might be useful elsewhere\<close>
-lemma interval_bisection_step:
+lemma%important interval_bisection_step:
fixes type :: "'a::euclidean_space"
assumes emp: "P {}"
and Un: "\<And>S T. \<lbrakk>P S; P T; interior(S) \<inter> interior(T) = {}\<rbrakk> \<Longrightarrow> P (S \<union> T)"
and non: "\<not> P (cbox a (b::'a))"
obtains c d where "\<not> P (cbox c d)"
and "\<And>i. i \<in> Basis \<Longrightarrow> a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
-proof -
+proof%unimportant -
have "cbox a b \<noteq> {}"
using emp non by metis
then have ab: "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
@@ -2029,14 +2029,14 @@
by (metis (no_types, lifting) assms(3) that)
qed
-lemma interval_bisection:
+lemma%important interval_bisection:
fixes type :: "'a::euclidean_space"
assumes "P {}"
and Un: "\<And>S T. \<lbrakk>P S; P T; interior(S) \<inter> interior(T) = {}\<rbrakk> \<Longrightarrow> P (S \<union> T)"
and "\<not> P (cbox a (b::'a))"
obtains x where "x \<in> cbox a b"
and "\<forall>e>0. \<exists>c d. x \<in> cbox c d \<and> cbox c d \<subseteq> ball x e \<and> cbox c d \<subseteq> cbox a b \<and> \<not> P (cbox c d)"
-proof -
+proof%unimportant -
have "\<forall>x. \<exists>y. \<not> P (cbox (fst x) (snd x)) \<longrightarrow> (\<not> P (cbox (fst y) (snd y)) \<and>
(\<forall>i\<in>Basis. fst x\<bullet>i \<le> fst y\<bullet>i \<and> fst y\<bullet>i \<le> snd y\<bullet>i \<and> snd y\<bullet>i \<le> snd x\<bullet>i \<and>
2 * (snd y\<bullet>i - fst y\<bullet>i) \<le> snd x\<bullet>i - fst x\<bullet>i))" (is "\<forall>x. ?P x")
@@ -2180,13 +2180,13 @@
qed
-subsection \<open>Cousin's lemma\<close>
+subsection%important \<open>Cousin's lemma\<close>
-lemma fine_division_exists:
+lemma%important fine_division_exists:
fixes a b :: "'a::euclidean_space"
assumes "gauge g"
obtains p where "p tagged_division_of (cbox a b)" "g fine p"
-proof (cases "\<exists>p. p tagged_division_of (cbox a b) \<and> g fine p")
+proof%unimportant (cases "\<exists>p. p tagged_division_of (cbox a b) \<and> g fine p")
case True
then show ?thesis
using that by auto
@@ -2226,16 +2226,16 @@
obtains p where "p tagged_division_of {a .. b}" "g fine p"
by (metis assms box_real(2) fine_division_exists)
-subsection \<open>A technical lemma about "refinement" of division\<close>
+subsection%important \<open>A technical lemma about "refinement" of division\<close>
-lemma tagged_division_finer:
+lemma%important tagged_division_finer:
fixes p :: "('a::euclidean_space \<times> ('a::euclidean_space set)) set"
assumes ptag: "p tagged_division_of (cbox a b)"
and "gauge d"
obtains q where "q tagged_division_of (cbox a b)"
and "d fine q"
and "\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> q"
-proof -
+proof%unimportant -
have p: "finite p" "p tagged_partial_division_of (cbox a b)"
using ptag unfolding tagged_division_of_def by auto
have "(\<exists>q. q tagged_division_of (\<Union>{k. \<exists>x. (x,k) \<in> p}) \<and> d fine q \<and> (\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> q))"
@@ -2301,13 +2301,13 @@
with ptag that show ?thesis by auto
qed
-subsubsection \<open>Covering lemma\<close>
+subsubsection%important \<open>Covering lemma\<close>
text\<open> Some technical lemmas used in the approximation results that follow. Proof of the covering
lemma is an obvious multidimensional generalization of Lemma 3, p65 of Swartz's
"Introduction to Gauge Integrals". \<close>
-proposition covering_lemma:
+proposition%important covering_lemma:
assumes "S \<subseteq> cbox a b" "box a b \<noteq> {}" "gauge g"
obtains \<D> where
"countable \<D>" "\<Union>\<D> \<subseteq> cbox a b"
@@ -2316,7 +2316,7 @@
"\<And>K. K \<in> \<D> \<Longrightarrow> \<exists>x \<in> S \<inter> K. K \<subseteq> g x"
"\<And>u v. cbox u v \<in> \<D> \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
"S \<subseteq> \<Union>\<D>"
-proof -
+proof%unimportant -
have aibi: "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" and normab: "0 < norm(b - a)"
using \<open>box a b \<noteq> {}\<close> box_eq_empty box_sing by fastforce+
let ?K0 = "\<lambda>(n, f::'a\<Rightarrow>nat).
@@ -2571,18 +2571,18 @@
qed
qed
-subsection \<open>Division filter\<close>
+subsection%important \<open>Division filter\<close>
text \<open>Divisions over all gauges towards finer divisions.\<close>
-definition division_filter :: "'a::euclidean_space set \<Rightarrow> ('a \<times> 'a set) set filter"
+definition%important division_filter :: "'a::euclidean_space set \<Rightarrow> ('a \<times> 'a set) set filter"
where "division_filter s = (INF g:{g. gauge g}. principal {p. p tagged_division_of s \<and> g fine p})"
-lemma eventually_division_filter:
+lemma%important eventually_division_filter:
"(\<forall>\<^sub>F p in division_filter s. P p) \<longleftrightarrow>
(\<exists>g. gauge g \<and> (\<forall>p. p tagged_division_of s \<and> g fine p \<longrightarrow> P p))"
- unfolding division_filter_def
-proof (subst eventually_INF_base; clarsimp)
+ unfolding%unimportant division_filter_def
+proof%unimportant (subst eventually_INF_base; clarsimp)
fix g1 g2 :: "'a \<Rightarrow> 'a set" show "gauge g1 \<Longrightarrow> gauge g2 \<Longrightarrow> \<exists>x. gauge x \<and>
{p. p tagged_division_of s \<and> x fine p} \<subseteq> {p. p tagged_division_of s \<and> g1 fine p} \<and>
{p. p tagged_division_of s \<and> x fine p} \<subseteq> {p. p tagged_division_of s \<and> g2 fine p}"
@@ -2593,7 +2593,7 @@
unfolding trivial_limit_def eventually_division_filter
by (auto elim: fine_division_exists)
-lemma eventually_division_filter_tagged_division:
+lemma%important eventually_division_filter_tagged_division:
"eventually (\<lambda>p. p tagged_division_of s) (division_filter s)"
unfolding eventually_division_filter by (intro exI[of _ "\<lambda>x. ball x 1"]) auto