proposition: Lemma ad_SF_inf_r (f : R -> R) (a b : R) (n : nat) : ((a <= b) -> adapted_couple (fun x => real (SF_inf_fun f a b n x)) a b (unif_part a b n) (behead (pairmap (fun x y => real (Inf_fct f x y)) 0 (unif_part a b n)))) /\ (~(a <= b) -> adapted_couple (fun x => real (SF_inf_fun f a b n x)) a b (unif_part b a n) (behead (pairmap (fun x y => real (Inf_fct f x y)) 0 (unif_part b a n)))).
proof: Proof. wlog : a b / (a <= b) => [Hw|Hab]. case: (Rle_dec a b) => // Hab ; split => // _. by apply (Hw a b). apply Rnot_le_lt, Rlt_le in Hab ; case : (Hw b a Hab) => {} Hw _ ; move: (Hw Hab) => {} Hw ; rewrite /adapted_couple in Hw |-* ; rewrite Rmin_comm Rmax_comm ; intuition => x Hx ; rewrite SF_inf_fun_bound ; by apply H4. split ; case: (Rle_dec a b)=> // _ _. rewrite /SF_inf_fun ; case: (Rle_dec a b) => // _. have Hs : (SF_sorted Rle (SF_map real (SF_inf_seq f a b n))). rewrite /SF_sorted SF_map_lx SF_lx_f2. replace (head 0 (unif_part a b n) :: behead (unif_part a b n)) with (unif_part a b n) by intuition. by apply unif_part_sort. by apply Nat.lt_0_succ. have {2}<-: head 0 (unif_part a b n) = a. apply head_unif_part. have {3}<-: last 0 (unif_part a b n) = b. apply last_unif_part. replace (behead (pairmap (fun x y : R => real (Inf_fct f x y)) 0 (unif_part a b n))) with (SF_ly (SF_map real (SF_inf_seq f a b n))). replace (unif_part a b n) with (SF_lx (SF_map real (SF_inf_seq f a b n))). move: (ad_SF_compat (f ((0+0)/2)) (SF_map real (SF_inf_seq f a b n)) Hs) ; rewrite /adapted_couple => Had ; intuition. move: (H4 i H3) => {H4} H3' x H4. move: (H3' x H4) => {H3'} <-. rewrite -(SF_fun_map real). 2: rewrite SF_map_lx SF_lx_f2 // ; by apply Nat.lt_0_succ. 2: rewrite SF_map_ly SF_ly_f2 ; by rewrite -behead_map map_pairmap. move: H3 H4. rewrite /SF_inf_seq. rewrite !nth_compat size_compat SF_map_lx SF_lx_f2. 2: apply Nat.lt_0_succ. unfold SF_fun. elim: (unif_part a b n) (unif_part_sort a b n Hab) {3}(0) {1}(f ((0 + 0) / 2)) i => [ | x0 l IH] Hl z0 z1 i Hi Hx. by apply Nat.nlt_0_r in Hi. simpl in Hi. destruct l as [ | x1 l]. by apply Nat.nlt_0_r in Hi. rewrite SF_cons_f2. 2: by apply Nat.lt_0_succ. rewrite SF_map_cons. case: i Hi Hx => [ | i] Hi /= Hx. case: Rlt_dec => Hx0 //. contradict Hx0 ; apply Rle_not_lt, Rlt_le, Hx. case: (l) => [ | x2 l'] /=. case: Rle_dec => // Hx1. contradict Hx1 ; by apply Rlt_le, Hx. case: Rlt_dec (proj2 Hx) => //. case: Rlt_dec => //= Hx0. contradict Hx0. apply Rle_not_lt, Rlt_le. eapply Rle_lt_trans, Hx. eapply Rle_trans, sorted_head. by apply Hl. by apply Hl. eapply Nat.lt_trans, Hi. by apply Nat.lt_succ_diag_r. eapply (IH (proj2 Hl) (Inf_fct f x0 x1) (Inf_fct f x0 x1)). 2: apply Hx. simpl ; by apply Nat.succ_lt_mono. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy