test module

`Tests.Reversibility`

1 named declarations scanned from Tests/Reversibility.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Reversibility

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

def AutoSamplingTheory.Tests.Reversibility.identitySemigroup Partial Not mapped

No declaration docstring.

def identitySemigroup : ContinuousLinearSemigroup H where
  op := fun _ => ContinuousLinearMap.id ℝ H
  op_zero := rfl
  op_add := by
    intro s t
    ext f
    rfl

example : IsReversible (identitySemigroup : ContinuousLinearSemigroup H) := by
  apply isReversible_identity
  intro t
  rfl

end

end AutoSamplingTheory.Tests.Reversibility

Tests/Reversibility.lean:14published source at 0e31a3cda412