--- a/src/HOL/Analysis/Derivative.thy Thu Jul 18 15:40:15 2019 +0100
+++ b/src/HOL/Analysis/Derivative.thy Fri Jul 19 12:57:14 2019 +0100
@@ -1439,7 +1439,7 @@
qed (use assms in auto)
-text \<open>Invertible derivative continous at a point implies local
+text \<open>Invertible derivative continuous at a point implies local
injectivity. It's only for this we need continuity of the derivative,
except of course if we want the fact that the inverse derivative is
also continuous. So if we know for some other reason that the inverse
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Jul 18 15:40:15 2019 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Jul 19 12:57:14 2019 +0100
@@ -816,6 +816,36 @@
finally show ?thesis .
qed
+lemma has_integral_integral_lebesgue_on:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "integrable (lebesgue_on S) f" "S \<in> sets lebesgue"
+ shows "(f has_integral (integral\<^sup>L (lebesgue_on S) f)) S"
+proof -
+ let ?f = "\<lambda>x. if x \<in> S then f x else 0"
+ have "integrable lebesgue (\<lambda>x. indicat_real S x *\<^sub>R f x)"
+ using indicator_scaleR_eq_if [of S _ f] assms
+ by (metis (full_types) integrable_restrict_space sets.Int_space_eq2)
+ then have "integrable lebesgue ?f"
+ using indicator_scaleR_eq_if [of S _ f] assms by auto
+ then have "(?f has_integral (integral\<^sup>L lebesgue ?f)) UNIV"
+ by (rule has_integral_integral_lebesgue)
+ then have "(f has_integral (integral\<^sup>L lebesgue ?f)) S"
+ using has_integral_restrict_UNIV by blast
+ moreover
+ have "S \<inter> space lebesgue \<in> sets lebesgue"
+ by (simp add: assms)
+ then have "(integral\<^sup>L lebesgue ?f) = (integral\<^sup>L (lebesgue_on S) f)"
+ by (simp add: integral_restrict_space indicator_scaleR_eq_if)
+ ultimately show ?thesis
+ by auto
+qed
+
+lemma lebesgue_integral_eq_integral:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "integrable (lebesgue_on S) f" "S \<in> sets lebesgue"
+ shows "integral\<^sup>L (lebesgue_on S) f = integral S f"
+ by (metis has_integral_integral_lebesgue_on assms integral_unique)
+
lemma integrable_on_lebesgue:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
shows "integrable lebesgue f \<Longrightarrow> f integrable_on UNIV"
@@ -3141,7 +3171,7 @@
using absolutely_integrable_integrable_bound
by (simp add: absolutely_integrable_on_def continuous_on_norm integrable_continuous)
-lemma continous_imp_integrable:
+lemma continuous_imp_integrable:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "continuous_on (cbox a b) f"
shows "integrable (lebesgue_on (cbox a b)) f"
@@ -3152,6 +3182,13 @@
by (simp add: integrable_restrict_space set_integrable_def)
qed
+lemma continuous_imp_integrable_real:
+ fixes f :: "real \<Rightarrow> 'b::euclidean_space"
+ assumes "continuous_on {a..b} f"
+ shows "integrable (lebesgue_on {a..b}) f"
+ by (metis assms continuous_imp_integrable interval_cbox)
+
+
subsection \<open>Componentwise\<close>
@@ -4485,6 +4522,24 @@
qed
qed
+lemma measurable_bounded_by_integrable_imp_lebesgue_integrable:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes f: "f \<in> borel_measurable (lebesgue_on S)" and g: "integrable (lebesgue_on S) g"
+ and normf: "\<And>x. x \<in> S \<Longrightarrow> norm(f x) \<le> g x" and S: "S \<in> sets lebesgue"
+ shows "integrable (lebesgue_on S) f"
+proof -
+ have "f absolutely_integrable_on S"
+ by (metis (no_types) S absolutely_integrable_integrable_bound f g integrable_on_lebesgue_on measurable_bounded_by_integrable_imp_integrable normf)
+ then show ?thesis
+ by (simp add: S integrable_restrict_space set_integrable_def)
+qed
+
+lemma measurable_bounded_by_integrable_imp_integrable_real:
+ fixes f :: "'a::euclidean_space \<Rightarrow> real"
+ assumes "f \<in> borel_measurable (lebesgue_on S)" "g integrable_on S" "\<And>x. x \<in> S \<Longrightarrow> abs(f x) \<le> g x" "S \<in> sets lebesgue"
+ shows "f integrable_on S"
+ using measurable_bounded_by_integrable_imp_integrable [of f S g] assms by simp
+
subsection\<open> Relation between Borel measurability and integrability.\<close>
lemma integrable_imp_measurable_weak:
@@ -4504,6 +4559,53 @@
using assms borel_measurable_If_D borel_measurable_UNIV_eq integrable_imp_measurable_weak integrable_restrict_UNIV by blast
qed
+lemma integrable_iff_integrable_on:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "S \<in> sets lebesgue" "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>lebesgue_on S) < \<infinity>"
+ shows "integrable (lebesgue_on S) f \<longleftrightarrow> f integrable_on S"
+ using assms integrable_iff_bounded integrable_imp_measurable integrable_on_lebesgue_on by blast
+
+lemma absolutely_integrable_measurable:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "S \<in> sets lebesgue"
+ shows "f absolutely_integrable_on S \<longleftrightarrow> f \<in> borel_measurable (lebesgue_on S) \<and> integrable (lebesgue_on S) (norm \<circ> f)"
+ (is "?lhs = ?rhs")
+proof
+ assume L: ?lhs
+ then have "f \<in> borel_measurable (lebesgue_on S)"
+ by (simp add: absolutely_integrable_on_def integrable_imp_measurable)
+ then show ?rhs
+ using assms set_integrable_norm [of lebesgue S f] L
+ by (simp add: integrable_restrict_space set_integrable_def)
+next
+ assume ?rhs then show ?lhs
+ using assms integrable_on_lebesgue_on
+ by (metis absolutely_integrable_integrable_bound comp_def eq_iff measurable_bounded_by_integrable_imp_integrable)
+qed
+
+lemma absolutely_integrable_measurable_real:
+ fixes f :: "'a::euclidean_space \<Rightarrow> real"
+ assumes "S \<in> sets lebesgue"
+ shows "f absolutely_integrable_on S \<longleftrightarrow>
+ f \<in> borel_measurable (lebesgue_on S) \<and> integrable (lebesgue_on S) (\<lambda>x. \<bar>f x\<bar>)"
+ by (simp add: absolutely_integrable_measurable assms o_def)
+
+lemma absolutely_integrable_measurable_real':
+ fixes f :: "'a::euclidean_space \<Rightarrow> real"
+ assumes "S \<in> sets lebesgue"
+ shows "f absolutely_integrable_on S \<longleftrightarrow> f \<in> borel_measurable (lebesgue_on S) \<and> (\<lambda>x. \<bar>f x\<bar>) integrable_on S"
+ using assms
+ apply (auto simp: absolutely_integrable_measurable integrable_on_lebesgue_on)
+ apply (simp add: integrable_on_lebesgue_on measurable_bounded_by_integrable_imp_lebesgue_integrable)
+ using abs_absolutely_integrableI_1 absolutely_integrable_measurable measurable_bounded_by_integrable_imp_integrable_real by blast
+
+lemma measurable_bounded_by_integrable_imp_absolutely_integrable:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "f \<in> borel_measurable (lebesgue_on S)" "S \<in> sets lebesgue"
+ and "g integrable_on S" and "\<And>x. x \<in> S \<Longrightarrow> norm(f x) \<le> (g x)"
+ shows "f absolutely_integrable_on S"
+ using assms absolutely_integrable_integrable_bound measurable_bounded_by_integrable_imp_integrable by blast
+
proposition negligible_differentiable_vimage:
fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
assumes "negligible T"
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Thu Jul 18 15:40:15 2019 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Fri Jul 19 12:57:14 2019 +0100
@@ -1072,6 +1072,13 @@
assumes "bounded S" "S \<in> sets lebesgue" shows "S \<in> lmeasurable"
by (metis assms bounded_Un emeasure_bounded_finite emeasure_completion fmeasurableI main_part_null_part_Un)
+lemma finite_measure_lebesgue_on: "S \<in> lmeasurable \<Longrightarrow> finite_measure (lebesgue_on S)"
+ by (auto simp: finite_measureI fmeasurable_def emeasure_restrict_space)
+
+lemma integrable_const_ivl [iff]:
+ fixes a::"'a::ordered_euclidean_space"
+ shows "integrable (lebesgue_on {a..b}) (\<lambda>x. c)"
+ by (metis cbox_interval finite_measure.integrable_const finite_measure_lebesgue_on lmeasurable_cbox)
subsection\<^marker>\<open>tag unimportant\<close>\<open>Translation preserves Lebesgue measure\<close>
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy Thu Jul 18 15:40:15 2019 +0100
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy Fri Jul 19 12:57:14 2019 +0100
@@ -985,7 +985,7 @@
subsection \<open>Stone-Weierstrass theorem for polynomial functions\<close>
-text\<open>First, we need to show that they are continous, differentiable and separable.\<close>
+text\<open>First, we need to show that they are continuous, differentiable and separable.\<close>
lemma continuous_real_polymonial_function:
assumes "real_polynomial_function f"
--- a/src/HOL/HOLCF/IOA/Abstraction.thy Thu Jul 18 15:40:15 2019 +0100
+++ b/src/HOL/HOLCF/IOA/Abstraction.thy Fri Jul 19 12:57:14 2019 +0100
@@ -43,7 +43,7 @@
is_abstraction h (fst CL) (fst AM) \<and> temp_weakening (snd AM) (snd CL) h"
-(* thm about ex2seq which is not provable by induction as ex2seq is not continous *)
+(* thm about ex2seq which is not provable by induction as ex2seq is not continuous *)
axiomatization where
ex2seq_abs_cex: "ex2seq (cex_abs h ex) = cex_absSeq h (ex2seq ex)"
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Jul 18 15:40:15 2019 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Fri Jul 19 12:57:14 2019 +0100
@@ -1113,6 +1113,9 @@
lemma enn2real_eq_posreal_iff[simp]: "c > 0 \<Longrightarrow> enn2real x = c \<longleftrightarrow> x = c"
by (cases x) auto
+lemma ennreal_enn2real_if: "ennreal (enn2real r) = (if r = top then 0 else r)"
+ by(auto intro!: ennreal_enn2real simp add: less_top)
+
subsection \<open>Coercion from \<^typ>\<open>enat\<close> to \<^typ>\<open>ennreal\<close>\<close>
@@ -1324,6 +1327,9 @@
continuous_on_e2ennreal[THEN continuous_on_tendsto_compose, of "\<lambda>x. enn2ereal (f x)" "enn2ereal x" F UNIV]
by auto
+lemma ennreal_tendsto_0_iff: "(\<And>n. f n \<ge> 0) \<Longrightarrow> ((\<lambda>n. ennreal (f n)) \<longlonglongrightarrow> 0) \<longleftrightarrow> (f \<longlonglongrightarrow> 0)"
+ by (metis (mono_tags) ennreal_0 eventuallyI order_refl tendsto_ennreal_iff)
+
lemma continuous_on_add_ennreal:
fixes f g :: "'a::topological_space \<Rightarrow> ennreal"
shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. f x + g x)"
@@ -1730,6 +1736,20 @@
lemma less_top_ennreal: "x < top \<longleftrightarrow> (\<exists>r\<ge>0. x = ennreal r)"
by (cases x) auto
+lemma enn2real_less_iff[simp]: "x < top \<Longrightarrow> enn2real x < c \<longleftrightarrow> x < c"
+ using ennreal_less_iff less_top_ennreal by auto
+
+lemma enn2real_le_iff[simp]: "\<lbrakk>x < top; c > 0\<rbrakk> \<Longrightarrow> enn2real x \<le> c \<longleftrightarrow> x \<le> c"
+ by (cases x) auto
+
+lemma enn2real_less:
+ assumes "enn2real e < r" "e \<noteq> top" shows "e < ennreal r"
+ using enn2real_less_iff assms top.not_eq_extremum by blast
+
+lemma enn2real_le:
+ assumes "enn2real e \<le> r" "e \<noteq> top" shows "e \<le> ennreal r"
+ by (metis assms enn2real_less ennreal_enn2real_if eq_iff less_le)
+
lemma tendsto_top_iff_ennreal:
fixes f :: "'a \<Rightarrow> ennreal"
shows "(f \<longlongrightarrow> top) F \<longleftrightarrow> (\<forall>l\<ge>0. eventually (\<lambda>x. ennreal l < f x) F)"
--- a/src/HOL/Library/Indicator_Function.thy Thu Jul 18 15:40:15 2019 +0100
+++ b/src/HOL/Library/Indicator_Function.thy Fri Jul 19 12:57:14 2019 +0100
@@ -169,6 +169,16 @@
"A \<subseteq> B \<Longrightarrow> indicator A x * indicator B x = (indicator A x :: 'a::comm_semiring_1)"
by (auto split: split_indicator simp: fun_eq_iff)
+lemma indicator_times_eq_if:
+ fixes f :: "'a \<Rightarrow> 'b::comm_ring_1"
+ shows "indicator S x * f x = (if x \<in> S then f x else 0)" "f x * indicator S x = (if x \<in> S then f x else 0)"
+ by auto
+
+lemma indicator_scaleR_eq_if:
+ fixes f :: "'a \<Rightarrow> 'b::real_vector"
+ shows "indicator S x *\<^sub>R f x = (if x \<in> S then f x else 0)"
+ by simp
+
lemma indicator_sums:
assumes "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
shows "(\<lambda>i. indicator (A i) x::real) sums indicator (\<Union>i. A i) x"
--- a/src/HOL/Probability/SPMF.thy Thu Jul 18 15:40:15 2019 +0100
+++ b/src/HOL/Probability/SPMF.thy Fri Jul 19 12:57:14 2019 +0100
@@ -20,9 +20,6 @@
and ennreal_max_0': "ennreal (max x 0) = ennreal x"
by(simp_all add: max_def ennreal_eq_0_iff)
-lemma ennreal_enn2real_if: "ennreal (enn2real r) = (if r = \<top> then 0 else r)"
-by(auto intro!: ennreal_enn2real simp add: less_top)
-
lemma e2ennreal_0 [simp]: "e2ennreal 0 = 0"
by(simp add: zero_ennreal_def)