src/HOL/Analysis/Simplex_Content.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 months ago)
changeset 69981 3dced198b9ec
parent 69737 ec3cc98c38db
permissions -rw-r--r--
more strict AFP properties;
eberlm@68625
     1
(*
eberlm@68625
     2
   File:      Analysis/Simplex_Content.thy
eberlm@68625
     3
   Author:    Manuel Eberl <eberlm@in.tum.de>
eberlm@68625
     4
eberlm@68625
     5
   The content of an n-dimensional simplex, including the formula for the content of a
eberlm@68625
     6
   triangle and Heron's formula.
eberlm@68625
     7
*)
ak2110@69737
     8
section \<open>Volume of a Simplex\<close>
nipkow@69517
     9
eberlm@68625
    10
theory Simplex_Content
nipkow@69517
    11
imports Change_Of_Vars
eberlm@68625
    12
begin
eberlm@68625
    13
eberlm@68625
    14
lemma fact_neq_top_ennreal [simp]: "fact n \<noteq> (top :: ennreal)"
eberlm@68625
    15
  by (induction n) (auto simp: ennreal_mult_eq_top_iff)
eberlm@68625
    16
eberlm@68625
    17
lemma ennreal_fact: "ennreal (fact n) = fact n"
eberlm@68625
    18
  by (induction n) (auto simp: ennreal_mult algebra_simps ennreal_of_nat_eq_real_of_nat)
eberlm@68625
    19
eberlm@68625
    20
context
eberlm@68625
    21
  fixes S :: "'a set \<Rightarrow> real \<Rightarrow> ('a \<Rightarrow> real) set"
eberlm@68625
    22
  defines "S \<equiv> (\<lambda>A t. {x. (\<forall>i\<in>A. 0 \<le> x i) \<and> sum x A \<le> t})"
eberlm@68625
    23
begin
eberlm@68625
    24
eberlm@68625
    25
lemma emeasure_std_simplex_aux_step:
eberlm@68625
    26
  assumes "b \<notin> A" "finite A"
eberlm@68625
    27
  shows   "x(b := y) \<in> S (insert b A) t \<longleftrightarrow> y \<in> {0..t} \<and> x \<in> S A (t - y)"
eberlm@68625
    28
  using assms sum_nonneg[of A x] unfolding S_def
eberlm@68625
    29
  by (force simp: sum_delta_notmem algebra_simps)
eberlm@68625
    30
ak2110@69737
    31
lemma emeasure_std_simplex_aux:
eberlm@68625
    32
  fixes t :: real
eberlm@68625
    33
  assumes "finite (A :: 'a set)" "t \<ge> 0"
eberlm@68625
    34
  shows   "emeasure (Pi\<^sub>M A (\<lambda>_. lborel)) 
eberlm@68625
    35
             (S A t \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) = t ^ card A / fact (card A)"
eberlm@68625
    36
  using assms(1,2)
ak2110@69737
    37
proof (induction arbitrary: t rule: finite_induct)
eberlm@68625
    38
  case (empty t)
eberlm@68625
    39
  thus ?case by (simp add: PiM_empty S_def)
eberlm@68625
    40
next
eberlm@68625
    41
  case (insert b A t)
eberlm@68625
    42
  define n where "n = Suc (card A)"
eberlm@68625
    43
  have n_pos: "n > 0" by (simp add: n_def)
eberlm@68625
    44
  let ?M = "\<lambda>A. (Pi\<^sub>M A (\<lambda>_. lborel))"
