# HG changeset patch # User huffman # Date 1312905192 25200 # Node ID 4c2a61a897d8ded471303d8d2fca84c8461ee7ca # Parent 2362a970e3485ef18d8da42da32148639cb2da96 Derivative.thy: more sensible subsection headings diff -r 2362a970e348 -r 4c2a61a897d8 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Aug 09 07:37:18 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Aug 09 08:53:12 2011 -0700 @@ -73,7 +73,7 @@ apply(rule_tac x=d in exI) apply(erule conjE,rule,assumption) apply rule apply(erule_tac x="xa + x" in allE) unfolding dist_norm netlimit_at_vector[of x] by (auto simp add: diff_diff_eq add.commute) qed qed -subsection {* These are the only cases we'll care about, probably. *} +text {* These are the only cases we'll care about, probably. *} lemma has_derivative_within: "(f has_derivative f') (at x within s) \ bounded_linear f' \ ((\y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x within s)" @@ -83,7 +83,7 @@ bounded_linear f' \ ((\y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x)" apply(subst within_UNIV[THEN sym]) unfolding has_derivative_within unfolding within_UNIV by auto -subsection {* More explicit epsilon-delta forms. *} +text {* More explicit epsilon-delta forms. *} lemma has_derivative_within': "(f has_derivative f')(at x within s) \ bounded_linear f' \ @@ -133,7 +133,7 @@ "(f has_derivative f') net \ linear f'" by (rule derivative_linear [THEN bounded_linear_imp_linear]) -subsection {* Combining theorems. *} +subsubsection {* Combining theorems. *} lemma (in bounded_linear) has_derivative: "(f has_derivative f) net" unfolding has_derivative_def apply(rule,rule bounded_linear_axioms) @@ -199,7 +199,7 @@ ((\x. setsum (\i. f i x) {m..n::nat}) has_derivative (\h. setsum (\i. f' i h) {m..n})) net" by (rule has_derivative_setsum) simp_all -subsection {* somewhat different results for derivative of scalar multiplier. *} +text {* Somewhat different results for derivative of scalar multiplier. *} (** move **) lemma linear_vmul_component: @@ -269,7 +269,7 @@ has_derivative_vmul_at has_derivative_vmul_within has_derivative_cmul bounded_linear.has_derivative has_derivative_lift_dot -subsection {* limit transformation for derivatives. *} +subsubsection {* Limit transformation for derivatives *} lemma has_derivative_transform_within: assumes "0 < d" "x \ s" "\x'\s. dist x' x < d \ f x' = g x'" "(f has_derivative f') (at x within s)" @@ -291,7 +291,7 @@ apply(rule Lim_transform_within_open[OF assms(1,2)]) defer apply assumption apply(rule,rule) apply(drule assms(3)[rule_format]) using assms(3)[rule_format, OF assms(2)] by auto -subsection {* differentiability. *} +subsection {* Differentiability *} no_notation Deriv.differentiable (infixl "differentiable" 60) @@ -343,7 +343,7 @@ unfolding frechet_derivative_works has_derivative_def by (auto intro: bounded_linear_imp_linear) -subsection {* Differentiability implies continuity. *} +subsection {* Differentiability implies continuity *} lemma Lim_mul_norm_within: fixes f::"'a::real_normed_vector \ 'b::real_normed_vector" @@ -402,8 +402,8 @@ lemma differentiable_on_empty: "f differentiable_on {}" unfolding differentiable_on_def by auto -subsection {* Several results are easier using a "multiplied-out" variant. *) -(* (I got this idea from Dieudonne's proof of the chain rule). *} +text {* Several results are easier using a "multiplied-out" variant. +(I got this idea from Dieudonne's proof of the chain rule). *} lemma has_derivative_within_alt: "(f has_derivative f') (at x within s) \ bounded_linear f' \ @@ -781,7 +781,7 @@ unfolding algebra_simps by (auto intro: mult_pos_pos) qed -subsection {* In particular if we have a mapping into @{typ "real"}. *} +text {* In particular if we have a mapping into @{typ "real"}. *} lemma differential_zero_maxmin: fixes f::"'a\euclidean_space \ real" @@ -887,7 +887,7 @@ case False thus ?thesis using mvt_simple[OF _ assms(2)] using assms(1) by auto qed -subsection {* A nice generalization (see Havin's proof of 5.19 from Rudin's book). *} +text {* A nice generalization (see Havin's proof of 5.19 from Rudin's book). *} lemma mvt_general: fixes f::"real\'a::euclidean_space" @@ -918,7 +918,7 @@ qed qed -subsection {* Still more general bound theorem. *} +text {* Still more general bound theorem. *} lemma differentiable_bound: fixes f::"'a::euclidean_space \ 'b::euclidean_space" @@ -976,7 +976,7 @@ using differentiable_bound[of s f f' B x y] unfolding Ball_def image_iff o_def using assms by auto -subsection {* In particular. *} +text {* In particular. *} lemma has_derivative_zero_constant: fixes f::"real\real" @@ -1076,7 +1076,7 @@ qed qed -subsection {* Simply rewrite that based on the domain point x. *} +text {* Simply rewrite that based on the domain point x. *} lemma has_derivative_inverse_basic_x: fixes f::"'b::euclidean_space \ 'c::euclidean_space" @@ -1085,7 +1085,7 @@ shows "(g has_derivative g') (at (f(x)))" apply(rule has_derivative_inverse_basic) using assms by auto -subsection {* This is the version in Dieudonne', assuming continuity of f and g. *} +text {* This is the version in Dieudonne', assuming continuity of f and g. *} lemma has_derivative_inverse_dieudonne: fixes f::"'a::euclidean_space \ 'b::euclidean_space" @@ -1096,7 +1096,7 @@ using assms(3-6) unfolding continuous_on_eq_continuous_at[OF assms(1)] continuous_on_eq_continuous_at[OF assms(2)] by auto -subsection {* Here's the simplest way of not assuming much about g. *} +text {* Here's the simplest way of not assuming much about g. *} lemma has_derivative_inverse: fixes f::"'a::euclidean_space \ 'b::euclidean_space" @@ -1302,7 +1302,7 @@ using assms by auto qed -subsection {* A rewrite based on the other domain. *} +text {* A rewrite based on the other domain. *} lemma has_derivative_inverse_strong_x: fixes f::"'a::ordered_euclidean_space \ 'a" @@ -1312,7 +1312,7 @@ shows "(g has_derivative g') (at y)" using has_derivative_inverse_strong[OF assms(1-6)] unfolding assms(7) by simp -subsection {* On a region. *} +text {* On a region. *} lemma has_derivative_inverse_on: fixes f::"'n::ordered_euclidean_space \ 'n" @@ -1597,7 +1597,7 @@ qed qed -subsection {* Can choose to line up antiderivatives if we want. *} +text {* Can choose to line up antiderivatives if we want. *} lemma has_antiderivative_sequence: fixes f::"nat\ 'm::euclidean_space \ 'n::euclidean_space"