test module

`Tests.RNLogRatio`

0 named declarations scanned from Tests/RNLogRatio.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio

Imported by

No local reverse import.

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

Tests/RNLogRatio.lean — full module with imports and context

Download module (.lean)

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