Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412

Exact source context

import AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio

#check AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.density
#check AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.logRatio
#check AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.logRatio_apply
#check AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.measurable_density
#check AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.measurable_logRatio
#check AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.density_nonneg
#check AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.density_ae_pos_of_absolutelyContinuous
#check AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.exp_logRatio_ae_eq_density_of_absolutelyContinuous
#check AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.density_self_ae
#check AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.logRatio_self_ae
#check AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.toReal_klDiv_eq_integral_logRatio_of_probability