test module

`Tests.CanonicalRelativeFisher`

0 named declarations scanned from Tests/CanonicalRelativeFisher.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher

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/CanonicalRelativeFisher.lean — full module with imports and context

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher

#check AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.scoreSq
#check AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.SmoothFiniteScoreDomain
#check AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.information
#check AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.information_eq_relativeFisher
#check AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.information_eq_integral_scoreSq
#check AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.information_eq_integral_density_mul_scoreSq
#check AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.scoreSq_integrable
#check AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.information_nonneg
#check AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.information_proof_irrel