AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerSemigroup

- A transition-kernel Markov semigroup which maps bounded continuous real observables to continuous observables. Boundedness of the image is derived from the Markov property rather than included as a field.

structure FellerTransitionKernelContract (K : ℝ≥0 → Kernel E E) : Prop
    extends TransitionKernelContract K where
  mapsContinuous : ∀ t (f : E →ᵇ ℝ),
    Continuous fun x => ∫ y, f y ∂K t x

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FellerSemigroup.lean:42published source at ed709a7f320d

No declaration docstring.

private theorem integrable_boundedContinuousFunction
    (f : E →ᵇ ℝ) (μ : Measure E) [IsFiniteMeasure μ] :
    Integrable (fun x => f x) μ := by
  refine Integrable.of_bound f.continuous.aestronglyMeasurable ‖f‖ ?_
  exact ae_of_all _ fun x => f.norm_coe_le_norm x

omit [BorelSpace E] in

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FellerSemigroup.lean:47published source at ed709a7f320d

No declaration docstring.

private theorem norm_kernelIntegral_le
    {K : ℝ≥0 → Kernel E E} (hK : FellerTransitionKernelContract K)
    (t : ℝ≥0) (f : E →ᵇ ℝ) (x : E) :
    ‖∫ y, f y ∂K t x‖ ≤ ‖f‖ := by
  let : IsMarkovKernel (K t) := hK.toTransitionKernelContract.isMarkov t
  simpa using
    (norm_integral_le_of_norm_le_const (μ := K t x)
      (ae_of_all _ fun y => f.norm_coe_le_norm y))

/-- The bounded continuous observable obtained by integrating against the
transition kernel at time `t`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FellerSemigroup.lean:54published source at ed709a7f320d

- The bounded continuous observable obtained by integrating against the transition kernel at time `t`.

def fellerOperatorValue {K : ℝ≥0 → Kernel E E}
    (hK : FellerTransitionKernelContract K) (t : ℝ≥0)
    (f : E →ᵇ ℝ) : E →ᵇ ℝ :=
  BoundedContinuousFunction.ofNormedAddCommGroup
    (fun x => ∫ y, f y ∂K t x)
    (hK.mapsContinuous t f) ‖f‖
    (norm_kernelIntegral_le hK t f)

omit [BorelSpace E] in
@[simp]

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FellerSemigroup.lean:65published source at ed709a7f320d

No declaration docstring.

theorem fellerOperatorValue_apply {K : ℝ≥0 → Kernel E E}
    (hK : FellerTransitionKernelContract K) (t : ℝ≥0)
    (f : E →ᵇ ℝ) (x : E) :
    fellerOperatorValue hK t f x = ∫ y, f y ∂K t x := rfl

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FellerSemigroup.lean:75published source at ed709a7f320d

No declaration docstring.

private theorem fellerOperatorValue_add {K : ℝ≥0 → Kernel E E}
    (hK : FellerTransitionKernelContract K) (t : ℝ≥0)
    (f g : E →ᵇ ℝ) :
    fellerOperatorValue hK t (f + g) =
      fellerOperatorValue hK t f + fellerOperatorValue hK t g := by
  let : IsMarkovKernel (K t) := hK.toTransitionKernelContract.isMarkov t
  ext x
  change (∫ y, f y + g y ∂K t x) =
    (∫ y, f y ∂K t x) + ∫ y, g y ∂K t x
  exact integral_add
    (integrable_boundedContinuousFunction f (K t x))
    (integrable_boundedContinuousFunction g (K t x))

omit [BorelSpace E] in

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FellerSemigroup.lean:80published source at ed709a7f320d

No declaration docstring.

private theorem fellerOperatorValue_smul {K : ℝ≥0 → Kernel E E}
    (hK : FellerTransitionKernelContract K) (t : ℝ≥0)
    (c : ℝ) (f : E →ᵇ ℝ) :
    fellerOperatorValue hK t (c • f) =
      c • fellerOperatorValue hK t f := by
  let : IsMarkovKernel (K t) := hK.toTransitionKernelContract.isMarkov t
  ext x
  change (∫ y, c • f y ∂K t x) = c • ∫ y, f y ∂K t x
  rw [integral_smul]

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FellerSemigroup.lean:94published source at ed709a7f320d

No declaration docstring.

