AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator

- A nonnegative-time semigroup of continuous linear operators on a real normed space.

structure ContinuousLinearSemigroup (M : Type*) [NormedAddCommGroup M]
    [NormedSpace ℝ M] where
  op : ℝ≥0 → M →L[ℝ] M
  op_zero : op 0 = ContinuousLinearMap.id ℝ M
  op_add : ∀ s t, op (s + t) = (op s).comp (op t)

/-- Application form of the semigroup law. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/OperatorGenerator.lean:33published source at 77184245109a

- Application form of the semigroup law.

theorem ContinuousLinearSemigroup.op_add_apply
    (S : ContinuousLinearSemigroup M) (s t : ℝ≥0) (f : M) :
    S.op (s + t) f = S.op s (S.op t f) := by
  rw [S.op_add]
  rfl

/-- Operators in a one-parameter semigroup commute. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/OperatorGenerator.lean:40published source at 77184245109a

- Operators in a one-parameter semigroup commute.

theorem ContinuousLinearSemigroup.op_comm_apply
    (S : ContinuousLinearSemigroup M) (s t : ℝ≥0) (f : M) :
    S.op s (S.op t f) = S.op t (S.op s f) := by
  calc
    S.op s (S.op t f) = S.op (s + t) f :=
      (S.op_add_apply s t f).symm
    _ = S.op (t + s) f := by rw [add_comm]
    _ = S.op t (S.op s f) := S.op_add_apply t s f

/-- The right difference quotient used to define the infinitesimal generator
in the chosen norm topology. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/OperatorGenerator.lean:47published source at 77184245109a

- The right difference quotient used to define the infinitesimal generator in the chosen norm topology.

def rightDifferenceQuotient (S : ContinuousLinearSemigroup M)
    (h : ℝ≥0) (f : M) : M :=
  ((h : ℝ)⁻¹) • (S.op h f - f)

/-- `g` is the right-generator value of `f` when the semigroup difference
quotient converges to `g` through strictly positive times. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/OperatorGenerator.lean:58published source at 77184245109a

- `g` is the right-generator value of `f` when the semigroup difference quotient converges to `g` through strictly positive times.

def HasRightGeneratorAt (S : ContinuousLinearSemigroup M)
    (f g : M) : Prop :=
  Tendsto (fun h : ℝ≥0 => rightDifferenceQuotient S h f)
    (nhdsWithin 0 (Ioi 0)) (𝓝 g)

/-- The domain of the right generator in the chosen norm topology. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/OperatorGenerator.lean:64published source at 77184245109aOpen detailed card

- The domain of the right generator in the chosen norm topology.

def generatorDomain (S : ContinuousLinearSemigroup M) : Set M :=
  {f | ∃ g, HasRightGeneratorAt S f g}

/-- The right difference quotient commutes with every semigroup operator. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/OperatorGenerator.lean:70published source at 77184245109a

- The right difference quotient commutes with every semigroup operator.

theorem rightDifferenceQuotient_map
    (S : ContinuousLinearSemigroup M) (t h : ℝ≥0) (f : M) :
    rightDifferenceQuotient S h (S.op t f) =
      S.op t (rightDifferenceQuotient S h f) := by
  unfold rightDifferenceQuotient
  rw [S.op_comm_apply h t f]
  rw [← (S.op t).map_sub]
  rw [(S.op t).map_smul]

/-- The generator graph is invariant under the semigroup, and the generator
commutes with the semigroup on its domain. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/OperatorGenerator.lean:74published source at 77184245109a

- The generator graph is invariant under the semigroup, and the generator commutes with the semigroup on its domain.

theorem HasRightGeneratorAt.map
    {S : ContinuousLinearSemigroup M} {f g : M}
    (hfg : HasRightGeneratorAt S f g) (t : ℝ≥0) :
    HasRightGeneratorAt S (S.op t f) (S.op t g) := by
  unfold HasRightGeneratorAt at hfg ⊢
  have hop :
      Tendsto (S.op t) (𝓝 g) (𝓝 (S.op t g)) :=
    (S.op t).continuous.continuousAt
  have hmapped :
      Tendsto (fun h : ℝ≥0 => S.op t (rightDifferenceQuotient S h f))
        (nhdsWithin 0 (Ioi 0)) (𝓝 (S.op t g)) :=
    hop.comp hfg
  simpa only [rightDifferenceQuotient_map] using hmapped

/-- In particular, the right-generator domain is preserved by the semigroup. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/OperatorGenerator.lean:85published source at 77184245109a

- In particular, the right-generator domain is preserved by the semigroup.

theorem generatorDomain_map
    (S : ContinuousLinearSemigroup M) {f : M}
    (hf : f ∈ generatorDomain S) (t : ℝ≥0) :
    S.op t f ∈ generatorDomain S := by
  rcases hf with ⟨g, hfg⟩
  exact ⟨S.op t g, hfg.map t⟩

/-- The forward right difference quotient of the semigroup orbit at time `t`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/OperatorGenerator.lean:100published source at 77184245109aOpen detailed card

- The forward right difference quotient of the semigroup orbit at time `t`.

def rightOrbitDifferenceQuotient (S : ContinuousLinearSemigroup M)
    (t h : ℝ≥0) (f : M) : M :=
  ((h : ℝ)⁻¹) • (S.op (t + h) f - S.op t f)

/-- Semigroup algebra rewrites the orbit quotient at time `t` as the generator
quotient applied to `S.op t f`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/OperatorGenerator.lean:108published source at 77184245109a

- Semigroup algebra rewrites the orbit quotient at time `t` as the generator quotient applied to `S.op t f`.

theorem rightOrbitDifferenceQuotient_eq
    (S : ContinuousLinearSemigroup M) (t h : ℝ≥0) (f : M) :
    rightOrbitDifferenceQuotient S t h f =
      rightDifferenceQuotient S h (S.op t f) := by
  unfold rightOrbitDifferenceQuotient rightDifferenceQuotient
  rw [add_comm t h]
  rw [S.op_add_apply h t f]

/-- Chewi's backward-equation calculation, in a precise right-difference
quotient form: if `g` is the generator value of `f`, then the orbit derivative
at time `t` converges to `S.op t g`, and this is also the generator value of
`S.op t f`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/OperatorGenerator.lean:114published source at 77184245109a

- Chewi's backward-equation calculation, in a precise right-difference quotient form: if `g` is the generator value of `f`, then the orbit derivative at time `t` converges to `S.op t g`, and this is also the generator value of `S.op t f`.

theorem kolmogorov_backward_right
    (S : ContinuousLinearSemigroup M) {f g : M}
    (hfg : HasRightGeneratorAt S f g) (t : ℝ≥0) :
    HasRightGeneratorAt S (S.op t f) (S.op t g) ∧
      Tendsto (fun h : ℝ≥0 => rightOrbitDifferenceQuotient S t h f)
        (nhdsWithin 0 (Ioi 0)) (𝓝 (S.op t g)) := by
  have hmap := hfg.map t
  constructor
  · exact hmap
  · simpa only [HasRightGeneratorAt, rightOrbitDifferenceQuotient_eq] using hmap

end

end OperatorGenerator
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/OperatorGenerator.lean:126published source at 77184245109aOpen detailed card