proposition: Lemma dyadic_itv_image n T (f : T -> \bar R) x : (n%:R%:E <= f x < n.+1%:R%:E)%E -> exists k, (2 ^ n.+1 * n <= k < 2 ^ n.+1 * n.+1)%N /\ f x \in EFin @` [set` I n.+1 k].
proof: Proof. move=> fxn; have fxfin : f x \is a fin_num. by rewrite fin_numE; move: fxn; case: (f x) => // /andP[]. have : f x \in EFin @` `[n%:R, n.+1%:R[%classic. rewrite inE /=; exists (fine (f x)); last by rewrite fineK. by rewrite in_itv /= -lee_fin -lte_fin (fineK fxfin). rewrite (bigsetU_dyadic_itv n) inE /= => -[r]; rewrite -bigcup_seq => -[k /=]. rewrite mem_index_iota => nk Ir rfx. by exists k; split; [rewrite !(mulnC (2 ^ n.+1)%N)|rewrite !inE /=; exists r]. 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