2519 then show "continuous (at x) f" |
2519 then show "continuous (at x) f" |
2520 unfolding continuous_on_eq_continuous_at[OF open_ball] |
2520 unfolding continuous_on_eq_continuous_at[OF open_ball] |
2521 using \<open>d > 0\<close> by auto |
2521 using \<open>d > 0\<close> by auto |
2522 qed |
2522 qed |
2523 |
2523 |
|
2524 |
|
2525 section \<open>Line Segments\<close> |
|
2526 |
|
2527 subsection \<open>Midpoint\<close> |
|
2528 |
|
2529 definition\<^marker>\<open>tag important\<close> midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a" |
|
2530 where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)" |
|
2531 |
|
2532 lemma midpoint_idem [simp]: "midpoint x x = x" |
|
2533 unfolding midpoint_def by simp |
|
2534 |
|
2535 lemma midpoint_sym: "midpoint a b = midpoint b a" |
|
2536 unfolding midpoint_def by (auto simp add: scaleR_right_distrib) |
|
2537 |
|
2538 lemma midpoint_eq_iff: "midpoint a b = c \<longleftrightarrow> a + b = c + c" |
|
2539 proof - |
|
2540 have "midpoint a b = c \<longleftrightarrow> scaleR 2 (midpoint a b) = scaleR 2 c" |
|
2541 by simp |
|
2542 then show ?thesis |
|
2543 unfolding midpoint_def scaleR_2 [symmetric] by simp |
|
2544 qed |
|
2545 |
|
2546 lemma |
|
2547 fixes a::real |
|
2548 assumes "a \<le> b" shows ge_midpoint_1: "a \<le> midpoint a b" |
|
2549 and le_midpoint_1: "midpoint a b \<le> b" |
|
2550 by (simp_all add: midpoint_def assms) |
|
2551 |
|
2552 lemma dist_midpoint: |
|
2553 fixes a b :: "'a::real_normed_vector" shows |
|
2554 "dist a (midpoint a b) = (dist a b) / 2" (is ?t1) |
|
2555 "dist b (midpoint a b) = (dist a b) / 2" (is ?t2) |
|
2556 "dist (midpoint a b) a = (dist a b) / 2" (is ?t3) |
|
2557 "dist (midpoint a b) b = (dist a b) / 2" (is ?t4) |
|
2558 proof - |
|
2559 have *: "\<And>x y::'a. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2" |
|
2560 unfolding equation_minus_iff by auto |
|
2561 have **: "\<And>x y::'a. 2 *\<^sub>R x = y \<Longrightarrow> norm x = (norm y) / 2" |
|
2562 by auto |
|
2563 note scaleR_right_distrib [simp] |
|
2564 show ?t1 |
|
2565 unfolding midpoint_def dist_norm |
|
2566 apply (rule **) |
|
2567 apply (simp add: scaleR_right_diff_distrib) |
|
2568 apply (simp add: scaleR_2) |
|
2569 done |
|
2570 show ?t2 |
|
2571 unfolding midpoint_def dist_norm |
|
2572 apply (rule *) |
|
2573 apply (simp add: scaleR_right_diff_distrib) |
|
2574 apply (simp add: scaleR_2) |
|
2575 done |
|
2576 show ?t3 |
|
2577 unfolding midpoint_def dist_norm |
|
2578 apply (rule *) |
|
2579 apply (simp add: scaleR_right_diff_distrib) |
|
2580 apply (simp add: scaleR_2) |
|
2581 done |
|
2582 show ?t4 |
|
2583 unfolding midpoint_def dist_norm |
|
2584 apply (rule **) |
|
2585 apply (simp add: scaleR_right_diff_distrib) |
|
2586 apply (simp add: scaleR_2) |
|
2587 done |
|
2588 qed |
|
2589 |
|
2590 lemma midpoint_eq_endpoint [simp]: |
|
2591 "midpoint a b = a \<longleftrightarrow> a = b" |
|
2592 "midpoint a b = b \<longleftrightarrow> a = b" |
|
2593 unfolding midpoint_eq_iff by auto |
|
2594 |
|
2595 lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b" |
|
2596 using midpoint_eq_iff by metis |
|
2597 |
|
2598 lemma midpoint_linear_image: |
|
2599 "linear f \<Longrightarrow> midpoint(f a)(f b) = f(midpoint a b)" |
|
2600 by (simp add: linear_iff midpoint_def) |
|
2601 |
|
2602 |
|
2603 subsection \<open>Line segments\<close> |
|
2604 |
|
2605 definition\<^marker>\<open>tag important\<close> closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" |
|
2606 where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}" |
|
2607 |
|
2608 definition\<^marker>\<open>tag important\<close> open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where |
|
2609 "open_segment a b \<equiv> closed_segment a b - {a,b}" |
|
2610 |
|
2611 lemmas segment = open_segment_def closed_segment_def |
|
2612 |
|
2613 lemma in_segment: |
|
2614 "x \<in> closed_segment a b \<longleftrightarrow> (\<exists>u. 0 \<le> u \<and> u \<le> 1 \<and> x = (1 - u) *\<^sub>R a + u *\<^sub>R b)" |
|
2615 "x \<in> open_segment a b \<longleftrightarrow> a \<noteq> b \<and> (\<exists>u. 0 < u \<and> u < 1 \<and> x = (1 - u) *\<^sub>R a + u *\<^sub>R b)" |
|
2616 using less_eq_real_def by (auto simp: segment algebra_simps) |
|
2617 |
|
2618 lemma closed_segment_linear_image: |
|
2619 "closed_segment (f a) (f b) = f ` (closed_segment a b)" if "linear f" |
|
2620 proof - |
|
2621 interpret linear f by fact |
|
2622 show ?thesis |
|
2623 by (force simp add: in_segment add scale) |
|
2624 qed |
|
2625 |
|
2626 lemma open_segment_linear_image: |
|
2627 "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> open_segment (f a) (f b) = f ` (open_segment a b)" |
|
2628 by (force simp: open_segment_def closed_segment_linear_image inj_on_def) |
|
2629 |
|
2630 lemma closed_segment_translation: |
|
2631 "closed_segment (c + a) (c + b) = image (\<lambda>x. c + x) (closed_segment a b)" |
|
2632 apply safe |
|
2633 apply (rule_tac x="x-c" in image_eqI) |
|
2634 apply (auto simp: in_segment algebra_simps) |
|
2635 done |
|
2636 |
|
2637 lemma open_segment_translation: |
|
2638 "open_segment (c + a) (c + b) = image (\<lambda>x. c + x) (open_segment a b)" |
|
2639 by (simp add: open_segment_def closed_segment_translation translation_diff) |
|
2640 |
|
2641 lemma closed_segment_of_real: |
|
2642 "closed_segment (of_real x) (of_real y) = of_real ` closed_segment x y" |
|
2643 apply (auto simp: image_iff in_segment scaleR_conv_of_real) |
|
2644 apply (rule_tac x="(1-u)*x + u*y" in bexI) |
|
2645 apply (auto simp: in_segment) |
|
2646 done |
|
2647 |
|
2648 lemma open_segment_of_real: |
|
2649 "open_segment (of_real x) (of_real y) = of_real ` open_segment x y" |
|
2650 apply (auto simp: image_iff in_segment scaleR_conv_of_real) |
|
2651 apply (rule_tac x="(1-u)*x + u*y" in bexI) |
|
2652 apply (auto simp: in_segment) |
|
2653 done |
|
2654 |
|
2655 lemma closed_segment_Reals: |
|
2656 "\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> closed_segment x y = of_real ` closed_segment (Re x) (Re y)" |
|
2657 by (metis closed_segment_of_real of_real_Re) |
|
2658 |
|
2659 lemma open_segment_Reals: |
|
2660 "\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> open_segment x y = of_real ` open_segment (Re x) (Re y)" |
|
2661 by (metis open_segment_of_real of_real_Re) |
|
2662 |
|
2663 lemma open_segment_PairD: |
|
2664 "(x, x') \<in> open_segment (a, a') (b, b') |
|
2665 \<Longrightarrow> (x \<in> open_segment a b \<or> a = b) \<and> (x' \<in> open_segment a' b' \<or> a' = b')" |
|
2666 by (auto simp: in_segment) |
|
2667 |
|
2668 lemma closed_segment_PairD: |
|
2669 "(x, x') \<in> closed_segment (a, a') (b, b') \<Longrightarrow> x \<in> closed_segment a b \<and> x' \<in> closed_segment a' b'" |
|
2670 by (auto simp: closed_segment_def) |
|
2671 |
|
2672 lemma closed_segment_translation_eq [simp]: |
|
2673 "d + x \<in> closed_segment (d + a) (d + b) \<longleftrightarrow> x \<in> closed_segment a b" |
|
2674 proof - |
|
2675 have *: "\<And>d x a b. x \<in> closed_segment a b \<Longrightarrow> d + x \<in> closed_segment (d + a) (d + b)" |
|
2676 apply (simp add: closed_segment_def) |
|
2677 apply (erule ex_forward) |
|
2678 apply (simp add: algebra_simps) |
|
2679 done |
|
2680 show ?thesis |
|
2681 using * [where d = "-d"] * |
|
2682 by (fastforce simp add:) |
|
2683 qed |
|
2684 |
|
2685 lemma open_segment_translation_eq [simp]: |
|
2686 "d + x \<in> open_segment (d + a) (d + b) \<longleftrightarrow> x \<in> open_segment a b" |
|
2687 by (simp add: open_segment_def) |
|
2688 |
|
2689 lemma of_real_closed_segment [simp]: |
|
2690 "of_real x \<in> closed_segment (of_real a) (of_real b) \<longleftrightarrow> x \<in> closed_segment a b" |
|
2691 apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward) |
|
2692 using of_real_eq_iff by fastforce |
|
2693 |
|
2694 lemma of_real_open_segment [simp]: |
|
2695 "of_real x \<in> open_segment (of_real a) (of_real b) \<longleftrightarrow> x \<in> open_segment a b" |
|
2696 apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward del: exE) |
|
2697 using of_real_eq_iff by fastforce |
|
2698 |
|
2699 lemma convex_contains_segment: |
|
2700 "convex S \<longleftrightarrow> (\<forall>a\<in>S. \<forall>b\<in>S. closed_segment a b \<subseteq> S)" |
|
2701 unfolding convex_alt closed_segment_def by auto |
|
2702 |
|
2703 lemma closed_segment_in_Reals: |
|
2704 "\<lbrakk>x \<in> closed_segment a b; a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> x \<in> Reals" |
|
2705 by (meson subsetD convex_Reals convex_contains_segment) |
|
2706 |
|
2707 lemma open_segment_in_Reals: |
|
2708 "\<lbrakk>x \<in> open_segment a b; a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> x \<in> Reals" |
|
2709 by (metis Diff_iff closed_segment_in_Reals open_segment_def) |
|
2710 |
|
2711 lemma closed_segment_subset: "\<lbrakk>x \<in> S; y \<in> S; convex S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> S" |
|
2712 by (simp add: convex_contains_segment) |
|
2713 |
|
2714 lemma closed_segment_subset_convex_hull: |
|
2715 "\<lbrakk>x \<in> convex hull S; y \<in> convex hull S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> convex hull S" |
|
2716 using convex_contains_segment by blast |
|
2717 |
|
2718 lemma segment_convex_hull: |
|
2719 "closed_segment a b = convex hull {a,b}" |
|
2720 proof - |
|
2721 have *: "\<And>x. {x} \<noteq> {}" by auto |
|
2722 show ?thesis |
|
2723 unfolding segment convex_hull_insert[OF *] convex_hull_singleton |
|
2724 by (safe; rule_tac x="1 - u" in exI; force) |
|
2725 qed |
|
2726 |
|
2727 lemma open_closed_segment: "u \<in> open_segment w z \<Longrightarrow> u \<in> closed_segment w z" |
|
2728 by (auto simp add: closed_segment_def open_segment_def) |
|
2729 |
|
2730 lemma segment_open_subset_closed: |
|
2731 "open_segment a b \<subseteq> closed_segment a b" |
|
2732 by (auto simp: closed_segment_def open_segment_def) |
|
2733 |
|
2734 lemma bounded_closed_segment: |
|
2735 fixes a :: "'a::euclidean_space" shows "bounded (closed_segment a b)" |
|
2736 by (simp add: segment_convex_hull compact_convex_hull compact_imp_bounded) |
|
2737 |
|
2738 lemma bounded_open_segment: |
|
2739 fixes a :: "'a::euclidean_space" shows "bounded (open_segment a b)" |
|
2740 by (rule bounded_subset [OF bounded_closed_segment segment_open_subset_closed]) |
|
2741 |
|
2742 lemmas bounded_segment = bounded_closed_segment open_closed_segment |
|
2743 |
|
2744 lemma ends_in_segment [iff]: "a \<in> closed_segment a b" "b \<in> closed_segment a b" |
|
2745 unfolding segment_convex_hull |
|
2746 by (auto intro!: hull_subset[unfolded subset_eq, rule_format]) |
|
2747 |
|
2748 lemma eventually_closed_segment: |
|
2749 fixes x0::"'a::real_normed_vector" |
|
2750 assumes "open X0" "x0 \<in> X0" |
|
2751 shows "\<forall>\<^sub>F x in at x0 within U. closed_segment x0 x \<subseteq> X0" |
|
2752 proof - |
|
2753 from openE[OF assms] |
|
2754 obtain e where e: "0 < e" "ball x0 e \<subseteq> X0" . |
|
2755 then have "\<forall>\<^sub>F x in at x0 within U. x \<in> ball x0 e" |
|
2756 by (auto simp: dist_commute eventually_at) |
|
2757 then show ?thesis |
|
2758 proof eventually_elim |
|
2759 case (elim x) |
|
2760 have "x0 \<in> ball x0 e" using \<open>e > 0\<close> by simp |
|
2761 from convex_ball[unfolded convex_contains_segment, rule_format, OF this elim] |
|
2762 have "closed_segment x0 x \<subseteq> ball x0 e" . |
|
2763 also note \<open>\<dots> \<subseteq> X0\<close> |
|
2764 finally show ?case . |
|
2765 qed |
|
2766 qed |
|
2767 |
|
2768 lemma segment_furthest_le: |
|
2769 fixes a b x y :: "'a::euclidean_space" |
|
2770 assumes "x \<in> closed_segment a b" |
|
2771 shows "norm (y - x) \<le> norm (y - a) \<or> norm (y - x) \<le> norm (y - b)" |
|
2772 proof - |
|
2773 obtain z where "z \<in> {a, b}" "norm (x - y) \<le> norm (z - y)" |
|
2774 using simplex_furthest_le[of "{a, b}" y] |
|
2775 using assms[unfolded segment_convex_hull] |
|
2776 by auto |
|
2777 then show ?thesis |
|
2778 by (auto simp add:norm_minus_commute) |
|
2779 qed |
|
2780 |
|
2781 lemma closed_segment_commute: "closed_segment a b = closed_segment b a" |
|
2782 proof - |
|
2783 have "{a, b} = {b, a}" by auto |
|
2784 thus ?thesis |
|
2785 by (simp add: segment_convex_hull) |
|
2786 qed |
|
2787 |
|
2788 lemma segment_bound1: |
|
2789 assumes "x \<in> closed_segment a b" |
|
2790 shows "norm (x - a) \<le> norm (b - a)" |
|
2791 proof - |
|
2792 obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1" |
|
2793 using assms by (auto simp add: closed_segment_def) |
|
2794 then show "norm (x - a) \<le> norm (b - a)" |
|
2795 apply clarify |
|
2796 apply (auto simp: algebra_simps) |
|
2797 apply (simp add: scaleR_diff_right [symmetric] mult_left_le_one_le) |
|
2798 done |
|
2799 qed |
|
2800 |
|
2801 lemma segment_bound: |
|
2802 assumes "x \<in> closed_segment a b" |
|
2803 shows "norm (x - a) \<le> norm (b - a)" "norm (x - b) \<le> norm (b - a)" |
|
2804 apply (simp add: assms segment_bound1) |
|
2805 by (metis assms closed_segment_commute dist_commute dist_norm segment_bound1) |
|
2806 |
|
2807 lemma open_segment_commute: "open_segment a b = open_segment b a" |
|
2808 proof - |
|
2809 have "{a, b} = {b, a}" by auto |
|
2810 thus ?thesis |
|
2811 by (simp add: closed_segment_commute open_segment_def) |
|
2812 qed |
|
2813 |
|
2814 lemma closed_segment_idem [simp]: "closed_segment a a = {a}" |
|
2815 unfolding segment by (auto simp add: algebra_simps) |
|
2816 |
|
2817 lemma open_segment_idem [simp]: "open_segment a a = {}" |
|
2818 by (simp add: open_segment_def) |
|
2819 |
|
2820 lemma closed_segment_eq_open: "closed_segment a b = open_segment a b \<union> {a,b}" |
|
2821 using open_segment_def by auto |
|
2822 |
|
2823 lemma convex_contains_open_segment: |
|
2824 "convex s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. open_segment a b \<subseteq> s)" |
|
2825 by (simp add: convex_contains_segment closed_segment_eq_open) |
|
2826 |
|
2827 lemma closed_segment_eq_real_ivl: |
|
2828 fixes a b::real |
|
2829 shows "closed_segment a b = (if a \<le> b then {a .. b} else {b .. a})" |
|
2830 proof - |
|
2831 have "b \<le> a \<Longrightarrow> closed_segment b a = {b .. a}" |
|
2832 and "a \<le> b \<Longrightarrow> closed_segment a b = {a .. b}" |
|
2833 by (auto simp: convex_hull_eq_real_cbox segment_convex_hull) |
|
2834 thus ?thesis |
|
2835 by (auto simp: closed_segment_commute) |
|
2836 qed |
|
2837 |
|
2838 lemma open_segment_eq_real_ivl: |
|
2839 fixes a b::real |
|
2840 shows "open_segment a b = (if a \<le> b then {a<..<b} else {b<..<a})" |
|
2841 by (auto simp: closed_segment_eq_real_ivl open_segment_def split: if_split_asm) |
|
2842 |
|
2843 lemma closed_segment_real_eq: |
|
2844 fixes u::real shows "closed_segment u v = (\<lambda>x. (v - u) * x + u) ` {0..1}" |
|
2845 by (simp add: add.commute [of u] image_affinity_atLeastAtMost [where c=u] closed_segment_eq_real_ivl) |
|
2846 |
|
2847 lemma dist_in_closed_segment: |
|
2848 fixes a :: "'a :: euclidean_space" |
|
2849 assumes "x \<in> closed_segment a b" |
|
2850 shows "dist x a \<le> dist a b \<and> dist x b \<le> dist a b" |
|
2851 proof (intro conjI) |
|
2852 obtain u where u: "0 \<le> u" "u \<le> 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" |
|
2853 using assms by (force simp: in_segment algebra_simps) |
|
2854 have "dist x a = u * dist a b" |
|
2855 apply (simp add: dist_norm algebra_simps x) |
|
2856 by (metis \<open>0 \<le> u\<close> abs_of_nonneg norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib) |
|
2857 also have "... \<le> dist a b" |
|
2858 by (simp add: mult_left_le_one_le u) |
|
2859 finally show "dist x a \<le> dist a b" . |
|
2860 have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)" |
|
2861 by (simp add: dist_norm algebra_simps x) |
|
2862 also have "... = (1-u) * dist a b" |
|
2863 proof - |
|
2864 have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)" |
|
2865 using \<open>u \<le> 1\<close> by force |
|
2866 then show ?thesis |
|
2867 by (simp add: dist_norm real_vector.scale_right_diff_distrib) |
|
2868 qed |
|
2869 also have "... \<le> dist a b" |
|
2870 by (simp add: mult_left_le_one_le u) |
|
2871 finally show "dist x b \<le> dist a b" . |
|
2872 qed |
|
2873 |
|
2874 lemma dist_in_open_segment: |
|
2875 fixes a :: "'a :: euclidean_space" |
|
2876 assumes "x \<in> open_segment a b" |
|
2877 shows "dist x a < dist a b \<and> dist x b < dist a b" |
|
2878 proof (intro conjI) |
|
2879 obtain u where u: "0 < u" "u < 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" |
|
2880 using assms by (force simp: in_segment algebra_simps) |
|
2881 have "dist x a = u * dist a b" |
|
2882 apply (simp add: dist_norm algebra_simps x) |
|
2883 by (metis abs_of_nonneg less_eq_real_def norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib \<open>0 < u\<close>) |
|
2884 also have *: "... < dist a b" |
|
2885 by (metis (no_types) assms dist_eq_0_iff dist_not_less_zero in_segment(2) linorder_neqE_linordered_idom mult.left_neutral real_mult_less_iff1 \<open>u < 1\<close>) |
|
2886 finally show "dist x a < dist a b" . |
|
2887 have ab_ne0: "dist a b \<noteq> 0" |
|
2888 using * by fastforce |
|
2889 have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)" |
|
2890 by (simp add: dist_norm algebra_simps x) |
|
2891 also have "... = (1-u) * dist a b" |
|
2892 proof - |
|
2893 have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)" |
|
2894 using \<open>u < 1\<close> by force |
|
2895 then show ?thesis |
|
2896 by (simp add: dist_norm real_vector.scale_right_diff_distrib) |
|
2897 qed |
|
2898 also have "... < dist a b" |
|
2899 using ab_ne0 \<open>0 < u\<close> by simp |
|
2900 finally show "dist x b < dist a b" . |
|
2901 qed |
|
2902 |
|
2903 lemma dist_decreases_open_segment_0: |
|
2904 fixes x :: "'a :: euclidean_space" |
|
2905 assumes "x \<in> open_segment 0 b" |
|
2906 shows "dist c x < dist c 0 \<or> dist c x < dist c b" |
|
2907 proof (rule ccontr, clarsimp simp: not_less) |
|
2908 obtain u where u: "0 \<noteq> b" "0 < u" "u < 1" and x: "x = u *\<^sub>R b" |
|
2909 using assms by (auto simp: in_segment) |
|
2910 have xb: "x \<bullet> b < b \<bullet> b" |
|
2911 using u x by auto |
|
2912 assume "norm c \<le> dist c x" |
|
2913 then have "c \<bullet> c \<le> (c - x) \<bullet> (c - x)" |
|
2914 by (simp add: dist_norm norm_le) |
|
2915 moreover have "0 < x \<bullet> b" |
|
2916 using u x by auto |
|
2917 ultimately have less: "c \<bullet> b < x \<bullet> b" |
|
2918 by (simp add: x algebra_simps inner_commute u) |
|
2919 assume "dist c b \<le> dist c x" |
|
2920 then have "(c - b) \<bullet> (c - b) \<le> (c - x) \<bullet> (c - x)" |
|
2921 by (simp add: dist_norm norm_le) |
|
2922 then have "(b \<bullet> b) * (1 - u*u) \<le> 2 * (b \<bullet> c) * (1-u)" |
|
2923 by (simp add: x algebra_simps inner_commute) |
|
2924 then have "(1+u) * (b \<bullet> b) * (1-u) \<le> 2 * (b \<bullet> c) * (1-u)" |
|
2925 by (simp add: algebra_simps) |
|
2926 then have "(1+u) * (b \<bullet> b) \<le> 2 * (b \<bullet> c)" |
|
2927 using \<open>u < 1\<close> by auto |
|
2928 with xb have "c \<bullet> b \<ge> x \<bullet> b" |
|
2929 by (auto simp: x algebra_simps inner_commute) |
|
2930 with less show False by auto |
|
2931 qed |
|
2932 |
|
2933 proposition dist_decreases_open_segment: |
|
2934 fixes a :: "'a :: euclidean_space" |
|
2935 assumes "x \<in> open_segment a b" |
|
2936 shows "dist c x < dist c a \<or> dist c x < dist c b" |
|
2937 proof - |
|
2938 have *: "x - a \<in> open_segment 0 (b - a)" using assms |
|
2939 by (metis diff_self open_segment_translation_eq uminus_add_conv_diff) |
|
2940 show ?thesis |
|
2941 using dist_decreases_open_segment_0 [OF *, of "c-a"] assms |
|
2942 by (simp add: dist_norm) |
|
2943 qed |
|
2944 |
|
2945 corollary open_segment_furthest_le: |
|
2946 fixes a b x y :: "'a::euclidean_space" |
|
2947 assumes "x \<in> open_segment a b" |
|
2948 shows "norm (y - x) < norm (y - a) \<or> norm (y - x) < norm (y - b)" |
|
2949 by (metis assms dist_decreases_open_segment dist_norm) |
|
2950 |
|
2951 corollary dist_decreases_closed_segment: |
|
2952 fixes a :: "'a :: euclidean_space" |
|
2953 assumes "x \<in> closed_segment a b" |
|
2954 shows "dist c x \<le> dist c a \<or> dist c x \<le> dist c b" |
|
2955 apply (cases "x \<in> open_segment a b") |
|
2956 using dist_decreases_open_segment less_eq_real_def apply blast |
|
2957 by (metis DiffI assms empty_iff insertE open_segment_def order_refl) |
|
2958 |
|
2959 lemma convex_intermediate_ball: |
|
2960 fixes a :: "'a :: euclidean_space" |
|
2961 shows "\<lbrakk>ball a r \<subseteq> T; T \<subseteq> cball a r\<rbrakk> \<Longrightarrow> convex T" |
|
2962 apply (simp add: convex_contains_open_segment, clarify) |
|
2963 by (metis (no_types, hide_lams) less_le_trans mem_ball mem_cball subsetCE dist_decreases_open_segment) |
|
2964 |
|
2965 lemma csegment_midpoint_subset: "closed_segment (midpoint a b) b \<subseteq> closed_segment a b" |
|
2966 apply (clarsimp simp: midpoint_def in_segment) |
|
2967 apply (rule_tac x="(1 + u) / 2" in exI) |
|
2968 apply (auto simp: algebra_simps add_divide_distrib diff_divide_distrib) |
|
2969 by (metis field_sum_of_halves scaleR_left.add) |
|
2970 |
|
2971 lemma notin_segment_midpoint: |
|
2972 fixes a :: "'a :: euclidean_space" |
|
2973 shows "a \<noteq> b \<Longrightarrow> a \<notin> closed_segment (midpoint a b) b" |
|
2974 by (auto simp: dist_midpoint dest!: dist_in_closed_segment) |
|
2975 |
|
2976 lemma segment_to_closest_point: |
|
2977 fixes S :: "'a :: euclidean_space set" |
|
2978 shows "\<lbrakk>closed S; S \<noteq> {}\<rbrakk> \<Longrightarrow> open_segment a (closest_point S a) \<inter> S = {}" |
|
2979 apply (subst disjoint_iff_not_equal) |
|
2980 apply (clarify dest!: dist_in_open_segment) |
|
2981 by (metis closest_point_le dist_commute le_less_trans less_irrefl) |
|
2982 |
|
2983 lemma segment_to_point_exists: |
|
2984 fixes S :: "'a :: euclidean_space set" |
|
2985 assumes "closed S" "S \<noteq> {}" |
|
2986 obtains b where "b \<in> S" "open_segment a b \<inter> S = {}" |
|
2987 by (metis assms segment_to_closest_point closest_point_exists that) |
|
2988 |
|
2989 subsubsection\<open>More lemmas, especially for working with the underlying formula\<close> |
|
2990 |
|
2991 lemma segment_eq_compose: |
|
2992 fixes a :: "'a :: real_vector" |
|
2993 shows "(\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) = (\<lambda>x. a + x) o (\<lambda>u. u *\<^sub>R (b - a))" |
|
2994 by (simp add: o_def algebra_simps) |
|
2995 |
|
2996 lemma segment_degen_1: |
|
2997 fixes a :: "'a :: real_vector" |
|
2998 shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = b \<longleftrightarrow> a=b \<or> u=1" |
|
2999 proof - |
|
3000 { assume "(1 - u) *\<^sub>R a + u *\<^sub>R b = b" |
|
3001 then have "(1 - u) *\<^sub>R a = (1 - u) *\<^sub>R b" |
|
3002 by (simp add: algebra_simps) |
|
3003 then have "a=b \<or> u=1" |
|
3004 by simp |
|
3005 } then show ?thesis |
|
3006 by (auto simp: algebra_simps) |
|
3007 qed |
|
3008 |
|
3009 lemma segment_degen_0: |
|
3010 fixes a :: "'a :: real_vector" |
|
3011 shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = a \<longleftrightarrow> a=b \<or> u=0" |
|
3012 using segment_degen_1 [of "1-u" b a] |
|
3013 by (auto simp: algebra_simps) |
|
3014 |
|
3015 lemma add_scaleR_degen: |
|
3016 fixes a b ::"'a::real_vector" |
|
3017 assumes "(u *\<^sub>R b + v *\<^sub>R a) = (u *\<^sub>R a + v *\<^sub>R b)" "u \<noteq> v" |
|
3018 shows "a=b" |
|
3019 by (metis (no_types, hide_lams) add.commute add_diff_eq diff_add_cancel real_vector.scale_cancel_left real_vector.scale_left_diff_distrib assms) |
|
3020 |
|
3021 lemma closed_segment_image_interval: |
|
3022 "closed_segment a b = (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0..1}" |
|
3023 by (auto simp: set_eq_iff image_iff closed_segment_def) |
|
3024 |
|
3025 lemma open_segment_image_interval: |
|
3026 "open_segment a b = (if a=b then {} else (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1})" |
|
3027 by (auto simp: open_segment_def closed_segment_def segment_degen_0 segment_degen_1) |
|
3028 |
|
3029 lemmas segment_image_interval = closed_segment_image_interval open_segment_image_interval |
|
3030 |
|
3031 lemma open_segment_bound1: |
|
3032 assumes "x \<in> open_segment a b" |
|
3033 shows "norm (x - a) < norm (b - a)" |
|
3034 proof - |
|
3035 obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 < u" "u < 1" "a \<noteq> b" |
|
3036 using assms by (auto simp add: open_segment_image_interval split: if_split_asm) |
|
3037 then show "norm (x - a) < norm (b - a)" |
|
3038 apply clarify |
|
3039 apply (auto simp: algebra_simps) |
|
3040 apply (simp add: scaleR_diff_right [symmetric]) |
|
3041 done |
|
3042 qed |
|
3043 |
|
3044 lemma compact_segment [simp]: |
|
3045 fixes a :: "'a::real_normed_vector" |
|
3046 shows "compact (closed_segment a b)" |
|
3047 by (auto simp: segment_image_interval intro!: compact_continuous_image continuous_intros) |
|
3048 |
|
3049 lemma closed_segment [simp]: |
|
3050 fixes a :: "'a::real_normed_vector" |
|
3051 shows "closed (closed_segment a b)" |
|
3052 by (simp add: compact_imp_closed) |
|
3053 |
|
3054 lemma closure_closed_segment [simp]: |
|
3055 fixes a :: "'a::real_normed_vector" |
|
3056 shows "closure(closed_segment a b) = closed_segment a b" |
|
3057 by simp |
|
3058 |
|
3059 lemma open_segment_bound: |
|
3060 assumes "x \<in> open_segment a b" |
|
3061 shows "norm (x - a) < norm (b - a)" "norm (x - b) < norm (b - a)" |
|
3062 apply (simp add: assms open_segment_bound1) |
|
3063 by (metis assms norm_minus_commute open_segment_bound1 open_segment_commute) |
|
3064 |
|
3065 lemma closure_open_segment [simp]: |
|
3066 "closure (open_segment a b) = (if a = b then {} else closed_segment a b)" |
|
3067 for a :: "'a::euclidean_space" |
|
3068 proof (cases "a = b") |
|
3069 case True |
|
3070 then show ?thesis |
|
3071 by simp |
|
3072 next |
|
3073 case False |
|
3074 have "closure ((\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1}) = (\<lambda>u. u *\<^sub>R (b - a)) ` closure {0<..<1}" |
|
3075 apply (rule closure_injective_linear_image [symmetric]) |
|
3076 apply (use False in \<open>auto intro!: injI\<close>) |
|
3077 done |
|
3078 then have "closure |
|
3079 ((\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1}) = |
|
3080 (\<lambda>x. (1 - x) *\<^sub>R a + x *\<^sub>R b) ` closure {0<..<1}" |
|
3081 using closure_translation [of a "((\<lambda>x. x *\<^sub>R b - x *\<^sub>R a) ` {0<..<1})"] |
|
3082 by (simp add: segment_eq_compose field_simps scaleR_diff_left scaleR_diff_right image_image) |
|
3083 then show ?thesis |
|
3084 by (simp add: segment_image_interval closure_greaterThanLessThan [symmetric] del: closure_greaterThanLessThan) |
|
3085 qed |
|
3086 |
|
3087 lemma closed_open_segment_iff [simp]: |
|
3088 fixes a :: "'a::euclidean_space" shows "closed(open_segment a b) \<longleftrightarrow> a = b" |
|
3089 by (metis open_segment_def DiffE closure_eq closure_open_segment ends_in_segment(1) insert_iff segment_image_interval(2)) |
|
3090 |
|
3091 lemma compact_open_segment_iff [simp]: |
|
3092 fixes a :: "'a::euclidean_space" shows "compact(open_segment a b) \<longleftrightarrow> a = b" |
|
3093 by (simp add: bounded_open_segment compact_eq_bounded_closed) |
|
3094 |
|
3095 lemma convex_closed_segment [iff]: "convex (closed_segment a b)" |
|
3096 unfolding segment_convex_hull by(rule convex_convex_hull) |
|
3097 |
|
3098 lemma convex_open_segment [iff]: "convex (open_segment a b)" |
|
3099 proof - |
|
3100 have "convex ((\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1})" |
|
3101 by (rule convex_linear_image) auto |
|
3102 then have "convex ((+) a ` (\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1})" |
|
3103 by (rule convex_translation) |
|
3104 then show ?thesis |
|
3105 by (simp add: image_image open_segment_image_interval segment_eq_compose field_simps scaleR_diff_left scaleR_diff_right) |
|
3106 qed |
|
3107 |
|
3108 lemmas convex_segment = convex_closed_segment convex_open_segment |
|
3109 |
|
3110 lemma connected_segment [iff]: |
|
3111 fixes x :: "'a :: real_normed_vector" |
|
3112 shows "connected (closed_segment x y)" |
|
3113 by (simp add: convex_connected) |
|
3114 |
|
3115 lemma is_interval_closed_segment_1[intro, simp]: "is_interval (closed_segment a b)" for a b::real |
|
3116 by (auto simp: is_interval_convex_1) |
|
3117 |
|
3118 lemma IVT'_closed_segment_real: |
|
3119 fixes f :: "real \<Rightarrow> real" |
|
3120 assumes "y \<in> closed_segment (f a) (f b)" |
|
3121 assumes "continuous_on (closed_segment a b) f" |
|
3122 shows "\<exists>x \<in> closed_segment a b. f x = y" |
|
3123 using IVT'[of f a y b] |
|
3124 IVT'[of "-f" a "-y" b] |
|
3125 IVT'[of f b y a] |
|
3126 IVT'[of "-f" b "-y" a] assms |
|
3127 by (cases "a \<le> b"; cases "f b \<ge> f a") (auto simp: closed_segment_eq_real_ivl continuous_on_minus) |
|
3128 |
2524 end |
3129 end |