proposition: Lemma sintegralrM : sintegral m (cst r \* f)%R = r%:E * sintegral m f.
proof: Proof. have [->|r0] := eqVneq r 0%R. by rewrite mul0e (eq_sintegral (cst 0%R)) ?sintegral0// => x/=; rewrite mul0r. rewrite !sintegralET. transitivity (\sum_(x \in [set: R]) x%:E * m (f @^-1` [set x / r])). by under eq_fsbigr do rewrite preimage_cstM//. transitivity (\sum_(x \in [set: R]) r%:E * (x%:E * m (f @^-1` [set x]))). rewrite (reindex_fsbigT (fun x => r * x)%R)//; last first. by exists ( *%R r ^-1)%R; [exact: mulKf|exact: mulVKf]. by apply: eq_fsbigr => x; rewrite mulrAC divrr ?unitfE// mul1r muleA EFinM. by rewrite ge0_mule_fsumr// => x; exact: nnsfun_mulemu_ge0. 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