private def fellerLinearMap {K : ℝ≥0 → Kernel E E}
    (hK : FellerTransitionKernelContract K) (t : ℝ≥0) :
    (E →ᵇ ℝ) →ₗ[ℝ] (E →ᵇ ℝ) :=
  { toFun := fellerOperatorValue hK t
    map_add' := fellerOperatorValue_add hK t
    map_smul' := fellerOperatorValue_smul hK t }

/-- The Feller Markov operator as a continuous linear map on bounded
continuous real observables. Its operator norm is at most one. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FellerSemigroup.lean:104published source at ed709a7f320d

- The Feller Markov operator as a continuous linear map on bounded continuous real observables. Its operator norm is at most one.

def fellerOperator {K : ℝ≥0 → Kernel E E}
    (hK : FellerTransitionKernelContract K) (t : ℝ≥0) :
    (E →ᵇ ℝ) →L[ℝ] (E →ᵇ ℝ) :=
  LinearMap.mkContinuous (fellerLinearMap hK t) 1 fun f => by
    change ‖fellerOperatorValue hK t f‖ ≤ 1 * ‖f‖
    rw [one_mul]
    unfold fellerOperatorValue
    exact BoundedContinuousFunction.norm_ofNormedAddCommGroup_le
      (hK.mapsContinuous t f) (norm_nonneg f)
      (norm_kernelIntegral_le hK t f)

@[simp]

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FellerSemigroup.lean:113published source at ed709a7f320d

No declaration docstring.

theorem fellerOperator_apply {K : ℝ≥0 → Kernel E E}
    (hK : FellerTransitionKernelContract K) (t : ℝ≥0)
    (f : E →ᵇ ℝ) (x : E) :
    fellerOperator hK t f x = ∫ y, f y ∂K t x := rfl

/-- The pointwise contraction estimate inherited from integration against a
probability kernel. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FellerSemigroup.lean:125published source at ed709a7f320d

- The pointwise contraction estimate inherited from integration against a probability kernel.

theorem norm_fellerOperator_apply_le {K : ℝ≥0 → Kernel E E}
    (hK : FellerTransitionKernelContract K) (t : ℝ≥0)
    (f : E →ᵇ ℝ) :
    ‖fellerOperator hK t f‖ ≤ ‖f‖ := by
  exact BoundedContinuousFunction.norm_ofNormedAddCommGroup_le
    (hK.mapsContinuous t f) (norm_nonneg f)
    (norm_kernelIntegral_le hK t f)

/-- Jensen's inequality for the square under a Feller Markov operator:
`(P_t f x)^2 ≤ P_t(f^2)(x)`. This is equation (1.2.11) in Chewi's
2026-08-09 edition. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FellerSemigroup.lean:132published source at ed709a7f320dOpen detailed card

- Jensen's inequality for the square under a Feller Markov operator: `(P_t f x)^2 ≤ P_t(f^2)(x)`. This is equation (1.2.11) in Chewi's 2026-08-09 edition.

theorem sq_fellerOperator_apply_le {K : ℝ≥0 → Kernel E E}
    (hK : FellerTransitionKernelContract K) (t : ℝ≥0)
    (f : E →ᵇ ℝ) (x : E) :
    (fellerOperator hK t f x) ^ 2 ≤
      fellerOperator hK t (f * f) x := by
  let : IsMarkovKernel (K t) := hK.toTransitionKernelContract.isMarkov t
  have hsquare : Integrable ((fun r : ℝ => r ^ 2) ∘ fun y => f y) (K t x) := by
    simpa [Function.comp_def, pow_two] using
      (integrable_boundedContinuousFunction (f * f) (K t x))
  have hJensen :=
    (even_two.convexOn_pow : ConvexOn ℝ Set.univ fun r : ℝ => r ^ 2).map_integral_le
      (continuousOn_pow 2) isClosed_univ
      (ae_of_all _ fun y => Set.mem_univ (f y))
      (integrable_boundedContinuousFunction f (K t x))
      hsquare
  simpa [Function.comp_def, pow_two] using hJensen

/-- The zero-time Feller operator is the identity continuous linear map. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FellerSemigroup.lean:143published source at ed709a7f320dOpen detailed card

- The zero-time Feller operator is the identity continuous linear map.

theorem fellerOperator_zero {K : ℝ≥0 → Kernel E E}
    (hK : FellerTransitionKernelContract K) :
    fellerOperator hK 0 = ContinuousLinearMap.id ℝ (E →ᵇ ℝ) := by
  ext f x
  change (∫ y, f y ∂K 0 x) = f x
  rw [hK.toTransitionKernelContract.initial, Kernel.id_apply]
  exact integral_dirac' f x f.continuous.stronglyMeasurable

/-- Chapman--Kolmogorov yields the continuous-linear operator semigroup law. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FellerSemigroup.lean:161published source at ed709a7f320d

- Chapman--Kolmogorov yields the continuous-linear operator semigroup law.

theorem fellerOperator_add {K : ℝ≥0 → Kernel E E}
    (hK : FellerTransitionKernelContract K) (s t : ℝ≥0) :
    fellerOperator hK (s + t) =
      (fellerOperator hK s).comp (fellerOperator hK t) := by
  let : IsMarkovKernel (K s) := hK.toTransitionKernelContract.isMarkov s
  let : IsMarkovKernel (K t) := hK.toTransitionKernelContract.isMarkov t
  ext f x
  change (∫ z, f z ∂K (s + t) x) =
    ∫ y, (∫ z, f z ∂K t y) ∂K s x
  rw [hK.toTransitionKernelContract.chapmanKolmogorov s t]
  exact Kernel.integral_comp
    (integrable_boundedContinuousFunction f ((K t ∘ₖ K s) x))

/-- A Feller transition-kernel contract therefore supplies the exact
continuous-linear semigroup consumed by the right-generator development. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FellerSemigroup.lean:170published source at ed709a7f320dOpen detailed card

- A Feller transition-kernel contract therefore supplies the exact continuous-linear semigroup consumed by the right-generator development.

def continuousLinearSemigroupOfFeller {K : ℝ≥0 → Kernel E E}
    (hK : FellerTransitionKernelContract K) :
    ContinuousLinearSemigroup (E →ᵇ ℝ) where
  op := fellerOperator hK
  op_zero := fellerOperator_zero hK
  op_add := fellerOperator_add hK

@[simp]

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FellerSemigroup.lean:185published source at ed709a7f320dOpen detailed card

No declaration docstring.

theorem continuousLinearSemigroupOfFeller_op_apply
    {K : ℝ≥0 → Kernel E E} (hK : FellerTransitionKernelContract K)
    (t : ℝ≥0) (f : E →ᵇ ℝ) (x : E) :
    (continuousLinearSemigroupOfFeller hK).op t f x =
      ∫ y, f y ∂K t x := rfl

end

end FellerSemigroup
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FellerSemigroup.lean:193published source at ed709a7f320d