--- a/src/HOL/Archimedean_Field.thy Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Archimedean_Field.thy Mon Nov 02 11:56:28 2015 +0100
@@ -486,6 +486,11 @@
"- numeral v < ceiling x \<longleftrightarrow> - numeral v < x"
by (simp add: less_ceiling_iff)
+lemma ceiling_altdef: "ceiling x = (if x = of_int (floor x) then floor x else floor x + 1)"
+ by (intro ceiling_unique, (simp, linarith?)+)
+
+lemma floor_le_ceiling [simp]: "floor x \<le> ceiling x" by (simp add: ceiling_altdef)
+
text \<open>Addition and subtraction of integers\<close>
lemma ceiling_add_of_int [simp]: "ceiling (x + of_int z) = ceiling x + z"
@@ -592,4 +597,79 @@
apply (simp add: frac_def)
by (meson frac_lt_1 less_iff_diff_less_0 not_le not_less_iff_gr_or_eq)
+
+subsection \<open>Rounding to the nearest integer\<close>
+
+definition round where "round x = \<lfloor>x + 1/2\<rfloor>"
+
+lemma of_int_round_ge: "of_int (round x) \<ge> x - 1/2"
+ and of_int_round_le: "of_int (round x) \<le> x + 1/2"
+ and of_int_round_abs_le: "\<bar>of_int (round x) - x\<bar> \<le> 1/2"
+ and of_int_round_gt: "of_int (round x) > x - 1/2"
+proof -
+ from floor_correct[of "x + 1/2"] have "x + 1/2 < of_int (round x) + 1" by (simp add: round_def)
+ from add_strict_right_mono[OF this, of "-1"] show A: "of_int (round x) > x - 1/2" by simp
+ thus "of_int (round x) \<ge> x - 1/2" by simp
+ from floor_correct[of "x + 1/2"] show "of_int (round x) \<le> x + 1/2" by (simp add: round_def)
+ with A show "\<bar>of_int (round x) - x\<bar> \<le> 1/2" by linarith
+qed
+
+lemma round_of_int [simp]: "round (of_int n) = n"
+ unfolding round_def by (subst floor_unique_iff) force
+
+lemma round_0 [simp]: "round 0 = 0"
+ using round_of_int[of 0] by simp
+
+lemma round_1 [simp]: "round 1 = 1"
+ using round_of_int[of 1] by simp
+
+lemma round_numeral [simp]: "round (numeral n) = numeral n"
+ using round_of_int[of "numeral n"] by simp
+
+lemma round_neg_numeral [simp]: "round (-numeral n) = -numeral n"
+ using round_of_int[of "-numeral n"] by simp
+
+lemma round_of_nat [simp]: "round (of_nat n) = of_nat n"
+ using round_of_int[of "int n"] by simp
+
+lemma round_mono: "x \<le> y \<Longrightarrow> round x \<le> round y"
+ unfolding round_def by (intro floor_mono) simp
+
+lemma round_unique: "of_int y > x - 1/2 \<Longrightarrow> of_int y \<le> x + 1/2 \<Longrightarrow> round x = y"
+unfolding round_def
+proof (rule floor_unique)
+ assume "x - 1 / 2 < of_int y"
+ from add_strict_left_mono[OF this, of 1] show "x + 1 / 2 < of_int y + 1" by simp
+qed
+
+lemma round_altdef: "round x = (if frac x \<ge> 1/2 then ceiling x else floor x)"
+ by (cases "frac x \<ge> 1/2")
+ (rule round_unique, ((simp add: frac_def field_simps ceiling_altdef, linarith?)+)[2])+
+
+lemma floor_le_round: "\<lfloor>x\<rfloor> \<le> round x"
+ unfolding round_def by (intro floor_mono) simp
+
+lemma ceiling_ge_round: "\<lceil>x\<rceil> \<ge> round x" unfolding round_altdef by simp
+
+lemma round_diff_minimal:
+ fixes z :: "'a :: floor_ceiling"
+ shows "abs (z - of_int (round z)) \<le> abs (z - of_int m)"
+proof (cases "of_int m \<ge> z")
+ case True
+ hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int (ceiling z) - z\<bar>"
+ unfolding round_altdef by (simp add: ceiling_altdef frac_def) linarith?
+ also have "of_int \<lceil>z\<rceil> - z \<ge> 0" by linarith
+ with True have "\<bar>of_int (ceiling z) - z\<bar> \<le> \<bar>z - of_int m\<bar>"
+ by (simp add: ceiling_le_iff)
+ finally show ?thesis .
+next
+ case False
+ hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int (floor z) - z\<bar>"
+ unfolding round_altdef by (simp add: ceiling_altdef frac_def) linarith?
+ also have "z - of_int \<lfloor>z\<rfloor> \<ge> 0" by linarith
+ with False have "\<bar>of_int (floor z) - z\<bar> \<le> \<bar>z - of_int m\<bar>"
+ by (simp add: le_floor_iff)
+ finally show ?thesis .
+qed
+
end
--- a/src/HOL/Binomial.thy Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Binomial.thy Mon Nov 02 11:56:28 2015 +0100
@@ -38,6 +38,10 @@
lemma fact_mono_nat: "m \<le> n \<Longrightarrow> fact m \<le> (fact n :: nat)"
by (induct n) (auto simp: le_Suc_eq)
+lemma fact_in_Nats: "fact n \<in> \<nat>" by (induction n) auto
+
+lemma fact_in_Ints: "fact n \<in> \<int>" by (induction n) auto
+
context
assumes "SORT_CONSTRAINT('a::linordered_semidom)"
begin
@@ -381,6 +385,41 @@
lemma sum_choose_upper: "(\<Sum>k=0..n. k choose m) = Suc n choose Suc m"
by (induct n) auto
+lemma choose_alternating_sum:
+ "n > 0 \<Longrightarrow> (\<Sum>i\<le>n. (-1)^i * of_nat (n choose i)) = (0 :: 'a :: comm_ring_1)"
+ using binomial_ring[of "-1 :: 'a" 1 n] by (simp add: atLeast0AtMost mult_of_nat_commute zero_power)
+
+lemma choose_even_sum:
+ assumes "n > 0"
+ shows "2 * (\<Sum>i\<le>n. if even i then of_nat (n choose i) else 0) = (2 ^ n :: 'a :: comm_ring_1)"
+proof -
+ have "2 ^ n = (\<Sum>i\<le>n. of_nat (n choose i)) + (\<Sum>i\<le>n. (-1) ^ i * of_nat (n choose i) :: 'a)"
+ using choose_row_sum[of n]
+ by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_setsum[symmetric] of_nat_power)
+ also have "\<dots> = (\<Sum>i\<le>n. of_nat (n choose i) + (-1) ^ i * of_nat (n choose i))"
+ by (simp add: setsum.distrib)
+ also have "\<dots> = 2 * (\<Sum>i\<le>n. if even i then of_nat (n choose i) else 0)"
+ by (subst setsum_right_distrib, intro setsum.cong) simp_all
+ finally show ?thesis ..
+qed
+
+lemma choose_odd_sum:
+ assumes "n > 0"
+ shows "2 * (\<Sum>i\<le>n. if odd i then of_nat (n choose i) else 0) = (2 ^ n :: 'a :: comm_ring_1)"
+proof -
+ have "2 ^ n = (\<Sum>i\<le>n. of_nat (n choose i)) - (\<Sum>i\<le>n. (-1) ^ i * of_nat (n choose i) :: 'a)"
+ using choose_row_sum[of n]
+ by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_setsum[symmetric] of_nat_power)
+ also have "\<dots> = (\<Sum>i\<le>n. of_nat (n choose i) - (-1) ^ i * of_nat (n choose i))"
+ by (simp add: setsum_subtractf)
+ also have "\<dots> = 2 * (\<Sum>i\<le>n. if odd i then of_nat (n choose i) else 0)"
+ by (subst setsum_right_distrib, intro setsum.cong) simp_all
+ finally show ?thesis ..
+qed
+
+lemma choose_row_sum': "(\<Sum>k\<le>n. (n choose k)) = 2 ^ n"
+ using choose_row_sum[of n] by (simp add: atLeast0AtMost)
+
lemma natsum_reverse_index:
fixes m::nat
shows "(\<And>k. m \<le> k \<Longrightarrow> k \<le> n \<Longrightarrow> g k = f (m + n - k)) \<Longrightarrow> (\<Sum>k=m..n. f k) = (\<Sum>k=m..n. g k)"
@@ -417,6 +456,12 @@
lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\<lambda>n. a + of_nat n) {0 .. n}"
by (simp add: pochhammer_def)
+
+lemma pochhammer_of_nat: "pochhammer (of_nat x) n = of_nat (pochhammer x n)"
+ by (simp add: pochhammer_def of_nat_setprod)
+
+lemma pochhammer_of_int: "pochhammer (of_int x) n = of_int (pochhammer x n)"
+ by (simp add: pochhammer_def of_int_setprod)
lemma setprod_nat_ivl_Suc: "setprod f {0 .. Suc n} = setprod f {0..n} * f (Suc n)"
proof -
@@ -460,6 +505,18 @@
done
qed
+lemma pochhammer_rec': "pochhammer z (Suc n) = (z + of_nat n) * pochhammer z n"
+proof (induction n arbitrary: z)
+ case (Suc n z)
+ have "pochhammer z (Suc (Suc n)) = z * pochhammer (z + 1) (Suc n)"
+ by (simp add: pochhammer_rec)
+ also note Suc
+ also have "z * ((z + 1 + of_nat n) * pochhammer (z + 1) n) =
+ (z + of_nat (Suc n)) * pochhammer z (Suc n)"
+ by (simp_all add: pochhammer_rec algebra_simps)
+ finally show ?case .
+qed simp_all
+
lemma pochhammer_fact: "fact n = pochhammer 1 n"
unfolding fact_altdef
apply (cases n)
@@ -547,6 +604,32 @@
unfolding pochhammer_minus
by (simp add: of_nat_diff pochhammer_fact)
+lemma pochhammer_product':
+ "pochhammer z (n + m) = pochhammer z n * pochhammer (z + of_nat n) m"
+proof (induction n arbitrary: z)
+ case (Suc n z)
+ have "pochhammer z (Suc n) * pochhammer (z + of_nat (Suc n)) m =
+ z * (pochhammer (z + 1) n * pochhammer (z + 1 + of_nat n) m)"
+ by (simp add: pochhammer_rec ac_simps)
+ also note Suc[symmetric]
+ also have "z * pochhammer (z + 1) (n + m) = pochhammer z (Suc (n + m))"
+ by (subst pochhammer_rec) simp
+ finally show ?case by simp
+qed simp
+
+lemma pochhammer_product:
+ "m \<le> n \<Longrightarrow> pochhammer z n = pochhammer z m * pochhammer (z + of_nat m) (n - m)"
+ using pochhammer_product'[of z m "n - m"] by simp
+
+lemma pochhammer_absorb_comp:
+ "((r :: 'a :: comm_ring_1) - of_nat k) * pochhammer (- r) k = r * pochhammer (-r + 1) k"
+ (is "?lhs = ?rhs")
+proof -
+ have "?lhs = -pochhammer (-r) (Suc k)" by (subst pochhammer_rec') (simp add: algebra_simps)
+ also have "\<dots> = ?rhs" by (subst pochhammer_rec) simp
+ finally show ?thesis .
+qed
+
subsection\<open>Generalized binomial coefficients\<close>
@@ -729,6 +812,89 @@
then show ?thesis using kn by simp
qed
+lemma choose_rising_sum:
+ "(\<Sum>j\<le>m. ((n + j) choose n)) = ((n + m + 1) choose (n + 1))"
+ "(\<Sum>j\<le>m. ((n + j) choose n)) = ((n + m + 1) choose m)"
+proof -
+ show "(\<Sum>j\<le>m. ((n + j) choose n)) = ((n + m + 1) choose (n + 1))" by (induction m) simp_all
+ also have "... = ((n + m + 1) choose m)" by (subst binomial_symmetric) simp_all
+ finally show "(\<Sum>j\<le>m. ((n + j) choose n)) = ((n + m + 1) choose m)" .
+qed
+
+lemma choose_linear_sum:
+ "(\<Sum>i\<le>n. i * (n choose i)) = n * 2 ^ (n - 1)"
+proof (cases n)
+ case (Suc m)
+ have "(\<Sum>i\<le>n. i * (n choose i)) = (\<Sum>i\<le>Suc m. i * (Suc m choose i))" by (simp add: Suc)
+ also have "... = Suc m * 2 ^ m"
+ by (simp only: setsum_atMost_Suc_shift Suc_times_binomial setsum_right_distrib[symmetric])
+ (simp add: choose_row_sum')
+ finally show ?thesis using Suc by simp
+qed simp_all
+
+lemma choose_alternating_linear_sum:
+ assumes "n \<noteq> 1"
+ shows "(\<Sum>i\<le>n. (-1)^i * of_nat i * of_nat (n choose i) :: 'a :: comm_ring_1) = 0"
+proof (cases n)
+ case (Suc m)
+ with assms have "m > 0" by simp
+ have "(\<Sum>i\<le>n. (-1) ^ i * of_nat i * of_nat (n choose i) :: 'a) =
+ (\<Sum>i\<le>Suc m. (-1) ^ i * of_nat i * of_nat (Suc m choose i))" by (simp add: Suc)
+ also have "... = (\<Sum>i\<le>m. (-1) ^ (Suc i) * of_nat (Suc i * (Suc m choose Suc i)))"
+ by (simp only: setsum_atMost_Suc_shift setsum_right_distrib[symmetric] of_nat_mult mult_ac) simp
+ also have "... = -of_nat (Suc m) * (\<Sum>i\<le>m. (-1) ^ i * of_nat ((m choose i)))"
+ by (subst setsum_right_distrib, rule setsum.cong[OF refl], subst Suc_times_binomial)
+ (simp add: algebra_simps of_nat_mult)
+ also have "(\<Sum>i\<le>m. (-1 :: 'a) ^ i * of_nat ((m choose i))) = 0"
+ using choose_alternating_sum[OF `m > 0`] by simp
+ finally show ?thesis by simp
+qed simp
+
+lemma vandermonde:
+ "(\<Sum>k\<le>r. (m choose k) * (n choose (r - k))) = (m + n) choose r"
+proof (induction n arbitrary: r)
+ case 0
+ have "(\<Sum>k\<le>r. (m choose k) * (0 choose (r - k))) = (\<Sum>k\<le>r. if k = r then (m choose k) else 0)"
+ by (intro setsum.cong) simp_all
+ also have "... = m choose r" by (simp add: setsum.delta)
+ finally show ?case by simp
+next
+ case (Suc n r)
+ show ?case by (cases r) (simp_all add: Suc [symmetric] algebra_simps setsum.distrib Suc_diff_le)
+qed
+
+lemma choose_square_sum:
+ "(\<Sum>k\<le>n. (n choose k)^2) = ((2*n) choose n)"
+ using vandermonde[of n n n] by (simp add: power2_eq_square mult_2 binomial_symmetric [symmetric])
+
+lemma pochhammer_binomial_sum:
+ fixes a b :: "'a :: comm_ring_1"
+ shows "pochhammer (a + b) n = (\<Sum>k\<le>n. of_nat (n choose k) * pochhammer a k * pochhammer b (n - k))"
+proof (induction n arbitrary: a b)
+ case (Suc n a b)
+ have "(\<Sum>k\<le>Suc n. of_nat (Suc n choose k) * pochhammer a k * pochhammer b (Suc n - k)) =
+ (\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a (Suc i) * pochhammer b (n - i)) +
+ ((\<Sum>i\<le>n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) +
+ pochhammer b (Suc n))"
+ by (subst setsum_atMost_Suc_shift) (simp add: ring_distribs setsum.distrib)
+ also have "(\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a (Suc i) * pochhammer b (n - i)) =
+ a * pochhammer ((a + 1) + b) n"
+ by (subst Suc) (simp add: setsum_right_distrib pochhammer_rec mult_ac)
+ also have "(\<Sum>i\<le>n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) + pochhammer b (Suc n) =
+ (\<Sum>i=0..Suc n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))"
+ by (subst setsum_head_Suc, simp, subst setsum_shift_bounds_cl_Suc_ivl) (simp add: atLeast0AtMost)
+ also have "... = (\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))"
+ using Suc by (intro setsum.mono_neutral_right) (auto simp: not_le binomial_eq_0)
+ also have "... = (\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc (n - i)))"
+ by (intro setsum.cong) (simp_all add: Suc_diff_le)
+ also have "... = b * pochhammer (a + (b + 1)) n"
+ by (subst Suc) (simp add: setsum_right_distrib mult_ac pochhammer_rec)
+ also have "a * pochhammer ((a + 1) + b) n + b * pochhammer (a + (b + 1)) n =
+ pochhammer (a + b) (Suc n)" by (simp add: pochhammer_rec algebra_simps)
+ finally show ?case ..
+qed simp_all
+
+
text\<open>Contributed by Manuel Eberl, generalised by LCP.
Alternative definition of the binomial coefficient as @{term "\<Prod>i<k. (n - i) / (k - i)"}\<close>
lemma gbinomial_altdef_of_nat:
@@ -774,6 +940,285 @@
finally show ?thesis .
qed
+lemma gbinomial_negated_upper: "(a gchoose b) = (-1) ^ b * ((of_nat b - a - 1) gchoose b)"
+ by (simp add: gbinomial_pochhammer pochhammer_minus algebra_simps)
+
+lemma gbinomial_minus: "((-a) gchoose b) = (-1) ^ b * ((a + of_nat b - 1) gchoose b)"
+ by (subst gbinomial_negated_upper) (simp add: add_ac)
+
+lemma Suc_times_gbinomial:
+ "of_nat (Suc b) * ((a + 1) gchoose (Suc b)) = (a + 1) * (a gchoose b)"
+proof (cases b)
+ case (Suc b)
+ hence "((a + 1) gchoose (Suc (Suc b))) =
+ (\<Prod>i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)"
+ by (simp add: field_simps gbinomial_def)
+ also have "(\<Prod>i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
+ by (simp add: setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)
+ also have "... / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)"
+ by (simp_all add: gbinomial_def setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)
+ finally show ?thesis by (simp add: Suc field_simps del: of_nat_Suc)
+qed simp
+
+lemma gbinomial_factors:
+ "((a + 1) gchoose (Suc b)) = (a + 1) / of_nat (Suc b) * (a gchoose b)"
+proof (cases b)
+ case (Suc b)
+ hence "((a + 1) gchoose (Suc (Suc b))) =
+ (\<Prod>i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)"
+ by (simp add: field_simps gbinomial_def)
+ also have "(\<Prod>i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
+ by (simp add: setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)
+ also have "... / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)"
+ by (simp_all add: gbinomial_def setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)
+ finally show ?thesis by (simp add: Suc)
+qed simp
+
+lemma gbinomial_rec: "((r + 1) gchoose (Suc k)) = (r gchoose k) * ((r + 1) / of_nat (Suc k))"
+ using gbinomial_mult_1[of r k]
+ by (subst gbinomial_Suc_Suc) (simp add: field_simps del: of_nat_Suc, simp add: algebra_simps)
+
+lemma gbinomial_of_nat_symmetric: "k \<le> n \<Longrightarrow> (of_nat n) gchoose k = (of_nat n) gchoose (n - k)"
+ using binomial_symmetric[of k n] by (simp add: binomial_gbinomial [symmetric])
+
+
+text \<open>The absorption identity (equation 5.5 \cite[p.~157]{GKP}):\[
+{r \choose k} = \frac{r}{k}{r - 1 \choose k - 1},\quad \textnormal{integer } k \neq 0.
+\]\<close>
+lemma gbinomial_absorption':
+ "k > 0 \<Longrightarrow> (r gchoose k) = (r / of_nat(k)) * (r - 1 gchoose (k - 1))"
+ using gbinomial_rec[of "r - 1" "k - 1"]
+ by (simp_all add: gbinomial_rec field_simps del: of_nat_Suc)
+
+text \<open>The absorption identity is written in the following form to avoid
+division by $k$ (the lower index) and therefore remove the $k \neq 0$
+restriction\cite[p.~157]{GKP}:\[
+k{r \choose k} = r{r - 1 \choose k - 1}, \quad \textnormal{integer } k.
+\]\<close>
+lemma gbinomial_absorption:
+ "of_nat (Suc k) * (r gchoose Suc k) = r * ((r - 1) gchoose k)"
+ using gbinomial_absorption'[of "Suc k" r] by (simp add: field_simps del: of_nat_Suc)
+
+text \<open>The absorption identity for natural number binomial coefficients:\<close>
+lemma binomial_absorption:
+ "Suc k * (n choose Suc k) = n * ((n - 1) choose k)"
+ by (cases n) (simp_all add: binomial_eq_0 Suc_times_binomial del: binomial_Suc_Suc mult_Suc)
+
+text \<open>The absorption companion identity for natural number coefficients,
+following the proof by GKP \cite[p.~157]{GKP}:\<close>
+lemma binomial_absorb_comp:
+ "(n - k) * (n choose k) = n * ((n - 1) choose k)" (is "?lhs = ?rhs")
+proof (cases "n \<le> k")
+ case False
+ then have "?rhs = Suc ((n - 1) - k) * (n choose Suc ((n - 1) - k))"
+ using binomial_symmetric[of k "n - 1"] binomial_absorption[of "(n - 1) - k" n]
+ by simp
+ also from False have "Suc ((n - 1) - k) = n - k" by simp
+ also from False have "n choose \<dots> = n choose k" by (intro binomial_symmetric [symmetric]) simp_all
+ finally show ?thesis ..
+qed auto
+
+text \<open>The generalised absorption companion identity:\<close>
+lemma gbinomial_absorb_comp: "(r - of_nat k) * (r gchoose k) = r * ((r - 1) gchoose k)"
+ using pochhammer_absorb_comp[of r k] by (simp add: gbinomial_pochhammer)
+
+lemma gbinomial_addition_formula:
+ "r gchoose (Suc k) = ((r - 1) gchoose (Suc k)) + ((r - 1) gchoose k)"
+ using gbinomial_Suc_Suc[of "r - 1" k] by (simp add: algebra_simps)
+
+lemma binomial_addition_formula:
+ "0 < n \<Longrightarrow> n choose (Suc k) = ((n - 1) choose (Suc k)) + ((n - 1) choose k)"
+ by (subst choose_reduce_nat) simp_all
+
+
+text \<open>
+ Equation 5.9 of the reference material \cite[p.~159]{GKP} is a useful
+ summation formula, operating on both indices:\[
+ \sum\limits_{k \leq n}{r + k \choose k} = {r + n + 1 \choose n},
+ \quad \textnormal{integer } n.
+ \]
+\<close>
+lemma gbinomial_parallel_sum:
+"(\<Sum>k\<le>n. (r + of_nat k) gchoose k) = (r + of_nat n + 1) gchoose n"
+proof (induction n)
+ case (Suc m)
+ thus ?case using gbinomial_Suc_Suc[of "(r + of_nat m + 1)" m] by (simp add: add_ac)
+qed auto
+
+subsection \<open>Summation on the upper index\<close>
+text \<open>
+ Another summation formula is equation 5.10 of the reference material \cite[p.~160]{GKP},
+ aptly named \emph{summation on the upper index}:\[\sum_{0 \leq k \leq n} {k \choose m} =
+ {n + 1 \choose m + 1}, \quad \textnormal{integers } m, n \geq 0.\]
+\<close>
+lemma gbinomial_sum_up_index:
+ "(\<Sum>k = 0..n. (of_nat k gchoose m) :: 'a :: field_char_0) = (of_nat n + 1) gchoose (m + 1)"
+proof (induction n)
+ case 0
+ show ?case using gbinomial_Suc_Suc[of 0 m] by (cases m) auto
+next
+ case (Suc n)
+ thus ?case using gbinomial_Suc_Suc[of "of_nat (Suc n) :: 'a" m] by (simp add: add_ac)
+qed
+
+lemma gbinomial_index_swap:
+ "((-1) ^ m) * ((- (of_nat n) - 1) gchoose m) = ((-1) ^ n) * ((- (of_nat m) - 1) gchoose n)"
+ (is "?lhs = ?rhs")
+proof -
+ have "?lhs = (of_nat (m + n) gchoose m)"
+ by (subst gbinomial_negated_upper) (simp add: power_mult_distrib [symmetric])
+ also have "\<dots> = (of_nat (m + n) gchoose n)" by (subst gbinomial_of_nat_symmetric) simp_all
+ also have "\<dots> = ?rhs" by (subst gbinomial_negated_upper) simp
+ finally show ?thesis .
+qed
+
+lemma gbinomial_sum_lower_neg:
+ "(\<Sum>k\<le>m. (r gchoose k) * (- 1) ^ k) = (- 1) ^ m * (r - 1 gchoose m)" (is "?lhs = ?rhs")
+proof -
+ have "?lhs = (\<Sum>k\<le>m. -(r + 1) + of_nat k gchoose k)"
+ by (intro setsum.cong[OF refl]) (subst gbinomial_negated_upper, simp add: power_mult_distrib)
+ also have "\<dots> = -r + of_nat m gchoose m" by (subst gbinomial_parallel_sum) simp
+ also have "\<dots> = ?rhs" by (subst gbinomial_negated_upper) (simp add: power_mult_distrib)
+ finally show ?thesis .
+qed
+
+lemma gbinomial_partial_row_sum:
+"(\<Sum>k\<le>m. (r gchoose k) * ((r / 2) - of_nat k)) = ((of_nat m + 1)/2) * (r gchoose (m + 1))"
+proof (induction m)
+ case (Suc mm)
+ hence "(\<Sum>k\<le>Suc mm. (r gchoose k) * (r / 2 - of_nat k)) =
+ (r - of_nat (Suc mm)) * (r gchoose Suc mm) / 2" by (simp add: algebra_simps)
+ also have "\<dots> = r * (r - 1 gchoose Suc mm) / 2" by (subst gbinomial_absorb_comp) (rule refl)
+ also have "\<dots> = (of_nat (Suc mm) + 1) / 2 * (r gchoose (Suc mm + 1))"
+ by (subst gbinomial_absorption [symmetric]) simp
+ finally show ?case .
+qed simp_all
+
+lemma setsum_bounds_lt_plus1: "(\<Sum>k<mm. f (Suc k)) = (\<Sum>k=1..mm. f k)"
+ by (induction mm) simp_all
+
+lemma gbinomial_partial_sum_poly:
+ "(\<Sum>k\<le>m. (of_nat m + r gchoose k) * x^k * y^(m-k)) =
+ (\<Sum>k\<le>m. (-r gchoose k) * (-x)^k * (x + y)^(m-k))" (is "?lhs m = ?rhs m")
+proof (induction m)
+ case (Suc mm)
+ def G \<equiv> "\<lambda>i k. (of_nat i + r gchoose k) * x^k * y^(i-k)" and S \<equiv> ?lhs
+ have SG_def: "S = (\<lambda>i. (\<Sum>k\<le>i. (G i k)))" unfolding S_def G_def ..
+
+ have "S (Suc mm) = G (Suc mm) 0 + (\<Sum>k=Suc 0..Suc mm. G (Suc mm) k)"
+ using SG_def by (simp add: setsum_head_Suc atLeast0AtMost [symmetric])
+ also have "(\<Sum>k=Suc 0..Suc mm. G (Suc mm) k) = (\<Sum>k=0..mm. G (Suc mm) (Suc k))"
+ by (subst setsum_shift_bounds_cl_Suc_ivl) simp
+ also have "\<dots> = (\<Sum>k=0..mm. ((of_nat mm + r gchoose (Suc k))
+ + (of_nat mm + r gchoose k)) * x^(Suc k) * y^(mm - k))"
+ unfolding G_def by (subst gbinomial_addition_formula) simp
+ also have "\<dots> = (\<Sum>k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k))
+ + (\<Sum>k=0..mm. (of_nat mm + r gchoose k) * x^(Suc k) * y^(mm - k))"
+ by (subst setsum.distrib [symmetric]) (simp add: algebra_simps)
+ also have "(\<Sum>k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k)) =
+ (\<Sum>k<Suc mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k))"
+ by (simp only: atLeast0AtMost lessThan_Suc_atMost)
+ also have "\<dots> = (\<Sum>k<mm. (of_nat mm + r gchoose Suc k) * x^(Suc k) * y^(mm-k))
+ + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)" (is "_ = ?A + ?B")
+ by (subst setsum_lessThan_Suc) simp
+ also have "?A = (\<Sum>k=1..mm. (of_nat mm + r gchoose k) * x^k * y^(mm - k + 1))"
+ proof (subst setsum_bounds_lt_plus1 [symmetric], intro setsum.cong[OF refl], clarify)
+ fix k assume "k < mm"
+ hence "mm - k = mm - Suc k + 1" by linarith
+ thus "(of_nat mm + r gchoose Suc k) * x ^ Suc k * y ^ (mm - k) =
+ (of_nat mm + r gchoose Suc k) * x ^ Suc k * y ^ (mm - Suc k + 1)" by (simp only:)
+ qed
+ also have "\<dots> + ?B = y * (\<Sum>k=1..mm. (G mm k)) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)"
+ unfolding G_def by (subst setsum_right_distrib) (simp add: algebra_simps)
+ also have "(\<Sum>k=0..mm. (of_nat mm + r gchoose k) * x^(Suc k) * y^(mm - k)) = x * (S mm)"
+ unfolding S_def by (subst setsum_right_distrib) (simp add: atLeast0AtMost algebra_simps)
+ also have "(G (Suc mm) 0) = y * (G mm 0)" by (simp add: G_def)
+ finally have "S (Suc mm) = y * ((G mm 0) + (\<Sum>k=1..mm. (G mm k)))
+ + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm) + x * (S mm)"
+ by (simp add: ring_distribs)
+ also have "(G mm 0) + (\<Sum>k=1..mm. (G mm k)) = S mm"
+ by (simp add: setsum_head_Suc[symmetric] SG_def atLeast0AtMost)
+ finally have "S (Suc mm) = (x + y) * (S mm) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)"
+ by (simp add: algebra_simps)
+ also have "(of_nat mm + r gchoose (Suc mm)) = (-1) ^ (Suc mm) * (-r gchoose (Suc mm))"
+ by (subst gbinomial_negated_upper) simp
+ also have "(-1) ^ Suc mm * (- r gchoose Suc mm) * x ^ Suc mm =
+ (-r gchoose (Suc mm)) * (-x) ^ Suc mm" by (simp add: power_minus[of x])
+ also have "(x + y) * S mm + \<dots> = (x + y) * ?rhs mm + (-r gchoose (Suc mm)) * (-x)^Suc mm"
+ unfolding S_def by (subst Suc.IH) simp
+ also have "(x + y) * ?rhs mm = (\<Sum>n\<le>mm. ((- r gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n)))"
+ by (subst setsum_right_distrib, rule setsum.cong) (simp_all add: Suc_diff_le)
+ also have "\<dots> + (-r gchoose (Suc mm)) * (-x)^Suc mm =
+ (\<Sum>n\<le>Suc mm. (- r gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n))" by simp
+ finally show ?case unfolding S_def .
+qed simp_all
+
+lemma gbinomial_partial_sum_poly_xpos:
+ "(\<Sum>k\<le>m. (of_nat m + r gchoose k) * x^k * y^(m-k)) =
+ (\<Sum>k\<le>m. (of_nat k + r - 1 gchoose k) * x^k * (x + y)^(m-k))"
+ apply (subst gbinomial_partial_sum_poly)
+ apply (subst gbinomial_negated_upper)
+ apply (intro setsum.cong, rule refl)
+ apply (simp add: power_mult_distrib [symmetric])
+ done
+
+lemma setsum_nat_symmetry:
+ "(\<Sum>k = 0..(m::nat). f k) = (\<Sum>k = 0..m. f (m - k))"
+ by (rule setsum.reindex_bij_witness[where i="\<lambda>i. m - i" and j="\<lambda>i. m - i"]) auto
+
+lemma binomial_r_part_sum: "(\<Sum>k\<le>m. (2 * m + 1 choose k)) = 2 ^ (2 * m)"
+proof -
+ have "2 * 2^(2*m) = (\<Sum>k = 0..(2 * m + 1). (2 * m + 1 choose k))"
+ using choose_row_sum[where n="2 * m + 1"] by simp
+ also have "(\<Sum>k = 0..(2 * m + 1). (2 * m + 1 choose k)) = (\<Sum>k = 0..m. (2 * m + 1 choose k))
+ + (\<Sum>k = m+1..2*m+1. (2 * m + 1 choose k))"
+ using setsum_ub_add_nat[of 0 m "\<lambda>k. 2 * m + 1 choose k" "m+1"] by (simp add: mult_2)
+ also have "(\<Sum>k = m+1..2*m+1. (2 * m + 1 choose k)) =
+ (\<Sum>k = 0..m. (2 * m + 1 choose (k + (m + 1))))"
+ by (subst setsum_shift_bounds_cl_nat_ivl [symmetric]) (simp add: mult_2)
+ also have "\<dots> = (\<Sum>k = 0..m. (2 * m + 1 choose (m - k)))"
+ by (intro setsum.cong[OF refl], subst binomial_symmetric) simp_all
+ also have "\<dots> = (\<Sum>k = 0..m. (2 * m + 1 choose k))"
+ by (subst (2) setsum_nat_symmetry) (rule refl)
+ also have "\<dots> + \<dots> = 2 * \<dots>" by simp
+ finally show ?thesis by (subst (asm) mult_cancel1) (simp add: atLeast0AtMost)
+qed
+
+lemma gbinomial_r_part_sum:
+ "(\<Sum>k\<le>m. (2 * (of_nat m) + 1 gchoose k)) = 2 ^ (2 * m)" (is "?lhs = ?rhs")
+proof -
+ have "?lhs = of_nat (\<Sum>k\<le>m. (2 * m + 1) choose k)"
+ by (simp add: binomial_gbinomial of_nat_mult add_ac of_nat_setsum)
+ also have "\<dots> = of_nat (2 ^ (2 * m))" by (subst binomial_r_part_sum) (rule refl)
+ finally show ?thesis by (simp add: of_nat_power)
+qed
+
+lemma gbinomial_sum_nat_pow2:
+ "(\<Sum>k\<le>m. (of_nat (m + k) gchoose k :: 'a :: field_char_0) / 2 ^ k) = 2 ^ m" (is "?lhs = ?rhs")
+proof -
+ have "2 ^ m * 2 ^ m = (2 ^ (2*m) :: 'a)" by (induction m) simp_all
+ also have "\<dots> = (\<Sum>k\<le>m. (2 * (of_nat m) + 1 gchoose k))" using gbinomial_r_part_sum ..
+ also have "\<dots> = (\<Sum>k\<le>m. (of_nat (m + k) gchoose k) * 2 ^ (m - k))"
+ using gbinomial_partial_sum_poly_xpos[where x="1" and y="1" and r="of_nat m + 1" and m="m"]
+ by (simp add: add_ac)
+ also have "\<dots> = 2 ^ m * (\<Sum>k\<le>m. (of_nat (m + k) gchoose k) / 2 ^ k)"
+ by (subst setsum_right_distrib) (simp add: algebra_simps power_diff)
+ finally show ?thesis by (subst (asm) mult_left_cancel) simp_all
+qed
+
+lemma gbinomial_trinomial_revision:
+ assumes "k \<le> m"
+ shows "(r gchoose m) * (of_nat m gchoose k) = (r gchoose k) * (r - of_nat k gchoose (m - k))"
+proof -
+ have "(r gchoose m) * (of_nat m gchoose k) =
+ (r gchoose m) * fact m / (fact k * fact (m - k))"
+ using assms by (simp add: binomial_gbinomial [symmetric] binomial_fact)
+ also have "\<dots> = (r gchoose k) * (r - of_nat k gchoose (m - k))" using assms
+ by (simp add: gbinomial_pochhammer power_diff pochhammer_product)
+ finally show ?thesis .
+qed
+
+
text\<open>Versions of the theorems above for the natural-number version of "choose"\<close>
lemma binomial_altdef_of_nat:
fixes n k :: nat
--- a/src/HOL/Complex.thy Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Complex.thy Mon Nov 02 11:56:28 2015 +0100
@@ -171,6 +171,17 @@
"z \<in> \<real> \<Longrightarrow> of_real (Re z) = z"
by (auto simp: Reals_def)
+lemma complex_Re_fact [simp]: "Re (fact n) = fact n"
+proof -
+ have "(fact n :: complex) = of_real (fact n)" by simp
+ also have "Re \<dots> = fact n" by (subst Re_complex_of_real) simp_all
+ finally show ?thesis .
+qed
+
+lemma complex_Im_fact [simp]: "Im (fact n) = 0"
+ by (subst of_nat_fact [symmetric]) (simp only: complex_Im_of_nat)
+
+
subsection \<open>The Complex Number $i$\<close>
primcorec "ii" :: complex ("\<i>") where
@@ -497,6 +508,12 @@
lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0"
by simp
+lemma complex_cnj_fact [simp]: "cnj (fact n) = fact n"
+ by (subst of_nat_fact [symmetric], subst complex_cnj_of_nat) simp
+
+lemma complex_cnj_pochhammer [simp]: "cnj (pochhammer z n) = pochhammer (cnj z) n"
+ by (induction n arbitrary: z) (simp_all add: pochhammer_rec)
+
lemma bounded_linear_cnj: "bounded_linear cnj"
using complex_cnj_add complex_cnj_scaleR
by (rule bounded_linear_intro [where K=1], simp)
--- a/src/HOL/Filter.thy Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Filter.thy Mon Nov 02 11:56:28 2015 +0100
@@ -393,6 +393,11 @@
lemma eventually_happens: "eventually P net \<Longrightarrow> net = bot \<or> (\<exists>x. P x)"
by (metis frequentlyE eventually_frequently)
+lemma eventually_happens':
+ assumes "F \<noteq> bot" "eventually P F"
+ shows "\<exists>x. P x"
+ using assms eventually_frequently frequentlyE by blast
+
abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
where "trivial_limit F \<equiv> F = bot"
@@ -611,6 +616,15 @@
lemma eventually_gt_at_top: "eventually (\<lambda>x. (c::_::{no_top, linorder}) < x) at_top"
unfolding eventually_at_top_dense by auto
+lemma eventually_all_ge_at_top:
+ assumes "eventually P (at_top :: ('a :: linorder) filter)"
+ shows "eventually (\<lambda>x. \<forall>y\<ge>x. P y) at_top"
+proof -
+ from assms obtain x where "\<And>y. y \<ge> x \<Longrightarrow> P y" by (auto simp: eventually_at_top_linorder)
+ hence "\<forall>z\<ge>y. P z" if "y \<ge> x" for y using that by simp
+ thus ?thesis by (auto simp: eventually_at_top_linorder)
+qed
+
definition at_bot :: "('a::order) filter"
where "at_bot = (INF k. principal {.. k})"
--- a/src/HOL/Int.thy Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Int.thy Mon Nov 02 11:56:28 2015 +0100
@@ -225,6 +225,9 @@
lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
by (transfer fixing: times) (clarsimp simp add: algebra_simps of_nat_mult)
+lemma mult_of_int_commute: "of_int x * y = y * of_int x"
+ by (transfer fixing: times) (auto simp: algebra_simps mult_of_nat_commute)
+
text\<open>Collapse nested embeddings\<close>
lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n"
by (induct n) auto
--- a/src/HOL/Library/Convex.thy Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Library/Convex.thy Mon Nov 02 11:56:28 2015 +0100
@@ -304,6 +304,42 @@
where "convex_on s f \<longleftrightarrow>
(\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y)"
+lemma convex_onI [intro?]:
+ assumes "\<And>t x y. t > 0 \<Longrightarrow> t < 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow>
+ f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
+ shows "convex_on A f"
+ unfolding convex_on_def
+proof clarify
+ fix x y u v assume A: "x \<in> A" "y \<in> A" "(u::real) \<ge> 0" "v \<ge> 0" "u + v = 1"
+ from A(5) have [simp]: "v = 1 - u" by (simp add: algebra_simps)
+ from A(1-4) show "f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y" using assms[of u y x]
+ by (cases "u = 0 \<or> u = 1") (auto simp: algebra_simps)
+qed
+
+lemma convex_on_linorderI [intro?]:
+ fixes A :: "('a::{linorder,real_vector}) set"
+ assumes "\<And>t x y. t > 0 \<Longrightarrow> t < 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x < y \<Longrightarrow>
+ f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
+ shows "convex_on A f"
+proof
+ fix t x y assume A: "x \<in> A" "y \<in> A" "(t::real) > 0" "t < 1"
+ case (goal1 t x y)
+ with goal1 assms[of t x y] assms[of "1 - t" y x]
+ show ?case by (cases x y rule: linorder_cases) (auto simp: algebra_simps)
+qed
+
+lemma convex_onD:
+ assumes "convex_on A f"
+ shows "\<And>t x y. t \<ge> 0 \<Longrightarrow> t \<le> 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow>
+ f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
+ using assms unfolding convex_on_def by auto
+
+lemma convex_onD_Icc:
+ assumes "convex_on {x..y} f" "x \<le> (y :: _ :: {real_vector,preorder})"
+ shows "\<And>t. t \<ge> 0 \<Longrightarrow> t \<le> 1 \<Longrightarrow>
+ f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
+ using assms(2) by (intro convex_onD[OF assms(1)]) simp_all
+
lemma convex_on_subset: "convex_on t f \<Longrightarrow> s \<subseteq> t \<Longrightarrow> convex_on s f"
unfolding convex_on_def by auto
@@ -835,4 +871,91 @@
show ?thesis by auto
qed
+
+subsection \<open>Convexity of real functions\<close>
+
+lemma convex_on_realI:
+ assumes "connected A"
+ assumes "\<And>x. x \<in> A \<Longrightarrow> (f has_real_derivative f' x) (at x)"
+ assumes "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<le> y \<Longrightarrow> f' x \<le> f' y"
+ shows "convex_on A f"
+proof (rule convex_on_linorderI)
+ fix t x y :: real
+ assume t: "t > 0" "t < 1" and xy: "x \<in> A" "y \<in> A" "x < y"
+ def z \<equiv> "(1 - t) * x + t * y"
+ with `connected A` and xy have ivl: "{x..y} \<subseteq> A" using connected_contains_Icc by blast
+
+ from xy t have xz: "z > x" by (simp add: z_def algebra_simps)
+ have "y - z = (1 - t) * (y - x)" by (simp add: z_def algebra_simps)
+ also from xy t have "... > 0" by (intro mult_pos_pos) simp_all
+ finally have yz: "z < y" by simp
+
+ from assms xz yz ivl t have "\<exists>\<xi>. \<xi> > x \<and> \<xi> < z \<and> f z - f x = (z - x) * f' \<xi>"
+ by (intro MVT2) (auto intro!: assms(2))
+ then obtain \<xi> where \<xi>: "\<xi> > x" "\<xi> < z" "f' \<xi> = (f z - f x) / (z - x)" by auto
+ from assms xz yz ivl t have "\<exists>\<eta>. \<eta> > z \<and> \<eta> < y \<and> f y - f z = (y - z) * f' \<eta>"
+ by (intro MVT2) (auto intro!: assms(2))
+ then obtain \<eta> where \<eta>: "\<eta> > z" "\<eta> < y" "f' \<eta> = (f y - f z) / (y - z)" by auto
+
+ from \<eta>(3) have "(f y - f z) / (y - z) = f' \<eta>" ..
+ also from \<xi> \<eta> ivl have "\<xi> \<in> A" "\<eta> \<in> A" by auto
+ with \<xi> \<eta> have "f' \<eta> \<ge> f' \<xi>" by (intro assms(3)) auto
+ also from \<xi>(3) have "f' \<xi> = (f z - f x) / (z - x)" .
+ finally have "(f y - f z) * (z - x) \<ge> (f z - f x) * (y - z)"
+ using xz yz by (simp add: field_simps)
+ also have "z - x = t * (y - x)" by (simp add: z_def algebra_simps)
+ also have "y - z = (1 - t) * (y - x)" by (simp add: z_def algebra_simps)
+ finally have "(f y - f z) * t \<ge> (f z - f x) * (1 - t)" using xy by simp
+ thus "(1 - t) * f x + t * f y \<ge> f ((1 - t) *\<^sub>R x + t *\<^sub>R y)"
+ by (simp add: z_def algebra_simps)
+qed
+
+lemma convex_on_inverse:
+ assumes "A \<subseteq> {0<..}"
+ shows "convex_on A (inverse :: real \<Rightarrow> real)"
+proof (rule convex_on_subset[OF _ assms], intro convex_on_realI[of _ _ "\<lambda>x. -inverse (x^2)"])
+ fix u v :: real assume "u \<in> {0<..}" "v \<in> {0<..}" "u \<le> v"
+ with assms show "-inverse (u^2) \<le> -inverse (v^2)"
+ by (intro le_imp_neg_le le_imp_inverse_le power_mono) (simp_all)
+qed (insert assms, auto intro!: derivative_eq_intros simp: divide_simps power2_eq_square)
+
+lemma convex_onD_Icc':
+ assumes "convex_on {x..y} f" "c \<in> {x..y}"
+ defines "d \<equiv> y - x"
+ shows "f c \<le> (f y - f x) / d * (c - x) + f x"
+proof (cases y x rule: linorder_cases)
+ assume less: "x < y"
+ hence d: "d > 0" by (simp add: d_def)
+ from assms(2) less have A: "0 \<le> (c - x) / d" "(c - x) / d \<le> 1"
+ by (simp_all add: d_def divide_simps)
+ have "f c = f (x + (c - x) * 1)" by simp
+ also from less have "1 = ((y - x) / d)" by (simp add: d_def)
+ also from d have "x + (c - x) * \<dots> = (1 - (c - x) / d) *\<^sub>R x + ((c - x) / d) *\<^sub>R y"
+ by (simp add: field_simps)
+ also have "f \<dots> \<le> (1 - (c - x) / d) * f x + (c - x) / d * f y" using assms less
+ by (intro convex_onD_Icc) simp_all
+ also from d have "\<dots> = (f y - f x) / d * (c - x) + f x" by (simp add: field_simps)
+ finally show ?thesis .
+qed (insert assms(2), simp_all)
+
+lemma convex_onD_Icc'':
+ assumes "convex_on {x..y} f" "c \<in> {x..y}"
+ defines "d \<equiv> y - x"
+ shows "f c \<le> (f x - f y) / d * (y - c) + f y"
+proof (cases y x rule: linorder_cases)
+ assume less: "x < y"
+ hence d: "d > 0" by (simp add: d_def)
+ from assms(2) less have A: "0 \<le> (y - c) / d" "(y - c) / d \<le> 1"
+ by (simp_all add: d_def divide_simps)
+ have "f c = f (y - (y - c) * 1)" by simp
+ also from less have "1 = ((y - x) / d)" by (simp add: d_def)
+ also from d have "y - (y - c) * \<dots> = (1 - (1 - (y - c) / d)) *\<^sub>R x + (1 - (y - c) / d) *\<^sub>R y"
+ by (simp add: field_simps)
+ also have "f \<dots> \<le> (1 - (1 - (y - c) / d)) * f x + (1 - (y - c) / d) * f y" using assms less
+ by (intro convex_onD_Icc) (simp_all add: field_simps)
+ also from d have "\<dots> = (f x - f y) / d * (y - c) + f y" by (simp add: field_simps)
+ finally show ?thesis .
+qed (insert assms(2), simp_all)
+
+
end
--- a/src/HOL/Limits.thy Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Limits.thy Mon Nov 02 11:56:28 2015 +0100
@@ -137,12 +137,34 @@
by (auto elim!: allE[of _ n])
qed
+lemma Bseq_bdd_above':
+ "Bseq (X::nat \<Rightarrow> 'a :: real_normed_vector) \<Longrightarrow> bdd_above (range (\<lambda>n. norm (X n)))"
+proof (elim BseqE, intro bdd_aboveI2)
+ fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "norm (X n) \<le> K"
+ by (auto elim!: allE[of _ n])
+qed
+
lemma Bseq_bdd_below: "Bseq (X::nat \<Rightarrow> real) \<Longrightarrow> bdd_below (range X)"
proof (elim BseqE, intro bdd_belowI2)
fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "- K \<le> X n"
by (auto elim!: allE[of _ n])
qed
+lemma Bseq_eventually_mono:
+ assumes "eventually (\<lambda>n. norm (f n) \<le> norm (g n)) sequentially" "Bseq g"
+ shows "Bseq f"
+proof -
+ from assms(1) obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> norm (f n) \<le> norm (g n)"
+ by (auto simp: eventually_at_top_linorder)
+ moreover from assms(2) obtain K where K: "\<And>n. norm (g n) \<le> K" by (blast elim!: BseqE)
+ ultimately have "norm (f n) \<le> max K (Max {norm (f n) |n. n < N})" for n
+ apply (cases "n < N")
+ apply (rule max.coboundedI2, rule Max.coboundedI, auto) []
+ apply (rule max.coboundedI1, force intro: order.trans[OF N K])
+ done
+ thus ?thesis by (blast intro: BseqI')
+qed
+
lemma lemma_NBseq_def:
"(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
proof safe
@@ -218,6 +240,73 @@
lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
by (simp add: Bseq_def)
+lemma Bseq_add:
+ assumes "Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)"
+ shows "Bseq (\<lambda>x. f x + c)"
+proof -
+ from assms obtain K where K: "\<And>x. norm (f x) \<le> K" unfolding Bseq_def by blast
+ {
+ fix x :: nat
+ have "norm (f x + c) \<le> norm (f x) + norm c" by (rule norm_triangle_ineq)
+ also have "norm (f x) \<le> K" by (rule K)
+ finally have "norm (f x + c) \<le> K + norm c" by simp
+ }
+ thus ?thesis by (rule BseqI')
+qed
+
+lemma Bseq_add_iff: "Bseq (\<lambda>x. f x + c) \<longleftrightarrow> Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)"
+ using Bseq_add[of f c] Bseq_add[of "\<lambda>x. f x + c" "-c"] by auto
+
+lemma Bseq_mult:
+ assumes "Bseq (f :: nat \<Rightarrow> 'a :: real_normed_field)"
+ assumes "Bseq (g :: nat \<Rightarrow> 'a :: real_normed_field)"
+ shows "Bseq (\<lambda>x. f x * g x)"
+proof -
+ from assms obtain K1 K2 where K: "\<And>x. norm (f x) \<le> K1" "K1 > 0" "\<And>x. norm (g x) \<le> K2" "K2 > 0"
+ unfolding Bseq_def by blast
+ hence "\<And>x. norm (f x * g x) \<le> K1 * K2" by (auto simp: norm_mult intro!: mult_mono)
+ thus ?thesis by (rule BseqI')
+qed
+
+lemma Bfun_const [simp]: "Bfun (\<lambda>_. c) F"
+ unfolding Bfun_metric_def by (auto intro!: exI[of _ c] exI[of _ "1::real"])
+
+lemma Bseq_cmult_iff: "(c :: 'a :: real_normed_field) \<noteq> 0 \<Longrightarrow> Bseq (\<lambda>x. c * f x) \<longleftrightarrow> Bseq f"
+proof
+ assume "c \<noteq> 0" "Bseq (\<lambda>x. c * f x)"
+ find_theorems "Bfun (\<lambda>_. ?c) _"
+ from Bfun_const this(2) have "Bseq (\<lambda>x. inverse c * (c * f x))" by (rule Bseq_mult)
+ with `c \<noteq> 0` show "Bseq f" by (simp add: divide_simps)
+qed (intro Bseq_mult Bfun_const)
+
+lemma Bseq_subseq: "Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector) \<Longrightarrow> Bseq (\<lambda>x. f (g x))"
+ unfolding Bseq_def by auto
+
+lemma Bseq_Suc_iff: "Bseq (\<lambda>n. f (Suc n)) \<longleftrightarrow> Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)"
+ using Bseq_offset[of f 1] by (auto intro: Bseq_subseq)
+
+lemma increasing_Bseq_subseq_iff:
+ assumes "\<And>x y. x \<le> y \<Longrightarrow> norm (f x :: 'a :: real_normed_vector) \<le> norm (f y)" "subseq g"
+ shows "Bseq (\<lambda>x. f (g x)) \<longleftrightarrow> Bseq f"
+proof
+ assume "Bseq (\<lambda>x. f (g x))"
+ then obtain K where K: "\<And>x. norm (f (g x)) \<le> K" unfolding Bseq_def by auto
+ {
+ fix x :: nat
+ from filterlim_subseq[OF assms(2)] obtain y where "g y \<ge> x"
+ by (auto simp: filterlim_at_top eventually_at_top_linorder)
+ hence "norm (f x) \<le> norm (f (g y))" using assms(1) by blast
+ also have "norm (f (g y)) \<le> K" by (rule K)
+ finally have "norm (f x) \<le> K" .
+ }
+ thus "Bseq f" by (rule BseqI')
+qed (insert Bseq_subseq[of f g], simp_all)
+
+lemma nonneg_incseq_Bseq_subseq_iff:
+ assumes "\<And>x. f x \<ge> 0" "incseq (f :: nat \<Rightarrow> real)" "subseq g"
+ shows "Bseq (\<lambda>x. f (g x)) \<longleftrightarrow> Bseq f"
+ using assms by (intro increasing_Bseq_subseq_iff) (auto simp: incseq_def)
+
lemma Bseq_eq_bounded: "range f \<subseteq> {a .. b::real} \<Longrightarrow> Bseq f"
apply (simp add: subset_eq)
apply (rule BseqI'[where K="max (norm a) (norm b)"])
@@ -679,6 +768,16 @@
shows "(\<And>i. i \<in> S \<Longrightarrow> continuous_on s (f i)) \<Longrightarrow> continuous_on s (\<lambda>x. \<Prod>i\<in>S. f i x)"
unfolding continuous_on_def by (auto intro: tendsto_setprod)
+lemma tendsto_of_real_iff:
+ "((\<lambda>x. of_real (f x) :: 'a :: real_normed_div_algebra) ---> of_real c) F \<longleftrightarrow> (f ---> c) F"
+ unfolding tendsto_iff by simp
+
+lemma tendsto_add_const_iff:
+ "((\<lambda>x. c + f x :: 'a :: real_normed_vector) ---> c + d) F \<longleftrightarrow> (f ---> d) F"
+ using tendsto_add[OF tendsto_const[of c], of f d]
+ tendsto_add[OF tendsto_const[of "-c"], of "\<lambda>x. c + f x" "c + d"] by auto
+
+
subsubsection \<open>Inverse and division\<close>
lemma (in bounded_bilinear) Zfun_prod_Bfun:
@@ -892,6 +991,55 @@
qed
qed force
+lemma not_tendsto_and_filterlim_at_infinity:
+ assumes "F \<noteq> bot"
+ assumes "(f ---> (c :: 'a :: real_normed_vector)) F"
+ assumes "filterlim f at_infinity F"
+ shows False
+proof -
+ from tendstoD[OF assms(2), of "1/2"]
+ have "eventually (\<lambda>x. dist (f x) c < 1/2) F" by simp
+ moreover from filterlim_at_infinity[of "norm c" f F] assms(3)
+ have "eventually (\<lambda>x. norm (f x) \<ge> norm c + 1) F" by simp
+ ultimately have "eventually (\<lambda>x. False) F"
+ proof eventually_elim
+ fix x assume A: "dist (f x) c < 1/2" and B: "norm (f x) \<ge> norm c + 1"
+ note B
+ also have "norm (f x) = dist (f x) 0" by (simp add: norm_conv_dist)
+ also have "... \<le> dist (f x) c + dist c 0" by (rule dist_triangle)
+ also note A
+ finally show False by (simp add: norm_conv_dist)
+ qed
+ with assms show False by simp
+qed
+
+lemma filterlim_at_infinity_imp_not_convergent:
+ assumes "filterlim f at_infinity sequentially"
+ shows "\<not>convergent f"
+ by (rule notI, rule not_tendsto_and_filterlim_at_infinity[OF _ _ assms])
+ (simp_all add: convergent_LIMSEQ_iff)
+
+lemma filterlim_at_infinity_imp_eventually_ne:
+ assumes "filterlim f at_infinity F"
+ shows "eventually (\<lambda>z. f z \<noteq> c) F"
+proof -
+ have "norm c + 1 > 0" by (intro add_nonneg_pos) simp_all
+ with filterlim_at_infinity[OF order.refl, of f F] assms
+ have "eventually (\<lambda>z. norm (f z) \<ge> norm c + 1) F" by blast
+ thus ?thesis by eventually_elim auto
+qed
+
+lemma tendsto_of_nat [tendsto_intros]:
+ "filterlim (of_nat :: nat \<Rightarrow> 'a :: real_normed_algebra_1) at_infinity sequentially"
+proof (subst filterlim_at_infinity[OF order.refl], intro allI impI)
+ fix r :: real assume r: "r > 0"
+ def n \<equiv> "nat \<lceil>r\<rceil>"
+ from r have n: "\<forall>m\<ge>n. of_nat m \<ge> r" unfolding n_def by linarith
+ from eventually_ge_at_top[of n] show "eventually (\<lambda>m. norm (of_nat m :: 'a) \<ge> r) sequentially"
+ by eventually_elim (insert n, simp_all)
+qed
+
+
subsection \<open>Relate @{const at}, @{const at_left} and @{const at_right}\<close>
text \<open>
@@ -1075,9 +1223,27 @@
by (auto intro: order_trans simp: filterlim_def filtermap_filtermap)
qed
+lemma tendsto_mult_filterlim_at_infinity:
+ assumes "F \<noteq> bot" "(f ---> (c :: 'a :: real_normed_field)) F" "c \<noteq> 0"
+ assumes "filterlim g at_infinity F"
+ shows "filterlim (\<lambda>x. f x * g x) at_infinity F"
+proof -
+ have "((\<lambda>x. inverse (f x) * inverse (g x)) ---> inverse c * 0) F"
+ by (intro tendsto_mult tendsto_inverse assms filterlim_compose[OF tendsto_inverse_0])
+ hence "filterlim (\<lambda>x. inverse (f x) * inverse (g x)) (at (inverse c * 0)) F"
+ unfolding filterlim_at using assms
+ by (auto intro: filterlim_at_infinity_imp_eventually_ne tendsto_imp_eventually_ne eventually_conj)
+ thus ?thesis by (subst filterlim_inverse_at_iff[symmetric]) simp_all
+qed
+
lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) ---> 0) F"
by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
+lemma mult_nat_left_at_top: "c > 0 \<Longrightarrow> filterlim (\<lambda>x. c * x :: nat) at_top sequentially"
+ by (rule filterlim_subseq) (auto simp: subseq_def)
+
+lemma mult_nat_right_at_top: "c > 0 \<Longrightarrow> filterlim (\<lambda>x. x * c :: nat) at_top sequentially"
+ by (rule filterlim_subseq) (auto simp: subseq_def)
lemma at_to_infinity:
fixes x :: "'a :: {real_normed_field,field}"
@@ -1471,6 +1637,23 @@
subsection \<open>Convergence on sequences\<close>
+lemma convergent_cong:
+ assumes "eventually (\<lambda>x. f x = g x) sequentially"
+ shows "convergent f \<longleftrightarrow> convergent g"
+ unfolding convergent_def by (subst filterlim_cong[OF refl refl assms]) (rule refl)
+
+lemma convergent_Suc_iff: "convergent (\<lambda>n. f (Suc n)) \<longleftrightarrow> convergent f"
+ by (auto simp: convergent_def LIMSEQ_Suc_iff)
+
+lemma convergent_ignore_initial_segment: "convergent (\<lambda>n. f (n + m)) = convergent f"
+proof (induction m arbitrary: f)
+ case (Suc m)
+ have "convergent (\<lambda>n. f (n + Suc m)) \<longleftrightarrow> convergent (\<lambda>n. f (Suc n + m))" by simp
+ also have "\<dots> \<longleftrightarrow> convergent (\<lambda>n. f (n + m))" by (rule convergent_Suc_iff)
+ also have "\<dots> \<longleftrightarrow> convergent f" by (rule Suc)
+ finally show ?case .
+qed simp_all
+
lemma convergent_add:
fixes X Y :: "nat \<Rightarrow> 'a::real_normed_vector"
assumes "convergent (\<lambda>n. X n)"
@@ -1505,6 +1688,71 @@
apply (drule tendsto_minus, auto)
done
+lemma convergent_diff:
+ fixes X Y :: "nat \<Rightarrow> 'a::real_normed_vector"
+ assumes "convergent (\<lambda>n. X n)"
+ assumes "convergent (\<lambda>n. Y n)"
+ shows "convergent (\<lambda>n. X n - Y n)"
+ using assms unfolding convergent_def by (fast intro: tendsto_diff)
+
+lemma convergent_norm:
+ assumes "convergent f"
+ shows "convergent (\<lambda>n. norm (f n))"
+proof -
+ from assms have "f ----> lim f" by (simp add: convergent_LIMSEQ_iff)
+ hence "(\<lambda>n. norm (f n)) ----> norm (lim f)" by (rule tendsto_norm)
+ thus ?thesis by (auto simp: convergent_def)
+qed
+
+lemma convergent_of_real:
+ "convergent f \<Longrightarrow> convergent (\<lambda>n. of_real (f n) :: 'a :: real_normed_algebra_1)"
+ unfolding convergent_def by (blast intro!: tendsto_of_real)
+
+lemma convergent_add_const_iff:
+ "convergent (\<lambda>n. c + f n :: 'a :: real_normed_vector) \<longleftrightarrow> convergent f"
+proof
+ assume "convergent (\<lambda>n. c + f n)"
+ from convergent_diff[OF this convergent_const[of c]] show "convergent f" by simp
+next
+ assume "convergent f"
+ from convergent_add[OF convergent_const[of c] this] show "convergent (\<lambda>n. c + f n)" by simp
+qed
+
+lemma convergent_add_const_right_iff:
+ "convergent (\<lambda>n. f n + c :: 'a :: real_normed_vector) \<longleftrightarrow> convergent f"
+ using convergent_add_const_iff[of c f] by (simp add: add_ac)
+
+lemma convergent_diff_const_right_iff:
+ "convergent (\<lambda>n. f n - c :: 'a :: real_normed_vector) \<longleftrightarrow> convergent f"
+ using convergent_add_const_right_iff[of f "-c"] by (simp add: add_ac)
+
+lemma convergent_mult:
+ fixes X Y :: "nat \<Rightarrow> 'a::real_normed_field"
+ assumes "convergent (\<lambda>n. X n)"
+ assumes "convergent (\<lambda>n. Y n)"
+ shows "convergent (\<lambda>n. X n * Y n)"
+ using assms unfolding convergent_def by (fast intro: tendsto_mult)
+
+lemma convergent_mult_const_iff:
+ assumes "c \<noteq> 0"
+ shows "convergent (\<lambda>n. c * f n :: 'a :: real_normed_field) \<longleftrightarrow> convergent f"
+proof
+ assume "convergent (\<lambda>n. c * f n)"
+ from assms convergent_mult[OF this convergent_const[of "inverse c"]]
+ show "convergent f" by (simp add: field_simps)
+next
+ assume "convergent f"
+ from convergent_mult[OF convergent_const[of c] this] show "convergent (\<lambda>n. c * f n)" by simp
+qed
+
+lemma convergent_mult_const_right_iff:
+ assumes "c \<noteq> 0"
+ shows "convergent (\<lambda>n. (f n :: 'a :: real_normed_field) * c) \<longleftrightarrow> convergent f"
+ using convergent_mult_const_iff[OF assms, of f] by (simp add: mult_ac)
+
+lemma convergent_imp_Bseq: "convergent f \<Longrightarrow> Bseq f"
+ by (simp add: Cauchy_Bseq convergent_Cauchy)
+
text \<open>A monotone sequence converges to its least upper bound.\<close>
@@ -1532,6 +1780,19 @@
lemma Bseq_mono_convergent: "Bseq X \<Longrightarrow> (\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n) \<Longrightarrow> convergent (X::nat\<Rightarrow>real)"
by (auto intro!: Bseq_monoseq_convergent incseq_imp_monoseq simp: incseq_def)
+lemma monoseq_imp_convergent_iff_Bseq: "monoseq (f :: nat \<Rightarrow> real) \<Longrightarrow> convergent f \<longleftrightarrow> Bseq f"
+ using Bseq_monoseq_convergent[of f] convergent_imp_Bseq[of f] by blast
+
+lemma Bseq_monoseq_convergent'_inc:
+ "Bseq (\<lambda>n. f (n + M) :: real) \<Longrightarrow> (\<And>m n. M \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> f m \<le> f n) \<Longrightarrow> convergent f"
+ by (subst convergent_ignore_initial_segment [symmetric, of _ M])
+ (auto intro!: Bseq_monoseq_convergent simp: monoseq_def)
+
+lemma Bseq_monoseq_convergent'_dec:
+ "Bseq (\<lambda>n. f (n + M) :: real) \<Longrightarrow> (\<And>m n. M \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> f m \<ge> f n) \<Longrightarrow> convergent f"
+ by (subst convergent_ignore_initial_segment [symmetric, of _ M])
+ (auto intro!: Bseq_monoseq_convergent simp: monoseq_def)
+
lemma Cauchy_iff:
fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
shows "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e)"
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Mon Nov 02 11:56:28 2015 +0100
@@ -819,6 +819,7 @@
subsection\<open>Complex differentiation of sequences and series\<close>
+(* TODO: Could probably be simplified using Uniform_Limit *)
lemma has_complex_derivative_sequence:
fixes s :: "complex set"
assumes cvs: "convex s"
@@ -899,6 +900,41 @@
qed
qed
+
+lemma complex_differentiable_series:
+ fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
+ assumes "convex s" "open s"
+ assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
+ assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
+ assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" and x: "x \<in> s"
+ shows "summable (\<lambda>n. f n x)" and "(\<lambda>x. \<Sum>n. f n x) complex_differentiable (at x)"
+proof -
+ from assms(4) obtain g' where A: "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
+ unfolding uniformly_convergent_on_def by blast
+ from x and `open s` have s: "at x within s = at x" by (rule at_within_open)
+ have "\<exists>g. \<forall>x\<in>s. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within s)"
+ by (intro has_field_derivative_series[of s f f' g' x0] assms A has_field_derivative_at_within)
+ then obtain g where g: "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
+ "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
+ from g[OF x] show "summable (\<lambda>n. f n x)" by (auto simp: summable_def)
+ from g(2)[OF x] have g': "(g has_derivative op * (g' x)) (at x)"
+ by (simp add: has_field_derivative_def s)
+ have "((\<lambda>x. \<Sum>n. f n x) has_derivative op * (g' x)) (at x)"
+ by (rule has_derivative_transform_within_open[OF `open s` x _ g'])
+ (insert g, auto simp: sums_iff)
+ thus "(\<lambda>x. \<Sum>n. f n x) complex_differentiable (at x)" unfolding differentiable_def
+ by (auto simp: summable_def complex_differentiable_def has_field_derivative_def)
+qed
+
+lemma complex_differentiable_series':
+ fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
+ assumes "convex s" "open s"
+ assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
+ assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
+ assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)"
+ shows "(\<lambda>x. \<Sum>n. f n x) complex_differentiable (at x0)"
+ using complex_differentiable_series[OF assms, of x0] `x0 \<in> s` by blast+
+
subsection\<open>Bound theorem\<close>
lemma complex_differentiable_bound:
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Nov 02 11:56:28 2015 +0100
@@ -1788,14 +1788,6 @@
subsubsection \<open>Another formulation from Lars Schewe\<close>
-lemma setsum_constant_scaleR:
- fixes y :: "'a::real_vector"
- shows "(\<Sum>x\<in>A. y) = of_nat (card A) *\<^sub>R y"
- apply (cases "finite A")
- apply (induct set: finite)
- apply (simp_all add: algebra_simps)
- done
-
lemma convex_hull_explicit:
fixes p :: "'a::real_vector set"
shows "convex hull p =
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Nov 02 11:56:28 2015 +0100
@@ -6,7 +6,7 @@
section \<open>Multivariate calculus in Euclidean space\<close>
theory Derivative
-imports Brouwer_Fixpoint Operator_Norm
+imports Brouwer_Fixpoint Operator_Norm "~~/src/HOL/Multivariate_Analysis/Uniform_Limit"
begin
lemma netlimit_at_vector: (* TODO: move *)
@@ -2202,6 +2202,92 @@
apply auto
done
+lemma has_field_derivative_series:
+ fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
+ assumes "convex s"
+ assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x within s)"
+ assumes "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
+ assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)"
+ shows "\<exists>g. \<forall>x\<in>s. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within s)"
+unfolding has_field_derivative_def
+proof (rule has_derivative_series)
+ show "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h"
+ proof (intro allI impI)
+ fix e :: real assume "e > 0"
+ with assms(3) obtain N where N: "\<And>n x. n \<ge> N \<Longrightarrow> x \<in> s \<Longrightarrow> norm ((\<Sum>i<n. f' i x) - g' x) < e"
+ unfolding uniform_limit_iff eventually_at_top_linorder dist_norm by blast
+ {
+ fix n :: nat and x h :: 'a assume nx: "n \<ge> N" "x \<in> s"
+ have "norm ((\<Sum>i<n. f' i x * h) - g' x * h) = norm ((\<Sum>i<n. f' i x) - g' x) * norm h"
+ by (simp add: norm_mult [symmetric] ring_distribs setsum_left_distrib)
+ also from N[OF nx] have "norm ((\<Sum>i<n. f' i x) - g' x) \<le> e" by simp
+ hence "norm ((\<Sum>i<n. f' i x) - g' x) * norm h \<le> e * norm h"
+ by (intro mult_right_mono) simp_all
+ finally have "norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h" .
+ }
+ thus "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h" by blast
+ qed
+qed (insert assms, auto simp: has_field_derivative_def)
+
+lemma has_field_derivative_series':
+ fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
+ assumes "convex s"
+ assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x within s)"
+ assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
+ assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" "x \<in> interior s"
+ shows "summable (\<lambda>n. f n x)" "((\<lambda>x. \<Sum>n. f n x) has_field_derivative (\<Sum>n. f' n x)) (at x)"
+proof -
+ from \<open>x \<in> interior s\<close> have "x \<in> s" using interior_subset by blast
+ def g' \<equiv> "\<lambda>x. \<Sum>i. f' i x"
+ from assms(3) have "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
+ by (simp add: uniformly_convergent_uniform_limit_iff suminf_eq_lim g'_def)
+ from has_field_derivative_series[OF assms(1,2) this assms(4,5)] obtain g where g:
+ "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
+ "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
+ from g(1)[OF \<open>x \<in> s\<close>] show "summable (\<lambda>n. f n x)" by (simp add: sums_iff)
+ from g(2)[OF \<open>x \<in> s\<close>] \<open>x \<in> interior s\<close> have "(g has_field_derivative g' x) (at x)"
+ by (simp add: at_within_interior[of x s])
+ also have "(g has_field_derivative g' x) (at x) \<longleftrightarrow>
+ ((\<lambda>x. \<Sum>n. f n x) has_field_derivative g' x) (at x)"
+ using eventually_nhds_in_nhd[OF \<open>x \<in> interior s\<close>] interior_subset[of s] g(1)
+ by (intro DERIV_cong_ev) (auto elim!: eventually_elim1 simp: sums_iff)
+ finally show "((\<lambda>x. \<Sum>n. f n x) has_field_derivative g' x) (at x)" .
+qed
+
+lemma differentiable_series:
+ fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
+ assumes "convex s" "open s"
+ assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
+ assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
+ assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" and x: "x \<in> s"
+ shows "summable (\<lambda>n. f n x)" and "(\<lambda>x. \<Sum>n. f n x) differentiable (at x)"
+proof -
+ from assms(4) obtain g' where A: "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
+ unfolding uniformly_convergent_on_def by blast
+ from x and `open s` have s: "at x within s = at x" by (rule at_within_open)
+ have "\<exists>g. \<forall>x\<in>s. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within s)"
+ by (intro has_field_derivative_series[of s f f' g' x0] assms A has_field_derivative_at_within)
+ then obtain g where g: "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
+ "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
+ from g[OF x] show "summable (\<lambda>n. f n x)" by (auto simp: summable_def)
+ from g(2)[OF x] have g': "(g has_derivative op * (g' x)) (at x)"
+ by (simp add: has_field_derivative_def s)
+ have "((\<lambda>x. \<Sum>n. f n x) has_derivative op * (g' x)) (at x)"
+ by (rule has_derivative_transform_within_open[OF `open s` x _ g'])
+ (insert g, auto simp: sums_iff)
+ thus "(\<lambda>x. \<Sum>n. f n x) differentiable (at x)" unfolding differentiable_def
+ by (auto simp: summable_def differentiable_def has_field_derivative_def)
+qed
+
+lemma differentiable_series':
+ fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
+ assumes "convex s" "open s"
+ assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
+ assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
+ assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)"
+ shows "(\<lambda>x. \<Sum>n. f n x) differentiable (at x0)"
+ using differentiable_series[OF assms, of x0] `x0 \<in> s` by blast+
+
text \<open>Considering derivative @{typ "real \<Rightarrow> 'b::real_normed_vector"} as a vector.\<close>
definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)"
@@ -2445,4 +2531,61 @@
vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x))"
by (metis vector_diff_chain_at vector_derivative_at vector_derivative_works assms)
+
+subsection \<open>Relation between convexity and derivative\<close>
+
+(* TODO: Generalise to real vector spaces? *)
+lemma convex_on_imp_above_tangent:
+ assumes convex: "convex_on A f" and connected: "connected A"
+ assumes c: "c \<in> interior A" and x : "x \<in> A"
+ assumes deriv: "(f has_field_derivative f') (at c within A)"
+ shows "f x - f c \<ge> f' * (x - c)"
+proof (cases x c rule: linorder_cases)
+ assume xc: "x > c"
+ let ?A' = "interior A \<inter> {c<..}"
+ from c have "c \<in> interior A \<inter> closure {c<..}" by auto
+ also have "\<dots> \<subseteq> closure (interior A \<inter> {c<..})" by (intro open_inter_closure_subset) auto
+ finally have "at c within ?A' \<noteq> bot" by (subst at_within_eq_bot_iff) auto
+ moreover from deriv have "((\<lambda>y. (f y - f c) / (y - c)) ---> f') (at c within ?A')"
+ unfolding DERIV_within_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
+ moreover from eventually_at_right_real[OF xc]
+ have "eventually (\<lambda>y. (f y - f c) / (y - c) \<le> (f x - f c) / (x - c)) (at_right c)"
+ proof eventually_elim
+ fix y assume y: "y \<in> {c<..<x}"
+ with convex connected x c have "f y \<le> (f x - f c) / (x - c) * (y - c) + f c"
+ using interior_subset[of A]
+ by (intro convex_onD_Icc' convex_on_subset[OF convex] connected_contains_Icc) auto
+ hence "f y - f c \<le> (f x - f c) / (x - c) * (y - c)" by simp
+ thus "(f y - f c) / (y - c) \<le> (f x - f c) / (x - c)" using y xc by (simp add: divide_simps)
+ qed
+ hence "eventually (\<lambda>y. (f y - f c) / (y - c) \<le> (f x - f c) / (x - c)) (at c within ?A')"
+ by (blast intro: filter_leD at_le)
+ ultimately have "f' \<le> (f x - f c) / (x - c)" by (rule tendsto_ge_const)
+ thus ?thesis using xc by (simp add: field_simps)
+next
+ assume xc: "x < c"
+ let ?A' = "interior A \<inter> {..<c}"
+ from c have "c \<in> interior A \<inter> closure {..<c}" by auto
+ also have "\<dots> \<subseteq> closure (interior A \<inter> {..<c})" by (intro open_inter_closure_subset) auto
+ finally have "at c within ?A' \<noteq> bot" by (subst at_within_eq_bot_iff) auto
+ moreover from deriv have "((\<lambda>y. (f y - f c) / (y - c)) ---> f') (at c within ?A')"
+ unfolding DERIV_within_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
+ moreover from eventually_at_left_real[OF xc]
+ have "eventually (\<lambda>y. (f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)) (at_left c)"
+ proof eventually_elim
+ fix y assume y: "y \<in> {x<..<c}"
+ with convex connected x c have "f y \<le> (f x - f c) / (c - x) * (c - y) + f c"
+ using interior_subset[of A]
+ by (intro convex_onD_Icc'' convex_on_subset[OF convex] connected_contains_Icc) auto
+ hence "f y - f c \<le> (f x - f c) * ((c - y) / (c - x))" by simp
+ also have "(c - y) / (c - x) = (y - c) / (x - c)" using y xc by (simp add: field_simps)
+ finally show "(f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)" using y xc
+ by (simp add: divide_simps)
+ qed
+ hence "eventually (\<lambda>y. (f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)) (at c within ?A')"
+ by (blast intro: filter_leD at_le)
+ ultimately have "f' \<ge> (f x - f c) / (x - c)" by (rule tendsto_le_const)
+ thus ?thesis using xc by (simp add: field_simps)
+qed simp_all
+
end
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Nov 02 11:56:28 2015 +0100
@@ -896,6 +896,15 @@
unfolding dist_norm norm_eq_sqrt_inner setL2_def
by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
+lemma eventually_nhds_ball: "d > 0 \<Longrightarrow> eventually (\<lambda>x. x \<in> ball z d) (nhds z)"
+ by (rule eventually_nhds_in_open) simp_all
+
+lemma eventually_at_ball: "d > 0 \<Longrightarrow> eventually (\<lambda>t. t \<in> ball z d \<and> t \<in> A) (at z within A)"
+ unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute)
+
+lemma eventually_at_ball': "d > 0 \<Longrightarrow> eventually (\<lambda>t. t \<in> ball z d \<and> t \<noteq> z \<and> t \<in> A) (at z within A)"
+ unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute)
+
subsection \<open>Boxes\<close>
@@ -1582,6 +1591,9 @@
using open_contains_ball_eq [where S="interior S"]
by (simp add: open_subset_interior)
+lemma eventually_nhds_in_nhd: "x \<in> interior s \<Longrightarrow> eventually (\<lambda>y. y \<in> s) (nhds x)"
+ using interior_subset[of s] by (subst eventually_nhds) blast
+
lemma interior_limit_point [intro]:
fixes x :: "'a::perfect_space"
assumes x: "x \<in> interior S"
@@ -1832,6 +1844,7 @@
"closed s \<Longrightarrow> (closedin (subtopology euclidean s) t \<longleftrightarrow> closed t \<and> t \<subseteq> s)"
by (meson closed_in_limpt closed_subset closedin_closed_trans)
+
subsection\<open>Connected components, considered as a connectedness relation or a set\<close>
definition
@@ -2258,6 +2271,9 @@
using islimpt_in_closure
by (metis trivial_limit_within)
+lemma at_within_eq_bot_iff: "(at c within A = bot) \<longleftrightarrow> (c \<notin> closure (A - {c}))"
+ using not_trivial_limit_within[of c A] by blast
+
text \<open>Some property holds "sufficiently close" to the limit point.\<close>
lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
--- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Mon Nov 02 11:56:28 2015 +0100
@@ -15,6 +15,12 @@
abbreviation
"uniform_limit S f l \<equiv> filterlim f (uniformly_on S l)"
+definition uniformly_convergent_on where
+ "uniformly_convergent_on X f \<longleftrightarrow> (\<exists>l. uniform_limit X f l sequentially)"
+
+definition uniformly_Cauchy_on where
+ "uniformly_Cauchy_on X f \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>x\<in>X. \<forall>(m::nat)\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e)"
+
lemma uniform_limit_iff:
"uniform_limit S f l F \<longleftrightarrow> (\<forall>e>0. \<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (f n x) (l x) < e)"
unfolding filterlim_iff uniformly_on_def
@@ -114,9 +120,115 @@
by (rule swap_uniform_limit) fact+
qed
-lemma weierstrass_m_test:
+lemma uniformly_Cauchy_onI:
+ assumes "\<And>e. e > 0 \<Longrightarrow> \<exists>M. \<forall>x\<in>X. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e"
+ shows "uniformly_Cauchy_on X f"
+ using assms unfolding uniformly_Cauchy_on_def by blast
+
+lemma uniformly_Cauchy_onI':
+ assumes "\<And>e. e > 0 \<Longrightarrow> \<exists>M. \<forall>x\<in>X. \<forall>m\<ge>M. \<forall>n>m. dist (f m x) (f n x) < e"
+ shows "uniformly_Cauchy_on X f"
+proof (rule uniformly_Cauchy_onI)
+ fix e :: real assume e: "e > 0"
+ from assms[OF this] obtain M
+ where M: "\<And>x m n. x \<in> X \<Longrightarrow> m \<ge> M \<Longrightarrow> n > m \<Longrightarrow> dist (f m x) (f n x) < e" by fast
+ {
+ fix x m n assume x: "x \<in> X" and m: "m \<ge> M" and n: "n \<ge> M"
+ with M[OF this(1,2), of n] M[OF this(1,3), of m] e have "dist (f m x) (f n x) < e"
+ by (cases m n rule: linorder_cases) (simp_all add: dist_commute)
+ }
+ thus "\<exists>M. \<forall>x\<in>X. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e" by fast
+qed
+
+lemma uniformly_Cauchy_imp_Cauchy:
+ "uniformly_Cauchy_on X f \<Longrightarrow> x \<in> X \<Longrightarrow> Cauchy (\<lambda>n. f n x)"
+ unfolding Cauchy_def uniformly_Cauchy_on_def by fast
+
+lemma uniform_limit_cong:
+ fixes f g :: "'a \<Rightarrow> 'b \<Rightarrow> ('c :: metric_space)" and h i :: "'b \<Rightarrow> 'c"
+ assumes "eventually (\<lambda>y. \<forall>x\<in>X. f y x = g y x) F"
+ assumes "\<And>x. x \<in> X \<Longrightarrow> h x = i x"
+ shows "uniform_limit X f h F \<longleftrightarrow> uniform_limit X g i F"
+proof -
+ {
+ fix f g :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" and h i :: "'b \<Rightarrow> 'c"
+ assume C: "uniform_limit X f h F" and A: "eventually (\<lambda>y. \<forall>x\<in>X. f y x = g y x) F"
+ and B: "\<And>x. x \<in> X \<Longrightarrow> h x = i x"
+ {
+ fix e ::real assume "e > 0"
+ with C have "eventually (\<lambda>y. \<forall>x\<in>X. dist (f y x) (h x) < e) F"
+ unfolding uniform_limit_iff by blast
+ with A have "eventually (\<lambda>y. \<forall>x\<in>X. dist (g y x) (i x) < e) F"
+ by eventually_elim (insert B, simp_all)
+ }
+ hence "uniform_limit X g i F" unfolding uniform_limit_iff by blast
+ } note A = this
+ show ?thesis by (rule iffI) (erule A; insert assms; simp add: eq_commute)+
+qed
+
+lemma uniform_limit_cong':
+ fixes f g :: "'a \<Rightarrow> 'b \<Rightarrow> ('c :: metric_space)" and h i :: "'b \<Rightarrow> 'c"
+ assumes "\<And>y x. x \<in> X \<Longrightarrow> f y x = g y x"
+ assumes "\<And>x. x \<in> X \<Longrightarrow> h x = i x"
+ shows "uniform_limit X f h F \<longleftrightarrow> uniform_limit X g i F"
+ using assms by (intro uniform_limit_cong always_eventually) blast+
+
+lemma uniformly_convergent_uniform_limit_iff:
+ "uniformly_convergent_on X f \<longleftrightarrow> uniform_limit X f (\<lambda>x. lim (\<lambda>n. f n x)) sequentially"
+proof
+ assume "uniformly_convergent_on X f"
+ then obtain l where l: "uniform_limit X f l sequentially"
+ unfolding uniformly_convergent_on_def by blast
+ from l have "uniform_limit X f (\<lambda>x. lim (\<lambda>n. f n x)) sequentially \<longleftrightarrow>
+ uniform_limit X f l sequentially"
+ by (intro uniform_limit_cong' limI tendsto_uniform_limitI[of f X l]) simp_all
+ also note l
+ finally show "uniform_limit X f (\<lambda>x. lim (\<lambda>n. f n x)) sequentially" .
+qed (auto simp: uniformly_convergent_on_def)
+
+lemma uniformly_convergentI: "uniform_limit X f l sequentially \<Longrightarrow> uniformly_convergent_on X f"
+ unfolding uniformly_convergent_on_def by blast
+
+lemma Cauchy_uniformly_convergent:
+ fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b :: complete_space"
+ assumes "uniformly_Cauchy_on X f"
+ shows "uniformly_convergent_on X f"
+unfolding uniformly_convergent_uniform_limit_iff uniform_limit_iff
+proof safe
+ let ?f = "\<lambda>x. lim (\<lambda>n. f n x)"
+ fix e :: real assume e: "e > 0"
+ hence "e/2 > 0" by simp
+ with assms obtain N where N: "\<And>x m n. x \<in> X \<Longrightarrow> m \<ge> N \<Longrightarrow> n \<ge> N \<Longrightarrow> dist (f m x) (f n x) < e/2"
+ unfolding uniformly_Cauchy_on_def by fast
+ show "eventually (\<lambda>n. \<forall>x\<in>X. dist (f n x) (?f x) < e) sequentially"
+ using eventually_ge_at_top[of N]
+ proof eventually_elim
+ fix n assume n: "n \<ge> N"
+ show "\<forall>x\<in>X. dist (f n x) (?f x) < e"
+ proof
+ fix x assume x: "x \<in> X"
+ with assms have "(\<lambda>n. f n x) ----> ?f x"
+ by (auto dest!: Cauchy_convergent uniformly_Cauchy_imp_Cauchy simp: convergent_LIMSEQ_iff)
+ with `e/2 > 0` have "eventually (\<lambda>m. m \<ge> N \<and> dist (f m x) (?f x) < e/2) sequentially"
+ by (intro tendstoD eventually_conj eventually_ge_at_top)
+ then obtain m where m: "m \<ge> N" "dist (f m x) (?f x) < e/2"
+ unfolding eventually_at_top_linorder by blast
+ have "dist (f n x) (?f x) \<le> dist (f n x) (f m x) + dist (f m x) (?f x)"
+ by (rule dist_triangle)
+ also from x n have "... < e/2 + e/2" by (intro add_strict_mono N m)
+ finally show "dist (f n x) (?f x) < e" by simp
+ qed
+ qed
+qed
+
+lemma uniformly_convergent_imp_convergent:
+ "uniformly_convergent_on X f \<Longrightarrow> x \<in> X \<Longrightarrow> convergent (\<lambda>n. f n x)"
+ unfolding uniformly_convergent_on_def convergent_def
+ by (auto dest: tendsto_uniform_limitI)
+
+lemma weierstrass_m_test_ev:
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
-assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n"
+assumes "eventually (\<lambda>n. \<forall>x\<in>A. norm (f n x) \<le> M n) sequentially"
assumes "summable M"
shows "uniform_limit A (\<lambda>n x. \<Sum>i<n. f i x) (\<lambda>x. suminf (\<lambda>i. f i x)) sequentially"
proof (rule uniform_limitI)
@@ -125,14 +237,15 @@
from suminf_exist_split[OF \<open>0 < e\<close> \<open>summable M\<close>]
have "\<forall>\<^sub>F k in sequentially. norm (\<Sum>i. M (i + k)) < e"
by (auto simp: eventually_sequentially)
- thus "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>A. dist (\<Sum>i<n. f i x) (\<Sum>i. f i x) < e"
+ with eventually_all_ge_at_top[OF assms(1)]
+ show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>A. dist (\<Sum>i<n. f i x) (\<Sum>i. f i x) < e"
proof eventually_elim
case (elim k)
show ?case
proof safe
fix x assume "x \<in> A"
have "\<exists>N. \<forall>n\<ge>N. norm (f n x) \<le> M n"
- using assms(1)[OF \<open>x \<in> A\<close>] by simp
+ using assms(1) \<open>x \<in> A\<close> by (force simp: eventually_at_top_linorder)
hence summable_norm_f: "summable (\<lambda>n. norm (f n x))"
by(rule summable_norm_comparison_test[OF _ \<open>summable M\<close>])
have summable_f: "summable (\<lambda>n. f n x)"
@@ -152,13 +265,32 @@
using summable_norm[OF summable_norm_f_plus_k] .
also have "... \<le> (\<Sum>i. M (i + k))"
by (rule suminf_le[OF _ summable_norm_f_plus_k summable_M_plus_k])
- (simp add: assms(1)[OF \<open>x \<in> A\<close>])
+ (insert elim(1) \<open>x \<in> A\<close>, simp)
finally show "dist (\<Sum>i<k. f i x) (\<Sum>i. f i x) < e"
using elim by auto
qed
qed
qed
+lemma weierstrass_m_test:
+fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
+assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n"
+assumes "summable M"
+shows "uniform_limit A (\<lambda>n x. \<Sum>i<n. f i x) (\<lambda>x. suminf (\<lambda>i. f i x)) sequentially"
+ using assms by (intro weierstrass_m_test_ev always_eventually) auto
+
+lemma weierstrass_m_test'_ev:
+ fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
+ assumes "eventually (\<lambda>n. \<forall>x\<in>A. norm (f n x) \<le> M n) sequentially" "summable M"
+ shows "uniformly_convergent_on A (\<lambda>n x. \<Sum>i<n. f i x)"
+ unfolding uniformly_convergent_on_def by (rule exI, rule weierstrass_m_test_ev[OF assms])
+
+lemma weierstrass_m_test':
+ fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
+ assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n" "summable M"
+ shows "uniformly_convergent_on A (\<lambda>n x. \<Sum>i<n. f i x)"
+ unfolding uniformly_convergent_on_def by (rule exI, rule weierstrass_m_test[OF assms])
+
lemma uniform_limit_eq_rhs: "uniform_limit X f l F \<Longrightarrow> l = m \<Longrightarrow> uniform_limit X f m F"
by simp
--- a/src/HOL/Nat.thy Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Nat.thy Mon Nov 02 11:56:28 2015 +0100
@@ -1472,6 +1472,9 @@
lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
by (induct m) (simp_all add: ac_simps distrib_right)
+lemma mult_of_nat_commute: "of_nat x * y = y * of_nat x"
+ by (induction x) (simp_all add: algebra_simps)
+
primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
"of_nat_aux inc 0 i = i"
| "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- \<open>tail recursive\<close>
--- a/src/HOL/Parity.thy Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Parity.thy Mon Nov 02 11:56:28 2015 +0100
@@ -233,7 +233,7 @@
subsection \<open>Parity and powers\<close>
-context comm_ring_1
+context ring_1
begin
lemma power_minus_even [simp]:
--- a/src/HOL/Power.thy Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Power.thy Mon Nov 02 11:56:28 2015 +0100
@@ -283,6 +283,9 @@
by (simp del: power_Suc add: power_Suc2 mult.assoc)
qed
+lemma power_minus': "NO_MATCH 1 x \<Longrightarrow> (-x) ^ n = (-1)^n * x ^ n"
+ by (rule power_minus)
+
lemma power_minus_Bit0:
"(- x) ^ numeral (Num.Bit0 k) = x ^ numeral (Num.Bit0 k)"
by (induct k, simp_all only: numeral_class.numeral.simps power_add
@@ -307,7 +310,7 @@
lemma power_minus1_odd:
"(- 1) ^ Suc (2*n) = -1"
by simp
-
+
lemma power_minus_even [simp]:
"(-a) ^ (2*n) = a ^ (2*n)"
by (simp add: power_minus [of a])
--- a/src/HOL/Real_Vector_Spaces.thy Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Mon Nov 02 11:56:28 2015 +0100
@@ -228,6 +228,14 @@
apply (erule (1) nonzero_inverse_scaleR_distrib)
done
+lemma setsum_constant_scaleR:
+ fixes y :: "'a::real_vector"
+ shows "(\<Sum>x\<in>A. y) = of_nat (card A) *\<^sub>R y"
+ apply (cases "finite A")
+ apply (induct set: finite)
+ apply (simp_all add: algebra_simps)
+ done
+
lemma real_vector_affinity_eq:
fixes x :: "'a :: real_vector"
assumes m0: "m \<noteq> 0"
@@ -1614,6 +1622,12 @@
apply auto
done
+lemma eventually_at_left_real: "a > (b :: real) \<Longrightarrow> eventually (\<lambda>x. x \<in> {b<..<a}) (at_left a)"
+ by (subst eventually_at, rule exI[of _ "a - b"]) (force simp: dist_real_def)
+
+lemma eventually_at_right_real: "a < (b :: real) \<Longrightarrow> eventually (\<lambda>x. x \<in> {a<..<b}) (at_right a)"
+ by (subst eventually_at, rule exI[of _ "b - a"]) (force simp: dist_real_def)
+
lemma metric_tendsto_imp_tendsto:
fixes a :: "'a :: metric_space" and b :: "'b :: metric_space"
assumes f: "(f ---> a) F"
@@ -1709,12 +1723,36 @@
definition (in metric_space) Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
"Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
-subsection \<open>Cauchy Sequences\<close>
+lemma Cauchy_altdef:
+ "Cauchy f = (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e)"
+proof
+ assume A: "\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e"
+ show "Cauchy f" unfolding Cauchy_def
+ proof (intro allI impI)
+ fix e :: real assume e: "e > 0"
+ with A obtain M where M: "\<And>m n. m \<ge> M \<Longrightarrow> n > m \<Longrightarrow> dist (f m) (f n) < e" by blast
+ have "dist (f m) (f n) < e" if "m \<ge> M" "n \<ge> M" for m n
+ using M[of m n] M[of n m] e that by (cases m n rule: linorder_cases) (auto simp: dist_commute)
+ thus "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m) (f n) < e" by blast
+ qed
+next
+ assume "Cauchy f"
+ show "\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e"
+ proof (intro allI impI)
+ fix e :: real assume e: "e > 0"
+ with `Cauchy f` obtain M where "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> dist (f m) (f n) < e"
+ unfolding Cauchy_def by fast
+ thus "\<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e" by (intro exI[of _ M]) force
+ qed
+qed
lemma metric_CauchyI:
"(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
by (simp add: Cauchy_def)
+lemma CauchyI': "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
+ unfolding Cauchy_altdef by blast
+
lemma metric_CauchyD:
"Cauchy X \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e"
by (simp add: Cauchy_def)
--- a/src/HOL/Series.thy Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Series.thy Mon Nov 02 11:56:28 2015 +0100
@@ -35,12 +35,20 @@
lemma sums_subst[trans]: "f = g \<Longrightarrow> g sums z \<Longrightarrow> f sums z"
by simp
+lemma sums_cong: "(\<And>n. f n = g n) \<Longrightarrow> f sums c \<longleftrightarrow> g sums c"
+ by (drule ext) simp
+
lemma sums_summable: "f sums l \<Longrightarrow> summable f"
by (simp add: sums_def summable_def, blast)
lemma summable_iff_convergent: "summable f \<longleftrightarrow> convergent (\<lambda>n. \<Sum>i<n. f i)"
by (simp add: summable_def sums_def convergent_def)
+lemma summable_iff_convergent':
+ "summable f \<longleftrightarrow> convergent (\<lambda>n. setsum f {..n})"
+ by (simp_all only: summable_iff_convergent convergent_def
+ lessThan_Suc_atMost [symmetric] LIMSEQ_Suc_iff[of "\<lambda>n. setsum f {..<n}"])
+
lemma suminf_eq_lim: "suminf f = lim (\<lambda>n. \<Sum>i<n. f i)"
by (simp add: suminf_def sums_def lim_def)
@@ -62,6 +70,34 @@
apply simp
done
+lemma suminf_cong: "(\<And>n. f n = g n) \<Longrightarrow> suminf f = suminf g"
+ by (rule arg_cong[of f g], rule ext) simp
+
+lemma summable_cong:
+ assumes "eventually (\<lambda>x. f x = (g x :: 'a :: real_normed_vector)) sequentially"
+ shows "summable f = summable g"
+proof -
+ from assms obtain N where N: "\<forall>n\<ge>N. f n = g n" by (auto simp: eventually_at_top_linorder)
+ def C \<equiv> "(\<Sum>k<N. f k - g k)"
+ from eventually_ge_at_top[of N]
+ have "eventually (\<lambda>n. setsum f {..<n} = C + setsum g {..<n}) sequentially"
+ proof eventually_elim
+ fix n assume n: "n \<ge> N"
+ from n have "{..<n} = {..<N} \<union> {N..<n}" by auto
+ also have "setsum f ... = setsum f {..<N} + setsum f {N..<n}"
+ by (intro setsum.union_disjoint) auto
+ also from N have "setsum f {N..<n} = setsum g {N..<n}" by (intro setsum.cong) simp_all
+ also have "setsum f {..<N} + setsum g {N..<n} = C + (setsum g {..<N} + setsum g {N..<n})"
+ unfolding C_def by (simp add: algebra_simps setsum_subtractf)
+ also have "setsum g {..<N} + setsum g {N..<n} = setsum g ({..<N} \<union> {N..<n})"
+ by (intro setsum.union_disjoint [symmetric]) auto
+ also from n have "{..<N} \<union> {N..<n} = {..<n}" by auto
+ finally show "setsum f {..<n} = C + setsum g {..<n}" .
+ qed
+ from convergent_cong[OF this] show ?thesis
+ by (simp add: summable_iff_convergent convergent_add_const_iff)
+qed
+
lemma sums_finite:
assumes [simp]: "finite N" and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
shows "f sums (\<Sum>n\<in>N. f n)"
@@ -125,6 +161,10 @@
lemma sums_iff: "f sums x \<longleftrightarrow> summable f \<and> (suminf f = x)"
by (metis summable_sums sums_summable sums_unique)
+lemma summable_sums_iff:
+ "summable (f :: nat \<Rightarrow> 'a :: {comm_monoid_add,t2_space}) \<longleftrightarrow> f sums suminf f"
+ by (auto simp: sums_iff summable_sums)
+
lemma sums_unique2:
fixes a b :: "'a::{comm_monoid_add,t2_space}"
shows "f sums a \<Longrightarrow> f sums b \<Longrightarrow> a = b"
@@ -221,6 +261,7 @@
by (auto intro: le_less_trans simp: eventually_sequentially) }
qed
+
subsection \<open>Infinite summability on real normed vector spaces\<close>
lemma sums_Suc_iff:
@@ -241,6 +282,14 @@
finally show ?thesis ..
qed
+lemma summable_Suc_iff: "summable (\<lambda>n. f (Suc n) :: 'a :: real_normed_vector) = summable f"
+proof
+ assume "summable f"
+ hence "f sums suminf f" by (rule summable_sums)
+ hence "(\<lambda>n. f (Suc n)) sums (suminf f - f 0)" by (simp add: sums_Suc_iff)
+ thus "summable (\<lambda>n. f (Suc n))" unfolding summable_def by blast
+qed (auto simp: sums_Suc_iff summable_def)
+
context
fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
begin
@@ -299,6 +348,9 @@
lemma suminf_split_initial_segment: "summable f \<Longrightarrow> suminf f = (\<Sum>n. f(n + k)) + (\<Sum>i<k. f i)"
by (auto simp add: suminf_minus_initial_segment)
+lemma suminf_split_head: "summable f \<Longrightarrow> (\<Sum>n. f (Suc n)) = suminf f - f 0"
+ using suminf_split_initial_segment[of 1] by simp
+
lemma suminf_exist_split:
fixes r :: real assumes "0 < r" and "summable f"
shows "\<exists>N. \<forall>n\<ge>N. norm (\<Sum>i. f (i + n)) < r"
@@ -319,6 +371,14 @@
apply (drule_tac x="n" in spec, simp)
done
+lemma summable_imp_convergent:
+ "summable (f :: nat \<Rightarrow> 'a) \<Longrightarrow> convergent f"
+ by (force dest!: summable_LIMSEQ_zero simp: convergent_def)
+
+lemma summable_imp_Bseq:
+ "summable f \<Longrightarrow> Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)"
+ by (simp add: convergent_imp_Bseq summable_imp_convergent)
+
end
lemma summable_minus_iff:
@@ -363,6 +423,23 @@
lemmas summable_scaleR_right = bounded_linear.summable[OF bounded_linear_scaleR_right]
lemmas suminf_scaleR_right = bounded_linear.suminf[OF bounded_linear_scaleR_right]
+lemma summable_const_iff: "summable (\<lambda>_. c) \<longleftrightarrow> (c :: 'a :: real_normed_vector) = 0"
+proof -
+ {
+ assume "c \<noteq> 0"
+ hence "filterlim (\<lambda>n. of_nat n * norm c) at_top sequentially"
+ unfolding real_of_nat_def[symmetric]
+ by (subst mult.commute)
+ (auto intro!: filterlim_tendsto_pos_mult_at_top filterlim_real_sequentially)
+ hence "\<not>convergent (\<lambda>n. norm (\<Sum>k<n. c))"
+ by (intro filterlim_at_infinity_imp_not_convergent filterlim_at_top_imp_at_infinity)
+ (simp_all add: setsum_constant_scaleR)
+ hence "\<not>summable (\<lambda>_. c)" unfolding summable_iff_convergent using convergent_norm by blast
+ }
+ thus ?thesis by auto
+qed
+
+
subsection \<open>Infinite summability on real normed algebras\<close>
context
@@ -389,6 +466,22 @@
end
+lemma sums_mult_iff:
+ assumes "c \<noteq> 0"
+ shows "(\<lambda>n. c * f n :: 'a :: {real_normed_algebra,field}) sums (c * d) \<longleftrightarrow> f sums d"
+ using sums_mult[of f d c] sums_mult[of "\<lambda>n. c * f n" "c * d" "inverse c"]
+ by (force simp: field_simps assms)
+
+lemma sums_mult2_iff:
+ assumes "c \<noteq> (0 :: 'a :: {real_normed_algebra, field})"
+ shows "(\<lambda>n. f n * c) sums (d * c) \<longleftrightarrow> f sums d"
+ using sums_mult_iff[OF assms, of f d] by (simp add: mult.commute)
+
+lemma sums_of_real_iff:
+ "(\<lambda>n. of_real (f n) :: 'a :: real_normed_div_algebra) sums of_real c \<longleftrightarrow> f sums c"
+ by (simp add: sums_def of_real_setsum[symmetric] tendsto_of_real_iff del: of_real_setsum)
+
+
subsection \<open>Infinite summability on real normed fields\<close>
context
@@ -427,6 +520,16 @@
lemma suminf_geometric: "norm c < 1 \<Longrightarrow> suminf (\<lambda>n. c^n) = 1 / (1 - c)"
by (rule sums_unique[symmetric]) (rule geometric_sums)
+lemma summable_geometric_iff: "summable (\<lambda>n. c ^ n) \<longleftrightarrow> norm c < 1"
+proof
+ assume "summable (\<lambda>n. c ^ n :: 'a :: real_normed_field)"
+ hence "(\<lambda>n. norm c ^ n) ----> 0"
+ by (simp add: norm_power [symmetric] tendsto_norm_zero_iff summable_LIMSEQ_zero)
+ from order_tendstoD(2)[OF this zero_less_one] obtain n where "norm c ^ n < 1"
+ by (auto simp: eventually_at_top_linorder)
+ thus "norm c < 1" using one_le_power[of "norm c" n] by (cases "norm c \<ge> 1") (linarith, simp)
+qed (rule summable_geometric)
+
end
lemma power_half_series: "(\<lambda>n. (1/2::real)^Suc n) sums 1"
@@ -439,6 +542,36 @@
by simp
qed
+
+subsection \<open>Telescoping\<close>
+
+lemma telescope_sums:
+ assumes "f ----> (c :: 'a :: real_normed_vector)"
+ shows "(\<lambda>n. f (Suc n) - f n) sums (c - f 0)"
+ unfolding sums_def
+proof (subst LIMSEQ_Suc_iff [symmetric])
+ have "(\<lambda>n. \<Sum>k<Suc n. f (Suc k) - f k) = (\<lambda>n. f (Suc n) - f 0)"
+ by (simp add: lessThan_Suc_atMost atLeast0AtMost [symmetric] setsum_Suc_diff)
+ also have "\<dots> ----> c - f 0" by (intro tendsto_diff LIMSEQ_Suc[OF assms] tendsto_const)
+ finally show "(\<lambda>n. \<Sum>n<Suc n. f (Suc n) - f n) ----> c - f 0" .
+qed
+
+lemma telescope_sums':
+ assumes "f ----> (c :: 'a :: real_normed_vector)"
+ shows "(\<lambda>n. f n - f (Suc n)) sums (f 0 - c)"
+ using sums_minus[OF telescope_sums[OF assms]] by (simp add: algebra_simps)
+
+lemma telescope_summable:
+ assumes "f ----> (c :: 'a :: real_normed_vector)"
+ shows "summable (\<lambda>n. f (Suc n) - f n)"
+ using telescope_sums[OF assms] by (simp add: sums_iff)
+
+lemma telescope_summable':
+ assumes "f ----> (c :: 'a :: real_normed_vector)"
+ shows "summable (\<lambda>n. f n - f (Suc n))"
+ using summable_minus[OF telescope_summable[OF assms]] by (simp add: algebra_simps)
+
+
subsection \<open>Infinite summability on Banach spaces\<close>
text\<open>Cauchy-type criterion for convergence of series (c.f. Harrison)\<close>
@@ -463,7 +596,7 @@
context
fixes f :: "nat \<Rightarrow> 'a::banach"
-begin
+begin
text\<open>Absolute convergence imples normal convergence\<close>
@@ -495,6 +628,10 @@
apply (auto intro: setsum_mono simp add: abs_less_iff)
done
+lemma summable_comparison_test_ev:
+ shows "eventually (\<lambda>n. norm (f n) \<le> g n) sequentially \<Longrightarrow> summable g \<Longrightarrow> summable f"
+ by (rule summable_comparison_test) (auto simp: eventually_at_top_linorder)
+
(*A better argument order*)
lemma summable_comparison_test': "summable g \<Longrightarrow> (\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> g n) \<Longrightarrow> summable f"
by (rule summable_comparison_test) auto
@@ -669,6 +806,21 @@
lemma summable_rabs: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> \<bar>suminf f\<bar> \<le> (\<Sum>n. \<bar>f n\<bar>)"
by (fold real_norm_def) (rule summable_norm)
+lemma summable_zero_power [simp]: "summable (\<lambda>n. 0 ^ n :: 'a :: {comm_ring_1,topological_space})"
+proof -
+ have "(\<lambda>n. 0 ^ n :: 'a) = (\<lambda>n. if n = 0 then 0^0 else 0)" by (intro ext) (simp add: zero_power)
+ moreover have "summable \<dots>" by simp
+ ultimately show ?thesis by simp
+qed
+
+lemma summable_zero_power' [simp]: "summable (\<lambda>n. f n * 0 ^ n :: 'a :: {ring_1,topological_space})"
+proof -
+ have "(\<lambda>n. f n * 0 ^ n :: 'a) = (\<lambda>n. if n = 0 then f 0 * 0^0 else 0)"
+ by (intro ext) (simp add: zero_power)
+ moreover have "summable \<dots>" by simp
+ ultimately show ?thesis by simp
+qed
+
lemma summable_power_series:
fixes z :: real
assumes le_1: "\<And>i. f i \<le> 1" and nonneg: "\<And>i. 0 \<le> f i" and z: "0 \<le> z" "z < 1"
@@ -679,6 +831,79 @@
using z by (auto intro!: exI[of _ 0] mult_left_le_one_le simp: abs_mult nonneg power_abs less_imp_le le_1)
qed
+lemma summable_0_powser:
+ "summable (\<lambda>n. f n * 0 ^ n :: 'a :: real_normed_div_algebra)"
+proof -
+ have A: "(\<lambda>n. f n * 0 ^ n) = (\<lambda>n. if n = 0 then f n else 0)"
+ by (intro ext) auto
+ thus ?thesis by (subst A) simp_all
+qed
+
+lemma summable_powser_split_head:
+ "summable (\<lambda>n. f (Suc n) * z ^ n :: 'a :: real_normed_div_algebra) = summable (\<lambda>n. f n * z ^ n)"
+proof -
+ have "summable (\<lambda>n. f (Suc n) * z ^ n) \<longleftrightarrow> summable (\<lambda>n. f (Suc n) * z ^ Suc n)"
+ proof
+ assume "summable (\<lambda>n. f (Suc n) * z ^ n)"
+ from summable_mult2[OF this, of z] show "summable (\<lambda>n. f (Suc n) * z ^ Suc n)"
+ by (simp add: power_commutes algebra_simps)
+ next
+ assume "summable (\<lambda>n. f (Suc n) * z ^ Suc n)"
+ from summable_mult2[OF this, of "inverse z"] show "summable (\<lambda>n. f (Suc n) * z ^ n)"
+ by (cases "z \<noteq> 0", subst (asm) power_Suc2) (simp_all add: algebra_simps)
+ qed
+ also have "\<dots> \<longleftrightarrow> summable (\<lambda>n. f n * z ^ n)" by (rule summable_Suc_iff)
+ finally show ?thesis .
+qed
+
+lemma powser_split_head:
+ assumes "summable (\<lambda>n. f n * z ^ n :: 'a :: {real_normed_div_algebra,banach})"
+ shows "suminf (\<lambda>n. f n * z ^ n) = f 0 + suminf (\<lambda>n. f (Suc n) * z ^ n) * z"
+ "suminf (\<lambda>n. f (Suc n) * z ^ n) * z = suminf (\<lambda>n. f n * z ^ n) - f 0"
+ "summable (\<lambda>n. f (Suc n) * z ^ n)"
+proof -
+ from assms show "summable (\<lambda>n. f (Suc n) * z ^ n)" by (subst summable_powser_split_head)
+
+ from suminf_mult2[OF this, of z]
+ have "(\<Sum>n. f (Suc n) * z ^ n) * z = (\<Sum>n. f (Suc n) * z ^ Suc n)"
+ by (simp add: power_commutes algebra_simps)
+ also from assms have "\<dots> = suminf (\<lambda>n. f n * z ^ n) - f 0"
+ by (subst suminf_split_head) simp_all
+ finally show "suminf (\<lambda>n. f n * z ^ n) = f 0 + suminf (\<lambda>n. f (Suc n) * z ^ n) * z" by simp
+ thus "suminf (\<lambda>n. f (Suc n) * z ^ n) * z = suminf (\<lambda>n. f n * z ^ n) - f 0" by simp
+qed
+
+lemma summable_partial_sum_bound:
+ fixes f :: "nat \<Rightarrow> 'a :: banach"
+ assumes summable: "summable f" and e: "e > (0::real)"
+ obtains N where "\<And>m n. m \<ge> N \<Longrightarrow> norm (\<Sum>k=m..n. f k) < e"
+proof -
+ from summable have "Cauchy (\<lambda>n. \<Sum>k<n. f k)"
+ by (simp add: Cauchy_convergent_iff summable_iff_convergent)
+ from CauchyD[OF this e] obtain N
+ where N: "\<And>m n. m \<ge> N \<Longrightarrow> n \<ge> N \<Longrightarrow> norm ((\<Sum>k<m. f k) - (\<Sum>k<n. f k)) < e" by blast
+ {
+ fix m n :: nat assume m: "m \<ge> N"
+ have "norm (\<Sum>k=m..n. f k) < e"
+ proof (cases "n \<ge> m")
+ assume n: "n \<ge> m"
+ with m have "norm ((\<Sum>k<Suc n. f k) - (\<Sum>k<m. f k)) < e" by (intro N) simp_all
+ also from n have "(\<Sum>k<Suc n. f k) - (\<Sum>k<m. f k) = (\<Sum>k=m..n. f k)"
+ by (subst setsum_diff [symmetric]) (simp_all add: setsum_last_plus)
+ finally show ?thesis .
+ qed (insert e, simp_all)
+ }
+ thus ?thesis by (rule that)
+qed
+
+lemma powser_sums_if:
+ "(\<lambda>n. (if n = m then (1 :: 'a :: {ring_1,topological_space}) else 0) * z^n) sums z^m"
+proof -
+ have "(\<lambda>n. (if n = m then 1 else 0) * z^n) = (\<lambda>n. if n = m then z^n else 0)"
+ by (intro ext) auto
+ thus ?thesis by (simp add: sums_single)
+qed
+
lemma
fixes f :: "nat \<Rightarrow> real"
assumes "summable f"
@@ -742,4 +967,82 @@
with le show "suminf (f \<circ> g) = suminf f" by(rule antisym)
qed
+lemma sums_mono_reindex:
+ assumes subseq: "subseq g" and zero: "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
+ shows "(\<lambda>n. f (g n)) sums c \<longleftrightarrow> f sums c"
+unfolding sums_def
+proof
+ assume lim: "(\<lambda>n. \<Sum>k<n. f k) ----> c"
+ have "(\<lambda>n. \<Sum>k<n. f (g k)) = (\<lambda>n. \<Sum>k<g n. f k)"
+ proof
+ fix n :: nat
+ from subseq have "(\<Sum>k<n. f (g k)) = (\<Sum>k\<in>g`{..<n}. f k)"
+ by (subst setsum.reindex) (auto intro: subseq_imp_inj_on)
+ also from subseq have "\<dots> = (\<Sum>k<g n. f k)"
+ by (intro setsum.mono_neutral_left ballI zero)
+ (auto dest: subseq_strict_mono simp: strict_mono_less strict_mono_less_eq)
+ finally show "(\<Sum>k<n. f (g k)) = (\<Sum>k<g n. f k)" .
+ qed
+ also from LIMSEQ_subseq_LIMSEQ[OF lim subseq] have "\<dots> ----> c" unfolding o_def .
+ finally show "(\<lambda>n. \<Sum>k<n. f (g k)) ----> c" .
+next
+ assume lim: "(\<lambda>n. \<Sum>k<n. f (g k)) ----> c"
+ def g_inv \<equiv> "\<lambda>n. LEAST m. g m \<ge> n"
+ from filterlim_subseq[OF subseq] have g_inv_ex: "\<exists>m. g m \<ge> n" for n
+ by (auto simp: filterlim_at_top eventually_at_top_linorder)
+ hence g_inv: "g (g_inv n) \<ge> n" for n unfolding g_inv_def by (rule LeastI_ex)
+ have g_inv_least: "m \<ge> g_inv n" if "g m \<ge> n" for m n using that
+ unfolding g_inv_def by (rule Least_le)
+ have g_inv_least': "g m < n" if "m < g_inv n" for m n using that g_inv_least[of n m] by linarith
+ have "(\<lambda>n. \<Sum>k<n. f k) = (\<lambda>n. \<Sum>k<g_inv n. f (g k))"
+ proof
+ fix n :: nat
+ {
+ fix k assume k: "k \<in> {..<n} - g`{..<g_inv n}"
+ have "k \<notin> range g"
+ proof (rule notI, elim imageE)
+ fix l assume l: "k = g l"
+ have "g l < g (g_inv n)" by (rule less_le_trans[OF _ g_inv]) (insert k l, simp_all)
+ with subseq have "l < g_inv n" by (simp add: subseq_strict_mono strict_mono_less)
+ with k l show False by simp
+ qed
+ hence "f k = 0" by (rule zero)
+ }
+ with g_inv_least' g_inv have "(\<Sum>k<n. f k) = (\<Sum>k\<in>g`{..<g_inv n}. f k)"
+ by (intro setsum.mono_neutral_right) auto
+ also from subseq have "\<dots> = (\<Sum>k<g_inv n. f (g k))" using subseq_imp_inj_on
+ by (subst setsum.reindex) simp_all
+ finally show "(\<Sum>k<n. f k) = (\<Sum>k<g_inv n. f (g k))" .
+ qed
+ also {
+ fix K n :: nat assume "g K \<le> n"
+ also have "n \<le> g (g_inv n)" by (rule g_inv)
+ finally have "K \<le> g_inv n" using subseq by (simp add: strict_mono_less_eq subseq_strict_mono)
+ }
+ hence "filterlim g_inv at_top sequentially"
+ by (auto simp: filterlim_at_top eventually_at_top_linorder)
+ from lim and this have "(\<lambda>n. \<Sum>k<g_inv n. f (g k)) ----> c" by (rule filterlim_compose)
+ finally show "(\<lambda>n. \<Sum>k<n. f k) ----> c" .
+qed
+
+lemma summable_mono_reindex:
+ assumes subseq: "subseq g" and zero: "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
+ shows "summable (\<lambda>n. f (g n)) \<longleftrightarrow> summable f"
+ using sums_mono_reindex[of g f, OF assms] by (simp add: summable_def)
+
+lemma suminf_mono_reindex:
+ assumes "subseq g" "\<And>n. n \<notin> range g \<Longrightarrow> f n = (0 :: 'a :: {t2_space,comm_monoid_add})"
+ shows "suminf (\<lambda>n. f (g n)) = suminf f"
+proof (cases "summable f")
+ case False
+ hence "\<not>(\<exists>c. f sums c)" unfolding summable_def by blast
+ hence "suminf f = The (\<lambda>_. False)" by (simp add: suminf_def)
+ moreover from False have "\<not>summable (\<lambda>n. f (g n))"
+ using summable_mono_reindex[of g f, OF assms] by simp
+ hence "\<not>(\<exists>c. (\<lambda>n. f (g n)) sums c)" unfolding summable_def by blast
+ hence "suminf (\<lambda>n. f (g n)) = The (\<lambda>_. False)" by (simp add: suminf_def)
+ ultimately show ?thesis by simp
+qed (insert sums_mono_reindex[of g f, OF assms] summable_mono_reindex[of g f, OF assms],
+ simp_all add: sums_iff)
+
end
--- a/src/HOL/Topological_Spaces.thy Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Topological_Spaces.thy Mon Nov 02 11:56:28 2015 +0100
@@ -353,6 +353,10 @@
"eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
unfolding nhds_def by (subst eventually_INF_base) (auto simp: eventually_principal)
+lemma (in topological_space) eventually_nhds_in_open:
+ "open s \<Longrightarrow> x \<in> s \<Longrightarrow> eventually (\<lambda>y. y \<in> s) (nhds x)"
+ by (subst eventually_nhds) blast
+
lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
unfolding trivial_limit_def eventually_nhds by simp
@@ -497,6 +501,12 @@
"(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
unfolding nhds_def filterlim_INF filterlim_principal by auto
+lemma tendsto_cong:
+ assumes "eventually (\<lambda>x. f x = g x) F"
+ shows "(f ---> c) F \<longleftrightarrow> (g ---> c) F"
+ by (rule filterlim_cong[OF refl refl assms])
+
+
lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f ---> l) F' \<Longrightarrow> (f ---> l) F"
unfolding tendsto_def le_filter_def by fast
@@ -625,6 +635,28 @@
using order_tendstoD[OF lim(2), of a] ev by (auto elim: eventually_elim2)
qed
+lemma limit_frequently_eq:
+ assumes "F \<noteq> bot"
+ assumes "frequently (\<lambda>x. f x = c) F"
+ assumes "(f ---> d) F"
+ shows "d = (c :: 'a :: t1_space)"
+proof (rule ccontr)
+ assume "d \<noteq> c"
+ from t1_space[OF this] obtain U where "open U" "d \<in> U" "c \<notin> U" by blast
+ from this assms have "eventually (\<lambda>x. f x \<in> U) F" unfolding tendsto_def by blast
+ hence "eventually (\<lambda>x. f x \<noteq> c) F" by eventually_elim (insert `c \<notin> U`, blast)
+ with assms(2) show False unfolding frequently_def by contradiction
+qed
+
+lemma tendsto_imp_eventually_ne:
+ assumes "F \<noteq> bot" "(f ---> c) F" "c \<noteq> (c' :: 'a :: t1_space)"
+ shows "eventually (\<lambda>z. f z \<noteq> c') F"
+proof (rule ccontr)
+ assume "\<not>eventually (\<lambda>z. f z \<noteq> c') F"
+ hence "frequently (\<lambda>z. f z = c') F" by (simp add: frequently_def)
+ from limit_frequently_eq[OF assms(1) this assms(2)] and assms(3) show False by contradiction
+qed
+
lemma tendsto_le:
fixes f g :: "'a \<Rightarrow> 'b::linorder_topology"
assumes F: "\<not> trivial_limit F"
@@ -657,6 +689,9 @@
shows "a \<ge> x"
by (rule tendsto_le [OF F tendsto_const x a])
+
+
+
subsubsection \<open>Rules about @{const Lim}\<close>
lemma tendsto_Lim:
@@ -924,6 +959,17 @@
lemma subseq_mono: assumes "subseq r" "m < n" shows "r m < r n"
using assms by (auto simp: subseq_def)
+lemma subseq_imp_inj_on: "subseq g \<Longrightarrow> inj_on g A"
+proof (rule inj_onI)
+ assume g: "subseq g"
+ fix x y assume "g x = g y"
+ with subseq_mono[OF g, of x y] subseq_mono[OF g, of y x] show "x = y"
+ by (cases x y rule: linorder_cases) simp_all
+qed
+
+lemma subseq_strict_mono: "subseq g \<Longrightarrow> strict_mono g"
+ by (intro strict_monoI subseq_mono[of g])
+
lemma incseq_imp_monoseq: "incseq X \<Longrightarrow> monoseq X"
by (simp add: incseq_def monoseq_def)
@@ -2142,6 +2188,15 @@
assumes A: "connected A" "a \<in> A" "b \<in> A" shows "{a <..< b} \<subseteq> A"
using connectedD_interval[OF A] by (simp add: subset_eq Ball_def less_imp_le)
+lemma connected_contains_Icc:
+ assumes "connected (A :: ('a :: {linorder_topology}) set)" "a \<in> A" "b \<in> A"
+ shows "{a..b} \<subseteq> A"
+proof
+ fix x assume "x \<in> {a..b}"
+ hence "x = a \<or> x = b \<or> x \<in> {a<..<b}" by auto
+ thus "x \<in> A" using assms connected_contains_Ioo[of A a b] by auto
+qed
+
subsection \<open>Intermediate Value Theorem\<close>
lemma IVT':
--- a/src/HOL/Transcendental.thy Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Transcendental.thy Mon Nov 02 11:56:28 2015 +0100
@@ -16,6 +16,11 @@
using floor_correct [of "x/y"] assms
by (auto simp: Real.real_of_nat_Suc field_simps intro: that [of "nat (floor (x/y))"])
+lemma fact_in_Reals: "fact n \<in> \<real>" by (induction n) auto
+
+lemma pochhammer_of_real: "pochhammer (of_real x) n = of_real (pochhammer x n)"
+ by (simp add: pochhammer_def)
+
lemma of_real_fact [simp]: "of_real (fact n) = fact n"
by (metis of_nat_fact of_real_of_nat_eq)
@@ -1081,6 +1086,15 @@
qed
+lemma isCont_pochhammer [continuous_intros]: "isCont (\<lambda>z::'a::real_normed_field. pochhammer z n) z"
+ by (induction n) (auto intro!: continuous_intros simp: pochhammer_rec')
+
+lemma continuous_on_pochhammer [continuous_intros]:
+ fixes A :: "'a :: real_normed_field set"
+ shows "continuous_on A (\<lambda>z. pochhammer z n)"
+ by (intro continuous_at_imp_continuous_on ballI isCont_pochhammer)
+
+
subsection \<open>Exponential Function\<close>
definition exp :: "'a \<Rightarrow> 'a::{real_normed_algebra_1,banach}"
@@ -4227,6 +4241,93 @@
lemma tan_cot: "tan(pi/2 - x) = inverse(tan x)"
by (simp add: tan_def sin_diff cos_diff)
+subsection \<open>Cotangent\<close>
+
+definition cot :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
+ where "cot = (\<lambda>x. cos x / sin x)"
+
+lemma cot_of_real:
+ "of_real (cot x) = (cot (of_real x) :: 'a::{real_normed_field,banach})"
+ by (simp add: cot_def sin_of_real cos_of_real)
+
+lemma cot_in_Reals [simp]:
+ fixes z :: "'a::{real_normed_field,banach}"
+ shows "z \<in> \<real> \<Longrightarrow> cot z \<in> \<real>"
+ by (simp add: cot_def)
+
+lemma cot_zero [simp]: "cot 0 = 0"
+ by (simp add: cot_def)
+
+lemma cot_pi [simp]: "cot pi = 0"
+ by (simp add: cot_def)
+
+lemma cot_npi [simp]: "cot (real (n::nat) * pi) = 0"
+ by (simp add: cot_def)
+
+lemma cot_minus [simp]: "cot (-x) = - cot x"
+ by (simp add: cot_def)
+
+lemma cot_periodic [simp]: "cot (x + 2*pi) = cot x"
+ by (simp add: cot_def)
+
+lemma cot_altdef: "cot x = inverse (tan x)"
+ by (simp add: cot_def tan_def)
+
+lemma tan_altdef: "tan x = inverse (cot x)"
+ by (simp add: cot_def tan_def)
+
+lemma tan_cot': "tan(pi/2 - x) = cot x"
+ by (simp add: tan_cot cot_altdef)
+
+lemma cot_gt_zero: "\<lbrakk>0 < x; x < pi/2\<rbrakk> \<Longrightarrow> 0 < cot x"
+ by (simp add: cot_def zero_less_divide_iff sin_gt_zero2 cos_gt_zero_pi)
+
+lemma cot_less_zero:
+ assumes lb: "- pi/2 < x" and "x < 0"
+ shows "cot x < 0"
+proof -
+ have "0 < cot (- x)" using assms by (simp only: cot_gt_zero)
+ thus ?thesis by simp
+qed
+
+lemma DERIV_cot [simp]:
+ fixes x :: "'a::{real_normed_field,banach}"
+ shows "sin x \<noteq> 0 \<Longrightarrow> DERIV cot x :> -inverse ((sin x)\<^sup>2)"
+ unfolding cot_def using cos_squared_eq[of x]
+ by (auto intro!: derivative_eq_intros, simp add: divide_inverse power2_eq_square)
+
+lemma isCont_cot:
+ fixes x :: "'a::{real_normed_field,banach}"
+ shows "sin x \<noteq> 0 \<Longrightarrow> isCont cot x"
+ by (rule DERIV_cot [THEN DERIV_isCont])
+
+lemma isCont_cot' [simp,continuous_intros]:
+ fixes a :: "'a::{real_normed_field,banach}" and f :: "'a \<Rightarrow> 'a"
+ shows "\<lbrakk>isCont f a; sin (f a) \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. cot (f x)) a"
+ by (rule isCont_o2 [OF _ isCont_cot])
+
+lemma tendsto_cot [tendsto_intros]:
+ fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
+ shows "\<lbrakk>(f ---> a) F; sin a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. cot (f x)) ---> cot a) F"
+ by (rule isCont_tendsto_compose [OF isCont_cot])
+
+lemma continuous_cot:
+ fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
+ shows "continuous F f \<Longrightarrow> sin (f (Lim F (\<lambda>x. x))) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. cot (f x))"
+ unfolding continuous_def by (rule tendsto_cot)
+
+lemma continuous_on_cot [continuous_intros]:
+ fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
+ shows "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. sin (f x) \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. cot (f x))"
+ unfolding continuous_on_def by (auto intro: tendsto_cot)
+
+lemma continuous_within_cot [continuous_intros]:
+ fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
+ shows
+ "continuous (at x within s) f \<Longrightarrow> sin (f x) \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. cot (f x))"
+ unfolding continuous_within by (rule tendsto_cot)
+
+
subsection \<open>Inverse Trigonometric Functions\<close>
definition arcsin :: "real => real"