The rational finite expectation is an integral in the finite integration space, across the embedding of the rationals in the reals

Recorded description

Fix m : Nat and let S be the finite integration space IntSpace.crealFinite m, whose carrier is the real-valued functions on the index range [0, m+1) and whose integral is the finite sum over that range. Let X and p be RATIONAL-valued functions on that range. Then the integral over S of the function k |-> ofRat(X k) * ofRat(p k) equals, up to CReal.Equiv, the image under CReal.ofRat of the rational expectation of X against the weights p over m+1 points. The embedding is not decoration: IntSpace is generic over the function space but hard-wired in the value type -- its integral returns a CReal and its total is a CReal -- so there is no rational-valued integration space and the rational expectation cannot be an integral in one. The transfer that discharges the mismatch is proved generically (an additive, multiplicative map between two setoid ordered rings carries a finite expectation to a finite expectation) and is instantiated here at the rationals, the reals and CReal.ofRat, whose additivity and multiplicativity were already proved. Consequently every theorem the generic integration layer proves -- integrand congruence, nonnegativity, the constant law, the derived counting measure, monotone convergence -- applies to the rational expectation through one named embedding rather than through a resemblance.