proposition: Lemma nd_approx : nondecreasing_seq approx.
proof: Proof. apply/nondecreasing_seqP => n; apply/lefP => x. have [Dx|Dx] := pselect (D x); last by rewrite ?notinD_approx0. have [fxn|fxn] := ltP (f x) n%:R%:E. rewrite {2}/approx fgtn_B0 ?mulr0 ?addr0; last first. by rewrite (lt_trans fxn) // lte_fin ltr_nat. have [/eqP ->|[k [/andP[k0 kn] xAnk -> _]]] := f_ub_approx fxn. by apply: sumr_ge0 => i _; rewrite mulr_ge0. move: (xAnk); rewrite inE {1}/A kn => -[_] /=. rewrite inE => -[r] /dyadic_itv_subU[|] rnk rfx. - have k2n : (k.*2 < n.+1 * 2 ^ n.+1)%N. rewrite expnS mulnCA mul2n ltn_double (ltn_trans kn) //. by rewrite ltn_mul2r expn_gt0 /= ltnS. rewrite (bigD1 (Ordinal k2n)) //= indicE. have xAn1k : x \in A n.+1 k.*2. by rewrite inE /A k2n; split => //=; rewrite inE; exists r. rewrite xAn1k mulr1 big1 ?addr0; last first. by move=> i ik2n; rewrite (disj_A0 (Ordinal k2n)) ?mulr0. rewrite exprS invrM ?unitfE// -muln2 natrM -mulrA (mulrCA 2). by rewrite divrr ?mulr1 ?unitfE. - have k2n : (k.*2.+1 < n.+1 * 2 ^ n.+1)%N. move: kn; rewrite -ltn_double -(ltn_add2r 1) 2!addn1 => /leq_trans; apply. by rewrite -muln2 -mulnA -expnSr ltn_mul2r expn_gt0 /= ltnS. rewrite (bigD1 (Ordinal k2n)) //= indicE. have xAn1k : x \in A n.+1 k.*2.+1. by rewrite /A /= k2n inE; split => //=; rewrite inE/=; exists r. rewrite xAn1k mulr1 big1 ?addr0; last first. by move=> i ik2n; rewrite (disj_A0 (Ordinal k2n)) // mulr0. rewrite -(@natr1 _ k.*2) mulrDl exprS -mul2n natrM -mulf_div divrr ?unitfE//. by rewrite !mul1r lerDl. have /orP[{}fxn|{}fxn] : ((n%:R%:E <= f x < n.+1%:R%:E) || (n.+1%:R%:E <= f x))%E. - by move: fxn; case: leP => /= [_ _|_ ->//]; rewrite orbT. - have [k [k1 k2]] := dyadic_itv_image fxn. have xBn : x \in B n by rewrite /B /= inE /=; case/andP : fxn => ->. rewrite /approx indicE xBn mulr1 big1 ?add0r; last first. by move=> /= i _; rewrite fgen_A0 ?mulr0//; case/andP : fxn. rewrite fgtn_B0 ?mulr0 ?addr0; last by case/andP : fxn. have kn2 : (k < n.+1 * 2 ^ n.+1)%N by case/andP : k1 => _; rewrite mulnC. rewrite (bigD1 (Ordinal kn2)) //=. have xAn1k : x \in A n.+1 k by rewrite inE /A kn2. rewrite indicE xAn1k mulr1 big1 ?addr0; last first. by move=> i /= ikn2; rewrite (disj_A0 (Ordinal kn2)) // mulr0. by rewrite -natrX ler_pdivlMr// mulrC -natrM ler_nat; case/andP : k1. - have xBn : x \in B n by rewrite /B inE /= (le_trans _ fxn) // lee_fin ler_nat. rewrite /approx indicE xBn mulr1. have xBn1 : x \in B n.+1 by rewrite /B /= inE. rewrite indicE xBn1 mulr1 big1 ?add0r. by rewrite big1 ?add0r ?ler_nat// => /= i _; rewrite fgen_A0// mulr0. by move=> /= i _; rewrite fgen_A0 ?mulr0// (le_trans _ fxn)// lee_fin ler_nat. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun