generalize {mfun _ >-> _}

[affeldt-aist]

analysis/theories/lebesgue_integral.v

Line 68 in bfa6d4b

HB.mixin Record IsMeasurableFun (aT : measurableType) (rT : realType) (f : aT -> rT) := {

while preserving the ring structure of simple functions @CohenCyril

[hoheinzollern]

This restriction is preventing a general definition of composition of measurable functions. Here is a restricted definition that works for defining composition of random variables with real-valued functions, used in proving Chernoff's bound.

Lemma measurableT_comp_subproof d1 (T1 : measurableType d1) (f : {mfun R >-> R}) (g : {mfun T1 >-> R}) :
  measurable_fun setT (f \o g).
Proof. apply: measurableT_comp. exact. apply: @measurable_funP _ _ _ g. Qed.

HB.instance Definition _ (d1 : measure_display) (T1 : measurableType d1)
  (f : {mfun R >-> R}) (g : {mfun T1 >-> R}) := isMeasurableFun.Build _ _ _ (f \o g) (@measurableT_comp_subproof _ _ _ _).