eberlm@68625
    45
  {
eberlm@68625
    46
    fix A :: "'a set" and t :: real assume "finite A" 
eberlm@68625
    47
    have "S A t \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel)) =
eberlm@68625
    48
            Pi\<^sub>E A (\<lambda>_. {0..}) \<inter> (\<lambda>x. sum x A) -` {..t} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))"
eberlm@68625
    49
      by (auto simp: S_def space_PiM)
eberlm@68625
    50
    also have "\<dots> \<in> sets (Pi\<^sub>M A (\<lambda>_. lborel))"
eberlm@68625
    51
      using \<open>finite A\<close> by measurable
eberlm@68625
    52
    finally have "S A t \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel)) \<in> sets (Pi\<^sub>M A (\<lambda>_. lborel))" .
eberlm@68625
    53
  } note meas [measurable] = this
eberlm@68625
    54
eberlm@68625
    55
  interpret product_sigma_finite "\<lambda>_. lborel"
eberlm@68625
    56
    by standard
eberlm@68625
    57
  have "emeasure (?M (insert b A)) (S (insert b A) t \<inter> space (?M (insert b A))) =
eberlm@68625
    58
        nn_integral (?M (insert b A))
eberlm@68625
    59
          (\<lambda>x. indicator (S (insert b A) t \<inter> space (?M (insert b A))) x)"
eberlm@68625
    60
    using insert.hyps by (subst nn_integral_indicator) auto
eberlm@68625
    61
  also have "\<dots> = (\<integral>\<^sup>+ y. \<integral>\<^sup>+ x. indicator (S (insert b A) t \<inter> space (?M (insert b A)))
eberlm@68625
    62
                    (x(b := y)) \<partial>?M A \<partial>lborel)"
eberlm@68625
    63
    using insert.prems insert.hyps by (intro product_nn_integral_insert_rev) auto
eberlm@68625
    64
  also have "\<dots> = (\<integral>\<^sup>+ y. \<integral>\<^sup>+ x. indicator {0..t} y * indicator (S A (t - y) \<inter> space (?M A)) x
eberlm@68625
    65
                    \<partial>?M A \<partial>lborel)"
eberlm@68625
    66
    using insert.hyps insert.prems emeasure_std_simplex_aux_step[of b A]
eberlm@68625
    67
    by (intro nn_integral_cong)
eberlm@68625
    68
       (auto simp: fun_eq_iff indicator_def space_PiM PiE_def extensional_def)
eberlm@68625
    69
  also have "\<dots> = (\<integral>\<^sup>+ y. indicator {0..t} y * (\<integral>\<^sup>+ x. indicator (S A (t - y) \<inter> space (?M A)) x
eberlm@68625
    70
                    \<partial>?M A) \<partial>lborel)" using \<open>finite A\<close>
eberlm@68625
    71
    by (subst nn_integral_cmult) auto
eberlm@68625
    72
  also have "\<dots> = (\<integral>\<^sup>+ y. indicator {0..t} y * emeasure (?M A) (S A (t - y) \<inter> space (?M A)) \<partial>lborel)"
eberlm@68625
    73
    using \<open>finite A\<close> by (subst nn_integral_indicator) auto
eberlm@68625
    74
  also have "\<dots> = (\<integral>\<^sup>+ y. indicator {0..t} y * (t - y) ^ card A / ennreal (fact (card A)) \<partial>lborel)"
eberlm@68625
    75
    using insert.IH by (intro nn_integral_cong) (auto simp: indicator_def divide_ennreal)
eberlm@68625
    76
  also have "\<dots> = (\<integral>\<^sup>+ y. indicator {0..t} y * (t - y) ^ card A \<partial>lborel) / ennreal (fact (card A))"
eberlm@68625
    77
    using \<open>finite A\<close> by (subst nn_integral_divide) auto
eberlm@68625
    78
  also have "(\<integral>\<^sup>+ y. indicator {0..t} y * (t - y) ^ card A \<partial>lborel) = 
eberlm@68625
    79
               (\<integral>\<^sup>+y\<in>{0..t}. ennreal ((t - y) ^ (n - 1)) \<partial>lborel)"
eberlm@68625
    80
    by (intro nn_integral_cong) (auto simp: indicator_def n_def)
eberlm@68625
    81
  also have "((\<lambda>x. - ((t - x) ^ n / n)) has_real_derivative (t - x) ^ (n - 1)) (at x)" 
eberlm@68625
    82
    if "x \<in> {0..t}" for x by (rule derivative_eq_intros refl | simp add: n_pos)+
eberlm@68625
    83
  hence "(\<integral>\<^sup>+y\<in>{0..t}. ennreal ((t - y) ^ (n - 1)) \<partial>lborel) = 
eberlm@68625
    84
           ennreal (-((t - t) ^ n / n) - (-((t - 0) ^ n / n)))"
eberlm@68625
    85
    using insert.prems insert.hyps by (intro nn_integral_FTC_Icc) auto
eberlm@68625
    86
  also have "\<dots> = ennreal (t ^ n / n)" using n_pos by (simp add: zero_power)
eberlm@68625
    87
  also have "\<dots> / ennreal (fact (card A)) = ennreal (t ^ n / n / fact (card A))"
eberlm@68625
    88
    using n_pos \<open>t \<ge> 0\<close> by (subst divide_ennreal) auto
eberlm@68625
    89
  also have "t ^ n / n / fact (card A) = t ^ n / fact n"
eberlm@68625
    90
    by (simp add: n_def)
eberlm@68625
    91
  also have "n = card (insert b A)"
eberlm@68625
    92
    using insert.hyps by (subst card_insert) (auto simp: n_def)
eberlm@68625
    93
  finally show ?case .
eberlm@68625
    94
qed
eberlm@68625
    95
eberlm@68625
    96
end
eberlm@68625
    97
eberlm@68625
    98
lemma emeasure_std_simplex:
eberlm@68625
    99
  "emeasure lborel (convex hull (insert 0 Basis :: 'a :: euclidean_space set)) =
eberlm@68625
   100
     ennreal (1 / fact DIM('a))"
eberlm@68625
   101
proof -
eberlm@68625
   102
  have "emeasure lborel {x::'a. (\<forall>i\<in>Basis. 0 \<le> x \<bullet> i) \<and> sum ((\<bullet>) x) Basis \<le> 1} =
eberlm@68625
   103
               emeasure (distr (Pi\<^sub>M Basis (\<lambda>b. lborel)) borel (\<lambda>f. \<Sum>b\<in>Basis. f b *\<^sub>R b))
eberlm@68625
   104
                 {x::'a. (\<forall>i\<in>Basis. 0 \<le> x \<bullet> i) \<and> sum ((\<bullet>) x) Basis \<le> 1}"
eberlm@68625
   105
    by (subst lborel_eq) simp
eberlm@68625
   106
  also have "\<dots> = emeasure (Pi\<^sub>M Basis (\<lambda>b. lborel))
eberlm@68625
   107
                    ({y::'a \<Rightarrow> real. (\<forall>i\<in>Basis. 0 \<le> y i) \<and> sum y Basis \<le> 1} \<inter>
eberlm@68625
   108
                      space (Pi\<^sub>M Basis (\<lambda>b. lborel)))"
eberlm@68625
   109
    by (subst emeasure_distr) auto
eberlm@68625
   110
  also have "\<dots> = ennreal (1 / fact DIM('a))"
eberlm@68625
   111
    by (subst emeasure_std_simplex_aux) auto
eberlm@68625
   112
  finally show ?thesis by (simp only: std_simplex)
eberlm@68625
   113
qed
eberlm@68625
   114
ak2110@69737
   115
theorem content_std_simplex:
eberlm@68625
   116
  "measure lborel (convex hull (insert 0 Basis :: 'a :: euclidean_space set)) =
eberlm@68625
   117
     1 / fact DIM('a)"
ak2110@69737
   118
  by (simp add: measure_def emeasure_std_simplex)
eberlm@68625
   119
eberlm@68625
   120
(* TODO: move to Change_of_Vars *)
ak2110@69737
   121
proposition measure_lebesgue_linear_transformation:
eberlm@68625
   122
  fixes A :: "(real ^ 'n :: {finite, wellorder}) set"
eberlm@68625
   123
  fixes f :: "_ \<Rightarrow> real ^ 'n :: {finite, wellorder}"
eberlm@68625
   124
  assumes "bounded A" "A \<in> sets lebesgue" "linear f"
eberlm@68625
   125
  shows   "measure lebesgue (f ` A) = \<bar>det (matrix f)\<bar> * measure lebesgue A"
