2551 THEN has_derivative_eq_rhs]) |
2545 THEN has_derivative_eq_rhs]) |
2552 subgoal by (rule f'[unfolded has_vector_derivative_def]; assumption) |
2546 subgoal by (rule f'[unfolded has_vector_derivative_def]; assumption) |
2553 subgoal by (rule g'[unfolded has_vector_derivative_def]; assumption) |
2547 subgoal by (rule g'[unfolded has_vector_derivative_def]; assumption) |
2554 by (auto simp: assms) |
2548 by (auto simp: assms) |
2555 |
2549 |
|
2550 subsection\<^marker>\<open>tag important\<close>\<open>The Inverse Function Theorem\<close> |
|
2551 |
|
2552 lemma linear_injective_contraction: |
|
2553 assumes "linear f" "c < 1" and le: "\<And>x. norm (f x - x) \<le> c * norm x" |
|
2554 shows "inj f" |
|
2555 unfolding linear_injective_0[OF \<open>linear f\<close>] |
|
2556 proof safe |
|
2557 fix x |
|
2558 assume "f x = 0" |
|
2559 with le [of x] have "norm x \<le> c * norm x" |
|
2560 by simp |
|
2561 then show "x = 0" |
|
2562 using \<open>c < 1\<close> by (simp add: mult_le_cancel_right1) |
|
2563 qed |
|
2564 |
|
2565 text\<open>From an online proof by J. Michael Boardman, Department of Mathematics, Johns Hopkins University\<close> |
|
2566 lemma inverse_function_theorem_scaled: |
|
2567 fixes f::"'a::euclidean_space \<Rightarrow> 'a" |
|
2568 and f'::"'a \<Rightarrow> ('a \<Rightarrow>\<^sub>L 'a)" |
|
2569 assumes "open U" |
|
2570 and derf: "\<And>x. x \<in> U \<Longrightarrow> (f has_derivative blinfun_apply (f' x)) (at x)" |
|
2571 and contf: "continuous_on U f'" |
|
2572 and "0 \<in> U" and [simp]: "f 0 = 0" |
|
2573 and id: "f' 0 = id_blinfun" |
|
2574 obtains U' V g g' where "open U'" "U' \<subseteq> U" "0 \<in> U'" "open V" "0 \<in> V" "homeomorphism U' V f g" |
|
2575 "\<And>y. y \<in> V \<Longrightarrow> (g has_derivative (g' y)) (at y)" |
|
2576 "\<And>y. y \<in> V \<Longrightarrow> g' y = inv (blinfun_apply (f'(g y)))" |
|
2577 "\<And>y. y \<in> V \<Longrightarrow> bij (blinfun_apply (f'(g y)))" |
|
2578 proof - |
|
2579 obtain d1 where "cball 0 d1 \<subseteq> U" "d1 > 0" |
|
2580 using \<open>open U\<close> \<open>0 \<in> U\<close> open_contains_cball by blast |
|
2581 obtain d2 where d2: "\<And>x. \<lbrakk>x \<in> U; dist x 0 \<le> d2\<rbrakk> \<Longrightarrow> dist (f' x) (f' 0) < 1/2" "0 < d2" |
|
2582 using continuous_onE [OF contf, of 0 "1/2"] by (metis \<open>0 \<in> U\<close> half_gt_zero_iff zero_less_one) |
|
2583 obtain \<delta> where le: "\<And>x. norm x \<le> \<delta> \<Longrightarrow> dist (f' x) id_blinfun \<le> 1/2" and "0 < \<delta>" |
|
2584 and subU: "cball 0 \<delta> \<subseteq> U" |
|
2585 proof |
|
2586 show "min d1 d2 > 0" |
|
2587 by (simp add: \<open>0 < d1\<close> \<open>0 < d2\<close>) |
|
2588 show "cball 0 (min d1 d2) \<subseteq> U" |
|
2589 using \<open>cball 0 d1 \<subseteq> U\<close> by auto |
|
2590 show "dist (f' x) id_blinfun \<le> 1/2" if "norm x \<le> min d1 d2" for x |
|
2591 using \<open>cball 0 d1 \<subseteq> U\<close> d2 that id by fastforce |
|
2592 qed |
|
2593 let ?D = "cball 0 \<delta>" |
|
2594 define V:: "'a set" where "V \<equiv> ball 0 (\<delta>/2)" |
|
2595 have 4: "norm (f (x + h) - f x - h) \<le> 1/2 * norm h" |
|
2596 if "x \<in> ?D" "x+h \<in> ?D" for x h |
|
2597 proof - |
|
2598 let ?w = "\<lambda>x. f x - x" |
|
2599 have B: "\<And>x. x \<in> ?D \<Longrightarrow> onorm (blinfun_apply (f' x - id_blinfun)) \<le> 1/2" |
|
2600 by (metis dist_norm le mem_cball_0 norm_blinfun.rep_eq) |
|
2601 have "\<And>x. x \<in> ?D \<Longrightarrow> (?w has_derivative (blinfun_apply (f' x - id_blinfun))) (at x)" |
|
2602 by (rule derivative_eq_intros derf subsetD [OF subU] | force simp: blinfun.diff_left)+ |
|
2603 then have Dw: "\<And>x. x \<in> ?D \<Longrightarrow> (?w has_derivative (blinfun_apply (f' x - id_blinfun))) (at x within ?D)" |
|
2604 using has_derivative_at_withinI by blast |
|
2605 have "norm (?w (x+h) - ?w x) \<le> (1/2) * norm h" |
|
2606 using differentiable_bound [OF convex_cball Dw B] that by fastforce |
|
2607 then show ?thesis |
|
2608 by (auto simp: algebra_simps) |
|
2609 qed |
|
2610 have for_g: "\<exists>!x. norm x < \<delta> \<and> f x = y" if y: "norm y < \<delta>/2" for y |
|
2611 proof - |
|
2612 let ?u = "\<lambda>x. x + (y - f x)" |
|
2613 have *: "norm (?u x) < \<delta>" if "x \<in> ?D" for x |
|
2614 proof - |
|
2615 have fxx: "norm (f x - x) \<le> \<delta>/2" |
|
2616 using 4 [of 0 x] \<open>0 < \<delta>\<close> \<open>f 0 = 0\<close> that by auto |
|
2617 have "norm (?u x) \<le> norm y + norm (f x - x)" |
|
2618 by (metis add.commute add_diff_eq norm_minus_commute norm_triangle_ineq) |
|
2619 also have "\<dots> < \<delta>/2 + \<delta>/2" |
|
2620 using fxx y by auto |
|
2621 finally show ?thesis |
|
2622 by simp |
|
2623 qed |
|
2624 have "\<exists>!x \<in> ?D. ?u x = x" |
|
2625 proof (rule banach_fix) |
|
2626 show "cball 0 \<delta> \<noteq> {}" |
|
2627 using \<open>0 < \<delta>\<close> by auto |
|
2628 show "(\<lambda>x. x + (y - f x)) ` cball 0 \<delta> \<subseteq> cball 0 \<delta>" |
|
2629 using * by force |
|
2630 have "dist (x + (y - f x)) (xh + (y - f xh)) * 2 \<le> dist x xh" |
|
2631 if "norm x \<le> \<delta>" and "norm xh \<le> \<delta>" for x xh |
|
2632 using that 4 [of x "xh-x"] by (auto simp: dist_norm norm_minus_commute algebra_simps) |
|
2633 then show "\<forall>x\<in>cball 0 \<delta>. \<forall>ya\<in>cball 0 \<delta>. dist (x + (y - f x)) (ya + (y - f ya)) \<le> (1/2) * dist x ya" |
|
2634 by auto |
|
2635 qed (auto simp: complete_eq_closed) |
|
2636 then show ?thesis |
|
2637 by (metis "*" add_cancel_right_right eq_iff_diff_eq_0 le_less mem_cball_0) |
|
2638 qed |
|
2639 define g where "g \<equiv> \<lambda>y. THE x. norm x < \<delta> \<and> f x = y" |
|
2640 have g: "norm (g y) < \<delta> \<and> f (g y) = y" if "norm y < \<delta>/2" for y |
|
2641 unfolding g_def using that theI' [OF for_g] by meson |
|
2642 then have fg[simp]: "f (g y) = y" if "y \<in> V" for y |
|
2643 using that by (auto simp: V_def) |
|
2644 have 5: "norm (g y' - g y) \<le> 2 * norm (y' - y)" if "y \<in> V" "y' \<in> V" for y y' |
|
2645 proof - |
|
2646 have no: "norm (g y) \<le> \<delta>" "norm (g y') \<le> \<delta>" and [simp]: "f (g y) = y" |
|
2647 using that g unfolding V_def by force+ |
|
2648 have "norm (g y' - g y) \<le> norm (g y' - g y - (y' - y)) + norm (y' - y)" |
|
2649 by (simp add: add.commute norm_triangle_sub) |
|
2650 also have "\<dots> \<le> (1/2) * norm (g y' - g y) + norm (y' - y)" |
|
2651 using 4 [of "g y" "g y' - g y"] that no by (simp add: g norm_minus_commute V_def) |
|
2652 finally show ?thesis |
|
2653 by auto |
|
2654 qed |
|
2655 have contg: "continuous_on V g" |
|
2656 proof |
|
2657 fix y::'a and e::real |
|
2658 assume "0 < e" and y: "y \<in> V" |
|
2659 show "\<exists>d>0. \<forall>x'\<in>V. dist x' y < d \<longrightarrow> dist (g x') (g y) \<le> e" |
|
2660 proof (intro exI conjI ballI impI) |
|
2661 show "0 < e/2" |
|
2662 by (simp add: \<open>0 < e\<close>) |
|
2663 qed (use 5 y in \<open>force simp: dist_norm\<close>) |
|
2664 qed |
|
2665 show thesis |
|
2666 proof |
|
2667 define U' where "U' \<equiv> (f -` V) \<inter> ball 0 \<delta>" |
|
2668 have contf: "continuous_on U f" |
|
2669 using derf has_derivative_at_withinI by (fast intro: has_derivative_continuous_on) |
|
2670 then have "continuous_on (ball 0 \<delta>) f" |
|
2671 by (meson ball_subset_cball continuous_on_subset subU) |
|
2672 then show "open U'" |
|
2673 by (simp add: U'_def V_def Int_commute continuous_open_preimage) |
|
2674 show "0 \<in> U'" "U' \<subseteq> U" "open V" "0 \<in> V" |
|
2675 using \<open>0 < \<delta>\<close> subU by (auto simp: U'_def V_def) |
|
2676 show hom: "homeomorphism U' V f g" |
|
2677 proof |
|
2678 show "continuous_on U' f" |
|
2679 using \<open>U' \<subseteq> U\<close> contf continuous_on_subset by blast |
|
2680 show "continuous_on V g" |
|
2681 using contg by blast |
|
2682 show "f ` U' \<subseteq> V" |
|
2683 using U'_def by blast |
|
2684 show "g ` V \<subseteq> U'" |
|
2685 by (simp add: U'_def V_def g image_subset_iff) |
|
2686 show "g (f x) = x" if "x \<in> U'" for x |
|
2687 by (metis that fg Int_iff U'_def V_def for_g g mem_ball_0 vimage_eq) |
|
2688 show "f (g y) = y" if "y \<in> V" for y |
|
2689 using that by (simp add: g V_def) |
|
2690 qed |
|
2691 show bij: "bij (blinfun_apply (f'(g y)))" if "y \<in> V" for y |
|
2692 proof - |
|
2693 have inj: "inj (blinfun_apply (f' (g y)))" |
|
2694 proof (rule linear_injective_contraction) |
|
2695 show "linear (blinfun_apply (f' (g y)))" |
|
2696 using blinfun.bounded_linear_right bounded_linear_def by blast |
|
2697 next |
|
2698 fix x |
|
2699 have "norm (blinfun_apply (f' (g y)) x - x) = norm (blinfun_apply (f' (g y) - id_blinfun) x)" |
|
2700 by (simp add: blinfun.diff_left) |
|
2701 also have "\<dots> \<le> norm (f' (g y) - id_blinfun) * norm x" |
|
2702 by (rule norm_blinfun) |
|
2703 also have "\<dots> \<le> (1/2) * norm x" |
|
2704 proof (rule mult_right_mono) |
|
2705 show "norm (f' (g y) - id_blinfun) \<le> 1/2" |
|
2706 using that g [of y] le by (auto simp: V_def dist_norm) |
|
2707 qed auto |
|
2708 finally show "norm (blinfun_apply (f' (g y)) x - x) \<le> (1/2) * norm x" . |
|
2709 qed auto |
|
2710 moreover |
|
2711 have "surj (blinfun_apply (f' (g y)))" |
|
2712 using blinfun.bounded_linear_right bounded_linear_def |
|
2713 by (blast intro!: linear_inj_imp_surj [OF _ inj]) |
|
2714 ultimately show ?thesis |
|
2715 using bijI by blast |
|
2716 qed |
|
2717 define g' where "g' \<equiv> \<lambda>y. inv (blinfun_apply (f'(g y)))" |
|
2718 show "(g has_derivative g' y) (at y)" if "y \<in> V" for y |
|
2719 proof - |
|
2720 have gy: "g y \<in> U" |
|
2721 using g subU that unfolding V_def by fastforce |
|
2722 obtain e where e: "\<And>h. f (g y + h) = y + blinfun_apply (f' (g y)) h + e h" |
|
2723 and e0: "(\<lambda>h. norm (e h) / norm h) \<midarrow>0\<rightarrow> 0" |
|
2724 using iffD1 [OF has_derivative_iff_Ex derf [OF gy]] \<open>y \<in> V\<close> by auto |
|
2725 have [simp]: "e 0 = 0" |
|
2726 using e [of 0] that by simp |
|
2727 let ?INV = "inv (blinfun_apply (f' (g y)))" |
|
2728 have inj: "inj (blinfun_apply (f' (g y)))" |
|
2729 using bij bij_betw_def that by blast |
|
2730 have "(g has_derivative g' y) (at y within V)" |
|
2731 unfolding has_derivative_at_within_iff_Ex [OF \<open>y \<in> V\<close> \<open>open V\<close>] |
|
2732 proof |
|
2733 show blinv: "bounded_linear (g' y)" |
|
2734 unfolding g'_def using derf gy inj inj_linear_imp_inv_bounded_linear by blast |
|
2735 define eg where "eg \<equiv> \<lambda>k. - ?INV (e (g (y+k) - g y))" |
|
2736 have "g (y+k) = g y + g' y k + eg k" if "y + k \<in> V" for k |
|
2737 proof - |
|
2738 have "?INV k = ?INV (blinfun_apply (f' (g y)) (g (y+k) - g y) + e (g (y+k) - g y))" |
|
2739 using e [of "g(y+k) - g y"] that by simp |
|
2740 then have "g (y+k) = g y + ?INV k - ?INV (e (g (y+k) - g y))" |
|
2741 using inj blinv by (simp add: linear_simps g'_def) |
|
2742 then show ?thesis |
|
2743 by (auto simp: eg_def g'_def) |
|
2744 qed |
|
2745 moreover have "(\<lambda>k. norm (eg k) / norm k) \<midarrow>0\<rightarrow> 0" |
|
2746 proof (rule Lim_null_comparison) |
|
2747 let ?g = "\<lambda>k. 2 * onorm ?INV * norm (e (g (y+k) - g y)) / norm (g (y+k) - g y)" |
|
2748 show "\<forall>\<^sub>F k in at 0. norm (norm (eg k) / norm k) \<le> ?g k" |
|
2749 unfolding eventually_at_topological |
|
2750 proof (intro exI conjI ballI impI) |
|
2751 show "open ((+)(-y) ` V)" |
|
2752 using \<open>open V\<close> open_translation by blast |
|
2753 show "0 \<in> (+)(-y) ` V" |
|
2754 by (simp add: that) |
|
2755 show "norm (norm (eg k) / norm k) \<le> 2 * onorm (inv (blinfun_apply (f' (g y)))) * norm (e (g (y+k) - g y)) / norm (g (y+k) - g y)" |
|
2756 if "k \<in> (+)(-y) ` V" "k \<noteq> 0" for k |
|
2757 proof - |
|
2758 have "y+k \<in> V" |
|
2759 using that by auto |
|
2760 have "norm (norm (eg k) / norm k) \<le> onorm ?INV * norm (e (g (y+k) - g y)) / norm k" |
|
2761 using blinv g'_def onorm by (force simp: eg_def divide_simps) |
|
2762 also have "\<dots> = (norm (g (y+k) - g y) / norm k) * (onorm ?INV * (norm (e (g (y+k) - g y)) / norm (g (y+k) - g y)))" |
|
2763 by (simp add: divide_simps) |
|
2764 also have "\<dots> \<le> 2 * (onorm ?INV * (norm (e (g (y+k) - g y)) / norm (g (y+k) - g y)))" |
|
2765 apply (rule mult_right_mono) |
|
2766 using 5 [of y "y+k"] \<open>y \<in> V\<close> \<open>y + k \<in> V\<close> onorm_pos_le [OF blinv] |
|
2767 apply (auto simp: divide_simps zero_le_mult_iff zero_le_divide_iff g'_def) |
|
2768 done |
|
2769 finally show "norm (norm (eg k) / norm k) \<le> 2 * onorm ?INV * norm (e (g (y+k) - g y)) / norm (g (y+k) - g y)" |
|
2770 by simp |
|
2771 qed |
|
2772 qed |
|
2773 have 1: "(\<lambda>h. norm (e h) / norm h) \<midarrow>0\<rightarrow> (norm (e 0) / norm 0)" |
|
2774 using e0 by auto |
|
2775 have 2: "(\<lambda>k. g (y+k) - g y) \<midarrow>0\<rightarrow> 0" |
|
2776 using contg \<open>open V\<close> \<open>y \<in> V\<close> LIM_offset_zero_iff LIM_zero_iff at_within_open continuous_on_def by fastforce |
|
2777 from tendsto_compose [OF 1 2, simplified] |
|
2778 have "(\<lambda>k. norm (e (g (y+k) - g y)) / norm (g (y+k) - g y)) \<midarrow>0\<rightarrow> 0" . |
|
2779 from tendsto_mult_left [OF this] show "?g \<midarrow>0\<rightarrow> 0" by auto |
|
2780 qed |
|
2781 ultimately show "\<exists>e. (\<forall>k. y + k \<in> V \<longrightarrow> g (y+k) = g y + g' y k + e k) \<and> (\<lambda>k. norm (e k) / norm k) \<midarrow>0\<rightarrow> 0" |
|
2782 by blast |
|
2783 qed |
|
2784 then show ?thesis |
|
2785 by (metis \<open>open V\<close> at_within_open that) |
|
2786 qed |
|
2787 show "g' y = inv (blinfun_apply (f' (g y)))" |
|
2788 if "y \<in> V" for y |
|
2789 by (simp add: g'_def) |
|
2790 qed |
|
2791 qed |
|
2792 |
|
2793 |
|
2794 text\<open>We need all this to justify the scaling and translations.\<close> |
|
2795 theorem inverse_function_theorem: |
|
2796 fixes f::"'a::euclidean_space \<Rightarrow> 'a" |
|
2797 and f'::"'a \<Rightarrow> ('a \<Rightarrow>\<^sub>L 'a)" |
|
2798 assumes "open U" |
|
2799 and derf: "\<And>x. x \<in> U \<Longrightarrow> (f has_derivative (blinfun_apply (f' x))) (at x)" |
|
2800 and contf: "continuous_on U f'" |
|
2801 and "x0 \<in> U" |
|
2802 and invf: "invf o\<^sub>L f' x0 = id_blinfun" |
|
2803 obtains U' V g g' where "open U'" "U' \<subseteq> U" "x0 \<in> U'" "open V" "f x0 \<in> V" "homeomorphism U' V f g" |
|
2804 "\<And>y. y \<in> V \<Longrightarrow> (g has_derivative (g' y)) (at y)" |
|
2805 "\<And>y. y \<in> V \<Longrightarrow> g' y = inv (blinfun_apply (f'(g y)))" |
|
2806 "\<And>y. y \<in> V \<Longrightarrow> bij (blinfun_apply (f'(g y)))" |
|
2807 proof - |
|
2808 have apply1 [simp]: "\<And>i. blinfun_apply invf (blinfun_apply (f' x0) i) = i" |
|
2809 by (metis blinfun_apply_blinfun_compose blinfun_apply_id_blinfun invf) |
|
2810 have apply2 [simp]: "\<And>i. blinfun_apply (f' x0) (blinfun_apply invf i) = i" |
|
2811 by (metis apply1 bij_inv_eq_iff blinfun_bij1 invf) |
|
2812 have [simp]: "(range (blinfun_apply invf)) = UNIV" |
|
2813 using apply1 surjI by blast |
|
2814 let ?f = "invf \<circ> (\<lambda>x. (f \<circ> (+)x0)x - f x0)" |
|
2815 let ?f' = "\<lambda>x. invf o\<^sub>L (f' (x + x0))" |
|
2816 obtain U' V g g' where "open U'" and U': "U' \<subseteq> (+)(-x0) ` U" "0 \<in> U'" |
|
2817 and "open V" "0 \<in> V" and hom: "homeomorphism U' V ?f g" |
|
2818 and derg: "\<And>y. y \<in> V \<Longrightarrow> (g has_derivative (g' y)) (at y)" |
|
2819 and g': "\<And>y. y \<in> V \<Longrightarrow> g' y = inv (?f'(g y))" |
|
2820 and bij: "\<And>y. y \<in> V \<Longrightarrow> bij (?f'(g y))" |
|
2821 proof (rule inverse_function_theorem_scaled [of "(+)(-x0) ` U" ?f "?f'"]) |
|
2822 show ope: "open ((+) (- x0) ` U)" |
|
2823 using \<open>open U\<close> open_translation by blast |
|
2824 show "(?f has_derivative blinfun_apply (?f' x)) (at x)" |
|
2825 if "x \<in> (+) (- x0) ` U" for x |
|
2826 using that |
|
2827 apply clarify |
|
2828 apply (rule derf derivative_eq_intros | simp add: blinfun_compose.rep_eq)+ |
|
2829 done |
|
2830 have YY: "(\<lambda>x. f' (x + x0)) \<midarrow>u-x0\<rightarrow> f' u" |
|
2831 if "f' \<midarrow>u\<rightarrow> f' u" "u \<in> U" for u |
|
2832 using that LIM_offset [where k = x0] by (auto simp: algebra_simps) |
|
2833 then have "continuous_on ((+) (- x0) ` U) (\<lambda>x. f' (x + x0))" |
|
2834 using contf \<open>open U\<close> Lim_at_imp_Lim_at_within |
|
2835 by (fastforce simp: continuous_on_def at_within_open_NO_MATCH ope) |
|
2836 then show "continuous_on ((+) (- x0) ` U) ?f'" |
|
2837 by (intro continuous_intros) simp |
|
2838 qed (auto simp: invf \<open>x0 \<in> U\<close>) |
|
2839 show thesis |
|
2840 proof |
|
2841 let ?U' = "(+)x0 ` U'" |
|
2842 let ?V = "((+)(f x0) \<circ> f' x0) ` V" |
|
2843 let ?g = "(+)x0 \<circ> g \<circ> invf \<circ> (+)(- f x0)" |
|
2844 let ?g' = "\<lambda>y. inv (blinfun_apply (f' (?g y)))" |
|
2845 show oU': "open ?U'" |
|
2846 by (simp add: \<open>open U'\<close> open_translation) |
|
2847 show subU: "?U' \<subseteq> U" |
|
2848 using ComplI \<open>U' \<subseteq> (+) (- x0) ` U\<close> by auto |
|
2849 show "x0 \<in> ?U'" |
|
2850 by (simp add: \<open>0 \<in> U'\<close>) |
|
2851 show "open ?V" |
|
2852 using blinfun_bij2 [OF invf] |
|
2853 by (metis \<open>open V\<close> bij_is_surj blinfun.bounded_linear_right bounded_linear_def image_comp open_surjective_linear_image open_translation) |
|
2854 show "f x0 \<in> ?V" |
|
2855 using \<open>0 \<in> V\<close> image_iff by fastforce |
|
2856 show "homeomorphism ?U' ?V f ?g" |
|
2857 proof |
|
2858 show "continuous_on ?U' f" |
|
2859 by (meson subU continuous_on_eq_continuous_at derf has_derivative_continuous oU' subsetD) |
|
2860 have "?f ` U' \<subseteq> V" |
|
2861 using hom homeomorphism_image1 by blast |
|
2862 then show "f ` ?U' \<subseteq> ?V" |
|
2863 unfolding image_subset_iff |
|
2864 by (clarsimp simp: image_def) (metis apply2 add.commute diff_add_cancel) |
|
2865 show "?g ` ?V \<subseteq> ?U'" |
|
2866 using hom invf by (auto simp: image_def homeomorphism_def) |
|
2867 show "?g (f x) = x" |
|
2868 if "x \<in> ?U'" for x |
|
2869 using that hom homeomorphism_apply1 by fastforce |
|
2870 have "continuous_on V g" |
|
2871 using hom homeomorphism_def by blast |
|
2872 then show "continuous_on ?V ?g" |
|
2873 by (intro continuous_intros) (auto elim!: continuous_on_subset) |
|
2874 have fg: "?f (g x) = x" if "x \<in> V" for x |
|
2875 using hom homeomorphism_apply2 that by blast |
|
2876 show "f (?g y) = y" |
|
2877 if "y \<in> ?V" for y |
|
2878 using that fg by (simp add: image_iff) (metis apply2 add.commute diff_add_cancel) |
|
2879 qed |
|
2880 show "(?g has_derivative ?g' y) (at y)" "bij (blinfun_apply (f' (?g y)))" |
|
2881 if "y \<in> ?V" for y |
|
2882 proof - |
|
2883 have 1: "bij (blinfun_apply invf)" |
|
2884 using blinfun_bij1 invf by blast |
|
2885 then have 2: "bij (blinfun_apply (f' (x0 + g x)))" if "x \<in> V" for x |
|
2886 by (metis add.commute bij bij_betw_comp_iff2 blinfun_compose.rep_eq that top_greatest) |
|
2887 then show "bij (blinfun_apply (f' (?g y)))" |
|
2888 using that by auto |
|
2889 have "g' x \<circ> blinfun_apply invf = inv (blinfun_apply (f' (x0 + g x)))" |
|
2890 if "x \<in> V" for x |
|
2891 using that |
|
2892 by (simp add: g' o_inv_distrib blinfun_compose.rep_eq 1 2 add.commute bij_is_inj flip: o_assoc) |
|
2893 then show "(?g has_derivative ?g' y) (at y)" |
|
2894 using that invf |
|
2895 by clarsimp (rule derg derivative_eq_intros | simp flip: id_def)+ |
|
2896 qed |
|
2897 qed auto |
|
2898 qed |
|
2899 |
2556 end |
2900 end |