test module

`Tests.CompletedIntegrand`

0 named declarations scanned from Tests/CompletedIntegrand.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CompletedIntegrand

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CompletedIntegrand

namespace AutoSamplingTheory.Tests.CompletedIntegrand

open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CompletedIntegrand

#check completedIntegrand
#check completedIntegrand_stronglyProgressive
#check sectionSquare_integrable
#check completedEnergy_eq_prefixIntegral
#check completedEnergy_stronglyProgressive

end AutoSamplingTheory.Tests.CompletedIntegrand