ak2110@69737
   126
proof -
eberlm@68625
   127
  from assms have [intro]: "A \<in> lmeasurable"
eberlm@68625
   128
    by (intro bounded_set_imp_lmeasurable) auto
eberlm@68625
   129
  hence [intro]: "f ` A \<in> lmeasurable"
eberlm@68625
   130
    by (intro lmeasure_integral measurable_linear_image assms)
eberlm@68625
   131
  have "measure lebesgue (f ` A) = integral (f ` A) (\<lambda>_. 1)"
eberlm@68625
   132
    by (intro lmeasure_integral measurable_linear_image assms) auto
eberlm@68625
   133
  also have "\<dots> = integral (f ` A) (\<lambda>_. 1 :: real ^ 1) $ 0"
eberlm@68625
   134
    by (subst integral_component_eq_cart [symmetric]) (auto intro: integrable_on_const)
eberlm@68625
   135
  also have "\<dots> = \<bar>det (matrix f)\<bar> * integral A (\<lambda>x. 1 :: real ^ 1) $ 0"
eberlm@68625
   136
    using assms
eberlm@68625
   137
    by (subst integral_change_of_variables_linear)
eberlm@68625
   138
       (auto simp: o_def absolutely_integrable_on_def intro: integrable_on_const)
eberlm@68625
   139
  also have "integral A (\<lambda>x. 1 :: real ^ 1) $ 0 = integral A (\<lambda>x. 1)"
