import AutoSamplingTheory.TechnicalLemmas.Probability.NormalizedFiniteMeasure

#check AutoSamplingTheory.TechnicalLemmas.Probability.NormalizedFiniteMeasure.compl_null_of_toMeasure_le_restrict
#check AutoSamplingTheory.TechnicalLemmas.Probability.NormalizedFiniteMeasure.normalize_apply_eq_one_of_toMeasure_le_restrict
#check AutoSamplingTheory.TechnicalLemmas.Probability.NormalizedFiniteMeasure.ae_mem_of_toMeasure_le_restrict