test module

`Tests.ReversibleGenerator`

0 named declarations scanned from Tests/ReversibleGenerator.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ReversibleGenerator

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ReversibleGenerator

namespace AutoSamplingTheory.Tests.ReversibleGenerator

open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses
open OperatorGenerator OperatorGeneratorDomain Reversibility ReversibleGenerator

#check ReversibleGenerator.inner_rightDifferenceQuotient_eq
#check ReversibleGenerator.inner_rightGenerator_eq

variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]

example (S : ContinuousLinearSemigroup H) (hrev : IsReversible S)
    (f g : generatorDomainSubmodule S) :
    inner ℝ (rightGenerator S f) (g : H) =
      inner ℝ (f : H) (rightGenerator S g) :=
  inner_rightGenerator_eq S hrev f g

end AutoSamplingTheory.Tests.ReversibleGenerator