eberlm@68625
   140
    by (subst integral_component_eq_cart [symmetric]) (auto intro: integrable_on_const)
eberlm@68625
   141
  also have "\<dots> = measure lebesgue A"
eberlm@68625
   142
    by (intro lmeasure_integral [symmetric]) auto
eberlm@68625
   143
  finally show ?thesis .
eberlm@68625
   144
qed
eberlm@68625
   145
ak2110@69737
   146
theorem content_simplex:
eberlm@68625
   147
  fixes X :: "(real ^ 'n :: {finite, wellorder}) set" and f :: "'n :: _ \<Rightarrow> real ^ ('n :: _)"
eberlm@68625
   148
  assumes "finite X" "card X = Suc CARD('n)" and x0: "x0 \<in> X" and bij: "bij_betw f UNIV (X - {x0})"
eberlm@68625
   149
  defines "M \<equiv> (\<chi> i. \<chi> j. f j $ i - x0 $ i)"
eberlm@68625
   150
  shows "content (convex hull X) = \<bar>det M\<bar> / fact (CARD('n))"
ak2110@69737
   151
proof -
eberlm@68625
   152
  define g where "g = (\<lambda>x. M *v x)"
eberlm@68625
   153
  have [simp]: "M *v axis i 1 = f i - x0" for i :: 'n
eberlm@68625
   154
    by (simp add: M_def matrix_vector_mult_basis column_def vec_eq_iff)
eberlm@68625
   155
  define std where "std = (convex hull insert 0 Basis :: (real ^ 'n :: _) set)"
eberlm@68625
   156
  have compact: "compact std" unfolding std_def
eberlm@68625
   157
    by (intro finite_imp_compact_convex_hull) auto
eberlm@68625
   158
eberlm@68625
   159
  have "measure lebesgue (convex hull X) = measure lebesgue (((+) (-x0)) ` (convex hull X))"
eberlm@68625
   160
    by (rule measure_translation [symmetric])
eberlm@68625
   161
  also have "((+) (-x0)) ` (convex hull X) = convex hull (((+) (-x0)) ` X)"
eberlm@68625
   162
    by (rule convex_hull_translation [symmetric])
eberlm@68625
   163
  also have "((+) (-x0)) ` X = insert 0 ((\<lambda>x. x - x0) ` (X - {x0}))"
eberlm@68625
   164
    using x0 by (auto simp: image_iff)
eberlm@68625
   165
  finally have eq: "measure lebesgue (convex hull X) = measure lebesgue (convex hull \<dots>)" .
eberlm@68625
   166
  
eberlm@68625
   167
  from compact have "measure lebesgue (g ` std) = \<bar>det M\<bar> * measure lebesgue std"
eberlm@68625
   168
    by (subst measure_lebesgue_linear_transformation)
eberlm@68625
   169
       (auto intro: finite_imp_bounded_convex_hull dest: compact_imp_closed simp: g_def std_def)
eberlm@68625
   170
  also have "measure lebesgue std = content std" using compact
eberlm@68625
   171
    by (intro measure_completion) (auto dest: compact_imp_closed)
eberlm@68625
   172
  also have "content std = 1 / fact CARD('n)" unfolding std_def
eberlm@68625
   173
    by (simp add: content_std_simplex)
eberlm@68625
   174
  also have "g ` std = convex hull (g ` insert 0 Basis)" unfolding std_def
