proving importance sampling theorem

Stream: new members

[Hao Wu]

Hello community,
this is Hao, Engineering, data related background,
just start to learn Lean4, the problem I want to solve is to (automatically) check /prove the formula deduction, e.g. this importance sampling theorem,
image.png
how to express this using Lean4 and eventually prove that the final expression is equivalent to the first one ?

[Rémy Degenne]

You can look at MeasureTheory.lintegral_rnDeriv_mul or MeasureTheory.integral_rnDeriv_smul for two possible statements of this lemma. I invite you to look at how they are written and explore the library around them.

[Hao Wu]

good thanks