generalize `{mfun _ >-> _}`

Open affeldt-aist opened this issue 3 years ago • 1 comments

https://github.com/math-comp/analysis/blob/bfa6d4bc2fa548644b87769267ea49f523a21858/theories/lebesgue_integral.v#L68

while preserving the ring structure of simple functions @CohenCyril

May 25 '22 07:05 affeldt-aist

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 _ _ _ _).

Oct 12 '23 08:10 hoheinzollern