AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.WeakForwardEquation

- The dual action of a semigroup on a continuous linear functional: `Pₜ* ℓ = ℓ ∘ Pₜ`.

def dualAction
    (S : ContinuousLinearSemigroup M) (t : ℝ≥0)
    (ell : M →L[ℝ] ℝ) : M →L[ℝ] ℝ :=
  ell.comp (S.op t)

@[simp]

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/WeakForwardEquation.lean:36published source at 0e31a3cda412

No declaration docstring.

theorem dualAction_apply
    (S : ContinuousLinearSemigroup M) (t : ℝ≥0)
    (ell : M →L[ℝ] ℝ) (f : M) :
    dualAction S t ell f = ell (S.op t f) :=
  rfl

/-- The dual action starts at the identity. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/WeakForwardEquation.lean:42published source at 0e31a3cda412

- The dual action starts at the identity.

theorem dualAction_zero
    (S : ContinuousLinearSemigroup M) (ell : M →L[ℝ] ℝ) :
    dualAction S 0 ell = ell := by
  ext f
  rw [dualAction_apply, S.op_zero]
  rfl

/-- Dual Chapman--Kolmogorov law.  The order is reversed by composition, as
expected for the adjoint action. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/WeakForwardEquation.lean:49published source at 0e31a3cda412

- Dual Chapman--Kolmogorov law. The order is reversed by composition, as expected for the adjoint action.

theorem dualAction_add
    (S : ContinuousLinearSemigroup M) (ell : M →L[ℝ] ℝ)
    (s t : ℝ≥0) :
    dualAction S (s + t) ell = dualAction S t (dualAction S s ell) := by
  ext f
  simp only [dualAction_apply]
  rw [S.op_add_apply]

/-- Right difference quotient of the weak pairing
`⟨f, Pₜ* ell⟩ = ell (Pₜ f)`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/WeakForwardEquation.lean:58published source at 0e31a3cda412

- Right difference quotient of the weak pairing `⟨f, Pₜ* ell⟩ = ell (Pₜ f)`.

def rightDualPairingDifferenceQuotient
    (S : ContinuousLinearSemigroup M) (ell : M →L[ℝ] ℝ)
    (t h : ℝ≥0) (f : M) : ℝ :=
  ((h : ℝ)⁻¹) •
    (dualAction S (t + h) ell f - dualAction S t ell f)

/-- The weak dual quotient is obtained by applying the functional to the
ordinary semigroup orbit quotient. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/WeakForwardEquation.lean:68published source at 0e31a3cda412

- The weak dual quotient is obtained by applying the functional to the ordinary semigroup orbit quotient.

theorem rightDualPairingDifferenceQuotient_eq
    (S : ContinuousLinearSemigroup M) (ell : M →L[ℝ] ℝ)
    (t h : ℝ≥0) (f : M) :
    rightDualPairingDifferenceQuotient S ell t h f =
      ell (rightOrbitDifferenceQuotient S t h f) := by
  simp only [rightDualPairingDifferenceQuotient, dualAction_apply,
    rightOrbitDifferenceQuotient]
  rw [map_smul, map_sub]

/-- Weak right-hand Kolmogorov forward equation.

For an observable in the canonical generator domain, differentiating the dual
pairing gives the evolved functional applied to the generator:

`d⁺/dt (Pₜ* ell)(f) = (Pₜ* ell)(A f)`.

This is the rigorous operator-level content of the calculation immediately
preceding Chewi Proposition 1.2.6.  A measure-valued identity involving `A*`
requires an additional adjoint-domain realization and is not claimed here. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/WeakForwardEquation.lean:76published source at 0e31a3cda412

- Weak right-hand Kolmogorov forward equation. For an observable in the canonical generator domain, differentiating the dual pairing gives the evolved functional applied to the generator: `d⁺/dt (Pₜ* ell)(f) = (Pₜ* ell)(A f)`. This is the rigorous operator-level content of the calculation immediately preceding Chewi Proposition 1.2.6. A measure-valued identity involving `A*` requires an additional adjoint-domain realization and is not claimed here.

theorem kolmogorov_forward_weak_right
    (S : ContinuousLinearSemigroup M) (ell : M →L[ℝ] ℝ)
    (f : generatorDomainSubmodule S) (t : ℝ≥0) :
    Tendsto
      (fun h : ℝ≥0 =>
        rightDualPairingDifferenceQuotient S ell t h (f : M))
      (nhdsWithin 0 (Ioi 0))
      (𝓝 (dualAction S t ell (rightGenerator S f))) := by
  have hell :
      Tendsto ell
        (𝓝 (S.op t (rightGenerator S f)))
        (𝓝 (ell (S.op t (rightGenerator S f)))) :=
    ell.continuous.continuousAt
  have hmap :
      Tendsto
        (fun h : ℝ≥0 =>
          ell (rightOrbitDifferenceQuotient S t h (f : M)))
        (nhdsWithin 0 (Ioi 0))
        (𝓝 (ell (S.op t (rightGenerator S f)))) :=
    hell.comp (kolmogorov_backward_right_generator S f t)
  simpa only [rightDualPairingDifferenceQuotient_eq, dualAction_apply] using hmap

end

end WeakForwardEquation
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/WeakForwardEquation.lean:95published source at 0e31a3cda412