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 ed709a7f320d

Complete Lean source

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Reversibility

namespace AutoSamplingTheory.Tests.Reversibility

open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator
open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Reversibility

noncomputable section

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

#check AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Reversibility.IsReversible

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