AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ReversibleGenerator

- Reversibility already makes every finite positive-time generator difference quotient symmetric.

theorem inner_rightDifferenceQuotient_eq
    (S : ContinuousLinearSemigroup H)
    (hrev : IsReversible S)
    (h : ℝ≥0) (f g : H) :
    inner ℝ (rightDifferenceQuotient S h f) g =
      inner ℝ f (rightDifferenceQuotient S h g) := by
  simp only [rightDifferenceQuotient, inner_smul_real_left,
    inner_smul_real_right, inner_sub_left, inner_sub_right]
  rw [hrev h f g]

/-- The canonical right generator of a reversible semigroup is symmetric on
its generator domain.

No closedness, self-adjointness, or concrete `L²(pi)` realization is claimed;
this is exactly the pairwise identity inherited by taking the generator limit
of the reversible semigroup identity. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ReversibleGenerator.lean:39published source at 0e31a3cda412

- The canonical right generator of a reversible semigroup is symmetric on its generator domain. No closedness, self-adjointness, or concrete `L²(pi)` realization is claimed; this is exactly the pairwise identity inherited by taking the generator limit of the reversible semigroup identity.

theorem inner_rightGenerator_eq
    (S : ContinuousLinearSemigroup H)
    (hrev : IsReversible S)
    (f g : generatorDomainSubmodule S) :
    inner ℝ (rightGenerator S f) (g : H) =
      inner ℝ (f : H) (rightGenerator S g) := by
  let l : Filter ℝ≥0 := nhdsWithin 0 (Ioi 0)
  have hf :
      Tendsto
        (fun h : ℝ≥0 =>
          inner ℝ (rightDifferenceQuotient S h (f : H)) (g : H))
        l
        (𝓝 (inner ℝ (rightGenerator S f) (g : H))) := by
    exact (rightGeneratorValue_spec S f).inner tendsto_const_nhds
  have hg :
      Tendsto
        (fun h : ℝ≥0 =>
          inner ℝ (f : H) (rightDifferenceQuotient S h (g : H)))
        l
        (𝓝 (inner ℝ (f : H) (rightGenerator S g))) := by
    exact tendsto_const_nhds.inner (rightGeneratorValue_spec S g)
  have hfun :
      (fun h : ℝ≥0 =>
        inner ℝ (rightDifferenceQuotient S h (f : H)) (g : H)) =
      fun h : ℝ≥0 =>
        inner ℝ (f : H) (rightDifferenceQuotient S h (g : H)) := by
    funext h
    exact inner_rightDifferenceQuotient_eq S hrev h (f : H) (g : H)
  rw [hfun] at hf
  exact tendsto_nhds_unique hf hg

end

end ReversibleGenerator
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ReversibleGenerator.lean:55published source at 0e31a3cda412