# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1641396923 0
# Node ID fa0020b47868d53fca63e9916a722baaba7c999a
# Parent  507203e30db4f4a1ef778aee9d46964ee7a17dc3
New and simplified theorems

diff -r 507203e30db4 -r fa0020b47868 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Mon Jan 03 13:29:05 2022 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Wed Jan 05 15:35:23 2022 +0000
@@ -2354,6 +2354,10 @@
   unfolding DERIV_deriv_iff_field_differentiable[symmetric]
   by (auto intro!: DERIV_imp_deriv derivative_intros)
 
+lemma deriv_minus [simp]:
+  "f field_differentiable at z \<Longrightarrow> deriv (\<lambda>w. - f w) z = - deriv f z"
+  by (simp add: DERIV_deriv_iff_field_differentiable DERIV_imp_deriv Deriv.field_differentiable_minus)
+
 lemma deriv_diff [simp]:
   "\<lbrakk>f field_differentiable at z; g field_differentiable at z\<rbrakk>
    \<Longrightarrow> deriv (\<lambda>w. f w - g w) z = deriv f z - deriv g z"
@@ -2390,6 +2394,17 @@
   "f field_differentiable at z \<Longrightarrow> deriv (\<lambda>w. f w / c) z = deriv f z / c"
   by (simp add: field_class.field_divide_inverse)
 
+lemma deriv_pow: "\<lbrakk>f field_differentiable at z\<rbrakk>
+   \<Longrightarrow> deriv (\<lambda>w. f w ^ n) z = (if n=0 then 0 else n * deriv f z * f z ^ (n - Suc 0))"
+  unfolding DERIV_deriv_iff_field_differentiable[symmetric]
+  by (auto intro!: DERIV_imp_deriv derivative_eq_intros)
+
+lemma deriv_sum [simp]:
+  "\<lbrakk>\<And>i. f i field_differentiable at z\<rbrakk>
+   \<Longrightarrow> deriv (\<lambda>w. sum (\<lambda>i. f i w) S) z = sum (\<lambda>i. deriv (f i) z) S"
+  unfolding DERIV_deriv_iff_field_differentiable[symmetric]
+  by (auto intro!: DERIV_imp_deriv derivative_intros)
+
 lemma deriv_compose_linear:
   "f field_differentiable at (c * z) \<Longrightarrow> deriv (\<lambda>w. f (c * w)) z = c * deriv f (c * z)"
 apply (rule DERIV_imp_deriv)
diff -r 507203e30db4 -r fa0020b47868 src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy
--- a/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy	Mon Jan 03 13:29:05 2022 +0100
+++ b/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy	Wed Jan 05 15:35:23 2022 +0000
@@ -1582,6 +1582,91 @@
     using measurable_on_UNIV by blast
 qed
 