eberlm@68625
   175
    by (rule convex_hull_linear_image) (auto simp: g_def)
eberlm@68625
   176
  also have "g ` insert 0 Basis = insert 0 (g ` Basis)"
eberlm@68625
   177
    by (auto simp: g_def)
eberlm@68625
   178
  also have "g ` Basis = (\<lambda>x. x - x0) ` range f"
eberlm@68625
   179
    by (auto simp: g_def Basis_vec_def image_iff)
eberlm@68625
   180
  also have "range f = X - {x0}" using bij
eberlm@68625
   181
    using bij_betw_imp_surj_on by blast
eberlm@68625
   182
  also note eq [symmetric]
eberlm@68625
   183
  finally show ?thesis 
eberlm@68625
   184
    using finite_imp_compact_convex_hull[OF \<open>finite X\<close>] by (auto dest: compact_imp_closed)
eberlm@68625
   185
qed
eberlm@68625
   186
ak2110@69737
   187
theorem content_triangle:
eberlm@68625
   188
  fixes A B C :: "real ^ 2"
eberlm@68625
   189
  shows "content (convex hull {A, B, C}) =
eberlm@68625
   190
           \<bar>(C $ 1 - A $ 1) * (B $ 2 - A $ 2) - (B $ 1 - A $ 1) * (C $ 2 - A $ 2)\<bar> / 2"
ak2110@69737
   191
proof -
eberlm@68625
   192
  define M :: "real ^ 2 ^ 2" where "M \<equiv> (\<chi> i. \<chi> j. (if j = 1 then B else C) $ i - A $ i)"
eberlm@68625
   193
  define g where "g = (\<lambda>x. M *v x)"
eberlm@68625
   194
  define std where "std = (convex hull insert 0 Basis :: (real ^ 2) set)"
eberlm@68625
   195
  have [simp]: "M *v axis i 1 = (if i = 1 then B - A else C - A)" for i
eberlm@68625
   196
    by (auto simp: M_def matrix_vector_mult_basis column_def vec_eq_iff)
eberlm@68625
   197
  have compact: "compact std" unfolding std_def
eberlm@68625
   198
    by (intro finite_imp_compact_convex_hull) auto
eberlm@68625
   199
eberlm@68625
   200
  have "measure lebesgue (convex hull {A, B, C}) =
