src/HOL/Library/Convex.thy
changeset 61694 6571c78c9667
parent 61585 a9599d3d7610
child 62376 85f38d5f8807
     1.1 --- a/src/HOL/Library/Convex.thy	Tue Nov 17 12:01:19 2015 +0100
     1.2 +++ b/src/HOL/Library/Convex.thy	Tue Nov 17 12:32:08 2015 +0000
     1.3 @@ -884,19 +884,19 @@
     1.4    assume t: "t > 0" "t < 1" and xy: "x \<in> A" "y \<in> A" "x < y"
     1.5    def z \<equiv> "(1 - t) * x + t * y"
     1.6    with \<open>connected A\<close> and xy have ivl: "{x..y} \<subseteq> A" using connected_contains_Icc by blast
     1.7 -  
     1.8 +
     1.9    from xy t have xz: "z > x" by (simp add: z_def algebra_simps)
    1.10    have "y - z = (1 - t) * (y - x)" by (simp add: z_def algebra_simps)
    1.11    also from xy t have "... > 0" by (intro mult_pos_pos) simp_all
    1.12    finally have yz: "z < y" by simp
    1.13 -    
    1.14 +
    1.15    from assms xz yz ivl t have "\<exists>\<xi>. \<xi> > x \<and> \<xi> < z \<and> f z - f x = (z - x) * f' \<xi>"
    1.16      by (intro MVT2) (auto intro!: assms(2))
    1.17    then obtain \<xi> where \<xi>: "\<xi> > x" "\<xi> < z" "f' \<xi> = (f z - f x) / (z - x)" by auto
    1.18    from assms xz yz ivl t have "\<exists>\<eta>. \<eta> > z \<and> \<eta> < y \<and> f y - f z = (y - z) * f' \<eta>"
    1.19      by (intro MVT2) (auto intro!: assms(2))
    1.20    then obtain \<eta> where \<eta>: "\<eta> > z" "\<eta> < y" "f' \<eta> = (f y - f z) / (y - z)" by auto
    1.21 -  
    1.22 +
    1.23    from \<eta>(3) have "(f y - f z) / (y - z) = f' \<eta>" ..
    1.24    also from \<xi> \<eta> ivl have "\<xi> \<in> A" "\<eta> \<in> A" by auto
    1.25    with \<xi> \<eta> have "f' \<eta> \<ge> f' \<xi>" by (intro assms(3)) auto
    1.26 @@ -926,11 +926,11 @@
    1.27  proof (cases y x rule: linorder_cases)
    1.28    assume less: "x < y"
    1.29    hence d: "d > 0" by (simp add: d_def)
    1.30 -  from assms(2) less have A: "0 \<le> (c - x) / d" "(c - x) / d \<le> 1" 
    1.31 +  from assms(2) less have A: "0 \<le> (c - x) / d" "(c - x) / d \<le> 1"
    1.32      by (simp_all add: d_def divide_simps)
    1.33    have "f c = f (x + (c - x) * 1)" by simp
    1.34    also from less have "1 = ((y - x) / d)" by (simp add: d_def)
    1.35 -  also from d have "x + (c - x) * \<dots> = (1 - (c - x) / d) *\<^sub>R x + ((c - x) / d) *\<^sub>R y" 
    1.36 +  also from d have "x + (c - x) * \<dots> = (1 - (c - x) / d) *\<^sub>R x + ((c - x) / d) *\<^sub>R y"
    1.37      by (simp add: field_simps)
    1.38    also have "f \<dots> \<le> (1 - (c - x) / d) * f x + (c - x) / d * f y" using assms less
    1.39      by (intro convex_onD_Icc) simp_all
    1.40 @@ -945,11 +945,11 @@
    1.41  proof (cases y x rule: linorder_cases)
    1.42    assume less: "x < y"
    1.43    hence d: "d > 0" by (simp add: d_def)
    1.44 -  from assms(2) less have A: "0 \<le> (y - c) / d" "(y - c) / d \<le> 1" 
    1.45 +  from assms(2) less have A: "0 \<le> (y - c) / d" "(y - c) / d \<le> 1"
    1.46      by (simp_all add: d_def divide_simps)
    1.47    have "f c = f (y - (y - c) * 1)" by simp
    1.48    also from less have "1 = ((y - x) / d)" by (simp add: d_def)
    1.49 -  also from d have "y - (y - c) * \<dots> = (1 - (1 - (y - c) / d)) *\<^sub>R x + (1 - (y - c) / d) *\<^sub>R y" 
    1.50 +  also from d have "y - (y - c) * \<dots> = (1 - (1 - (y - c) / d)) *\<^sub>R x + (1 - (y - c) / d) *\<^sub>R y"
    1.51      by (simp add: field_simps)
    1.52    also have "f \<dots> \<le> (1 - (1 - (y - c) / d)) * f x + (1 - (y - c) / d) * f y" using assms less
    1.53      by (intro convex_onD_Icc) (simp_all add: field_simps)