test module

`Tests.GeneratorStationarity`

0 named declarations scanned from Tests/GeneratorStationarity.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GeneratorStationarity

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GeneratorStationarity

namespace AutoSamplingTheory.Tests.GeneratorStationarity

open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses
open OperatorGenerator OperatorGeneratorDomain GeneratorStationarity

#check GeneratorStationarity.hasRightGeneratorAt_zero_of_fixed
#check GeneratorStationarity.mem_generatorDomainSubmodule_of_fixed
#check GeneratorStationarity.invariantFunctional_generator_eq_zero
#check GeneratorStationarity.invariantFunctional_rightGenerator_eq_zero

variable {M : Type*} [NormedAddCommGroup M] [NormedSpace ℝ M]

example (S : ContinuousLinearSemigroup M)
    (ell : M →L[ℝ] ℝ)
    (hinv : ∀ (t : ℝ≥0) (f : M), ell (S.op t f) = ell f)
    (f : generatorDomainSubmodule S) :
    ell (rightGenerator S f) = 0 :=
  invariantFunctional_rightGenerator_eq_zero S ell hinv f

end AutoSamplingTheory.Tests.GeneratorStationarity