23 (\<lambda>(a, b) (u, v) x. (\<Sum>i\<in>Basis. (u\<bullet>i + (x\<bullet>i - a\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (v\<bullet>i - u\<bullet>i)) *\<^sub>R i))" |
23 (\<lambda>(a, b) (u, v) x. (\<Sum>i\<in>Basis. (u\<bullet>i + (x\<bullet>i - a\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (v\<bullet>i - u\<bullet>i)) *\<^sub>R i))" |
24 |
24 |
25 lemma interval_bij_affine: |
25 lemma interval_bij_affine: |
26 "interval_bij (a,b) (u,v) = (\<lambda>x. (\<Sum>i\<in>Basis. ((v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (x\<bullet>i)) *\<^sub>R i) + |
26 "interval_bij (a,b) (u,v) = (\<lambda>x. (\<Sum>i\<in>Basis. ((v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (x\<bullet>i)) *\<^sub>R i) + |
27 (\<Sum>i\<in>Basis. (u\<bullet>i - (v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (a\<bullet>i)) *\<^sub>R i))" |
27 (\<Sum>i\<in>Basis. (u\<bullet>i - (v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (a\<bullet>i)) *\<^sub>R i))" |
28 by (auto simp: setsum_addf[symmetric] scaleR_add_left[symmetric] interval_bij_def fun_eq_iff |
28 by (auto simp: setsum.distrib[symmetric] scaleR_add_left[symmetric] interval_bij_def fun_eq_iff |
29 field_simps inner_simps add_divide_distrib[symmetric] intro!: setsum_cong) |
29 field_simps inner_simps add_divide_distrib[symmetric] intro!: setsum.cong) |
30 |
30 |
31 lemma continuous_interval_bij: |
31 lemma continuous_interval_bij: |
32 fixes a b :: "'a::euclidean_space" |
32 fixes a b :: "'a::euclidean_space" |
33 shows "continuous (at x) (interval_bij (a, b) (u, v))" |
33 shows "continuous (at x) (interval_bij (a, b) (u, v))" |
34 by (auto simp add: divide_inverse interval_bij_def intro!: continuous_setsum continuous_intros) |
34 by (auto simp add: divide_inverse interval_bij_def intro!: continuous_setsum continuous_intros) |