test module

`Tests.SampleWikiExampleCases`

0 named declarations scanned from Tests/SampleWikiExampleCases.lean.

Imports

AutoSamplingTheory.ExampleCases.SampleWikiAutoSamplingTheory.TechnicalLemmas.InformationTheory.FisherTransport

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

Download module (.lean)

import AutoSamplingTheory.ExampleCases.SampleWiki
import AutoSamplingTheory.TechnicalLemmas.InformationTheory.FisherTransport

namespace AutoSamplingTheory
namespace Tests
namespace SampleWikiExampleCases

open ExampleCases.SampleWiki

example : admissibleForScientificGraph VerificationStage.assimilated :=
  assimilated_admissible

example : ¬ admissibleForScientificGraph VerificationStage.compiled :=
  compiled_not_admissible

example : ¬ admissibleForScientificGraph VerificationStage.discovered :=
  discovered_not_admissible

#check SourceIdentity
#check VerificationStage
#check TechnicalLemmas.Algebra.linear_growth_of_step_growth
#check TechnicalLemmas.Algebra.reciprocal_growth_implies_inverse_time_bound
#check TechnicalLemmas.InformationTheory.FisherTransport.sq_div_le_fisher_of_sq_le_mul
#check TechnicalLemmas.InformationTheory.FisherTransport.neg_half_fisher_le_neg_half_sq_div
#check TechnicalLemmas.InformationTheory.FisherTransport.kl_derivative_upper_bound_of_fisher_transport
#check ExampleCases.SampleWiki.Cases.IdealProximalChain.kl_rate_from_reciprocal_step

end SampleWikiExampleCases
end Tests
end AutoSamplingTheory