--- a/src/HOL/Analysis/Derivative.thy Thu Jan 06 17:45:07 2022 +0100
+++ b/src/HOL/Analysis/Derivative.thy Fri Jan 07 08:50:12 2022 +0100
@@ -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)
--- a/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Thu Jan 06 17:45:07 2022 +0100
+++ b/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Fri Jan 07 08:50:12 2022 +0100
@@ -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:
--- a/src/HOL/Factorial.thy Thu Jan 06 17:45:07 2022 +0100
+++ b/src/HOL/Factorial.thy Fri Jan 07 08:50:12 2022 +0100
@@ -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
--- a/src/HOL/Set_Interval.thy Thu Jan 06 17:45:07 2022 +0100
+++ b/src/HOL/Set_Interval.thy Fri Jan 07 08:50:12 2022 +0100
@@ -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)