production module

`AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Reversibility`

2 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/Reversibility.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGeneratorMathlib.Analysis.InnerProductSpace.Basic external

Imported by

AutoSamplingTheory.TechnicalLemmas.StochasticProcessesTests.Reversibility

Placeholder scan

0 declaration(s) flagged

Gate status

Compiled

Declarations

def AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Reversibility.IsReversible Compiled Compiled

- Chewi Definition 1.2.10: every time operator is symmetric in the ambient real Hilbert-space inner product. Taking `H = L²(pi)` gives the source definition of reversibility with respect to `pi`.

def IsReversible (S : ContinuousLinearSemigroup H) : Prop :=
  ∀ (t : ℝ≥0) (f g : H),
    inner ℝ (S.op t f) g = inner ℝ f (S.op t g)

/-- The constant identity semigroup is reversible on every real inner-product
space. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/Reversibility.lean:29published source at 77184245109aOpen detailed card

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Reversibility.isReversible_identity Compiled Not mapped

- The constant identity semigroup is reversible on every real inner-product space.

theorem isReversible_identity
    (S : ContinuousLinearSemigroup H)
    (hop : ∀ t, S.op t = ContinuousLinearMap.id ℝ H) :
    IsReversible S := by
  intro t f g
  rw [hop t]
  rfl

end Reversibility
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/Reversibility.lean:35published source at 77184245109a