eberlm@68625
   201
          measure lebesgue (((+) (-A)) ` (convex hull {A, B, C}))"
eberlm@68625
   202
    by (rule measure_translation [symmetric])
eberlm@68625
   203
  also have "((+) (-A)) ` (convex hull {A, B, C}) = convex hull (((+) (-A)) ` {A, B, C})"
eberlm@68625
   204
    by (rule convex_hull_translation [symmetric])
eberlm@68625
   205
  also have "((+) (-A)) ` {A, B, C} = {0, B - A, C - A}"
eberlm@68625
   206
    by (auto simp: image_iff)
eberlm@68625
   207
  finally have eq: "measure lebesgue (convex hull {A, B, C}) =
eberlm@68625
   208
                      measure lebesgue (convex hull {0, B - A, C - A})" .
eberlm@68625
   209
  
eberlm@68625
   210
  from compact have "measure lebesgue (g ` std) = \<bar>det M\<bar> * measure lebesgue std"
eberlm@68625
   211
    by (subst measure_lebesgue_linear_transformation)
eberlm@68625
   212
       (auto intro: finite_imp_bounded_convex_hull dest: compact_imp_closed simp: g_def std_def)
eberlm@68625
   213
  also have "measure lebesgue std = content std" using compact
eberlm@68625
   214
    by (intro measure_completion) (auto dest: compact_imp_closed)
eberlm@68625
   215
  also have "content std = 1 / 2" unfolding std_def
eberlm@68625
   216
    by (simp add: content_std_simplex)
eberlm@68625
   217
  also have "g ` std = convex hull (g ` insert 0 Basis)" unfolding std_def
eberlm@68625
   218
    by (rule convex_hull_linear_image) (auto simp: g_def)
eberlm@68625
   219
  also have "g ` insert 0 Basis = insert 0 (g ` Basis)"
eberlm@68625
   220
    by (auto simp: g_def)
eberlm@68625
   221
  also have "(2 :: 2) \<noteq> 1" by auto
eberlm@68625
   222
  hence "\<not>(\<forall>y::2. y = 1)" by blast
eberlm@68625
   223
  hence "g ` Basis = {B - A, C - A}"
eberlm@68625
   224
    by (auto simp: g_def Basis_vec_def image_iff)
eberlm@68625
   225
  also note eq [symmetric]
eberlm@68625
   226
  finally show ?thesis 
eberlm@68625
   227
    using finite_imp_compact_convex_hull[of "{A, B, C}"]
eberlm@68625
   228
    by (auto dest!: compact_imp_closed simp: det_2 M_def)
eberlm@68625
   229
qed
eberlm@68625
   230
ak2110@69737
   231
theorem heron:
eberlm@68625
   232
  fixes A B C :: "real ^ 2"
eberlm@68625
   233
  defines "a \<equiv> dist B C" and "b \<equiv> dist A C" and "c \<equiv> dist A B"
eberlm@68625
   234
  defines "s \<equiv> (a + b + c) / 2"
eberlm@68625
   235
  shows   "content (convex hull {A, B, C}) = sqrt (s * (s - a) * (s - b) * (s - c))"
ak2110@69737
   236
proof -
eberlm@68625
   237
  have [simp]: "(UNIV :: 2 set) = {1, 2}"
eberlm@68625
   238
    using exhaust_2 by auto
eberlm@68625
   239
  have dist_eq: "dist (A :: real ^ 2) B ^ 2 = (A $ 1 - B $ 1) ^ 2 + (A $ 2 - B $ 2) ^ 2"
eberlm@68625
   240
    for A B by (simp add: dist_vec_def dist_real_def)
eberlm@68625
   241
  have nonneg: "s * (s - a) * (s - b) * (s - c) \<ge> 0"
eberlm@68625
   242
    using dist_triangle[of A B C] dist_triangle[of A C B] dist_triangle[of B C A]
eberlm@68625
   243
    by (intro mult_nonneg_nonneg) (auto simp: s_def a_def b_def c_def dist_commute)
eberlm@68625
   244
eberlm@68625
   245
  have "16 * content (convex hull {A, B, C}) ^ 2 =
eberlm@68625
   246
          4 * ((C $ 1 - A $ 1) * (B $ 2 - A $ 2) - (B $ 1 - A $ 1) * (C $ 2 - A $ 2)) ^ 2"
eberlm@68625
   247
    by (subst content_triangle) (simp add: power_divide)
eberlm@68625
   248
  also have "\<dots> = (2 * (dist A B ^ 2 * dist A C ^ 2 + dist A B ^ 2 * dist B C ^ 2 + 
eberlm@68625
   249
      dist A C ^ 2 * dist B C ^ 2) - (dist A B ^ 2) ^ 2 - (dist A C ^ 2) ^ 2 - (dist B C ^ 2) ^ 2)"
eberlm@68625
   250
    unfolding dist_eq unfolding power2_eq_square by algebra
eberlm@68625
   251
  also have "\<dots> = (a + b + c) * ((a + b + c) - 2 * a) * ((a + b + c) - 2 * b) *
eberlm@68625
   252
                    ((a + b + c) - 2 * c)"
eberlm@68625
   253
    unfolding power2_eq_square by (simp add: s_def a_def b_def c_def algebra_simps)
eberlm@68625
   254
  also have "\<dots> = 16 * s * (s - a) * (s - b) * (s - c)"
eberlm@68625
   255
    by (simp add: s_def divide_simps mult_ac)
eberlm@68625
   256
  finally have "content (convex hull {A, B, C}) ^ 2 = s * (s - a) * (s - b) * (s - c)"
eberlm@68625
   257
    by simp
eberlm@68625
   258
  also have "\<dots> = sqrt (s * (s - a) * (s - b) * (s - c)) ^ 2"
eberlm@68625
   259
    by (intro real_sqrt_pow2 [symmetric] nonneg)
eberlm@68625
   260
  finally show ?thesis using nonneg
eberlm@68625
   261
    by (subst (asm) power2_eq_iff_nonneg) auto
eberlm@68625
   262
qed
eberlm@68625
   263
eberlm@68625
   264
end