Hello Everyone,
A theorem named nn_integral_density' in
Nonnegative_Lebesgue_Integration theory of isabelle. They used induct
to prove it. When applied induct 5 cases where returned. Does someone
know of an alternative in HOL4 ?
I am trying to prove the same theorem in HOL4 i.e.,
`!f g M.
f IN measurable (m_space M,measurable_sets M) Borel /\
(?x. x IN m_space M /\ 0 <= f x) /\
g IN measurable (m_space M,measurable_sets M) Borel /\
(!x. 0 <= g x) ==>
(pos_fn_integral
(m_space M,measurable_sets M,
(\A.
if A IN measurable_sets M then
pos_fn_integral M (\x. f x * indicator_fn A x)
else 0)) g =
pos_fn_integral M (\x. f x * g x))`
Below is a link to the theory.
http://isabelle.in.tum.de/dist/library/HOL/HOL-Probability/Nonnegative_Lebesgue_Integration.html
Best Regards
Qasim
------------------------------------------------------------------------------
One dashboard for servers and applications across Physical-Virtual-Cloud
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
