--- a/src/HOL/Analysis/Ball_Volume.thy Sat Feb 24 17:21:35 2018 +0100
+++ b/src/HOL/Analysis/Ball_Volume.thy Sun Feb 25 12:54:55 2018 +0000
@@ -17,8 +17,11 @@
definition unit_ball_vol :: "real \<Rightarrow> real" where
"unit_ball_vol n = pi powr (n / 2) / Gamma (n / 2 + 1)"
+lemma unit_ball_vol_pos [simp]: "n \<ge> 0 \<Longrightarrow> unit_ball_vol n > 0"
+ by (force simp: unit_ball_vol_def intro: divide_nonneg_pos)
+
lemma unit_ball_vol_nonneg [simp]: "n \<ge> 0 \<Longrightarrow> unit_ball_vol n \<ge> 0"
- by (auto simp add: unit_ball_vol_def intro!: divide_nonneg_pos Gamma_real_pos)
+ by (simp add: dual_order.strict_implies_order)
text \<open>
We first need the value of the following integral, which is at the core of
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Sat Feb 24 17:21:35 2018 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Sun Feb 25 12:54:55 2018 +0000
@@ -7,19 +7,6 @@
lemma subspace_special_hyperplane: "subspace {x. x $ k = 0}"
by (simp add: subspace_def)
-lemma delta_mult_idempotent:
- "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)"
- by simp
-
-(*move up?*)
-lemma sum_UNIV_sum:
- fixes g :: "'a::finite + 'b::finite \<Rightarrow> _"
- shows "(\<Sum>x\<in>UNIV. g x) = (\<Sum>x\<in>UNIV. g (Inl x)) + (\<Sum>x\<in>UNIV. g (Inr x))"
- apply (subst UNIV_Plus_UNIV [symmetric])
- apply (subst sum.Plus)
- apply simp_all
- done
-
lemma sum_mult_product:
"sum h {..<A * B :: nat} = (\<Sum>i\<in>{..<A}. \<Sum>j\<in>{..<B}. h (j + i * B))"
unfolding sum_nat_group[of h B A, unfolded atLeast0LessThan, symmetric]
@@ -632,7 +619,7 @@
by simp
qed
-text\<open>Inverse matrices (not necessarily square)\<close>
+subsection\<open>Inverse matrices (not necessarily square)\<close>
definition
"invertible(A::'a::semiring_1^'n^'m) \<longleftrightarrow> (\<exists>A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"
@@ -728,9 +715,86 @@
done
-subsection \<open>lambda skolemization on cartesian products\<close>
+subsection\<open>Some bounds on components etc. relative to operator norm.\<close>
+
+lemma norm_column_le_onorm:
+ fixes A :: "real^'n^'m"
+ shows "norm(column i A) \<le> onorm(( *v) A)"
+proof -
+ have bl: "bounded_linear (( *v) A)"
+ by (simp add: linear_linear matrix_vector_mul_linear)
+ have "norm (\<chi> j. A $ j $ i) \<le> norm (A *v axis i 1)"
+ by (simp add: matrix_mult_dot cart_eq_inner_axis)
+ also have "\<dots> \<le> onorm (( *v) A)"
+ using onorm [OF bl, of "axis i 1"] by (auto simp: axis_in_Basis)
+ finally have "norm (\<chi> j. A $ j $ i) \<le> onorm (( *v) A)" .
+ then show ?thesis
+ unfolding column_def .
+qed
+
+lemma matrix_component_le_onorm:
+ fixes A :: "real^'n^'m"
+ shows "\<bar>A $ i $ j\<bar> \<le> onorm(( *v) A)"
+proof -
+ have "\<bar>A $ i $ j\<bar> \<le> norm (\<chi> n. (A $ n $ j))"
+ by (metis (full_types, lifting) component_le_norm_cart vec_lambda_beta)
+ also have "\<dots> \<le> onorm (( *v) A)"
+ by (metis (no_types) column_def norm_column_le_onorm)
+ finally show ?thesis .
+qed
+
+lemma component_le_onorm:
+ fixes f :: "real^'m \<Rightarrow> real^'n"
+ shows "linear f \<Longrightarrow> \<bar>matrix f $ i $ j\<bar> \<le> onorm f"
+ by (metis matrix_component_le_onorm matrix_vector_mul)
-(* FIXME: rename do choice_cart *)
+lemma onorm_le_matrix_component_sum:
+ fixes A :: "real^'n^'m"
+ shows "onorm(( *v) A) \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>A $ i $ j\<bar>)"
+proof (rule onorm_le)
+ fix x
+ have "norm (A *v x) \<le> (\<Sum>i\<in>UNIV. \<bar>(A *v x) $ i\<bar>)"
+ by (rule norm_le_l1_cart)
+ also have "\<dots> \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>A $ i $ j\<bar> * norm x)"
+ proof (rule sum_mono)
+ fix i
+ have "\<bar>(A *v x) $ i\<bar> \<le> \<bar>\<Sum>j\<in>UNIV. A $ i $ j * x $ j\<bar>"
+ by (simp add: matrix_vector_mult_def)
+ also have "\<dots> \<le> (\<Sum>j\<in>UNIV. \<bar>A $ i $ j * x $ j\<bar>)"
+ by (rule sum_abs)
+ also have "\<dots> \<le> (\<Sum>j\<in>UNIV. \<bar>A $ i $ j\<bar> * norm x)"
+ by (rule sum_mono) (simp add: abs_mult component_le_norm_cart mult_left_mono)
+ finally show "\<bar>(A *v x) $ i\<bar> \<le> (\<Sum>j\<in>UNIV. \<bar>A $ i $ j\<bar> * norm x)" .
+ qed
+ finally show "norm (A *v x) \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>A $ i $ j\<bar>) * norm x"
+ by (simp add: sum_distrib_right)
+qed
+
+lemma onorm_le_matrix_component:
+ fixes A :: "real^'n^'m"
+ assumes "\<And>i j. abs(A$i$j) \<le> B"
+ shows "onorm(( *v) A) \<le> real (CARD('m)) * real (CARD('n)) * B"
+proof (rule onorm_le)
+ fix x :: "(real, 'n) vec"
+ have "norm (A *v x) \<le> (\<Sum>i\<in>UNIV. \<bar>(A *v x) $ i\<bar>)"
+ by (rule norm_le_l1_cart)
+ also have "\<dots> \<le> (\<Sum>i::'m \<in>UNIV. real (CARD('n)) * B * norm x)"
+ proof (rule sum_mono)
+ fix i
+ have "\<bar>(A *v x) $ i\<bar> \<le> norm(A $ i) * norm x"
+ by (simp add: matrix_mult_dot Cauchy_Schwarz_ineq2)
+ also have "\<dots> \<le> (\<Sum>j\<in>UNIV. \<bar>A $ i $ j\<bar>) * norm x"
+ by (simp add: mult_right_mono norm_le_l1_cart)
+ also have "\<dots> \<le> real (CARD('n)) * B * norm x"
+ by (simp add: assms sum_bounded_above mult_right_mono)
+ finally show "\<bar>(A *v x) $ i\<bar> \<le> real (CARD('n)) * B * norm x" .
+ qed
+ also have "\<dots> \<le> CARD('m) * real (CARD('n)) * B * norm x"
+ by simp
+ finally show "norm (A *v x) \<le> CARD('m) * real (CARD('n)) * B * norm x" .
+qed
+
+subsection \<open>lambda skolemization on cartesian products\<close>
lemma lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow>
(\<exists>x::'a ^ 'n. \<forall>i. P i (x $ i))" (is "?lhs \<longleftrightarrow> ?rhs")
@@ -751,6 +815,32 @@
ultimately show ?thesis by metis
qed
+lemma rational_approximation:
+ assumes "e > 0"
+ obtains r::real where "r \<in> \<rat>" "\<bar>r - x\<bar> < e"
+ using Rats_dense_in_real [of "x - e/2" "x + e/2"] assms by auto
+
+lemma matrix_rational_approximation:
+ fixes A :: "real^'n^'m"
+ assumes "e > 0"
+ obtains B where "\<And>i j. B$i$j \<in> \<rat>" "onorm(\<lambda>x. (A - B) *v x) < e"
+proof -
+ have "\<forall>i j. \<exists>q \<in> \<rat>. \<bar>q - A $ i $ j\<bar> < e / (2 * CARD('m) * CARD('n))"
+ using assms by (force intro: rational_approximation [of "e / (2 * CARD('m) * CARD('n))"])
+ then obtain B where B: "\<And>i j. B$i$j \<in> \<rat>" and Bclo: "\<And>i j. \<bar>B$i$j - A $ i $ j\<bar> < e / (2 * CARD('m) * CARD('n))"
+ by (auto simp: lambda_skolem Bex_def)
+ show ?thesis
+ proof
+ have "onorm (( *v) (A - B)) \<le> real CARD('m) * real CARD('n) *
+ (e / (2 * real CARD('m) * real CARD('n)))"
+ apply (rule onorm_le_matrix_component)
+ using Bclo by (simp add: abs_minus_commute less_imp_le)
+ also have "\<dots> < e"
+ using \<open>0 < e\<close> by (simp add: divide_simps)
+ finally show "onorm (( *v) (A - B)) < e" .
+ qed (use B in auto)
+qed
+
lemma vector_sub_project_orthogonal_cart: "(b::real^'n) \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *s b) = 0"
unfolding inner_simps scalar_mult_eq_scaleR by auto
@@ -1139,7 +1229,7 @@
and "box a b \<inter> box c d = {} \<longleftrightarrow> (\<exists>i. (b$i \<le> a$i \<or> d$i \<le> c$i \<or> b$i \<le> c$i \<or> d$i \<le> a$i))" (is ?th4)
using disjoint_interval[of a b c d] by (simp_all add: Basis_vec_def inner_axis)
-lemma inter_interval_cart:
+lemma Int_interval_cart:
fixes a :: "real^'n"
shows "cbox a b \<inter> cbox c d = {(\<chi> i. max (a$i) (c$i)) .. (\<chi> i. min (b$i) (d$i))}"
unfolding Int_interval
@@ -1225,6 +1315,11 @@
by (auto simp: axis_eq_axis inj_on_def *)
qed
+lemma dim_subset_UNIV_cart:
+ fixes S :: "(real^'n) set"
+ shows "dim S \<le> CARD('n)"
+ by (metis dim_subset_UNIV DIM_cart DIM_real mult.right_neutral)
+
lemma affinity_inverses:
assumes m0: "m \<noteq> (0::'a::field)"
shows "(\<lambda>x. m *s x + c) \<circ> (\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) = id"
@@ -1430,13 +1525,7 @@
unfolding vector_def by simp_all
lemma forall_vector_1: "(\<forall>v::'a::zero^1. P v) \<longleftrightarrow> (\<forall>x. P(vector[x]))"
- apply auto
- apply (erule_tac x="v$1" in allE)
- apply (subgoal_tac "vector [v$1] = v")
- apply simp
- apply (vector vector_def)
- apply simp
- done
+ by (metis vector_1 vector_one)
lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))"
apply auto
--- a/src/HOL/Analysis/Great_Picard.thy Sat Feb 24 17:21:35 2018 +0100
+++ b/src/HOL/Analysis/Great_Picard.thy Sun Feb 25 12:54:55 2018 +0000
@@ -46,7 +46,7 @@
have "(n-1)^2 \<le> n^2 - 1"
using assms by (simp add: algebra_simps power2_eq_square)
then have "real (n - 1) \<le> sqrt (real (n\<^sup>2 - 1))"
- by (metis Extended_Nonnegative_Real.of_nat_le_iff of_nat_power real_le_rsqrt)
+ by (metis of_nat_le_iff of_nat_power real_le_rsqrt)
then have "n-1 \<le> sqrt(real n ^ 2 - 1)"
by (simp add: Suc_leI assms of_nat_diff)
then show ?thesis
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sat Feb 24 17:21:35 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sun Feb 25 12:54:55 2018 +0000
@@ -46,6 +46,14 @@
lemma content_cbox_if: "content (cbox a b) = (if cbox a b = {} then 0 else \<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
by (simp add: content_cbox')
+lemma content_cbox_cart:
+ "cbox a b \<noteq> {} \<Longrightarrow> content(cbox a b) = prod (\<lambda>i. b$i - a$i) UNIV"
+ by (simp add: content_cbox_if Basis_vec_def cart_eq_inner_axis axis_eq_axis prod.UNION_disjoint)
+
+lemma content_cbox_if_cart:
+ "content(cbox a b) = (if cbox a b = {} then 0 else prod (\<lambda>i. b$i - a$i) UNIV)"
+ by (simp add: content_cbox_cart)
+
lemma content_division_of:
assumes "K \<in> \<D>" "\<D> division_of S"
shows "content K = (\<Prod>i \<in> Basis. interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)"
@@ -357,6 +365,9 @@
unfolding integral_def
by (rule some_equality) (auto intro: has_integral_unique)
+lemma has_integral_iff: "(f has_integral i) S \<longleftrightarrow> (f integrable_on S \<and> integral S f = i)"
+ by blast
+
lemma eq_integralD: "integral k f = y \<Longrightarrow> (f has_integral y) k \<or> ~ f integrable_on k \<and> y=0"
unfolding integral_def integrable_on_def
apply (erule subst)
@@ -3005,7 +3016,6 @@
shows "f integrable_on {c..d}"
by (metis assms box_real(2) integrable_subinterval)
-
subsection \<open>Combining adjacent intervals in 1 dimension.\<close>
lemma has_integral_combine:
@@ -4673,6 +4683,46 @@
using as by auto
qed
+subsection\<open>Integrals on set differences\<close>
+
+lemma has_integral_setdiff:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
+ assumes S: "(f has_integral i) S" and T: "(f has_integral j) T"
+ and neg: "negligible (T - S)"
+ shows "(f has_integral (i - j)) (S - T)"
+proof -
+ show ?thesis
+ unfolding has_integral_restrict_UNIV [symmetric, of f]
+ proof (rule has_integral_spike [OF neg])
+ have eq: "(\<lambda>x. (if x \<in> S then f x else 0) - (if x \<in> T then f x else 0)) =
+ (\<lambda>x. if x \<in> T - S then - f x else if x \<in> S - T then f x else 0)"
+ by (force simp add: )
+ have "((\<lambda>x. if x \<in> S then f x else 0) has_integral i) UNIV"
+ "((\<lambda>x. if x \<in> T then f x else 0) has_integral j) UNIV"
+ using S T has_integral_restrict_UNIV by auto
+ from has_integral_diff [OF this]
+ show "((\<lambda>x. if x \<in> T - S then - f x else if x \<in> S - T then f x else 0)
+ has_integral i-j) UNIV"
+ by (simp add: eq)
+ qed force
+qed
+
+lemma integral_setdiff:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
+ assumes "f integrable_on S" "f integrable_on T" "negligible(T - S)"
+ shows "integral (S - T) f = integral S f - integral T f"
+ by (rule integral_unique) (simp add: assms has_integral_setdiff integrable_integral)
+
+lemma integrable_setdiff:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
+ assumes "(f has_integral i) S" "(f has_integral j) T" "negligible (T - S)"
+ shows "f integrable_on (S - T)"
+ using has_integral_setdiff [OF assms]
+ by (simp add: has_integral_iff)
+
+lemma negligible_setdiff [simp]: "T \<subseteq> S \<Longrightarrow> negligible (T - S)"
+ by (metis Diff_eq_empty_iff negligible_empty)
+
lemma negligible_on_intervals: "negligible s \<longleftrightarrow> (\<forall>a b. negligible(s \<inter> cbox a b))" (is "?l \<longleftrightarrow> ?r")
proof
assume ?r
@@ -4757,9 +4807,7 @@
lemma has_integral_closure:
fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
shows "negligible(frontier S) \<Longrightarrow> (f has_integral y) (closure S) \<longleftrightarrow> (f has_integral y) S"
- apply (rule has_integral_spike_set_eq)
- apply (auto simp: Un_Diff closure_Un_frontier negligible_diff)
- by (simp add: Diff_eq closure_Un_frontier)
+ by (rule has_integral_spike_set_eq) (simp add: Un_Diff closure_Un_frontier negligible_diff)
lemma has_integral_open_interval:
fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
@@ -5344,9 +5392,6 @@
subsection \<open>Also tagged divisions\<close>
-lemma has_integral_iff: "(f has_integral i) S \<longleftrightarrow> (f integrable_on S \<and> integral S f = i)"
- by blast
-
lemma has_integral_combine_tagged_division:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
assumes "p tagged_division_of S"
--- a/src/HOL/HOL.thy Sat Feb 24 17:21:35 2018 +0100
+++ b/src/HOL/HOL.thy Sun Feb 25 12:54:55 2018 +0000
@@ -1404,6 +1404,9 @@
lemma ex_if_distrib: "(\<exists>x. if x = a then P x else Q x) \<longleftrightarrow> P a \<or> (\<exists>x. x\<noteq>a \<and> Q x)"
by auto
+lemma if_if_eq_conj: "(if P then if Q then x else y else y) = (if P \<and> Q then x else y)"
+ by simp
+
text \<open>As a simplification rule, it replaces all function equalities by
first-order equalities.\<close>
lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Sat Feb 24 17:21:35 2018 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Sun Feb 25 12:54:55 2018 +0000
@@ -158,17 +158,6 @@
using tendsto_cmult_ereal[of c f "f x" "at x within A" for x]
by (auto simp: continuous_on_def simp del: tendsto_cmult_ereal)
-context linordered_nonzero_semiring
-begin
-
-lemma of_nat_nonneg [simp]: "0 \<le> of_nat n"
- by (induct n) simp_all
-
-lemma of_nat_mono[simp]: "i \<le> j \<Longrightarrow> of_nat i \<le> of_nat j"
- by (auto simp add: le_iff_add intro!: add_increasing2)
-
-end
-
lemma real_of_nat_Sup:
assumes "A \<noteq> {}" "bdd_above A"
shows "of_nat (Sup A) = (SUP a:A. of_nat a :: real)"
@@ -181,21 +170,6 @@
by (intro cSUP_upper bdd_above_image_mono assms) (auto simp: mono_def)
qed
-\<comment> \<open>These generalise their counterparts in \<open>Nat.linordered_semidom_class\<close>\<close>
-lemma of_nat_less[simp]:
- "m < n \<Longrightarrow> of_nat m < (of_nat n::'a::{linordered_nonzero_semiring, semiring_char_0})"
- by (auto simp: less_le)
-
-lemma of_nat_le_iff[simp]:
- "of_nat m \<le> (of_nat n::'a::{linordered_nonzero_semiring, semiring_char_0}) \<longleftrightarrow> m \<le> n"
-proof (safe intro!: of_nat_mono)
- assume "of_nat m \<le> (of_nat n::'a)" then show "m \<le> n"
- proof (intro leI notI)
- assume "n < m" from less_le_trans[OF of_nat_less[OF this] \<open>of_nat m \<le> of_nat n\<close>] show False
- by blast
- qed
-qed
-
lemma (in complete_lattice) SUP_sup_const1:
"I \<noteq> {} \<Longrightarrow> (SUP i:I. sup c (f i)) = sup c (SUP i:I. f i)"
using SUP_sup_distrib[of "\<lambda>_. c" I f] by simp