AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.L2GeneratorIdentities

- If expectation under `pi` is invariant under an `L²(pi)` semigroup, then its generator integrates to zero on the generator domain.

theorem integral_rightGenerator_eq_zero_of_expectation_invariant
    (pi : Measure α) [IsFiniteMeasure pi]
    (S : ContinuousLinearSemigroup (Lp ℝ 2 pi))
    (hinv : ∀ (t : ℝ≥0) (f : Lp ℝ 2 pi),
      TechnicalLemmas.Measure.L2Expectation.expectation pi (S.op t f) =
        TechnicalLemmas.Measure.L2Expectation.expectation pi f)
    (f : generatorDomainSubmodule S) :
    (∫ x, rightGenerator S f x ∂pi) = 0 := by
  have h :=
    GeneratorStationarity.invariantFunctional_rightGenerator_eq_zero
      S (TechnicalLemmas.Measure.L2Expectation.expectation pi) hinv f
  simpa [TechnicalLemmas.Measure.L2Expectation.expectation_apply_eq_integral]
    using h

/-- Reversibility of an `L²(pi)` semigroup gives the generator pair symmetry in
source-facing integral form:

`integral (Lf) g dpi = integral f (Lg) dpi`.

The actual construction of the Markov/Langevin semigroup on `L²(pi)` and
membership of canonical density/log-ratio observables in its generator domain
remain separate analytic nodes. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/L2GeneratorIdentities.lean:37published source at 0e31a3cda412

- Reversibility of an `L²(pi)` semigroup gives the generator pair symmetry in source-facing integral form: `integral (Lf) g dpi = integral f (Lg) dpi`. The actual construction of the Markov/Langevin semigroup on `L²(pi)` and membership of canonical density/log-ratio observables in its generator domain remain separate analytic nodes.

theorem integral_rightGenerator_mul_eq_integral_mul_rightGenerator
    (pi : Measure α) [IsFiniteMeasure pi]
    (S : ContinuousLinearSemigroup (Lp ℝ 2 pi))
    (hrev : Reversibility.IsReversible S)
    (f g : generatorDomainSubmodule S) :
    (∫ x, rightGenerator S f x * (g : Lp ℝ 2 pi) x ∂pi) =
      ∫ x, (f : Lp ℝ 2 pi) x * rightGenerator S g x ∂pi := by
  have h := ReversibleGenerator.inner_rightGenerator_eq S hrev f g
  rw [MeasureTheory.L2.inner_def, MeasureTheory.L2.inner_def] at h
  simpa using h

end

end L2GeneratorIdentities
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/L2GeneratorIdentities.lean:59published source at 0e31a3cda412