+subsection \<open>Monotonic functions are Lebesgue integrable\<close>
+
+(*Can these be generalised from type real?*)
+lemma integrable_mono_on_nonneg:
+  fixes f :: "real \<Rightarrow> real"
+  assumes mon: "mono_on f {a..b}" and 0: "\<And>x. 0 \<le> f x"
+  shows "integrable (lebesgue_on {a..b}) f" 
+proof -
+  have "space lborel = space lebesgue" "sets borel \<subseteq> sets lebesgue"
+    by force+
+  then have fborel: "f \<in> borel_measurable (lebesgue_on {a..b})"
+    by (metis mon borel_measurable_mono_on_fnc borel_measurable_subalgebra mono_restrict_space space_lborel space_restrict_space)
+  then obtain g where g: "incseq g" and simple: "\<And>i. simple_function (lebesgue_on {a..b}) (g i)" 
+                and bdd: " (\<forall>x. bdd_above (range (\<lambda>i. g i x)))" and nonneg: "\<forall>i x. 0 \<le> g i x"
+                and fsup: "f = (SUP i. g i)"
+    by (metis borel_measurable_implies_simple_function_sequence_real 0)
+  have "f ` {a..b} \<subseteq> {f a..f b}" 
+    using assms by (auto simp: mono_on_def)
+  have g_le_f: "g i x \<le> f x" for i x
+  proof -
+    have "bdd_above ((\<lambda>h. h x) ` range g)"
+      using bdd cSUP_lessD linorder_not_less by fastforce
+    then show ?thesis
+      by (metis SUP_apply UNIV_I bdd cSUP_upper fsup)
+  qed
+  then have gfb: "g i x \<le> f b" if "x \<in> {a..b}" for i x
+    by (smt (verit, best) mon atLeastAtMost_iff mono_on_def that)
+  have g_le: "g i x \<le> g j x" if "i\<le>j"  for i j x
+    using g by (simp add: incseq_def le_funD that)
+  show "integrable (lebesgue_on {a..b}) ( f)"
+  proof (rule integrable_dominated_convergence)
+    show "f \<in> borel_measurable (lebesgue_on {a..b})"
+      using fborel by blast
+    have "\<And>x. (\<lambda>i. g i x) \<longlonglongrightarrow> (SUP h \<in> range g. h  x)"
+    proof (rule order_tendstoI)
+      show "\<forall>\<^sub>F i in sequentially. y < g i x"
+        if "y < (SUP h\<in>range g. h x)" for x y
+      proof -
+        from that obtain h where h: "h \<in> range g" "y < h x"
+          using g_le_f by (subst (asm)less_cSUP_iff) fastforce+
+        then show ?thesis
+          by (smt (verit, ccfv_SIG) eventually_sequentially g_le imageE)
+      qed
+      show "\<forall>\<^sub>F i in sequentially. g i x < y"
+        if "(SUP h\<in>range g. h x) < y" for x y
+        by (smt (verit, best) that Sup_apply g_le_f always_eventually fsup image_cong)
+    qed
+    then show "AE x in lebesgue_on {a..b}. (\<lambda>i. g i x) \<longlonglongrightarrow> f x"
+      by (simp add: fsup)
+    fix i
+    show "g i \<in> borel_measurable (lebesgue_on {a..b})"
+      using borel_measurable_simple_function simple by blast
+    show "AE x in lebesgue_on {a..b}. norm (g i x) \<le> f b"
+      by (simp add: gfb nonneg Measure_Space.AE_I' [of "{}"])
+  qed auto
+qed
+
+lemma integrable_mono_on:
+  fixes f :: "real \<Rightarrow> real"
+  assumes "mono_on f {a..b}" 
+  shows "integrable (lebesgue_on {a..b}) f" 
+proof -
+  define f' where "f' \<equiv> \<lambda>x. if x \<in> {a..b} then f x - f a else 0"
+  have "mono_on f' {a..b}"
+    by (smt (verit, best) assms f'_def mono_on_def)
+  moreover have 0: "\<And>x. 0 \<le> f' x"
+    by (smt (verit, best) assms atLeastAtMost_iff f'_def mono_on_def)
+  ultimately have "integrable (lebesgue_on {a..b}) f'"
+    using integrable_mono_on_nonneg by presburger
+  then have "integrable (lebesgue_on {a..b}) (\<lambda>x. f' x + f a)"
+    by force
+  moreover have "space lborel = space lebesgue" "sets borel \<subseteq> sets lebesgue"
+    by force+
+  then have fborel: "f \<in> borel_measurable (lebesgue_on {a..b})"
+    by (metis assms borel_measurable_mono_on_fnc borel_measurable_subalgebra mono_restrict_space space_lborel space_restrict_space)
+  ultimately show ?thesis
+    by (rule integrable_cong_AE_imp) (auto simp add: f'_def)
+qed
+
+lemma integrable_on_mono_on:
+  fixes f :: "real \<Rightarrow> real"
+  assumes "mono_on f {a..b}" 
+  shows "f integrable_on {a..b}"
+  by (simp add: assms integrable_mono_on integrable_on_lebesgue_on) 
+
 subsection \<open>Measurability on generalisations of the binary product\<close>
 
 lemma measurable_on_bilinear:
diff -r 507203e30db4 -r fa0020b47868 src/HOL/Factorial.thy
--- a/src/HOL/Factorial.thy	Mon Jan 03 13:29:05 2022 +0100
+++ b/src/HOL/Factorial.thy	Wed Jan 05 15:35:23 2022 +0000
@@ -138,30 +138,16 @@
 lemma fact_mod: "m \<le> n \<Longrightarrow> fact n mod (fact m :: 'a::{semidom_modulo, linordered_semidom}) = 0"
   by (simp add: mod_eq_0_iff_dvd fact_dvd)
 
+lemma fact_eq_fact_times:
+  assumes "m \<ge> n"
+  shows "fact m = fact n * \<Prod>{Suc n..m}"
+  unfolding fact_prod
+  by (metis add.commute assms le_add1 le_add_diff_inverse of_nat_id plus_1_eq_Suc prod.ub_add_nat)
+
 lemma fact_div_fact:
   assumes "m \<ge> n"
   shows "fact m div fact n = \<Prod>{n + 1..m}"
-proof -
-  obtain d where "d = m - n"
-    by auto
-  with assms have "m = n + d"
-    by auto
-  have "fact (n + d) div (fact n) = \<Prod>{n + 1..n + d}"
-  proof (induct d)
-    case 0
-    show ?case by simp
-  next
-    case (Suc d')
-    have "fact (n + Suc d') div fact n = Suc (n + d') * fact (n + d') div fact n"
-      by simp
-    also from Suc.hyps have "\<dots> = Suc (n + d') * \<Prod>{n + 1..n + d'}"
-      unfolding div_mult1_eq[of _ "fact (n + d')"] by (simp add: fact_mod)
-    also have "\<dots> = \<Prod>{n + 1..n + Suc d'}"
-      by (simp add: atLeastAtMostSuc_conv)
-    finally show ?case .
-  qed
-  with \<open>m = n + d\<close> show ?thesis by simp
-qed
+  by (simp add: fact_eq_fact_times [OF assms])
 
 lemma fact_num_eq_if: "fact m = (if m = 0 then 1 else of_nat m * fact (m - 1))"
   by (cases m) auto
diff -r 507203e30db4 -r fa0020b47868 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Jan 03 13:29:05 2022 +0100
+++ b/src/HOL/Set_Interval.thy	Wed Jan 05 15:35:23 2022 +0000
@@ -1775,6 +1775,14 @@
   using atLeastAtMost_shift_bounds [of _ _ 1]
   by (simp add: plus_1_eq_Suc)
 
+lemma atLeast_atMost_pred_shift:
+  "F (g \<circ> (\<lambda>n. n - Suc 0)) {Suc m..Suc n} = F g {m..n}"
+  unfolding atLeast_Suc_atMost_Suc_shift by simp
+
+lemma atLeast_lessThan_pred_shift:
+  "F (g \<circ> (\<lambda>n. n - Suc 0)) {Suc m..<Suc n} = F g {m..<n}"
+  unfolding atLeast_Suc_lessThan_Suc_shift by simp
+
 lemma atLeast_int_lessThan_int_shift:
   "F g {int m..<int n} = F (g \<circ> int) {m..<n}"
   by (rule atLeastLessThan_reindex)