# HG changeset patch # User immler # Date 1453292218 -3600 # Node ID 45eee631ea4f39d65589504e101c8cbd94865157 # Parent aed720a91f2f4adbcd123f6161da40bd59d0c53c added lemma diff -r aed720a91f2f -r 45eee631ea4f src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Wed Jan 20 00:06:48 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Wed Jan 20 13:16:58 2016 +0100 @@ -6,7 +6,7 @@ section \Multivariate calculus in Euclidean space\ theory Derivative -imports Brouwer_Fixpoint Operator_Norm Uniform_Limit +imports Brouwer_Fixpoint Operator_Norm Uniform_Limit Bounded_Linear_Function begin lemma onorm_inner_left: @@ -2561,4 +2561,197 @@ thus ?thesis using xc by (simp add: field_simps) qed simp_all + +subsection \Partial derivatives\ + +lemma eventually_at_Pair_within_TimesI1: + fixes x::"'a::metric_space" + assumes "\\<^sub>F x' in at x within X. P x'" + assumes "P x" + shows "\\<^sub>F (x', y') in at (x, y) within X \ Y. P x'" +proof - + from assms[unfolded eventually_at_topological] + obtain S where S: "open S" "x \ S" "\x'. x' \ X \ x' \ S \ P x'" + by metis + show "\\<^sub>F (x', y') in at (x, y) within X \ Y. P x'" + unfolding eventually_at_topological + by (auto intro!: exI[where x="S \ UNIV"] S open_Times) +qed + +lemma eventually_at_Pair_within_TimesI2: + fixes x::"'a::metric_space" + assumes "\\<^sub>F y' in at y within Y. P y'" + assumes "P y" + shows "\\<^sub>F (x', y') in at (x, y) within X \ Y. P y'" +proof - + from assms[unfolded eventually_at_topological] + obtain S where S: "open S" "y \ S" "\y'. y' \ Y \ y' \ S \ P y'" + by metis + show "\\<^sub>F (x', y') in at (x, y) within X \ Y. P y'" + unfolding eventually_at_topological + by (auto intro!: exI[where x="UNIV \ S"] S open_Times) +qed + +lemma has_derivative_partialsI: + assumes fx: "\x y. x \ X \ y \ Y \ ((\x. f x y) has_derivative blinfun_apply (fx x y)) (at x within X)" + assumes fy: "\x y. x \ X \ y \ Y \ ((\y. f x y) has_derivative blinfun_apply (fy x y)) (at y within Y)" + assumes fx_cont: "continuous_on (X \ Y) (\(x, y). fx x y)" + assumes fy_cont: "continuous_on (X \ Y) (\(x, y). fy x y)" + assumes "x \ X" "y \ Y" + assumes "convex X" "convex Y" + shows "((\(x, y). f x y) has_derivative (\(tx, ty). fx x y tx + fy x y ty)) (at (x, y) within X \ Y)" +proof (safe intro!: has_derivativeI tendstoI, goal_cases) + case (2 e') + def e\"e' / 9" + have "e > 0" using \e' > 0\ by (simp add: e_def) + + have "(x, y) \ X \ Y" using assms by auto + from fy_cont[unfolded continuous_on_eq_continuous_within, rule_format, OF this, + unfolded continuous_within, THEN tendstoD, OF \e > 0\] + have "\\<^sub>F (x', y') in at (x, y) within X \ Y. dist (fy x' y') (fy x y) < e" + by (auto simp: split_beta') + from this[unfolded eventually_at] obtain d' where + "d' > 0" + "\x' y'. x' \ X \ y' \ Y \ (x', y') \ (x, y) \ dist (x', y') (x, y) < d' \ + dist (fy x' y') (fy x y) < e" + by auto + then + have d': "x' \ X \ y' \ Y \ dist (x', y') (x, y) < d' \ dist (fy x' y') (fy x y) < e" + for x' y' + using \0 < e\ + by (cases "(x', y') = (x, y)") auto + def d \ "d' / sqrt 2" + have "d > 0" using \0 < d'\ by (simp add: d_def) + have d: "x' \ X \ y' \ Y \ dist x' x < d \ dist y' y < d \ dist (fy x' y') (fy x y) < e" + for x' y' + by (auto simp: dist_prod_def d_def intro!: d' real_sqrt_sum_squares_less) + + let ?S = "ball y d \ Y" + have "convex ?S" + by (auto intro!: convex_Int \convex Y\) + { + fix x'::'a and y'::'b + assume x': "x' \ X" and y': "y' \ Y" + assume dx': "dist x' x < d" and dy': "dist y' y < d" + have "norm (fy x' y' - fy x' y) \ dist (fy x' y') (fy x y) + dist (fy x' y) (fy x y)" + by norm + also have "dist (fy x' y') (fy x y) < e" + by (rule d; fact) + also have "dist (fy x' y) (fy x y) < e" + by (auto intro!: d simp: dist_prod_def x' \d > 0\ \y \ Y\ dx') + finally + have "norm (fy x' y' - fy x' y) < e + e" + by arith + then have "onorm (blinfun_apply (fy x' y') - blinfun_apply (fy x' y)) < e + e" + by (auto simp: norm_blinfun.rep_eq blinfun.diff_left[abs_def] fun_diff_def) + } note onorm = this + + have ev_mem: "\\<^sub>F (x', y') in at (x, y) within X \ Y. (x', y') \ X \ Y" + using \x \ X\ \y \ Y\ + by (auto simp: eventually_at intro!: zero_less_one) + moreover + have ev_dist: "\\<^sub>F xy in at (x, y) within X \ Y. dist xy (x, y) < d" if "d > 0" for d + using eventually_at_ball[OF that] + by (rule eventually_elim2) (auto simp: dist_commute intro!: eventually_True) + note ev_dist[OF \0 < d\] + ultimately + have "\\<^sub>F (x', y') in at (x, y) within X \ Y. + norm (f x' y' - f x' y - (fy x' y) (y' - y)) \ norm (y' - y) * (e + e)" + proof (eventually_elim, safe) + fix x' y' + assume "x' \ X" and y': "y' \ Y" + assume dist: "dist (x', y') (x, y) < d" + then have dx: "dist x' x < d" and dy: "dist y' y < d" + unfolding dist_prod_def fst_conv snd_conv atomize_conj + by (metis le_less_trans real_sqrt_sum_squares_ge1 real_sqrt_sum_squares_ge2) + { + fix t::real + assume "t \ {0 .. 1}" + then have "y + t *\<^sub>R (y' - y) \ closed_segment y y'" + by (auto simp: closed_segment_def algebra_simps intro!: exI[where x=t]) + also + have "\ \ ball y d \ Y" + using \y \ Y\ \0 < d\ dy y' + by (intro \convex ?S\[unfolded convex_contains_segment, rule_format, of y y']) + (auto simp: dist_commute) + finally have "y + t *\<^sub>R (y' - y) \ ?S" . + } note seg = this + + have "\x\ball y d \ Y. onorm (blinfun_apply (fy x' x) - blinfun_apply (fy x' y)) \ e + e" + by (safe intro!: onorm less_imp_le \x' \ X\ dx) (auto simp: dist_commute \0 < d\ \y \ Y\) + with seg has_derivative_within_subset[OF assms(2)[OF \x' \ X\]] + show "norm (f x' y' - f x' y - (fy x' y) (y' - y)) \ norm (y' - y) * (e + e)" + by (rule differentiable_bound_linearization[where S="?S"]) + (auto intro!: \0 < d\ \y \ Y\) + qed + moreover + let ?le = "\x'. norm (f x' y - f x y - (fx x y) (x' - x)) \ norm (x' - x) * e" + from fx[OF \x \ X\ \y \ Y\, unfolded has_derivative_within, THEN conjunct2, THEN tendstoD, OF \0 < e\] + have "\\<^sub>F x' in at x within X. ?le x'" + by eventually_elim + (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps split: split_if_asm) + then have "\\<^sub>F (x', y') in at (x, y) within X \ Y. ?le x'" + by (rule eventually_at_Pair_within_TimesI1) + (simp add: blinfun.bilinear_simps) + moreover have "\\<^sub>F (x', y') in at (x, y) within X \ Y. norm ((x', y') - (x, y)) \ 0" + unfolding norm_eq_zero right_minus_eq + by (auto simp: eventually_at intro!: zero_less_one) + moreover + from fy_cont[unfolded continuous_on_eq_continuous_within, rule_format, OF SigmaI[OF \x \ X\ \y \ Y\], + unfolded continuous_within, THEN tendstoD, OF \0 < e\] + have "\\<^sub>F x' in at x within X. norm (fy x' y - fy x y) < e" + unfolding eventually_at + using \y \ Y\ + by (auto simp: dist_prod_def dist_norm) + then have "\\<^sub>F (x', y') in at (x, y) within X \ Y. norm (fy x' y - fy x y) < e" + by (rule eventually_at_Pair_within_TimesI1) + (simp add: blinfun.bilinear_simps \0 < e\) + ultimately + have "\\<^sub>F (x', y') in at (x, y) within X \ Y. + norm ((f x' y' - f x y - (fx x y (x' - x) + fy x y (y' - y))) /\<^sub>R + norm ((x', y') - (x, y))) + < e'" + apply eventually_elim + proof safe + fix x' y' + have "norm (f x' y' - f x y - (fx x y (x' - x) + fy x y (y' - y))) \ + norm (f x' y' - f x' y - fy x' y (y' - y)) + + norm (fy x y (y' - y) - fy x' y (y' - y)) + + norm (f x' y - f x y - fx x y (x' - x))" + by norm + also + assume nz: "norm ((x', y') - (x, y)) \ 0" + and nfy: "norm (fy x' y - fy x y) < e" + assume "norm (f x' y' - f x' y - blinfun_apply (fy x' y) (y' - y)) \ norm (y' - y) * (e + e)" + also assume "norm (f x' y - f x y - blinfun_apply (fx x y) (x' - x)) \ norm (x' - x) * e" + also + have "norm ((fy x y) (y' - y) - (fy x' y) (y' - y)) \ norm ((fy x y) - (fy x' y)) * norm (y' - y)" + by (auto simp: blinfun.bilinear_simps[symmetric] intro!: norm_blinfun) + also have "\ \ (e + e) * norm (y' - y)" + using \e > 0\ nfy + by (auto simp: norm_minus_commute intro!: mult_right_mono) + also have "norm (x' - x) * e \ norm (x' - x) * (e + e)" + using \0 < e\ by simp + also have "norm (y' - y) * (e + e) + (e + e) * norm (y' - y) + norm (x' - x) * (e + e) \ + (norm (y' - y) + norm (x' - x)) * (4 * e)" + using \e > 0\ + by (simp add: algebra_simps) + also have "\ \ 2 * norm ((x', y') - (x, y)) * (4 * e)" + using \0 < e\ real_sqrt_sum_squares_ge1[of "norm (x' - x)" "norm (y' - y)"] + real_sqrt_sum_squares_ge2[of "norm (y' - y)" "norm (x' - x)"] + by (auto intro!: mult_right_mono simp: norm_prod_def + simp del: real_sqrt_sum_squares_ge1 real_sqrt_sum_squares_ge2) + also have "\ \ norm ((x', y') - (x, y)) * (8 * e)" + by simp + also have "\ < norm ((x', y') - (x, y)) * e'" + using \0 < e'\ nz + by (auto simp: e_def) + finally show "norm ((f x' y' - f x y - (fx x y (x' - x) + fy x y (y' - y))) /\<^sub>R norm ((x', y') - (x, y))) < e'" + by (auto simp: divide_simps dist_norm mult.commute) + qed + then show ?case + by eventually_elim (auto simp: dist_norm field_simps) +qed (auto intro!: bounded_linear_intros simp: split_beta') + + end diff -r aed720a91f2f -r 45eee631ea4f src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Wed Jan 20 00:06:48 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed Jan 20 13:16:58 2016 +0100 @@ -9,7 +9,6 @@ Derivative Uniform_Limit "~~/src/HOL/Library/Indicator_Function" - Bounded_Linear_Function begin lemma cSup_abs_le: (* TODO: move to Conditionally_Complete_Lattices.thy? *)