proposition: Lemma iavg_restrict f D A : measurable D -> measurable A -> iavg (f \_ D) A = ((fine (mu A))^-1)%:E * \int[mu]_(y in D `&` A) `|f y|%:E.
proof: Proof. move=> mD mA; rewrite /iavg setIC integral_setI_indic//=; congr *%E. apply: eq_integral => /= y yx1. by rewrite patch_indic/= normrM EFinM (@ger0_norm _ (\1_D _)). Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun