proposition: Lemma SF_val_fun_rw (f : R -> R) (a b : R) (n : nat) (x : R) (Hx : a <= x <= b) : SF_val_fun f a b n x = match (unif_part_nat a b n x Hx) with | inleft H => f (a + (INR (proj1_sig H) + /2) * (b-a) / (INR n + 1)) | inright _ => f (a + (INR n + /2) * (b-a) / (INR n + 1)) end.
proof: Proof. have Hab : (a <= b) ; [by apply Rle_trans with (1 := proj1 Hx), Hx | ]. case: unif_part_nat => {Hx} [ [ i [Hx Hi] ] | Hx] /=. rewrite /SF_val_fun /SF_fun_f2. replace (a + (INR i + /2) * (b - a) / (INR n+1)) with ((nth 0 (unif_part a b n) i + nth 0 (unif_part a b n) (S i)) / 2) ; [ | rewrite size_mkseq in Hi ; rewrite ?nth_mkseq ?S_INR ; [field ; apply Rgt_not_eq | apply SSR_leq | apply SSR_leq ] ; intuition]. case: (unif_part a b n) (unif_part_sort a b n Hab) i Hi x Hx => {a b Hab n} [| h s] Hs /= i Hi. by apply Nat.nlt_0_r in Hi. case: (s) Hs (i) ((proj2 (Nat.succ_lt_mono _ _) Hi)) => {s i Hi} [| h0 s] Hs /= i Hi. by apply Nat.nlt_0_r in Hi. elim: (s) h h0 Hs (i) (proj2 (Nat.succ_lt_mono _ _) Hi) => {s i Hi} [|h1 s IH] h h0 Hs /= i Hi x Hx. by apply Nat.nlt_0_r in Hi. case: i Hx Hi => [|i]/= Hx Hi. rewrite /SF_fun /=. case: Rlt_dec => [Hx0 | _ ]. contradict Hx0 ; apply Rle_not_lt, Hx. case: Rlt_dec => // Hx0 ; contradict Hx0 ; apply Hx. rewrite -(IH h0 h1 (proj2 Hs) i ((proj2 (Nat.succ_lt_mono _ _) Hi)) x Hx). rewrite /SF_fun /= ; case: Rlt_dec => [ Hx0 | _ ] //. contradict Hx0 ; apply Rle_not_lt, Rle_trans with (1 := proj1 Hs), Rle_trans with (2 := proj1 Hx), (sorted_head [:: h0, h1 & s] _ (proj2 Hs)) ; simpl; intuition. case: Rlt_dec => [ Hx0 | _ ] //. contradict Hx0 ; apply Rle_not_lt, Rle_trans with (2 := proj1 Hx), (sorted_head [:: h0, h1 & s] _ (proj2 Hs)) ; simpl; intuition. replace (a + (INR n + /2) * (b - a) / (INR n + 1)) with ((nth 0 (unif_part a b n) (n) + nth 0 (unif_part a b n) (S n)) / 2) ; [ | rewrite ?nth_mkseq ?minus_INR ?S_INR /= ; [field ; apply Rgt_not_eq | apply SSR_leq | apply SSR_leq ] ; intuition]. suff : (1 < size (unif_part a b n))%nat. move: x Hx ; have: (n = size (unif_part a b n) - 2)%nat ; [ rewrite size_mkseq ; intuition | ]. move => {2 4 8 10}->. rewrite /SF_val_fun /SF_fun_f2. case: (unif_part a b n) (unif_part_sort a b n Hab) => {a b Hab n} [| h s Hs x Hx /= Hi] . intros _ x Hx Hi. by apply Nat.nlt_0_r in Hi. case: s h Hs Hi x Hx => [| h0 s] h Hs /= Hi. by apply Nat.lt_irrefl in Hi. elim: s h h0 Hs {Hi} => [| h1 s IH] h h0 Hs /= x Hx. rewrite /SF_fun /= ; case: Rlt_dec => [Hx0 | _]. contradict Hx0 ; apply Rle_not_lt, Hx. case: Rle_dec => [| Hx0] // ; contradict Hx0 ; apply Hx. rewrite Nat.sub_0_r in IH. rewrite -(IH h0 h1 (proj2 Hs) x Hx ). rewrite /SF_fun /= ; case: Rlt_dec => [ Hx0 | _ ] //. contradict Hx0 ; apply Rle_not_lt, Rle_trans with (1 := proj1 Hs), Rle_trans with (2 := proj1 Hx), (sorted_head [:: h0, h1 & s] _ (proj2 Hs)) ; simpl; intuition. case: Rlt_dec => [ Hx0 | _ ] //. contradict Hx0 ; apply Rle_not_lt, Rle_trans with (2 := proj1 Hx), (sorted_head [:: h0, h1 & s] _ (proj2 Hs)) ; simpl; intuition. rewrite size_mkseq ; by apply ->Nat.succ_lt_mono; apply Nat.lt_0_succ. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy