1.2 · Book p. 10 · PDF p. 22
Markov Semigroup Theory
Encodes a Markov process through its semigroup and generator, then relates reversibility, Dirichlet forms, functional inequalities, and convergence.
Open this section in the canonical August 9 source ↗Theorem 1.2.14
For a stationary reversible generator, the two negative-generator pairings equal each other and the integrated carre du champ.
\[-\int fLg\,d\pi=-\int gLf\,d\pi=\int\Gamma(f,g)\,d\pi\]
Proof
1
\[0=\int L(fg)\,d\pi=\int fLg\,d\pi+\int gLf\,d\pi+2\int\Gamma(f,g)\,d\pi\]
Lean
fundamental_integration_by_parts2
\[\int fLg\,d\pi=\int gLf\,d\pi\quad\Longrightarrow\quad-\int fLg\,d\pi=\int\Gamma(f,g)\,d\pi\]
Lean
fundamental_integration_by_partsIntegrating the definition of Gamma removes the L(fg) term by stationarity and identifies the remaining two terms by generator symmetry.
Why is this valid?
Stationarity and symmetry are concrete hypotheses produced by the semigroup route; they are not inferred from an algebraic generator display.
Source assumptions
- stationary law
- reversible generator
- functions in the generator form domain
Formal assumptions
- three explicit Integrable terms
- zero integral of L(fg)
- symmetric generator pairing
View Lean formalization
ASTIS performs this integral algebra and exposes integrability for L(fg), f Lg, and g Lf separately.
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp.fundamental_integration_by_parts
theorem fundamental_integration_by_parts
[MeasurableSpace X]
(mu : Measure X) (generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
(f g : X → ℝ)
(hLfg : Integrable (generator (f * g)) mu)
(hfLg : Integrable (fun x => f x * generator g x) mu)
(hgLf : Integrable (fun x => g x * generator f x) mu)
(hstationary : (∫ x, generator (f * g) x ∂mu) = 0)
(hsymmetric :
(∫ x, f x * generator g x ∂mu) =
∫ x, g x * generator f x ∂mu) :
FunctionalInequalities.Generator.dirichletForm mu generator f g =
FunctionalInequalities.Generator.dirichletForm mu generator g f ∧
FunctionalInequalities.Generator.dirichletForm mu generator f g =
∫ x, carreDuChamp generator f g x ∂mu := by
have hsub : Integrable
(fun x => generator (f * g) x - f x * generator g x) mu :=
hLfg.sub hfLg
have hgammaIntegral :
(∫ x, carreDuChamp generator f g x ∂mu) =
(2 : ℝ)⁻¹ *
((∫ x, generator (f * g) x ∂mu) -
(∫ x, f x * generator g x ∂mu) -
∫ x, g x * generator f x ∂mu) := by
change
(∫ x, (2 : ℝ)⁻¹ *
(generator (f * g) x - f x * generator g x -
g x * generator f x) ∂mu) = _
rw [integral_const_mul,
integral_sub hsub hgLf, integral_sub hLfg hfLg]
constructor
· simp only [FunctionalInequalities.Generator.dirichletForm]
rw [hsymmetric]
· simp only [FunctionalInequalities.Generator.dirichletForm]
rw [hgammaIntegral, hstationary, hsymmetric]
ring
/-- Chewi Corollary 1.2.15: the negative reversible generator has a
nonnegative quadratic form once Gamma is pointwise nonnegative. -/Imports
- Mathlib.Algebra.Module.LinearMap.Basic
- Mathlib.Data.Real.Basic
- Mathlib.MeasureTheory.Integral.Bochner.Basic
- Mathlib.Topology.Instances.NNReal.Lemmas
- Mathlib.Tactic.Ring
- AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Generator
Local dependencies
Downstream consumers
- negative generator
- Poincare inequality
- Langevin Dirichlet form
Corollary 1.2.15
The negative generator of a reversible Markov semigroup has a nonnegative quadratic form.
\[-\langle f,Lf\rangle_{L^2(\pi)}=\int\Gamma(f,f)\,d\pi\ge0\]
Proof
1
\[-\langle f,Lf\rangle_{L^2(\pi)}=\int\Gamma(f,f)\,d\pi\ge0\]
Lean
negativeGenerator_quadratic_nonnegThe quadratic pairing integral f(-L)f equals integral Gamma(f,f), which is nonnegative.
Why is this valid?
The theorem consumes pointwise Gamma nonnegativity and the stationary generator identity instead of assuming the desired quadratic conclusion.
Source assumptions
- the assumptions of Theorem 1.2.14
- Gamma(f,f) is nonnegative
Formal assumptions
- integrability of L(f squared) and f Lf
- stationarity
- pointwise Gamma nonnegativity
View Lean formalization
ASTIS invokes the compiled integration-by-parts theorem and Mathlib integral nonnegativity.
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp.negativeGenerator_quadratic_nonneg
theorem negativeGenerator_quadratic_nonneg
[MeasurableSpace X]
(mu : Measure X) (generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
(f : X → ℝ)
(hLf2 : Integrable (generator (f * f)) mu)
(hfLf : Integrable (fun x => f x * generator f x) mu)
(hstationary : (∫ x, generator (f * f) x ∂mu) = 0)
(hgamma : ∀ x, 0 ≤ carreDuChamp generator f f x) :
0 ≤ FunctionalInequalities.Generator.dirichletForm mu generator f f := by
have hibp := fundamental_integration_by_parts mu generator f f
hLf2 hfLf hfLf hstationary rfl
rw [hibp.2]
exact integral_nonneg_of_ae (Filter.Eventually.of_forall hgamma)
end CarreDuChamp
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheoryImports
- Mathlib.Algebra.Module.LinearMap.Basic
- Mathlib.Data.Real.Basic
- Mathlib.MeasureTheory.Integral.Bochner.Basic
- Mathlib.Topology.Instances.NNReal.Lemmas
- Mathlib.Tactic.Ring
- AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Generator
Local dependencies
Downstream consumers
- spectral gap
- Poincare inequality
Definition 1.2.19
A Markov process satisfies a Poincare inequality when variance is bounded by a constant times its generator Dirichlet energy.
\[\operatorname{Var}_\pi(f)\le C_{\mathrm P}\int\Gamma(f,f)\,d\pi\]
For every observable in the generator form domain, Var_mu(f) is at most C times integral f(-L)f dmu.
Why is this valid?
Probability normalization, positivity of C, finite mean/variance, and integrability of f Lf are explicit.
Source assumptions
- a stationary reversible Markov generator
- observables in its form domain
Formal assumptions
- a probability measure
- a real generator action
- PoincareAdmissible finite integrals
View Lean formalization
ASTIS separates this general generator definition from the gradient-energy identity special to Langevin diffusion.
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Generator.SatisfiesPoincare
def SatisfiesPoincare
(mu : Measure E) (generator : (E → ℝ) → E → ℝ)
(C : ℝ) : Prop :=
IsProbabilityMeasure mu ∧ 0 < C ∧
∀ f : E → ℝ, PoincareAdmissible mu generator f →
variance mu f ≤ C * dirichletForm mu generator f f
/-- Relative entropy of a density `rho` with respect to its reference
probability measure. Mathlib's totalized `Real.log 0 = 0` gives the standard
zero-density convention in the product `rho * log rho`. -/Imports
- Mathlib.MeasureTheory.Integral.Bochner.Basic
Local dependencies
Downstream consumers
- variance decay
- chi-squared decay
- spectral gap
Definition 1.2.25
A Markov process satisfies an LSI when density entropy is bounded by C/2 times the Dirichlet form of the density and its logarithm.
\[\operatorname{Ent}_\pi(f)\le\frac{C_{\mathrm{LSI}}}{2}\int\Gamma(f,\log f)\,d\pi,\qquad f\ge0,\quad\int f\,d\pi=1\]
For every density rho with respect to mu, KL(rho mu || mu) is at most (C/2) E(rho,log rho).
Why is this valid?
The zero-density log convention, normalization, probability reference law, positive constant, and both finite integrals are explicit.
Source assumptions
- a stationary reversible Markov generator
- a density with respect to its invariant law
Formal assumptions
- a probability measure
- LogSobolevAdmissible density
- generator Dirichlet form
View Lean formalization
ASTIS exposes positivity, unit mass, entropy integrability, and generator-energy integrability instead of relying on totalized integrals.
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Generator.SatisfiesLogSobolev
def SatisfiesLogSobolev
(mu : Measure E) (generator : (E → ℝ) → E → ℝ)
(C : ℝ) : Prop :=
IsProbabilityMeasure mu ∧ 0 < C ∧
∀ rho : E → ℝ, LogSobolevAdmissible mu generator rho →
densityEntropy mu rho ≤
(C / 2) * dirichletForm mu generator rho (fun x => Real.log (rho x))
end Generator
end FunctionalInequalities
end TechnicalLemmas
end AutoSamplingTheoryImports
- Mathlib.MeasureTheory.Integral.Bochner.Basic
Local dependencies
No Registry dependency inferred.
Downstream consumers
- KL decay
- Fisher-information specialization
Definition 1.2.1
The Markov operator sends an observable to its conditional expectation after elapsed time t, given the initial state.
\[P_t f(x):=\mathbb E[f(X_t)\mid X_0=x]\]
A transition kernel K_t represents the conditional law of X_t given X_0=x, so P_t f(x) is the integral of f against K_t(x,dy).
Why is this valid?
The state space is measurable, K_t is a Markov kernel, and the observable is measurable and ENNReal-valued so the kernel integral remains measurable.
Source assumptions
- a time-homogeneous Markov process and its conditional transition laws
Formal assumptions
- a transition-kernel contract
- measurable ENNReal observables
View Lean formalization
ASTIS uses a measurable transition-kernel family and defines the conditional-expectation operator by kernel lintegration.
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.MarkovSemigroup.markovOperator
def markovOperator {K : ℝ≥0 → Kernel E E}
(_hK : TransitionKernelContract K) (t : ℝ≥0) :
MeasurableENNReal E → MeasurableENNReal E :=
fun f => by
exact ⟨fun x => ∫⁻ y, f y ∂K t x, f.2.lintegral_kernel⟩
/-- A Markov operator preserves constant nonnegative observables. -/Imports
- Mathlib.Probability.Kernel.Composition.Comp
Local dependencies
Downstream consumers
- semigroup property
- Feller operators
- generator theory
Supporting concrete Markov/Feller realization route
A Markov semigroup records how the law or observables evolve with time.
\[P_0=I,\qquad P_{s+t}=P_sP_t=P_tP_s\]
For a time-homogeneous Markov process, the operator \(P_t\) sends an observable \(f\) to its conditional expectation at time \(t\). The identities \(P_0 = \mathrm{id}\) and \(P_sP_t = P_{s+t}\) encode the Markov evolution at the operator level.
Why is this valid?
The eventual packet must fix the measurable state space, the observable space, positivity and constant preservation, the semigroup law, and the continuity notion used to recover a generator.
Source assumptions
- Markov evolution
- time-homogeneous composition
Formal assumptions
- measurable state space
- specified operator domain
- chosen continuity topology
View Lean formalization
ASTIS separates the algebraic semigroup laws from measurability, continuity, and the choice of function space on which the operators act.
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.WeakGenerator.IntegratedSemigroupGeneratorContract
structure IntegratedSemigroupGeneratorContract {E : Type*} [MeasurableSpace E]
(P : ℝ → (E → ℝ) → E → ℝ)
(generator : (E → ℝ) → E → ℝ)
(domain : Set (E → ℝ))
(μ : Measure E) : Prop where
map_zero : ∀ f, P 0 f = f
map_add : ∀ s, 0 ≤ s → ∀ t, 0 ≤ t → ∀ f,
P (s + t) f = P s (P t f)
orbit_mem_domain : ∀ t, 0 ≤ t → ∀ f ∈ domain, P t f ∈ domain
pairing_continuousOn : ∀ t, 0 ≤ t → ∀ f ∈ domain,
ContinuousOn (fun s => ∫ x, P s f x ∂μ) (Set.Icc 0 t)
pairing_hasDerivWithinAt : ∀ t, 0 ≤ t → ∀ f ∈ domain,
HasDerivWithinAt
(fun s => ∫ x, P s f x ∂μ)
(∫ x, generator (P t f) x ∂μ) (Set.Ici t) t
/-- A semigroup is invariant on its declared generator domain when integrated
generator action vanishes throughout that domain.
This theorem is the operator-domain-to-invariance bridge. All analytic
content is visible in `IntegratedSemigroupGeneratorContract`; in particular,
the right derivative of the integral pairing and preservation of the domain
are not inferred from a formal differential expression. -/Imports
- AutoSamplingTheory.Probability
- Mathlib.Analysis.Calculus.MeanValue
Local dependencies
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.WeakGenerator.isInvariantOn_of_integral_generator_eq_zero
theorem isInvariantOn_of_integral_generator_eq_zero
{E : Type*} [MeasurableSpace E]
{P : ℝ → (E → ℝ) → E → ℝ}
{generator : (E → ℝ) → E → ℝ}
{domain : Set (E → ℝ)} {μ : Measure E}
(hsemigroup : IntegratedSemigroupGeneratorContract P generator domain μ)
(hgenerator_zero : ∀ f ∈ domain, ∫ x, generator f x ∂μ = 0) :
IsInvariantOn P μ domain := by
intro t ht f hf
have hconstant := constant_of_has_deriv_right_zero
(hsemigroup.pairing_continuousOn t ht f hf) (fun s hs => by
have hs0 : 0 ≤ s := hs.1
simpa [hgenerator_zero (P s f)
(hsemigroup.orbit_mem_domain s hs0 f hf)] using
hsemigroup.pairing_hasDerivWithinAt s hs0 f hf)
have htmem : t ∈ Set.Icc (0 : ℝ) t := ⟨ht, le_rfl⟩
simpa [hsemigroup.map_zero f] using hconstant t htmem
/-- Move a supplied sample-space generator derivative to a named law path.
In SDE applications, `hderiv` is usually the Ito-generator derivative for a
test function composed with a process, while `hDrift` and `hDiffusion` identify
the sample drift and diffusion-generator terms with law-level weak-test
integrals. The lemma proves only the reusable rewrite; it does not construct
the process, conditional drift, or Ito theorem.
-/Imports
- AutoSamplingTheory.Probability
- Mathlib.Analysis.Calculus.MeanValue
Local dependencies
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.MarkovSemigroup.chewi_lemma_1_2_2
theorem chewi_lemma_1_2_2 {K : ℝ≥0 → Kernel E E}
(hK : TransitionKernelContract K) :
markovOperator hK 0 = id ∧
∀ s t : ℝ≥0,
markovOperator hK s ∘ markovOperator hK t =
markovOperator hK (s + t) ∧
markovOperator hK t ∘ markovOperator hK s =
markovOperator hK (s + t) := by
constructor
· exact markovOperator_zero hK
· intro s t
constructor
· exact markovOperator_comp hK s t
· simpa [add_comm] using markovOperator_comp hK t s
end
end MarkovSemigroup
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheoryImports
- Mathlib.Probability.Kernel.Composition.Comp
Local dependencies
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.MarkovSemigroup.markovOperator_const
theorem markovOperator_const {K : ℝ≥0 → Kernel E E}
(hK : TransitionKernelContract K) (t : ℝ≥0) (c : ℝ≥0∞) :
markovOperator hK t (MeasurableENNReal.const c) =
MeasurableENNReal.const c := by
apply Subtype.ext
funext x
change (∫⁻ _y, c ∂K t x) = c
let : IsMarkovKernel (K t) := hK.isMarkov t
simp
/-- Markov integration is monotone in the observable. -/Imports
- Mathlib.Probability.Kernel.Composition.Comp
Local dependencies
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.MarkovSemigroup.markovOperator_apply_mono
theorem markovOperator_apply_mono {K : ℝ≥0 → Kernel E E}
(hK : TransitionKernelContract K) (t : ℝ≥0)
{f g : MeasurableENNReal E} (hfg : ∀ y, f y ≤ g y) (x : E) :
markovOperator hK t f x ≤ markovOperator hK t g x := by
change (∫⁻ y, f y ∂K t x) ≤ ∫⁻ y, g y ∂K t x
exact lintegral_mono hfg
/-- At time zero, the transition-kernel Markov operator is the identity. -/Imports
- Mathlib.Probability.Kernel.Composition.Comp
Local dependencies
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerSemigroup.norm_fellerOperator_apply_le
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. -/Imports
- AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.MarkovSemigroup
- AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator
- Mathlib.Analysis.Convex.Integral
- Mathlib.Analysis.Convex.Mul
- Mathlib.Probability.Kernel.Composition.IntegralCompProd
- Mathlib.Topology.ContinuousMap.Bounded.Normed
Local dependencies
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerSemigroup.fellerOperator_add
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. -/Imports
- AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.MarkovSemigroup
- AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator
- Mathlib.Analysis.Convex.Integral
- Mathlib.Analysis.Convex.Mul
- Mathlib.Probability.Kernel.Composition.IntegralCompProd
- Mathlib.Topology.ContinuousMap.Bounded.Normed
Local dependencies
No Registry dependency inferred.
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerSemigroup.continuousLinearSemigroupOfFeller
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]Imports
- AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.MarkovSemigroup
- AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator
- Mathlib.Analysis.Convex.Integral
- Mathlib.Analysis.Convex.Mul
- Mathlib.Probability.Kernel.Composition.IntegralCompProd
- Mathlib.Topology.ContinuousMap.Bounded.Normed
Local dependencies
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGeneratorDomain.StronglyContinuousSemigroup.tendsto_op_add
theorem StronglyContinuousSemigroup.tendsto_op_add
(S : StronglyContinuousSemigroup M) (t : ℝ≥0) (f : M) :
Tendsto (fun h : ℝ≥0 => S.op (t + h) f) (𝓝 0) (𝓝 (S.op t f)) := by
have hop : Tendsto (S.op t) (𝓝 f) (𝓝 (S.op t f)) :=
(S.op t).continuous.continuousAt
have hmapped :
Tendsto (fun h : ℝ≥0 => S.op t (S.op h f))
(𝓝 0) (𝓝 (S.op t f)) :=
hop.comp (S.stronglyContinuousAtZero f)
simpa only [ContinuousLinearSemigroup.op_add_apply] using hmapped
/-- The zero vector has generator value zero. -/Imports
- AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator
- Mathlib.Topology.Order.DenselyOrdered
Local dependencies
No Registry dependency inferred.
Downstream consumers
- generator domain
- stationarity
- mixing estimates
Lemma 1.2.2
Identity and Chapman-Kolmogorov transition-kernel laws induce the zero-time, composition, and commutation laws of Markov operators.
\[K_0(x,\cdot)=\delta_x,\quad K_{s+t}(x,A)=\int K_t(y,A)K_s(x,dy)\quad\Longrightarrow\quad P_{s+t}=P_sP_t\]
Proof
1
\[(P_sP_tf)(x)=\int_E\!\int_E f(z)\,K_t(y,dz)\,K_s(x,dy)\]
Lean
chewi_lemma_1_2_22
\[\int_E\!\int_E f(z)\,K_t(y,dz)\,K_s(x,dy)=\int_E f(z)\,K_{s+t}(x,dz)=(P_{s+t}f)(x)\]
Lean
chewi_lemma_1_2_2For measurable nonnegative observables, P_0 is the identity and P_s P_t = P_t P_s = P_{s+t}. The proof is iterated kernel integration plus commutativity of elapsed-time addition.
Why is this valid?
Each K_t is a Markov kernel, K_0 is the identity kernel, and K_{s+t} is the Chapman-Kolmogorov composition. Observables are measurable and ENNReal-valued.
Source assumptions
- a time-homogeneous Markov process
- the Markov property and iterated conditioning
Formal assumptions
- Markov transition kernels at NNReal times
- identity at zero
- Chapman-Kolmogorov kernel composition
View Lean formalization
ASTIS derives the operator identities from transition kernels instead of storing the desired semigroup conclusion as an operator assumption.
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.MarkovSemigroup.chewi_lemma_1_2_2
theorem chewi_lemma_1_2_2 {K : ℝ≥0 → Kernel E E}
(hK : TransitionKernelContract K) :
markovOperator hK 0 = id ∧
∀ s t : ℝ≥0,
markovOperator hK s ∘ markovOperator hK t =
markovOperator hK (s + t) ∧
markovOperator hK t ∘ markovOperator hK s =
markovOperator hK (s + t) := by
constructor
· exact markovOperator_zero hK
· intro s t
constructor
· exact markovOperator_comp hK s t
· simpa [add_comm] using markovOperator_comp hK t s
end
end MarkovSemigroup
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheoryImports
- Mathlib.Probability.Kernel.Composition.Comp
Local dependencies
Downstream consumers
- Feller operator semigroup
- infinitesimal generator
- Kolmogorov equations
Definition 1.2.3
The infinitesimal generator is the right derivative at zero of the semigroup orbit on its convergence domain.
\[Lf:=\lim_{t\downarrow0}\frac{P_tf-f}{t}\]
Lf = g means that (P_h f - f)/h converges to g as h decreases to zero through positive times. The generator domain consists exactly of observables for which such a g exists.
Why is this valid?
A continuous-linear semigroup acts on a real normed space; the right difference quotient uses NNReal time coerced to Real scalars and converges in the ambient norm topology.
Source assumptions
- a Markov semigroup
- existence of the right derivative for the selected observable
Formal assumptions
- a real normed observable space
- a continuous-linear semigroup
- Tendsto through nhdsWithin 0 (Ioi 0)
View Lean formalization
ASTIS resolves the source's stated technical ambiguity by fixing a real normed observable space, norm convergence, and the one-sided positive-time filter.
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator.HasRightGeneratorAt
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. -/Imports
- Mathlib.Analysis.Normed.Operator.Basic
Local dependencies
No Registry dependency inferred.
Downstream consumers
- generator domain
- Kolmogorov backward equation
- concrete Langevin generator identification
Proposition 1.2.5
The right derivative of P_t f is P_t Lf, and P_t f remains in the generator domain with generator P_t Lf.
\[\frac{d}{dt}P_tf=P_tLf=LP_tf\]
Proof
1
\[\frac{P_{t+h}f-P_tf}{h}=P_t\!\left(\frac{P_hf-f}{h}\right)\xrightarrow[h\downarrow0]{}P_tLf\]
Lean
kolmogorov_backward_right2
\[\frac{d}{dt}P_tf=P_tLf=LP_tf\]
Lean
kolmogorov_backward_rightFor f in the generator domain, the forward right orbit quotient at t converges to P_t Lf and L(P_t f) = P_t Lf. This is the one-sided rigorous form of the backward equation.
Why is this valid?
The observable has an actual right-generator witness, and all limits are taken in the selected norm topology through positive time increments.
Source assumptions
- f lies in the generator domain
- the Markov semigroup acts on the selected observable space
Formal assumptions
- ContinuousLinearSemigroup
- HasRightGeneratorAt S f g
- NNReal evaluation time
View Lean formalization
The proof uses semigroup commutation and continuity of each P_t to transport the generator limit; no formal differentiation symbol is left uninterpreted.
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator.kolmogorov_backward_right
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 AutoSamplingTheoryImports
- Mathlib.Analysis.Normed.Operator.Basic
Local dependencies
Downstream consumers
- semigroup energy dissipation
- Poincare and log-Sobolev decay
- concrete Langevin backward equation
Supporting generator and concrete-domain route
The generator is the derivative at time zero of the Markov semigroup.
\[L=\left.\frac{d}{dt}P_t\right|_{t=0}\]
The infinitesimal generator \(L\) records the first-order variation of \(P_t f\) as \(t\) decreases to zero. Its value is defined only for observables for which the difference quotient converges in the chosen function-space topology.
Why is this valid?
Specify the Banach or Hilbert space, the strong limit defining the generator, its domain, and the relation between that closed operator and any smooth-core differential expression.
Source assumptions
- existence of the derivative of the semigroup
Formal assumptions
- explicit difference-quotient convergence
- explicit observable and scalar field
View Lean formalization
The formal differential expression and the closed infinitesimal generator are different objects. ASTIS keeps the analytic domain as an explicit red node.
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.WeakGenerator.weakGeneratorFromSampleDerivative
theorem weakGeneratorFromSampleDerivative {Ω E : Type*}
[MeasurableSpace Ω] [MeasurableSpace E]
{P : Measure Ω} {X : ℝ → Ω → E} {ρ : ℝ → Measure E}
{φ driftTerm diffusionTerm : E → ℝ}
{sampleDrift sampleDiffusion : Ω → ℝ} {s0 σ : ℝ}
(hρ : ∀ s, ρ s = Measure.map (X s) P)
(hX : ∀ s, AEMeasurable (X s) P)
(hφ : ∀ s, AEStronglyMeasurable φ (ρ s))
(hderiv :
HasDerivAt (fun s => ∫ ω, φ (X s ω) ∂P)
((∫ ω, sampleDrift ω ∂P) +
(σ ^ 2 / 2) * (∫ ω, sampleDiffusion ω ∂P)) s0)
(hDrift :
(∫ ω, sampleDrift ω ∂P) = ∫ x, driftTerm x ∂ρ s0)
(hDiffusion :
(∫ ω, sampleDiffusion ω ∂P) = ∫ x, diffusionTerm x ∂ρ s0) :
HasDerivAt (fun s => ∫ x, φ x ∂ρ s)
((∫ x, driftTerm x ∂ρ s0) +
(σ ^ 2 / 2) * (∫ x, diffusionTerm x ∂ρ s0)) s0 := by
have hbase :
HasDerivAt (fun s => ∫ x, φ x ∂ρ s)
((∫ ω, sampleDrift ω ∂P) +
(σ ^ 2 / 2) * (∫ ω, sampleDiffusion ω ∂P)) s0 :=
AutoSamplingTheory.lawIntegralHasDerivAtOfMeasureMapEqAndSample
(P := P) (X := X) (ρ := ρ) (φ := φ)
hρ hX hφ hderiv
simpa [hDrift, hDiffusion] using hbase
end WeakGenerator
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheoryImports
- AutoSamplingTheory.Probability
- Mathlib.Analysis.Calculus.MeanValue
Local dependencies
No Registry dependency inferred.
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerSemigroup.continuousLinearSemigroupOfFeller
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]Imports
- AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.MarkovSemigroup
- AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator
- Mathlib.Analysis.Convex.Integral
- Mathlib.Analysis.Convex.Mul
- Mathlib.Probability.Kernel.Composition.IntegralCompProd
- Mathlib.Topology.ContinuousMap.Bounded.Normed
Local dependencies
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator.generatorDomain_map
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`. -/Imports
- Mathlib.Analysis.Normed.Operator.Basic
Local dependencies
No Registry dependency inferred.
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator.kolmogorov_backward_right
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 AutoSamplingTheoryImports
- Mathlib.Analysis.Normed.Operator.Basic
Local dependencies
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGeneratorDomain.hasRightGeneratorAt_unique
theorem hasRightGeneratorAt_unique
{S : ContinuousLinearSemigroup M} {f g₁ g₂ : M}
(hg₁ : HasRightGeneratorAt S f g₁)
(hg₂ : HasRightGeneratorAt S f g₂) :
g₁ = g₂ := by
unfold HasRightGeneratorAt at hg₁ hg₂
exact tendsto_nhds_unique hg₁ hg₂
/-- Generator limits add. -/Imports
- AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator
- Mathlib.Topology.Order.DenselyOrdered
Local dependencies
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGeneratorDomain.generatorDomainSubmodule
def generatorDomainSubmodule (S : ContinuousLinearSemigroup M) :
Submodule ℝ M where
carrier := generatorDomain S
zero_mem' := ⟨0, hasRightGeneratorAt_zero S⟩
add_mem' := by
intro f g hf hg
rcases hf with ⟨Af, hf⟩
rcases hg with ⟨Ag, hg⟩
exact ⟨Af + Ag, hasRightGeneratorAt_add hf hg⟩
smul_mem' := by
intro c f hf
rcases hf with ⟨Af, hf⟩
exact ⟨c • Af, hasRightGeneratorAt_smul hf c⟩
/-- The canonical right-generator value on its submodule domain. -/Imports
- AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator
- Mathlib.Topology.Order.DenselyOrdered
Local dependencies
No Registry dependency inferred.
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGeneratorDomain.rightGenerator
noncomputable def rightGenerator (S : ContinuousLinearSemigroup M) :
generatorDomainSubmodule S →ₗ[ℝ] M where
toFun := rightGeneratorValue S
map_add' := rightGeneratorValue_add S
map_smul' := rightGeneratorValue_smul S
/-- The canonical generator commutes with the semigroup on its invariant
domain. -/Imports
- AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator
- Mathlib.Topology.Order.DenselyOrdered
Local dependencies
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGeneratorDomain.rightGenerator_map
theorem rightGenerator_map
(S : ContinuousLinearSemigroup M) (t : ℝ≥0)
(f : generatorDomainSubmodule S) :
rightGenerator S
⟨S.op t (f : M), generatorDomain_map S f.property t⟩ =
S.op t (rightGenerator S f) := by
apply hasRightGeneratorAt_unique
· exact rightGeneratorValue_spec S
⟨S.op t (f : M), generatorDomain_map S f.property t⟩
· exact (rightGeneratorValue_spec S f).map t
/-- Chewi's right Kolmogorov backward equation using the canonical bundled
generator rather than an existential generator witness. -/Imports
- AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator
- Mathlib.Topology.Order.DenselyOrdered
Local dependencies
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGeneratorDomain.kolmogorov_backward_right_generator
theorem kolmogorov_backward_right_generator
(S : ContinuousLinearSemigroup M)
(f : generatorDomainSubmodule S) (t : ℝ≥0) :
Tendsto
(fun h : ℝ≥0 => rightOrbitDifferenceQuotient S t h (f : M))
(nhdsWithin 0 (Ioi 0))
(𝓝 (S.op t (rightGenerator S f))) := by
exact (kolmogorov_backward_right S (rightGeneratorValue_spec S f) t).2
end
end OperatorGeneratorDomain
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheoryImports
- AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator
- Mathlib.Topology.Order.DenselyOrdered
Local dependencies
Downstream consumers
- generator/semigroup domain packet
- invariant Gibbs law
Definition 1.2.10
A Markov semigroup is reversible when every time operator is symmetric in the L2 inner product of its stationary law.
\[\int f\,P_tg\,d\pi=\int g\,P_tf\,d\pi\qquad(t\ge0)\]
Reversibility requires <P_t f,g> = <f,P_t g> for every time and every pair of L2 observables. ASTIS states the equality on an abstract real Hilbert space, instantiated by L2(pi) in the source application.
Why is this valid?
The ambient space must carry the real inner product representing L2(pi), and each P_t must be a continuous linear operator on that space.
Source assumptions
- a Markov semigroup acting on L2(pi)
- pi is the stationary reference law
Formal assumptions
- a real inner-product space
- a nonnegative-time continuous-linear semigroup
- the symmetry equality for every time and pair of observables
View Lean formalization
The predicate isolates self-adjointness from construction of the concrete L2 semigroup and from proof that pi is invariant.
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Reversibility.IsReversible
def IsReversible (S : ContinuousLinearSemigroup H) : Prop :=
∀ (t : ℝ≥0) (f g : H),
inner ℝ (S.op t f) g = inner ℝ f (S.op t g)
/-- The constant identity semigroup is reversible on every real inner-product
space. -/Imports
- AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator
- Mathlib.Analysis.InnerProductSpace.Basic
Local dependencies
No Registry dependency inferred.
Downstream consumers
- generator symmetry
- fundamental integration-by-parts identity
- spectral-gap analysis
Displayed identity (1.2.11)
A Markov semigroup satisfies the pointwise Jensen inequality: the square of P_t f is bounded by P_t applied to the square of f.
\[(P_tf)^2\le P_t(f^2)\]
For each starting point x, the transition law K_t(x,dy) is a probability measure. Convexity of the square gives (integral f dK_t(x)) squared at most integral f squared dK_t(x).
Why is this valid?
The observable is bounded and continuous, hence both it and its square are Bochner integrable under every transition probability. The Feller contract supplies the Markov-kernel instance.
Source assumptions
- a Markov transition semigroup
- a real observable for which the two expectations exist
Formal assumptions
- a Feller transition-kernel contract
- a bounded continuous real observable
View Lean formalization
ASTIS applies Mathlib's integral Jensen theorem to the actual probability transition kernel underlying the Feller operator. The inequality is derived rather than added to an operator contract.
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerSemigroup.sq_fellerOperator_apply_le
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. -/Imports
- AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.MarkovSemigroup
- AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator
- Mathlib.Analysis.Convex.Integral
- Mathlib.Analysis.Convex.Mul
- Mathlib.Probability.Kernel.Composition.IntegralCompProd
- Mathlib.Topology.ContinuousMap.Bounded.Normed
Local dependencies
Downstream consumers
- carre-du-champ non-negativity
- Markov variance contraction
Definition 1.2.12
The carre du champ is the bilinear defect between applying the generator after multiplication and multiplying after applying the generator.
\[\Gamma(f,g):=\frac12\bigl(L(fg)-fLg-gLf\bigr)\]
For a linear generator L, Gamma(f,g) = (L(fg) - f Lg - g Lf)/2. This definition is algebraic; non-negativity and identification with a gradient form require additional Markov and diffusion hypotheses.
Why is this valid?
The generator is a real linear map on real observables. The definition is pointwise and leaves domain closure and analytic regularity to downstream interfaces.
Source assumptions
- a linear Markov generator acting on products in its algebraic domain
Formal assumptions
- a real linear map on real-valued observables
- pointwise multiplication of observables
View Lean formalization
ASTIS records the exact generator formula without building positivity, reversibility, or a concrete Langevin process into the definition.
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp.carreDuChamp
def carreDuChamp
(generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
(f g : X → ℝ) : X → ℝ :=
fun x => (2 : ℝ)⁻¹ *
(generator (f * g) x - f x * generator g x - g x * generator f x)
/-- The carre du champ is symmetric in its observable arguments. -/Imports
- Mathlib.Algebra.Module.LinearMap.Basic
- Mathlib.Data.Real.Basic
- Mathlib.MeasureTheory.Integral.Bochner.Basic
- Mathlib.Topology.Instances.NNReal.Lemmas
- Mathlib.Tactic.Ring
- AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Generator
Local dependencies
No Registry dependency inferred.
Downstream consumers
- carre-du-champ non-negativity
- reversible integration by parts
- iterated carre du champ
Lemma 1.2.13
The carre du champ of a Markov generator is pointwise nonnegative on the diagonal.
\[\Gamma(f,f)\ge0\]
Proof
1
\[(P_hf)^2\le P_h(f^2)\quad(h>0)\]
Lean
carreDuChamp_nonneg_of_markov_jensen_rightGenerator2
\[0\le\lim_{h\downarrow0}\frac{P_h(f^2)-(P_hf)^2}{2h}=\frac12\bigl(L(f^2)-2fLf\bigr)=\Gamma(f,f)\]
Lean
carreDuChamp_nonneg_of_markov_jensen_rightGeneratorJensen's inequality makes the finite-time gap P_h(f squared) minus (P_h f) squared nonnegative. Dividing by 2h and taking the right-generator limit yields Gamma(f,f) at the selected state.
Why is this valid?
The theorem assumes the pointwise Markov Jensen inequality for every positive time, the actual right difference-quotient limits for f and f squared, and right continuity of P_h f at zero. No Gamma positivity premise is supplied.
Source assumptions
- a Markov semigroup satisfying Jensen's inequality
- f and f squared belong to the right-generator domain
Formal assumptions
- the pointwise Jensen inequality at every positive nonnegative-real time
- right difference-quotient convergence for f and f squared
- right continuity of the observable orbit at zero
View Lean formalization
ASTIS proves the limiting argument explicitly: the Jensen-gap quotient is rewritten into the two generator difference quotients and the orbit-continuity factor before closedness of the nonnegative half-line is applied.
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp.carreDuChamp_nonneg_of_markov_jensen_rightGenerator
theorem carreDuChamp_nonneg_of_markov_jensen_rightGenerator
(P : ℝ≥0 → (X → ℝ) → X → ℝ)
(generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
(f : X → ℝ) (x : X)
(hjensen : ∀ h : ℝ≥0, 0 < h → (P h f x) ^ 2 ≤ P h (f * f) x)
(hf : Tendsto
(fun h : ℝ≥0 => (P h f x - f x) / (h : ℝ))
(𝓝[>] 0) (𝓝 (generator f x)))
(hf2 : Tendsto
(fun h : ℝ≥0 => (P h (f * f) x - (f x) ^ 2) / (h : ℝ))
(𝓝[>] 0) (𝓝 (generator (f * f) x)))
(hcontinuous : Tendsto (fun h : ℝ≥0 => P h f x)
(𝓝[>] 0) (𝓝 (f x))) :
0 ≤ carreDuChamp generator f f x := by
let gap : ℝ≥0 → ℝ := fun h =>
(P h (f * f) x - (P h f x) ^ 2) / (2 * (h : ℝ))
have hgap_nonneg : ∀ᶠ h in 𝓝[>] (0 : ℝ≥0), 0 ≤ gap h := by
filter_upwards [self_mem_nhdsWithin] with h hh
have hh0 : 0 < h := by simpa only [mem_Ioi] using hh
exact div_nonneg (sub_nonneg.mpr (hjensen h hh0)) (by positivity)
have hrewrite : ∀ᶠ h in 𝓝[>] (0 : ℝ≥0),
gap h =
(2 : ℝ)⁻¹ * ((P h (f * f) x - (f x) ^ 2) / (h : ℝ)) -
(2 : ℝ)⁻¹ * (((P h f x - f x) / (h : ℝ)) *
(P h f x + f x)) := by
filter_upwards [self_mem_nhdsWithin] with h hh
have hh0 : (h : ℝ) ≠ 0 := by
have : 0 < h := by simpa only [mem_Ioi] using hh
exact_mod_cast this.ne'
dsimp [gap]
field_simp
ring
have hlimit : Tendsto gap (𝓝[>] (0 : ℝ≥0))
(𝓝 (carreDuChamp generator f f x)) := by
have hconst : Tendsto (fun _ : ℝ≥0 => f x)
(nhdsWithin 0 (Set.Ioi 0)) (nhds (f x)) :=
tendsto_const_nhds
have hsum : Tendsto (fun h : ℝ≥0 => P h f x + f x)
(nhdsWithin 0 (Set.Ioi 0)) (nhds (f x + f x)) :=
hcontinuous.add hconst
have hprod := hf.mul hsum
have hcombined := (hf2.const_mul (2 : ℝ)⁻¹).sub
(hprod.const_mul (2 : ℝ)⁻¹)
have hvalue :
(2 : ℝ)⁻¹ * generator (f * f) x -
(2 : ℝ)⁻¹ * (generator f x * (f x + f x)) =
carreDuChamp generator f f x := by
simp only [carreDuChamp]
ring
have htarget : Tendsto
(fun h : ℝ≥0 =>
(2 : ℝ)⁻¹ * ((P h (f * f) x - (f x) ^ 2) / (h : ℝ)) -
(2 : ℝ)⁻¹ * (((P h f x - f x) / (h : ℝ)) *
(P h f x + f x)))
(𝓝[>] 0) (𝓝 (carreDuChamp generator f f x)) := by
rw [← hvalue]
exact hcombined
exact htarget.congr' (hrewrite.mono fun h hh => hh.symm)
exact isClosed_Ici.mem_of_tendsto hlimit hgap_nonneg
/-- Chewi Theorem 1.2.14: stationarity and generator symmetry imply the
fundamental integration-by-parts identity between the Dirichlet form and the
integrated carre du champ.
The three integrability hypotheses are the exact terms expanded from Gamma;
they prevent the totalized Bochner integral from hiding a domain failure. -/Imports
- Mathlib.Algebra.Module.LinearMap.Basic
- Mathlib.Data.Real.Basic
- Mathlib.MeasureTheory.Integral.Bochner.Basic
- Mathlib.Topology.Instances.NNReal.Lemmas
- Mathlib.Tactic.Ring
- AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Generator
Local dependencies
Downstream consumers
- non-negativity of the reversible generator
- Dirichlet-form and functional-inequality arguments
Example 1.2.17
For the Langevin differential operator, the carre du champ is the gradient inner product, and on the diagonal it is the squared gradient norm.
\[L=\Delta-\langle\nabla V,\nabla\cdot\rangle\quad\Longrightarrow\quad \Gamma(f,g)=\langle\nabla f,\nabla g\rangle,\qquad \Gamma(f,f)=\|\nabla f\|^2\]
Proof
1
\[\Delta(fg)=f\Delta g+g\Delta f+2\langle\nabla f,\nabla g\rangle\]
Lean
laplacian_mul2
\[\nabla(fg)=f\nabla g+g\nabla f\]
Lean
gradient_mul3
\[\Gamma(f,g)=\frac12\bigl(L(fg)-fLg-gLf\bigr)=\langle\nabla f,\nabla g\rangle\]
Lean
langevinCarreDuChamp_eq_innerThe product identities for the Laplacian and gradient expand L(fg). The potential-gradient drift terms cancel against f Lg and g Lf, leaving twice the gradient inner product before the factor one half.
Why is this valid?
The observables are globally C2 on finite-dimensional Euclidean space. The potential enters only through the displayed Langevin differential expression; no semigroup-domain identification is needed for this pointwise calculation.
Source assumptions
- twice differentiable observables
- the displayed Langevin differential operator
Formal assumptions
- finite-dimensional real Euclidean state space
- global ContDiff R 2 hypotheses for both observables
View Lean formalization
ASTIS proves the missing Laplacian product rule from second Frechet derivatives and an orthonormal-basis expansion, then performs the concrete Langevin cancellation.
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LangevinCarreDuChamp.langevinCarreDuChamp_eq_inner
theorem langevinCarreDuChamp_eq_inner
{n : ℕ}
(V f g : EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
(hf : ContDiff ℝ 2 f) (hg : ContDiff ℝ 2 g)
(x : EuclideanSpace ℝ (Fin (n + 1))) :
(2 : ℝ)⁻¹ *
(LangevinGenerator.operator V (f * g) x -
f x * LangevinGenerator.operator V g x -
g x * LangevinGenerator.operator V f x) =
inner ℝ (gradient f x) (gradient g x) := by
have hf1 : Differentiable ℝ f := hf.differentiable (by norm_num)
have hg1 : Differentiable ℝ g := hg.differentiable (by norm_num)
simp only [LangevinGenerator.operator]
rw [laplacian_mul f g hf hg x, gradient_mul f g hf1 hg1 x]
simp only [inner_add_right, real_inner_smul_right]
ring
/-- Diagonal form of Chewi Example 1.2.17. -/Imports
- AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp
- AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LangevinGenerator
- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
- Mathlib.Analysis.Calculus.FDeriv.Mul
Local dependencies
Downstream consumers
- Langevin Dirichlet form
- Poincare and log-Sobolev specializations
- Bakry-Emery calculations
Definition 1.2.28
The iterated carre du champ applies the generator to Gamma and subtracts the two mixed generator terms.
\[\Gamma_2(f,g):=\frac12\bigl(L\Gamma(f,g)-\Gamma(f,Lg)-\Gamma(g,Lf)\bigr)\]
Gamma_2(f,g) = (L Gamma(f,g) - Gamma(f,Lg) - Gamma(g,Lf))/2. It measures the second-order evolution of the energy form.
Why is this valid?
The pointwise algebraic definition is compiled independently of the diffusion chain rule or any Hessian representation.
Source assumptions
- the generator and carre du champ expressions are defined on the required observables
Formal assumptions
- a real linear generator on real-valued observables
- the compiled carreDuChamp definition
View Lean formalization
The definition reuses the same generator and the compiled Gamma interface, exposing a shared node for curvature and functional-inequality routes.
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp.iteratedCarreDuChamp
def iteratedCarreDuChamp
(generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
(f g : X → ℝ) : X → ℝ :=
fun x => (2 : ℝ)⁻¹ *
(generator (carreDuChamp generator f g) x
- carreDuChamp generator f (generator g) x
- carreDuChamp generator g (generator f) x)
/-- The iterated carre du champ inherits symmetry from the first one. -/Imports
- Mathlib.Algebra.Module.LinearMap.Basic
- Mathlib.Data.Real.Basic
- Mathlib.MeasureTheory.Integral.Bochner.Basic
- Mathlib.Topology.Instances.NNReal.Lemmas
- Mathlib.Tactic.Ring
- AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Generator
Local dependencies
Downstream consumers
- Bakry-Emery curvature-dimension condition
- Langevin curvature calculation
Definition 1.2.29
The Bakry-Emery curvature-dimension condition requires positive alpha and the pointwise inequality Gamma_2(f) at least alpha Gamma(f).
\[\mathrm{CD}(\alpha,\infty):\qquad \Gamma_2(f,f)\ge\alpha\,\Gamma(f,f)\qquad(\alpha>0)\]
CD(alpha,infinity) holds when alpha > 0 and alpha Gamma(f,f)(x) <= Gamma_2(f,f)(x) for every observable and state.
Why is this valid?
The predicate quantifies over every real observable and state for the selected linear generator; domain restrictions for unbounded generators remain a downstream refinement.
Source assumptions
- a positive curvature constant
- the pointwise Gamma_2 lower bound
Formal assumptions
- 0 < alpha
- the inequality holds for every observable and state
View Lean formalization
ASTIS keeps positivity of alpha inside the predicate and does not identify the condition with strong convexity until a separate Langevin theorem proves it.
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp.SatisfiesBakryEmery
def SatisfiesBakryEmery
(generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
(alpha : ℝ) : Prop :=
0 < alpha ∧ ∀ (f : X → ℝ) (x : X),
alpha * carreDuChamp generator f f x ≤
iteratedCarreDuChamp generator f f x
/-- Chewi Lemma 1.2.13: the Markov-semigroup Jensen inequality implies
nonnegativity of the carre du champ after taking the right-generator limit.
The theorem is pointwise. `hf` and `hf2` are the actual right difference-
quotient limits for `f` and `f²`; `hcontinuous` is strong/right continuity of
the orbit at the selected state. -/Imports
- Mathlib.Algebra.Module.LinearMap.Basic
- Mathlib.Data.Real.Basic
- Mathlib.MeasureTheory.Integral.Bochner.Basic
- Mathlib.Topology.Instances.NNReal.Lemmas
- Mathlib.Tactic.Ring
- AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Generator
Local dependencies
Downstream consumers
- Bakry-Emery criterion for Poincare and log-Sobolev inequalities
- strongly convex Langevin potentials
Lemma 1.2.20
A differentiable scalar curve satisfying g'(t) at most c times g(t) is bounded by g(0) exp(ct) on the same finite interval.
\[g'(t)\le c\,g(t)\quad\Longrightarrow\quad g(t)\le e^{ct}g(0)\]
Proof
1
\[\frac{d}{dt}\bigl(e^{-ct}g(t)\bigr)=e^{-ct}\bigl(g'(t)-cg(t)\bigr)\le0\]
Lean
chewi_lemma_1_2_202
\[g(t)\le e^{ct}g(0)\]
Lean
chewi_lemma_1_2_20Differentiating the integrating-factor curve exp(-ct)g(t) makes its derivative nonpositive. Equivalently, Mathlib's one-sided Gronwall comparison bounds g by the exact zero-forcing exponential solution.
Why is this valid?
The Lean theorem uses a real-valued function differentiable on the ambient line, the pointwise derivative inequality on [0,T], and an explicit membership proof for the evaluation time.
Source assumptions
- T is positive
- g is differentiable
- g'(t) is at most c times g(t) throughout [0,T]
Formal assumptions
- g is differentiable as a real function
- the derivative inequality is supplied at every point of Icc 0 T
- the requested time belongs to Icc 0 T
View Lean formalization
ASTIS derives the exact textbook statement from Mathlib's more general right-slope Gronwall theorem, preserving the source interval, differentiability, constant, and exponential factor.
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.chewi_lemma_1_2_20
theorem chewi_lemma_1_2_20
{T c : ℝ} (_hT : 0 < T) (g : ℝ → ℝ)
(hg : Differentiable ℝ g)
(hbound : ∀ t ∈ Icc (0 : ℝ) T, deriv g t ≤ c * g t)
{t : ℝ} (ht : t ∈ Icc (0 : ℝ) T) :
g t ≤ g 0 * Real.exp (c * t) := by
have hgronwall :=
le_gronwallBound_of_liminf_deriv_right_le
(f := g)
(f' := deriv g)
(δ := g 0)
(K := c)
(ε := 0)
(a := 0)
(b := T)
hg.continuous.continuousOn
(fun x _ r hr =>
(hg x).hasDerivAt.hasDerivWithinAt.liminf_right_slope_le hr)
le_rfl
(fun x hx => by
simpa using hbound x ⟨hx.1, le_of_lt hx.2⟩)
t
ht
rw [gronwallBound_ε0, sub_zero] at hgronwall
exact hgronwall
/-- A scalar energy/dissipation curve with an exact right-derivative identity.
`scale` records the coefficient in
`d/dt energy(t) = -scale * dissipation(t)`. The derivative is taken within
`[t, ∞)`, matching semigroups defined by nonnegative time increments. -/Imports
- Mathlib.Analysis.Calculus.LocalExtr.Basic
- Mathlib.Analysis.ODE.Gronwall
Local dependencies
No Registry dependency inferred.
Downstream consumers
- Poincare variance and chi-squared decay
- log-Sobolev KL decay
- gradient-flow convergence inequalities
Example 1.2.4
For overdamped Langevin diffusion, Itô's formula displays the formal generator as a Laplacian minus a score-directional derivative.
\[dX_t=-\nabla V(X_t)\,dt+\sqrt2\,dB_t,\qquad Lf=\Delta f-\langle\nabla V,\nabla f\rangle\]
Proof
1
\[b(x)=-\nabla V(x),\qquad \sigma=\sqrt2\,I,\qquad \frac12\sigma\sigma^{\mathsf T}=I\]
Lean
finiteEuclidean_langevinGenerator_basisDisplay2
\[Lf=\langle b,\nabla f\rangle+\frac12\operatorname{Tr}(\sigma\sigma^{\mathsf T}\nabla^2f)=\Delta f-\langle\nabla V,\nabla f\rangle\]
Lean
finiteEuclidean_langevinGenerator_coordinateDisplayApplying Itô's formula to \(dX_t=-\nabla V(X_t)\,dt+\sqrt{2}\,dB_t\) gives \(Lf=\Delta f-\langle\nabla V,\nabla f\rangle\) on sufficiently regular test functions. This differential expression is the starting point for the semigroup analysis.
Why is this valid?
The display requires the relevant first and second derivatives at the point. A semigroup generator theorem additionally needs a process, Itô integration, and a core/domain argument.
Source assumptions
- twice differentiable test function with controlled derivatives
- differentiable potential
Formal assumptions
- finite-dimensional Euclidean index type
- explicit Fréchet derivatives
- pointwise differentiability hypotheses where genuine derivatives are used
View Lean formalization
ASTIS owns algebraic, basis, coordinate, and differentiability-aware display lemmas. None of these alone identifies a closed generator domain.
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Langevin.finiteEuclidean_langevinGenerator_basisDisplay
theorem finiteEuclidean_langevinGenerator_basisDisplay
{ι : Type*} [Fintype ι]
(V f : EuclideanSpace ℝ ι → ℝ) (x : EuclideanSpace ℝ ι) :
Laplacian.laplacian f x - inner ℝ (gradient V x) (gradient f x) =
(∑ i, iteratedFDeriv ℝ 2 f x
![(EuclideanSpace.basisFun ι ℝ) i, (EuclideanSpace.basisFun ι ℝ) i]) -
∑ i, (gradient V x) i * (gradient f x) i := by
have hlap_fun :
Laplacian.laplacian f =
fun x => ∑ i, iteratedFDeriv ℝ 2 f x
![(EuclideanSpace.basisFun ι ℝ) i, (EuclideanSpace.basisFun ι ℝ) i] :=
InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis f
(EuclideanSpace.basisFun ι ℝ)
have hlap :
Laplacian.laplacian f x =
∑ i, iteratedFDeriv ℝ 2 f x
![(EuclideanSpace.basisFun ι ℝ) i, (EuclideanSpace.basisFun ι ℝ) i] :=
congrFun hlap_fun x
have hinner :
inner ℝ (gradient V x) (gradient f x) =
∑ i, (gradient V x) i * (gradient f x) i :=
_root_.AutoSamplingTheory.TechnicalLemmas.Geometry.EuclideanSpaceCoordinates.euclideanSpace_inner_eq_sum_mul
(gradient V x) (gradient f x)
rw [hlap, hinner]
/-- Explicit coordinate-unit version of
`finiteEuclidean_langevinGenerator_basisDisplay`.
The additional `[DecidableEq ι]` instance is only used to unfold Mathlib's
`EuclideanSpace.basisFun` into `EuclideanSpace.single i 1`. -/Imports
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Laplacian
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.LineDeriv
- AutoSamplingTheory.TechnicalLemmas.Geometry.EuclideanSpaceCoordinates
- Mathlib.Analysis.InnerProductSpace.Basic
- Mathlib.Analysis.SpecialFunctions.ExpDeriv
- Mathlib.Analysis.Calculus.Deriv.Mul
- Mathlib.Algebra.BigOperators.Fin
- Mathlib.Tactic.Ring
Local dependencies
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Langevin.finiteEuclidean_langevinGenerator_coordinateDisplay
theorem finiteEuclidean_langevinGenerator_coordinateDisplay
{ι : Type*} [Fintype ι] [DecidableEq ι]
(V f : EuclideanSpace ℝ ι → ℝ) (x : EuclideanSpace ℝ ι) :
Laplacian.laplacian f x - inner ℝ (gradient V x) (gradient f x) =
(∑ i, iteratedFDeriv ℝ 2 f x
![(EuclideanSpace.single i (1 : ℝ)), (EuclideanSpace.single i (1 : ℝ))]) -
∑ i, (gradient V x) i * (gradient f x) i := by
simpa [EuclideanSpace.basisFun_apply] using
finiteEuclidean_langevinGenerator_basisDisplay V f x
/-- Supplied-hypothesis finite-coordinate handoff from weighted-divergence
algebra to the Mathlib pointwise expression `Δ f - <∇V, ∇f>`.
The hypotheses still provide the coordinate product-rule output, the
Gibbs-weight chain-rule output, and the coordinate divergence sum. This theorem
only replaces the coordinate second-derivative and gradient-product sums by
Mathlib's `Laplacian.laplacian` and `gradient` display. -/Imports
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Laplacian
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.LineDeriv
- AutoSamplingTheory.TechnicalLemmas.Geometry.EuclideanSpaceCoordinates
- Mathlib.Analysis.InnerProductSpace.Basic
- Mathlib.Analysis.SpecialFunctions.ExpDeriv
- Mathlib.Analysis.Calculus.Deriv.Mul
- Mathlib.Algebra.BigOperators.Fin
- Mathlib.Tactic.Ring
Local dependencies
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Langevin.finiteEuclidean_expNeg_lineDeriv_fderiv_coordinateSum_langevinGenerator_display
theorem finiteEuclidean_expNeg_lineDeriv_fderiv_coordinateSum_langevinGenerator_display
{ι : Type*} [Fintype ι] [DecidableEq ι]
{V f : EuclideanSpace ℝ ι → ℝ} {x : EuclideanSpace ℝ ι}
(hV : DifferentiableAt ℝ V x)
(hf : DifferentiableAt ℝ
(fun y : EuclideanSpace ℝ ι => fderiv ℝ f y) x)
(hgradF : ∀ i,
fderiv ℝ f x (EuclideanSpace.single i (1 : ℝ)) = (gradient f x) i) :
(∑ i, lineDeriv ℝ
(fun y : EuclideanSpace ℝ ι =>
Real.exp (-V y) * fderiv ℝ f y (EuclideanSpace.single i (1 : ℝ)))
x (EuclideanSpace.single i (1 : ℝ))) =
Real.exp (-V x) * (Laplacian.laplacian f x -
inner ℝ (gradient V x) (gradient f x)) := by
have hcoordLineDeriv : ∀ i,
lineDeriv ℝ
(fun y : EuclideanSpace ℝ ι =>
Real.exp (-V y) * fderiv ℝ f y (EuclideanSpace.single i (1 : ℝ)))
x (EuclideanSpace.single i (1 : ℝ)) =
Real.exp (-V x) * iteratedFDeriv ℝ 2 f x
![(EuclideanSpace.single i (1 : ℝ)), (EuclideanSpace.single i (1 : ℝ))] +
(gradient (fun y : EuclideanSpace ℝ ι => Real.exp (-V y)) x) i *
(gradient f x) i := by
intro i
have hline :=
_root_.AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.LineDeriv.lineDeriv_expNegPotential_mul_fderiv_coordinate_eq
(V := V) (f := f) (x := x) i hV hf
have hgradRho :=
_root_.AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient.gradient_expNegPotential_coordinate_eq_of_differentiableAt
(V := V) (x := x) hV i
calc
lineDeriv ℝ
(fun y : EuclideanSpace ℝ ι =>
Real.exp (-V y) * fderiv ℝ f y (EuclideanSpace.single i (1 : ℝ)))
x (EuclideanSpace.single i (1 : ℝ)) =
Real.exp (-V x) * iteratedFDeriv ℝ 2 f x
![(EuclideanSpace.single i (1 : ℝ)), (EuclideanSpace.single i (1 : ℝ))] -
Real.exp (-V x) * (gradient V x) i *
fderiv ℝ f x (EuclideanSpace.single i (1 : ℝ)) := by
simpa only [EuclideanSpace.single, PiLp.single] using hline
_ = Real.exp (-V x) * iteratedFDeriv ℝ 2 f x
![(EuclideanSpace.single i (1 : ℝ)), (EuclideanSpace.single i (1 : ℝ))] +
(gradient (fun y : EuclideanSpace ℝ ι => Real.exp (-V y)) x) i *
(gradient f x) i := by
rw [hgradF i, hgradRho]
ring
exact finiteEuclidean_expNeg_weightedDivergence_langevinGenerator_coordinateHandoff
(V := V) (f := f) (x := x)
(divCoord := fun i => lineDeriv ℝ
(fun y : EuclideanSpace ℝ ι =>
Real.exp (-V y) * fderiv ℝ f y (EuclideanSpace.single i (1 : ℝ)))
x (EuclideanSpace.single i (1 : ℝ)))
hV rfl hcoordLineDeriv
/-- Coordinate-line-derivative sum display with the local gradient-coordinate
bridge discharged.
Compared with
`finiteEuclidean_expNeg_lineDeriv_fderiv_coordinateSum_langevinGenerator_display`,
this theorem removes the supplied hypothesis
`fderiv ℝ f x eᵢ = (gradient f x) i` using the pointwise
`fderiv`/`gradient` coordinate bridge from `DifferentiableAt ℝ f x`.
It is still only a pointwise finite-coordinate sum display. It does not define
a divergence operator, assert that the sum is a divergence, prove integration
by parts, establish generator domains, or prove invariant Gibbs law,
reversibility, or KL/FI dissipation. -/Imports
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Laplacian
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.LineDeriv
- AutoSamplingTheory.TechnicalLemmas.Geometry.EuclideanSpaceCoordinates
- Mathlib.Analysis.InnerProductSpace.Basic
- Mathlib.Analysis.SpecialFunctions.ExpDeriv
- Mathlib.Analysis.Calculus.Deriv.Mul
- Mathlib.Algebra.BigOperators.Fin
- Mathlib.Tactic.Ring
Local dependencies
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Langevin.finiteEuclidean_expNeg_lineDeriv_fderiv_coordinateSum_langevinGenerator_display_of_differentiableAt
theorem finiteEuclidean_expNeg_lineDeriv_fderiv_coordinateSum_langevinGenerator_display_of_differentiableAt
{ι : Type*} [Fintype ι] [DecidableEq ι]
{V f : EuclideanSpace ℝ ι → ℝ} {x : EuclideanSpace ℝ ι}
(hV : DifferentiableAt ℝ V x)
(hfderiv : DifferentiableAt ℝ
(fun y : EuclideanSpace ℝ ι => fderiv ℝ f y) x)
(hf : DifferentiableAt ℝ f x) :
(∑ i, lineDeriv ℝ
(fun y : EuclideanSpace ℝ ι =>
Real.exp (-V y) * fderiv ℝ f y (EuclideanSpace.single i (1 : ℝ)))
x (EuclideanSpace.single i (1 : ℝ))) =
Real.exp (-V x) * (Laplacian.laplacian f x -
inner ℝ (gradient V x) (gradient f x)) :=
finiteEuclidean_expNeg_lineDeriv_fderiv_coordinateSum_langevinGenerator_display
(V := V) (f := f) (x := x) hV hfderiv
(fun i =>
_root_.AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient.fderiv_apply_coordinate_eq_gradient_coordinate_of_differentiableAt
(f := f) (x := x) i hf)
/-- Named coordinate-divergence version of the finite Euclidean Gibbs-weighted
first-derivative display.
The vector field is the coordinate representative
`y ↦ exp (-V y) * fderiv ℝ f y eᵢ`. The theorem only rewrites the compiled
coordinate-sum display through the local pointwise `coordinateDivergence`
definition. It does not identify this with any integration theorem, prove
weighted integration by parts, establish generator domains, or prove invariant
Gibbs law, reversibility, or KL/FI dissipation. -/Imports
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Laplacian
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.LineDeriv
- AutoSamplingTheory.TechnicalLemmas.Geometry.EuclideanSpaceCoordinates
- Mathlib.Analysis.InnerProductSpace.Basic
- Mathlib.Analysis.SpecialFunctions.ExpDeriv
- Mathlib.Analysis.Calculus.Deriv.Mul
- Mathlib.Algebra.BigOperators.Fin
- Mathlib.Tactic.Ring
Local dependencies
Downstream consumers
- weighted integration by parts
- formal symmetry
- generator core
Example 1.2.8
A weighted integration-by-parts calculation makes the Langevin generator formally symmetric under its Gibbs weight.
\[\int fLg\,d\pi=-\int\langle\nabla f,\nabla g\rangle\,d\pi=\int gLf\,d\pi,\qquad d\pi\propto e^{-V}dx\]
Proof
1
\[\nabla(e^{-V})=-e^{-V}\nabla V\]
Lean
weightedDivergence_gibbsWeight_langevinGenerator_algebra2
\[\int f(\Delta g-\langle\nabla V,\nabla g\rangle)e^{-V}dx=-\int\langle\nabla f,\nabla g\rangle e^{-V}dx\]
Lean
integral_expNeg_langevinGenerator_rhs_eq_zero_of_contDiff_of_hasCompactSupportWith density proportional to \(\exp(-V)\), integration by parts cancels the drift derivative against the derivative of the weight. On an admissible test class this yields \(\int (Lf)g\,d\pi=-\int\langle\nabla f,\nabla g\rangle\,d\pi\) and the corresponding symmetry identity.
Why is this valid?
Do not pass directly from an algebraic divergence display to a whole-space integral identity. The cutoff-gradient error and the main weighted term require distinct integrability arguments.
Source assumptions
- sufficiently regular test functions
- vanishing boundary contribution
Formal assumptions
- measurability and integrability of every source field
- compact support at the bounded-domain stage
- dominating functions for both cutoff-limit terms
- genuine differentiability where derivative formulas are invoked
View Lean formalization
ASTIS expands this short calculation into cutoff construction, compact-support divergence, boundary cancellation, source-field integrability, dominated convergence, and only then a whole-space identity.
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Langevin.weightedDivergence_gibbsWeight_langevinGenerator_algebra
theorem weightedDivergence_gibbsWeight_langevinGenerator_algebra
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
{rho lapF divWeighted : ℝ} {gradRho gradV gradF : E}
(hdiv : divWeighted = rho * lapF + inner ℝ gradRho gradF)
(hgrad : gradRho = (-rho) • gradV) :
divWeighted = rho * (lapF - inner ℝ gradV gradF) := by
calc
divWeighted = rho * lapF + inner ℝ gradRho gradF := hdiv
_ = rho * lapF + inner ℝ ((-rho) • gradV) gradF := by rw [hgrad]
_ = rho * lapF + (-rho) * inner ℝ gradV gradF := by
simp [real_inner_smul_left]
_ = rho * (lapF - inner ℝ gradV gradF) := by ring
/-- Source-facing specialization of
`weightedDivergence_gibbsWeight_langevinGenerator_algebra` with the Gibbs weight
`rho = exp (-Vx)`. This is still only algebra after the product-rule and
chain-rule facts have been supplied. -/Imports
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Laplacian
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.LineDeriv
- AutoSamplingTheory.TechnicalLemmas.Geometry.EuclideanSpaceCoordinates
- Mathlib.Analysis.InnerProductSpace.Basic
- Mathlib.Analysis.SpecialFunctions.ExpDeriv
- Mathlib.Analysis.Calculus.Deriv.Mul
- Mathlib.Algebra.BigOperators.Fin
- Mathlib.Tactic.Ring
Local dependencies
No Registry dependency inferred.
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff_hasCompactSupport
theorem radialSmoothCutoff_hasCompactSupport [NormedSpace ℝ E] [FiniteDimensional ℝ E]
{R : ℝ} (hR : 0 < R) :
HasCompactSupport (radialSmoothCutoff R : E → ℝ) := by
rw [hasCompactSupport_def]
exact IsCompact.of_isClosed_subset
(isCompact_closedBall (0 : E) (2 * R)) isClosed_closure
(radialSmoothCutoff_tsupport_subset_closedBall hR)
/-- A single positive constant controls the second iterated Fréchet
derivative of every positive-scale radial cutoff by `C / R^2`.
The proof first bounds the second derivative of the unit-scale radial cutoff
using continuity and compact support. It then writes the radius-`R` cutoff as
the unit cutoff composed with scalar dilation and applies Mathlib's exact
iterated-derivative composition rule for continuous linear maps. -/Imports
- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
- Mathlib.Analysis.Calculus.ContDiff.Bounds
- Mathlib.Analysis.Calculus.LocalExtr.Basic
Local dependencies
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff_tendsto_one
theorem radialSmoothCutoff_tendsto_one (x : E) :
Tendsto (fun R : ℝ => radialSmoothCutoff R x) atTop (𝓝 1) := by
apply tendsto_atTop_of_eventually_const (i₀ := ‖x‖ + 1)
intro R hR
have hR_pos : 0 < R := by
calc
0 < ‖x‖ + 1 := by positivity
_ ≤ R := hR
apply radialSmoothCutoff_eq_one_of_norm_le hR_pos
linarith
end Radial
section Plateau
/-- A compact subset of an open set admits a smooth compactly supported plateau in that set.
The function takes values in `[0, 1]` and is identically one on the compact set. -/Imports
- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
- Mathlib.Analysis.Calculus.ContDiff.Bounds
- Mathlib.Analysis.Calculus.LocalExtr.Basic
Local dependencies
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.tendsto_integral_norm_fderiv_radialSmoothCutoff_comp_toLp_apply
theorem tendsto_integral_norm_fderiv_radialSmoothCutoff_comp_toLp_apply
{n : ℕ} {μ : Measure (Fin (n + 1) → ℝ)}
{G : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ}
(hG : Integrable G μ) :
Tendsto
(fun R : ℝ =>
∫ x, ‖fderiv ℝ
(fun z => Cutoff.radialSmoothCutoff R
(WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
x (G x)‖ ∂μ)
atTop (𝓝 0) := by
let e : EuclideanSpace ℝ (Fin (n + 1)) ≃L[ℝ] (Fin (n + 1) → ℝ) :=
PiLp.continuousLinearEquiv 2 ℝ (fun _ : Fin (n + 1) => ℝ)
obtain ⟨C, hC_pos, hC⟩ :=
Cutoff.radialSmoothCutoff_fderiv_bound
(E := EuclideanSpace ℝ (Fin (n + 1)))
let bound : (Fin (n + 1) → ℝ) → ℝ :=
fun x => (C * ‖e.symm.toContinuousLinearMap‖) * ‖G x‖
have hbound_integrable : Integrable bound μ := by
exact (hG.norm.const_mul (C * ‖e.symm.toContinuousLinearMap‖))
have hmeas :
∀ᶠ R : ℝ in atTop,
AEStronglyMeasurable
(fun x => ‖fderiv ℝ
(fun z => Cutoff.radialSmoothCutoff R
(WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
x (G x)‖) μ := by
filter_upwards [eventually_gt_atTop (0 : ℝ)] with R hR
have hsmooth :
ContDiff ℝ (⊤ : ℕ∞)
(fun z : Fin (n + 1) → ℝ =>
Cutoff.radialSmoothCutoff R
(WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1)))) :=
(Cutoff.radialSmoothCutoff_contDiff hR).comp
(PiLp.contDiff_toLp (𝕜 := ℝ) (E := fun _ : Fin (n + 1) => ℝ))
have hderiv :
AEStronglyMeasurable
(fun x => fderiv ℝ
(fun z : Fin (n + 1) → ℝ =>
Cutoff.radialSmoothCutoff R
(WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
x) μ :=
(hsmooth.continuous_fderiv
(WithTop.coe_ne_zero.mpr WithTop.top_ne_zero)).aestronglyMeasurable
let eval :
((Fin (n + 1) → ℝ) →L[ℝ] ℝ) →L[ℝ]
(Fin (n + 1) → ℝ) →L[ℝ] ℝ :=
ContinuousLinearMap.flip (ContinuousLinearMap.apply ℝ ℝ)
exact
(eval.aestronglyMeasurable_comp₂
hderiv hG.aestronglyMeasurable).norm
have hdom :
∀ᶠ R : ℝ in atTop, ∀ᵐ x ∂μ,
‖(fun x => ‖fderiv ℝ
(fun z => Cutoff.radialSmoothCutoff R
(WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
x (G x)‖) x‖ ≤ bound x := by
filter_upwards [eventually_ge_atTop (1 : ℝ)] with R hR
filter_upwards with x
have hR_pos : 0 < R := lt_of_lt_of_le zero_lt_one hR
have hfderiv :
fderiv ℝ
(fun z => Cutoff.radialSmoothCutoff R
(WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
x =
(fderiv ℝ
(Cutoff.radialSmoothCutoff R :
EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
(WithLp.toLp 2 x)).comp e.symm.toContinuousLinearMap :=
(hasFDerivAt_radialSmoothCutoff_comp_toLp hR_pos x).fderiv
rw [norm_norm, hfderiv]
calc
‖((fderiv ℝ
(Cutoff.radialSmoothCutoff R :
EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
(WithLp.toLp 2 x)).comp e.symm.toContinuousLinearMap) (G x)‖
≤ ‖(fderiv ℝ
(Cutoff.radialSmoothCutoff R :
EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
(WithLp.toLp 2 x)).comp e.symm.toContinuousLinearMap‖ * ‖G x‖ :=
ContinuousLinearMap.le_opNorm _ _
_ ≤ ((C / R) * ‖e.symm.toContinuousLinearMap‖) * ‖G x‖ := by
gcongr
exact (ContinuousLinearMap.opNorm_comp_le _ _).trans
(mul_le_mul_of_nonneg_right
(hC R hR_pos (WithLp.toLp 2 x)) (norm_nonneg _))
_ ≤ bound x := by
dsimp [bound]
gcongr
exact div_le_self hC_pos.le hR
have hpoint :
∀ᵐ x ∂μ,
Tendsto
(fun R : ℝ => ‖fderiv ℝ
(fun z => Cutoff.radialSmoothCutoff R
(WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
x (G x)‖)
atTop (𝓝 0) := by
filter_upwards with x
refine squeeze_zero'
(g := fun R =>
((C / R) * ‖e.symm.toContinuousLinearMap‖) * ‖G x‖) ?_ ?_ ?_
· exact Filter.Eventually.of_forall fun R => norm_nonneg _
· filter_upwards [eventually_gt_atTop (0 : ℝ)] with R hR
have hfderiv :
fderiv ℝ
(fun z => Cutoff.radialSmoothCutoff R
(WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
x =
(fderiv ℝ
(Cutoff.radialSmoothCutoff R :
EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
(WithLp.toLp 2 x)).comp e.symm.toContinuousLinearMap :=
(hasFDerivAt_radialSmoothCutoff_comp_toLp hR x).fderiv
rw [hfderiv]
calc
‖((fderiv ℝ
(Cutoff.radialSmoothCutoff R :
EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
(WithLp.toLp 2 x)).comp e.symm.toContinuousLinearMap) (G x)‖
≤ ‖(fderiv ℝ
(Cutoff.radialSmoothCutoff R :
EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
(WithLp.toLp 2 x)).comp e.symm.toContinuousLinearMap‖ *
‖G x‖ := ContinuousLinearMap.le_opNorm _ _
_ ≤ ((C / R) * ‖e.symm.toContinuousLinearMap‖) * ‖G x‖ := by
gcongr
exact (ContinuousLinearMap.opNorm_comp_le _ _).trans
(mul_le_mul_of_nonneg_right
(hC R hR (WithLp.toLp 2 x)) (norm_nonneg _))
· simpa [mul_assoc] using
(tendsto_const_nhds.div_atTop tendsto_id).mul_const
(‖e.symm.toContinuousLinearMap‖ * ‖G x‖)
have hDCT :=
MeasureTheory.tendsto_integral_filter_of_dominated_convergence
(μ := μ) (l := atTop)
(F := fun R x => ‖fderiv ℝ
(fun z => Cutoff.radialSmoothCutoff R
(WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
x (G x)‖)
(f := fun _ => (0 : ℝ)) bound hmeas hdom hbound_integrable hpoint
simpa using hDCT
/-- Multiplication by the PiLp-wrapped radial cutoff converges to the identity
under integration for every integrable real normed-space-valued source field.
The statement is measure-generic and uses only integrability of the source.
It proves the cutoff main-term limit, but no Gibbs-specific integrability,
cutoff-gradient estimate, integration by parts, generator-domain result, or
invariant-law statement. -/Imports
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.LineDeriv
- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
- Mathlib.Analysis.Calculus.FDeriv.WithLp
- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
- Mathlib.MeasureTheory.Integral.DivergenceTheorem
Local dependencies
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.tendsto_integral_radialSmoothCutoff_comp_toLp_smul
theorem tendsto_integral_radialSmoothCutoff_comp_toLp_smul
{n : ℕ} {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
{μ : Measure (Fin (n + 1) → ℝ)}
{H : (Fin (n + 1) → ℝ) → F}
(hH : Integrable H μ) :
Tendsto
(fun R : ℝ => ∫ x,
Cutoff.radialSmoothCutoff R
(WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) • H x ∂μ)
atTop (𝓝 (∫ x, H x ∂μ)) := by
have hmeas :
∀ᶠ R : ℝ in atTop,
AEStronglyMeasurable
(fun x : Fin (n + 1) → ℝ =>
Cutoff.radialSmoothCutoff R
(WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) • H x) μ := by
filter_upwards [eventually_gt_atTop (0 : ℝ)] with R hR
exact
(((Cutoff.radialSmoothCutoff_contDiff hR).continuous.comp
(PiLp.continuous_toLp 2 _)).aestronglyMeasurable).smul
hH.aestronglyMeasurable
have hdom :
∀ᶠ R : ℝ in atTop, ∀ᵐ x ∂μ,
‖Cutoff.radialSmoothCutoff R
(WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) • H x‖ ≤
‖H x‖ := by
filter_upwards with R
filter_upwards with x
have hcutoff :=
Cutoff.radialSmoothCutoff_mem_Icc R
(WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1)))
rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg hcutoff.1]
exact mul_le_of_le_one_left (norm_nonneg _) hcutoff.2
have hpoint :
∀ᵐ x ∂μ,
Tendsto
(fun R : ℝ =>
Cutoff.radialSmoothCutoff R
(WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) • H x)
atTop (𝓝 (H x)) := by
filter_upwards with x
simpa using
(Cutoff.radialSmoothCutoff_tendsto_one
(WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1)))).smul_const (H x)
exact MeasureTheory.tendsto_integral_filter_of_dominated_convergence
(μ := μ) (l := atTop)
(F := fun R x =>
Cutoff.radialSmoothCutoff R
(WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) • H x)
(f := H) (fun x => ‖H x‖) hmeas hdom hH.norm hpoint
/-- The `L¹` norm of an integrable field on the complement of an expanding
Euclidean ball tends to zero, expressed in raw finite-Pi coordinates.
The tail sets are `R ≤ ‖WithLp.toLp 2 x‖`. They form an antitone family with
empty intersection, so Mathlib's antitone set-integral convergence theorem
applies to `‖H‖`. This is measure-generic and contains no Gibbs, generator,
integration-by-parts, or invariance semantics. -/Imports
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.LineDeriv
- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
- Mathlib.Analysis.Calculus.FDeriv.WithLp
- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
- Mathlib.MeasureTheory.Integral.DivergenceTheorem
Local dependencies
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Langevin.integral_expNeg_langevinGenerator_rhs_eq_zero_of_contDiff_of_hasCompactSupport
theorem integral_expNeg_langevinGenerator_rhs_eq_zero_of_contDiff_of_hasCompactSupport
{n : ℕ}
{V f : EuclideanSpace ℝ (Fin (n + 1)) → ℝ}
(hV : ContDiff ℝ 1 V)
(hf : ContDiff ℝ 2 f)
(hf_support : HasCompactSupport f) :
∫ y : EuclideanSpace ℝ (Fin (n + 1)),
Real.exp (-V y) *
(Laplacian.laplacian f y - inner ℝ (gradient V y) (gradient f y)) = 0 := by
let e : EuclideanSpace ℝ (Fin (n + 1)) ≃L[ℝ] (Fin (n + 1) → ℝ) :=
PiLp.continuousLinearEquiv 2 ℝ (fun _ : Fin (n + 1) => ℝ)
let F : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ :=
fun z => fun i =>
Real.exp (-V (e.symm z)) *
fderiv ℝ f (e.symm z) (EuclideanSpace.single i (1 : ℝ))
have hF : ContDiff ℝ 1 F := by
apply contDiff_pi.2
intro i
exact (hV.comp e.symm.contDiff).neg.exp.mul
(((hf.fderiv_right (m := 1) (by norm_num)).comp e.symm.contDiff).clm_apply
contDiff_const)
have hF_support : HasCompactSupport F := by
refine HasCompactSupport.of_support_subset_isCompact
(hf_support.isCompact.image e.continuous) ?_
intro x hx
have hxe : e.symm x ∈ tsupport f := by
by_contra hxe
have hzero : fderiv ℝ f (e.symm x) = 0 :=
fderiv_of_notMem_tsupport ℝ hxe
exact hx (by
funext i
simp [F, hzero])
exact ⟨e.symm x, hxe, e.apply_symm_apply x⟩
have hdiv :=
_root_.AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.integral_coordinateDivergence_wrapped_eq_zero_of_contDiff_of_hasCompactSupport
F hF hF_support
have hraw :
∫ x : Fin (n + 1) → ℝ,
Real.exp (-V (e.symm x)) *
(Laplacian.laplacian f (e.symm x) -
inner ℝ (gradient V (e.symm x)) (gradient f (e.symm x))) = 0 := by
calc
∫ x : Fin (n + 1) → ℝ,
Real.exp (-V (e.symm x)) *
(Laplacian.laplacian f (e.symm x) -
inner ℝ (gradient V (e.symm x)) (gradient f (e.symm x))) =
∫ x : Fin (n + 1) → ℝ,
_root_.AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.coordinateDivergence
(fun y : EuclideanSpace ℝ (Fin (n + 1)) =>
(WithLp.toLp 2 (F (WithLp.ofLp y)) :
EuclideanSpace ℝ (Fin (n + 1))))
(WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) := by
apply integral_congr_ae
exact Filter.Eventually.of_forall fun x => by
have htrace :=
trace_expNeg_fderivCoordinateField_langevinGenerator_display_of_hasFDerivAt
(V := V) (f := f) (x := x) (F' := fderiv ℝ F x)
(by simpa [F, e] using (hF.differentiable one_ne_zero x).hasFDerivAt)
(hV.differentiable one_ne_zero _)
((hf.fderiv_right (m := 1) (by norm_num)).differentiable one_ne_zero _)
(hf.differentiable (by norm_num) _)
have hwrapped :=
_root_.AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.coordinateDivergence_wrapped_toPi_trace_of_hasFDerivAt
(ι := Fin (n + 1)) (hF.differentiable one_ne_zero x).hasFDerivAt
change
Real.exp (-V (e.symm x)) *
(Laplacian.laplacian f (e.symm x) -
inner ℝ (gradient V (e.symm x)) (gradient f (e.symm x))) =
_root_.AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.coordinateDivergence
(fun y : EuclideanSpace ℝ (Fin (n + 1)) =>
(WithLp.toLp 2 (F (WithLp.ofLp y)) :
EuclideanSpace ℝ (Fin (n + 1))))
(WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1)))
calc
_ = ∑ i, fderiv ℝ F x (Pi.single i (1 : ℝ)) i := by
simpa [e] using htrace.symm
_ = _ := hwrapped.symm
_ = 0 := by simpa [F, e] using hdiv
rw [← (PiLp.volume_preserving_toLp (Fin (n + 1))).integral_comp
(MeasurableEquiv.toLp 2 _).measurableEmbedding]
simpa [e] using hraw
/-- Whole-space integrability of the Gibbs-weighted coordinate derivative
field from finiteness of the unnormalized Gibbs mass and a uniform operator
norm bound on the test-function derivative.
This theorem proves only source-field integrability. It does not prove a
cutoff main-term limit, weighted integration by parts, stationarity, or an
invariant Gibbs law. -/Imports
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Laplacian
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.LineDeriv
- AutoSamplingTheory.TechnicalLemmas.Geometry.EuclideanSpaceCoordinates
- Mathlib.Analysis.InnerProductSpace.Basic
- Mathlib.Analysis.SpecialFunctions.ExpDeriv
- Mathlib.Analysis.Calculus.Deriv.Mul
- Mathlib.Algebra.BigOperators.Fin
- Mathlib.Tactic.Ring
Local dependencies
Downstream consumers
- whole-space weighted integration by parts
- generator symmetry
- Gibbs stationarity
Corollary 1.2.9
The Gibbs measure is the stationary law suggested by the weighted generator identity.
\[\int P_tf\,d\pi=\int f\,d\pi\qquad(t\ge0)\]
Proof
1
\[\int Lf\,d\pi=0\]
Lean
integral_operator_normalizedGibbs_eq_zero_on_compactlySupportedC22
\[\int P_tf\,d\pi=\int f\,d\pi\]
Lean
isInvariantOn_normalizedGibbs_on_compactlySupportedC2The formal adjoint equation \(L^*\pi=0\) is solved by a density proportional to \(\exp(-V)\), provided the normalizing integral is finite. Turning this calculation into uniqueness and semigroup invariance requires the process and generator domain to be fixed.
Why is this valid?
Bridge from a core identity to the generator domain, identify the forward or adjoint equation in a justified sense, and connect it to the semigroup law.
Source assumptions
- normalizable Gibbs density
- formal integration by parts
Formal assumptions
- probability normalization
- whole-space weighted integration by parts
- generator/semigroup domain
- well-posed Markov evolution
View Lean formalization
ASTIS marks this as red. A formal density calculation does not by itself prove invariance for the Markov semigroup.
AutoSamplingTheory.TechnicalLemmas.Measure.Gibbs.isProbabilityMeasure_withDensity_normalized_gibbs
theorem isProbabilityMeasure_withDensity_normalized_gibbs
(μ : MeasureTheory.Measure α) (V : α → ℝ)
(h0 : ∫⁻ x, gibbsDensityENNReal V x ∂μ ≠ 0)
(hfin : ∫⁻ x, gibbsDensityENNReal V x ∂μ ≠ ∞) :
IsProbabilityMeasure
(μ.withDensity fun x =>
(∫⁻ y, gibbsDensityENNReal V y ∂μ)⁻¹ * gibbsDensityENNReal V x) :=
RadonNikodym.isProbabilityMeasure_withDensity_normalized_lintegral μ
(gibbsDensityENNReal V) h0 hfin
/-- A nonzero base measure and a finite a.e. envelope are enough to normalize a
Gibbs density into a probability measure. This is the reusable contract that
later coercivity/growth leaves should target. -/Imports
- AutoSamplingTheory.TechnicalLemmas.Measure.RadonNikodym
- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Local dependencies
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LangevinGenerator.integral_operator_normalizedGibbs_eq_zero_on_compactlySupportedC2
theorem integral_operator_normalizedGibbs_eq_zero_on_compactlySupportedC2
{n : ℕ}
{V f : EuclideanSpace ℝ (Fin (n + 1)) → ℝ}
(hV : ContDiff ℝ 1 V)
(hf : CompactlySupportedC2 f) :
∫ x, operator V f x ∂volume.withDensity
(fun x =>
(∫⁻ y, Measure.Gibbs.gibbsDensityENNReal V y ∂volume)⁻¹ *
Measure.Gibbs.gibbsDensityENNReal V x) = 0 := by
rw [TechnicalLemmas.Measure.GibbsIntegral.integral_withDensity_lintegral_inv_mul_gibbsDensityENNReal_eq_integral_lintegral_inv_mul_exp_smul_of_neZero
volume hV.continuous.measurable.aemeasurable]
simp_rw [operator, smul_eq_mul, mul_assoc]
rw [integral_const_mul]
rw [Langevin.integral_expNeg_langevinGenerator_rhs_eq_zero_of_contDiff_of_hasCompactSupport
hV hf.1 hf.2]
simp
/-- A semigroup satisfying the integrated-generator contract on the
compactly supported `C²` core preserves normalized Gibbs expectations on that
core.
This theorem composes the concrete Gibbs integration-by-parts identity with
the abstract semigroup-to-invariance bridge. The semigroup contract remains
an explicit hypothesis: no Langevin SDE, Markov semigroup, core closure, or
measure-determining extension is constructed here. -/Imports
- AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Langevin
- AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.WeakGenerator
- AutoSamplingTheory.TechnicalLemmas.Measure.GibbsIntegral
Local dependencies
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LangevinGenerator.isInvariantOn_normalizedGibbs_on_compactlySupportedC2
theorem isInvariantOn_normalizedGibbs_on_compactlySupportedC2
{n : ℕ}
{V : EuclideanSpace ℝ (Fin (n + 1)) → ℝ}
{P : ℝ →
(EuclideanSpace ℝ (Fin (n + 1)) → ℝ) →
EuclideanSpace ℝ (Fin (n + 1)) → ℝ}
{generator :
(EuclideanSpace ℝ (Fin (n + 1)) → ℝ) →
EuclideanSpace ℝ (Fin (n + 1)) → ℝ}
(hV : ContDiff ℝ 1 V)
(hcore : CoreContract V generator (Set.ofPred CompactlySupportedC2))
(hsemigroup : WeakGenerator.IntegratedSemigroupGeneratorContract
P generator (Set.ofPred CompactlySupportedC2)
(volume.withDensity
(fun x =>
(∫⁻ y, Measure.Gibbs.gibbsDensityENNReal V y ∂volume)⁻¹ *
Measure.Gibbs.gibbsDensityENNReal V x))) :
WeakGenerator.IsInvariantOn P
(volume.withDensity
(fun x =>
(∫⁻ y, Measure.Gibbs.gibbsDensityENNReal V y ∂volume)⁻¹ *
Measure.Gibbs.gibbsDensityENNReal V x))
(Set.ofPred CompactlySupportedC2) := by
refine WeakGenerator.isInvariantOn_of_integral_generator_eq_zero hsemigroup ?_
intro f hf
rw [hcore.generator_eq_operator_on_core f hf]
exact integral_operator_normalizedGibbs_eq_zero_on_compactlySupportedC2 hV hf
end LangevinGenerator
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheoryImports
- AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Langevin
- AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.WeakGenerator
- AutoSamplingTheory.TechnicalLemmas.Measure.GibbsIntegral
Local dependencies
Downstream consumers
- equilibrium convergence
- algorithmic sampling interpretation
Supporting Poincare-to-decay realization route
Variance is bounded by an energy involving the gradient.
\[\frac{d}{dt}\operatorname{Var}_\pi(P_tf)=-2\int\Gamma(P_tf,P_tf)\,d\pi\le-\frac{2}{C_{\mathrm P}}\operatorname{Var}_\pi(P_tf)\]
Proof
1
\[V'(t)\le-\frac{2}{C_{\mathrm P}}V(t),\qquad V(t):=\operatorname{Var}_\pi(P_tf)\]
Lean
exponential_decay_of_scaled_dissipation2
\[V(t)\le e^{-2t/C_{\mathrm P}}V(0)\]
Lean
chewi_theorem_1_2_21_forwardA Poincaré inequality controls the centered L2 norm of an observable by its Dirichlet energy. Equivalently, it gives a spectral gap on the orthogonal complement of constant functions and therefore exponential variance decay along the semigroup.
Why is this valid?
Variance and energy must both be defined and finite in the intended function space; extension from a smooth core requires a density or closure theorem.
Source assumptions
- sufficiently regular functions
Formal assumptions
- explicit measure and scalar field
- probability normalization
- integrability/square-integrability
- explicit Dirichlet form
View Lean formalization
The ASTIS layer makes the measure, function class, integrability, and gradient representation visible.
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance
noncomputable def variance (μ : Measure E) (f : E → ℝ) : ℝ :=
∫ x, (f x - ∫ y, f y ∂μ) ^ 2 ∂μ
/-- The Euclidean/inner-product Dirichlet energy of a test function. -/Imports
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient
- Mathlib.MeasureTheory.Integral.Bochner.Basic
Local dependencies
No Registry dependency inferred.
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.dirichletEnergy
noncomputable def dirichletEnergy (μ : Measure E) (f : E → ℝ) : ℝ :=
∫ x, ‖gradient f x‖ ^ 2 ∂μ
/-- Exact integrability domain used by the local Poincare interface. -/Imports
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient
- Mathlib.MeasureTheory.Integral.Bochner.Basic
Local dependencies
No Registry dependency inferred.
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.Admissible
def Admissible (μ : Measure E) (f : E → ℝ) : Prop :=
Integrable f μ ∧
Integrable (fun x => (f x - ∫ y, f y ∂μ) ^ 2) μ ∧
Integrable (fun x => ‖gradient f x‖ ^ 2) μ
/-- A measure satisfies the Poincare inequality with constant `C` on an
explicit test class.
The convention is `Var_μ(f) ≤ C * E_μ(f)`. Probability normalization is
part of the contract rather than an implicit convention. -/Imports
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient
- Mathlib.MeasureTheory.Integral.Bochner.Basic
Local dependencies
No Registry dependency inferred.
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.Satisfies
def Satisfies (μ : Measure E) (tests : Set (E → ℝ)) (C : ℝ) : Prop :=
IsProbabilityMeasure μ ∧ 0 ≤ C ∧
∀ f ∈ tests, Admissible μ f → variance μ f ≤ C * dirichletEnergy μ f
omit [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] in
/-- Variance is nonnegative on its stated integral representation. -/Imports
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient
- Mathlib.MeasureTheory.Integral.Bochner.Basic
Local dependencies
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance_nonneg
theorem variance_nonneg {μ : Measure E} {f : E → ℝ} :
0 ≤ variance μ f := by
rw [variance]
exact integral_nonneg_of_ae
(Filter.Eventually.of_forall fun x => sq_nonneg (f x - ∫ y, f y ∂μ))
/-- Dirichlet energy is nonnegative on its stated integrability domain. -/Imports
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient
- Mathlib.MeasureTheory.Integral.Bochner.Basic
Local dependencies
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.dirichletEnergy_nonneg
theorem dirichletEnergy_nonneg {μ : Measure E} {f : E → ℝ} :
0 ≤ dirichletEnergy μ f := by
rw [dirichletEnergy]
exact integral_nonneg_of_ae
(Filter.Eventually.of_forall fun x => sq_nonneg ‖gradient f x‖)
/-- Increasing a nonnegative Poincare constant preserves the inequality on
the same test class and admissibility domain. -/Imports
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient
- Mathlib.MeasureTheory.Integral.Bochner.Basic
Local dependencies
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.mono_constant
theorem mono_constant {μ : Measure E} {tests : Set (E → ℝ)} {C D : ℝ}
(hC : Satisfies μ tests C) (hCD : C ≤ D) :
Satisfies μ tests D := by
refine ⟨hC.1, hC.2.1.trans hCD, ?_⟩
intro f hf_tests hf
exact (hC.2.2 f hf_tests hf).trans
(mul_le_mul_of_nonneg_right hCD dirichletEnergy_nonneg)
/-- The inequality component can be consumed without unpacking the probability
and nonnegative-constant fields manually. -/Imports
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient
- Mathlib.MeasureTheory.Integral.Bochner.Basic
Local dependencies
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance_le
theorem variance_le {μ : Measure E} {tests : Set (E → ℝ)} {C : ℝ}
(hC : Satisfies μ tests C) {f : E → ℝ}
(hf_tests : f ∈ tests) (hf : Admissible μ f) :
variance μ f ≤ C * dirichletEnergy μ f :=
hC.2.2 f hf_tests hf
/-- Restricting the test class preserves a Poincare inequality and all of its
measure and constant data. -/Imports
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient
- Mathlib.MeasureTheory.Integral.Bochner.Basic
Local dependencies
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.mono_tests
theorem mono_tests {μ : Measure E} {small large : Set (E → ℝ)} {C : ℝ}
(hC : Satisfies μ large C) (hsub : small ⊆ large) :
Satisfies μ small C := by
refine ⟨hC.1, hC.2.1, ?_⟩
intro f hf_tests
exact hC.2.2 f (hsub hf_tests)
end Poincare
end FunctionalInequalities
end TechnicalLemmas
end AutoSamplingTheoryImports
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient
- Mathlib.MeasureTheory.Integral.Bochner.Basic
Local dependencies
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.exponential_decay_of_scaled_dissipation
theorem exponential_decay_of_scaled_dissipation
{scale rate : ℝ} (curve : DissipationCurve scale)
(hcoercive : ∀ s : ℝ,
rate * curve.energy s ≤ scale * curve.dissipation s)
{t : ℝ} (ht : 0 ≤ t) :
curve.energy t ≤ curve.energy 0 * Real.exp (-rate * t) := by
simpa [sub_zero] using
exponential_decay_of_scaled_dissipation_from
curve hcoercive ht
/-- Exponential decay from every starting time forces the instantaneous
coercivity inequality.
The proof compares the energy with its exponential envelope on `[s, ∞)`. Their
difference has a local maximum at `s`; the one-sided Fermat inequality then
compares the two right derivatives. -/Imports
- Mathlib.Analysis.Calculus.LocalExtr.Basic
- Mathlib.Analysis.ODE.Gronwall
Local dependencies
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.chewi_theorem_1_2_21_forward
theorem chewi_theorem_1_2_21_forward
{C : ℝ} (hC : 0 < C) (curve : DissipationCurve 2)
(hPI : ∀ s : ℝ,
curve.energy s ≤ C * curve.dissipation s)
{t : ℝ} (ht : 0 ≤ t) :
curve.energy t ≤
curve.energy 0 * Real.exp (-(2 / C) * t) := by
simpa [sub_zero] using
chewi_theorem_1_2_21_forward_from hC curve hPI ht
/-- Backward scalar direction of Chewi, Theorem 1.2.21. -/Imports
- Mathlib.Analysis.Calculus.LocalExtr.Basic
- Mathlib.Analysis.ODE.Gronwall
Local dependencies
No Registry dependency inferred.
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.chewi_theorem_1_2_22_forward
theorem chewi_theorem_1_2_22_forward
{C : ℝ} (hC : 0 < C) (curve : DissipationCurve 2)
(hPI : ∀ s : ℝ,
curve.energy s ≤ C * curve.dissipation s)
{t : ℝ} (ht : 0 ≤ t) :
curve.energy t ≤
curve.energy 0 * Real.exp (-(2 / C) * t) :=
chewi_theorem_1_2_21_forward hC curve hPI ht
/-- Backward scalar direction of Chewi, Theorem 1.2.22. -/Imports
- Mathlib.Analysis.Calculus.LocalExtr.Basic
- Mathlib.Analysis.ODE.Gronwall
Local dependencies
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.exponential_decay_of_scaled_dissipation_from
theorem exponential_decay_of_scaled_dissipation_from
{scale rate : ℝ} (curve : DissipationCurve scale)
(hcoercive : ∀ u : ℝ,
rate * curve.energy u ≤ scale * curve.dissipation u)
{s t : ℝ} (hst : s ≤ t) :
curve.energy t ≤
curve.energy s * Real.exp (-rate * (t - s)) := by
have hbound : ∀ x ∈ Ico s t,
-scale * curve.dissipation x ≤
(-rate) * curve.energy x + 0 := by
intro x hx
have hneg := neg_le_neg (hcoercive x)
simpa [neg_mul] using hneg
have hgronwall :=
le_gronwallBound_of_liminf_deriv_right_le
(f := curve.energy)
(f' := fun x => -scale * curve.dissipation x)
(δ := curve.energy s)
(K := -rate)
(ε := 0)
(a := s)
(b := t)
curve.energy_continuous.continuousOn
(fun x hx r hr => by
simpa [slope] using
(curve.energy_hasDerivWithinAt x).liminf_right_slope_le hr)
le_rfl
hbound
t
⟨hst, le_rfl⟩
rw [gronwallBound_ε0] at hgronwall
exact hgronwall
/-- A coercive inequality along a dissipation curve implies exponential decay
from time zero. -/Imports
- Mathlib.Analysis.Calculus.LocalExtr.Basic
- Mathlib.Analysis.ODE.Gronwall
Local dependencies
No Registry dependency inferred.
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.scaled_dissipation_of_exponential_decay
theorem scaled_dissipation_of_exponential_decay
{scale rate : ℝ} (curve : DissipationCurve scale)
(hdecay : ∀ s t : ℝ, 0 ≤ t →
curve.energy (s + t) ≤
curve.energy s * Real.exp (-rate * t)) :
∀ s : ℝ,
rate * curve.energy s ≤ scale * curve.dissipation s := by
intro s
let comparison : ℝ → ℝ := fun x =>
curve.energy x -
curve.energy s * Real.exp (-rate * (x - s))
have hmax : IsLocalMaxOn comparison (Ici s) s := by
filter_upwards [self_mem_nhdsWithin] with x hx
have hdecay_x :
curve.energy x ≤
curve.energy s * Real.exp (-rate * (x - s)) := by
have h := hdecay s (x - s) (sub_nonneg.mpr hx)
calc
curve.energy x = curve.energy (s + (x - s)) := by
congr 1
ring
_ ≤ curve.energy s * Real.exp (-rate * (x - s)) := h
dsimp [comparison]
calc
curve.energy x -
curve.energy s * Real.exp (-rate * (x - s)) ≤ 0 :=
sub_nonpos.mpr hdecay_x
_ = curve.energy s -
curve.energy s * Real.exp (-rate * (s - s)) := by simp
have hinner :
HasDerivAt (fun x : ℝ => -rate * (x - s)) (-rate) s := by
change HasDerivAt (fun y : ℝ => -rate * (id y - s)) (-rate) s
have hraw := ((hasDerivAt_id s).sub_const s).const_mul (-rate)
exact hraw.congr_deriv (by ring)
have hexponential :
HasDerivAt
(fun x : ℝ =>
curve.energy s * Real.exp (-rate * (x - s)))
(-rate * curve.energy s) s := by
have hraw := hinner.exp.const_mul (curve.energy s)
apply hraw.congr_deriv
rw [sub_self, mul_zero, Real.exp_zero]
ring
have hderiv :
HasDerivWithinAt comparison
((-scale * curve.dissipation s) -
(-rate * curve.energy s))
(Ici s) s := by
change HasDerivWithinAt
(curve.energy - fun x : ℝ =>
curve.energy s * Real.exp (-rate * (x - s)))
((-scale * curve.dissipation s) - (-rate * curve.energy s))
(Ici s) s
exact (curve.energy_hasDerivWithinAt s).sub
hexponential.hasDerivWithinAt
have hone : (1 : ℝ) ∈ posTangentConeAt (Ici s) s := by
rw [one_mem_posTangentConeAt_iff_frequently]
have hev : ∀ᶠ x in 𝓝[>] s, x ∈ Ici s := by
filter_upwards [self_mem_nhdsWithin] with x hx
have hsx : s < x := by
simpa only [mem_Ioi] using hx
exact hsx.le
exact hev.frequently
have hnonpos :=
hmax.hasFDerivWithinAt_nonpos hderiv.hasFDerivWithinAt hone
have hscalar :
((-scale * curve.dissipation s) -
(-rate * curve.energy s)) ≤ 0 := by
simpa using hnonpos
linarith
/-- Forward direction of Chewi, Theorem 1.2.21, between arbitrary times. -/Imports
- Mathlib.Analysis.Calculus.LocalExtr.Basic
- Mathlib.Analysis.ODE.Gronwall
Local dependencies
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.chewi_theorem_1_2_21_scalar_equivalence
theorem chewi_theorem_1_2_21_scalar_equivalence
{C : ℝ} (hC : 0 < C) (curve : DissipationCurve 2) :
(∀ s : ℝ,
curve.energy s ≤ C * curve.dissipation s) ↔
(∀ s t : ℝ, 0 ≤ t →
curve.energy (s + t) ≤
curve.energy s * Real.exp (-(2 / C) * t)) := by
constructor
· intro hPI s t ht
have h := chewi_theorem_1_2_21_forward_from
hC curve hPI (show s ≤ s + t by linarith)
simpa using h
· exact chewi_theorem_1_2_21_backward hC curve
/-- Forward direction of Chewi, Theorem 1.2.22, between arbitrary times. -/Imports
- Mathlib.Analysis.Calculus.LocalExtr.Basic
- Mathlib.Analysis.ODE.Gronwall
Local dependencies
No Registry dependency inferred.
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.chewi_theorem_1_2_22_scalar_equivalence
theorem chewi_theorem_1_2_22_scalar_equivalence
{C : ℝ} (hC : 0 < C) (curve : DissipationCurve 2) :
(∀ s : ℝ,
curve.energy s ≤ C * curve.dissipation s) ↔
(∀ s t : ℝ, 0 ≤ t →
curve.energy (s + t) ≤
curve.energy s * Real.exp (-(2 / C) * t)) :=
chewi_theorem_1_2_21_scalar_equivalence hC curve
/-- Forward direction of Chewi, Theorem 1.2.26, between arbitrary times. -/Imports
- Mathlib.Analysis.Calculus.LocalExtr.Basic
- Mathlib.Analysis.ODE.Gronwall
Local dependencies
Downstream consumers
- variance decay
- spectral-gap estimates
Supporting log-Sobolev-to-decay realization route
Entropy is controlled by a Fisher-information or Dirichlet-form term.
\[\frac{d}{dt}\operatorname{Ent}_\pi(P_tf)=-\int\Gamma(P_tf,\log P_tf)\,d\pi\le-\frac{2}{C_{\mathrm{LSI}}}\operatorname{Ent}_\pi(P_tf)\]
Proof
1
\[H'(t)\le-\frac{2}{C_{\mathrm{LSI}}}H(t),\qquad H(t):=\operatorname{Ent}_\pi(P_tf)\]
Lean
exponential_decay_of_scaled_dissipation2
\[H(t)\le e^{-2t/C_{\mathrm{LSI}}}H(0)\]
Lean
chewi_theorem_1_2_26_forwardA log-Sobolev inequality bounds relative entropy by an entropy-production term. Along Langevin evolution, this converts the entropy dissipation identity into exponential decay of KL divergence.
Why is this valid?
The density, logarithm convention at zero, square-root derivative, and absolute continuity all need stated representatives and integrability.
Source assumptions
- density relative to the reference measure
- regularity sufficient for Fisher information
Formal assumptions
- nonnegative measurable density
- normalization
- finite entropy and energy terms in the handoff
View Lean formalization
ASTIS records the scalar handoff from a square-root density form to a KL/Fisher-information chain, while retaining all finiteness requirements.
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.Satisfies
def Satisfies (μ : Measure E) (tests : Set (E → ℝ)) (C : ℝ) : Prop :=
IsProbabilityMeasure μ ∧ 0 ≤ C ∧
∀ f ∈ tests, Admissible μ f → variance μ f ≤ C * dirichletEnergy μ f
omit [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] in
/-- Variance is nonnegative on its stated integral representation. -/Imports
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient
- Mathlib.MeasureTheory.Integral.Bochner.Basic
Local dependencies
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.mono_constant
theorem mono_constant {μ : Measure E} {tests : Set (E → ℝ)} {C D : ℝ}
(hC : Satisfies μ tests C) (hCD : C ≤ D) :
Satisfies μ tests D := by
refine ⟨hC.1, hC.2.1.trans hCD, ?_⟩
intro f hf_tests hf
exact (hC.2.2 f hf_tests hf).trans
(mul_le_mul_of_nonneg_right hCD dirichletEnergy_nonneg)
/-- The inequality component can be consumed without unpacking the probability
and nonnegative-constant fields manually. -/Imports
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient
- Mathlib.MeasureTheory.Integral.Bochner.Basic
Local dependencies
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.mono_tests
theorem mono_tests {μ : Measure E} {small large : Set (E → ℝ)} {C : ℝ}
(hC : Satisfies μ large C) (hsub : small ⊆ large) :
Satisfies μ small C := by
refine ⟨hC.1, hC.2.1, ?_⟩
intro f hf_tests
exact hC.2.2 f (hsub hf_tests)
end Poincare
end FunctionalInequalities
end TechnicalLemmas
end AutoSamplingTheoryImports
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient
- Mathlib.MeasureTheory.Integral.Bochner.Basic
Local dependencies
AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainIntegralHandoffScalar
theorem lsiKlFiSqrtDensityFisherChainIntegralHandoffScalar
{α ι : Type*} [MeasurableSpace α] [Fintype ι] (mu : Measure α)
{r : α → Real} {dirichlet fisher : Real} {dr dSqrt dLog : ι → α → Real}
(hdirichlet : dirichlet = ∫ x, (∑ i, dSqrt i x ^ 2) ∂mu)
(hfisher : fisher = ∫ x, (r x * ∑ i, dLog i x ^ 2) ∂mu)
(hr : ∀ᵐ x ∂mu, 0 < r x)
(hdSqrt : ∀ᵐ x ∂mu,
∀ i, dSqrt i x = (1 / (2 * Real.sqrt (r x))) * dr i x)
(hdLog : ∀ᵐ x ∂mu, ∀ i, dLog i x = dr i x / r x) :
dirichlet = (1 / 4) * fisher := by
rw [hdirichlet, hfisher]
rw [← integral_const_mul]
exact lsiKlFiSqrtDensityFisherChainIntegralFiniteSum mu hr hdSqrt hdLog
/-- Scalar rearrangement behind the one-sided use of the cited DV formula.
This is not a proof of Donsker--Varadhan. It starts after a cited or
eventually formalized entropy-duality theorem has supplied the variational
upper bound for an admissible test.
-/Imports
- Mathlib.Data.Real.Basic
- Mathlib.Algebra.Order.Archimedean.Real.Basic
- Mathlib.Analysis.Real.Sqrt
- Mathlib.Analysis.Calculus.ParametricIntegral
- Mathlib.Analysis.SpecialFunctions.Log.Basic
- Mathlib.InformationTheory.KullbackLeibler.Basic
- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
- Mathlib.MeasureTheory.Measure.Tilted
- Mathlib.Probability.Kernel.Condexp
- Mathlib.Probability.Moments.IntegrableExpMul
- AutoSamplingTheory.Core
Local dependencies
No Registry dependency inferred.
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.exponential_decay_of_scaled_dissipation
theorem exponential_decay_of_scaled_dissipation
{scale rate : ℝ} (curve : DissipationCurve scale)
(hcoercive : ∀ s : ℝ,
rate * curve.energy s ≤ scale * curve.dissipation s)
{t : ℝ} (ht : 0 ≤ t) :
curve.energy t ≤ curve.energy 0 * Real.exp (-rate * t) := by
simpa [sub_zero] using
exponential_decay_of_scaled_dissipation_from
curve hcoercive ht
/-- Exponential decay from every starting time forces the instantaneous
coercivity inequality.
The proof compares the energy with its exponential envelope on `[s, ∞)`. Their
difference has a local maximum at `s`; the one-sided Fermat inequality then
compares the two right derivatives. -/Imports
- Mathlib.Analysis.Calculus.LocalExtr.Basic
- Mathlib.Analysis.ODE.Gronwall
Local dependencies
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.chewi_theorem_1_2_26_forward
theorem chewi_theorem_1_2_26_forward
{C : ℝ} (hC : 0 < C) (curve : DissipationCurve 1)
(hLSI : ∀ s : ℝ,
curve.energy s ≤ (C / 2) * curve.dissipation s)
{t : ℝ} (ht : 0 ≤ t) :
curve.energy t ≤
curve.energy 0 * Real.exp (-(2 / C) * t) := by
simpa [sub_zero] using
chewi_theorem_1_2_26_forward_from hC curve hLSI ht
/-- Backward scalar direction of Chewi, Theorem 1.2.26. -/Imports
- Mathlib.Analysis.Calculus.LocalExtr.Basic
- Mathlib.Analysis.ODE.Gronwall
Local dependencies
No Registry dependency inferred.
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.exponential_decay_of_scaled_dissipation_from
theorem exponential_decay_of_scaled_dissipation_from
{scale rate : ℝ} (curve : DissipationCurve scale)
(hcoercive : ∀ u : ℝ,
rate * curve.energy u ≤ scale * curve.dissipation u)
{s t : ℝ} (hst : s ≤ t) :
curve.energy t ≤
curve.energy s * Real.exp (-rate * (t - s)) := by
have hbound : ∀ x ∈ Ico s t,
-scale * curve.dissipation x ≤
(-rate) * curve.energy x + 0 := by
intro x hx
have hneg := neg_le_neg (hcoercive x)
simpa [neg_mul] using hneg
have hgronwall :=
le_gronwallBound_of_liminf_deriv_right_le
(f := curve.energy)
(f' := fun x => -scale * curve.dissipation x)
(δ := curve.energy s)
(K := -rate)
(ε := 0)
(a := s)
(b := t)
curve.energy_continuous.continuousOn
(fun x hx r hr => by
simpa [slope] using
(curve.energy_hasDerivWithinAt x).liminf_right_slope_le hr)
le_rfl
hbound
t
⟨hst, le_rfl⟩
rw [gronwallBound_ε0] at hgronwall
exact hgronwall
/-- A coercive inequality along a dissipation curve implies exponential decay
from time zero. -/Imports
- Mathlib.Analysis.Calculus.LocalExtr.Basic
- Mathlib.Analysis.ODE.Gronwall
Local dependencies
No Registry dependency inferred.
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.scaled_dissipation_of_exponential_decay
theorem scaled_dissipation_of_exponential_decay
{scale rate : ℝ} (curve : DissipationCurve scale)
(hdecay : ∀ s t : ℝ, 0 ≤ t →
curve.energy (s + t) ≤
curve.energy s * Real.exp (-rate * t)) :
∀ s : ℝ,
rate * curve.energy s ≤ scale * curve.dissipation s := by
intro s
let comparison : ℝ → ℝ := fun x =>
curve.energy x -
curve.energy s * Real.exp (-rate * (x - s))
have hmax : IsLocalMaxOn comparison (Ici s) s := by
filter_upwards [self_mem_nhdsWithin] with x hx
have hdecay_x :
curve.energy x ≤
curve.energy s * Real.exp (-rate * (x - s)) := by
have h := hdecay s (x - s) (sub_nonneg.mpr hx)
calc
curve.energy x = curve.energy (s + (x - s)) := by
congr 1
ring
_ ≤ curve.energy s * Real.exp (-rate * (x - s)) := h
dsimp [comparison]
calc
curve.energy x -
curve.energy s * Real.exp (-rate * (x - s)) ≤ 0 :=
sub_nonpos.mpr hdecay_x
_ = curve.energy s -
curve.energy s * Real.exp (-rate * (s - s)) := by simp
have hinner :
HasDerivAt (fun x : ℝ => -rate * (x - s)) (-rate) s := by
change HasDerivAt (fun y : ℝ => -rate * (id y - s)) (-rate) s
have hraw := ((hasDerivAt_id s).sub_const s).const_mul (-rate)
exact hraw.congr_deriv (by ring)
have hexponential :
HasDerivAt
(fun x : ℝ =>
curve.energy s * Real.exp (-rate * (x - s)))
(-rate * curve.energy s) s := by
have hraw := hinner.exp.const_mul (curve.energy s)
apply hraw.congr_deriv
rw [sub_self, mul_zero, Real.exp_zero]
ring
have hderiv :
HasDerivWithinAt comparison
((-scale * curve.dissipation s) -
(-rate * curve.energy s))
(Ici s) s := by
change HasDerivWithinAt
(curve.energy - fun x : ℝ =>
curve.energy s * Real.exp (-rate * (x - s)))
((-scale * curve.dissipation s) - (-rate * curve.energy s))
(Ici s) s
exact (curve.energy_hasDerivWithinAt s).sub
hexponential.hasDerivWithinAt
have hone : (1 : ℝ) ∈ posTangentConeAt (Ici s) s := by
rw [one_mem_posTangentConeAt_iff_frequently]
have hev : ∀ᶠ x in 𝓝[>] s, x ∈ Ici s := by
filter_upwards [self_mem_nhdsWithin] with x hx
have hsx : s < x := by
simpa only [mem_Ioi] using hx
exact hsx.le
exact hev.frequently
have hnonpos :=
hmax.hasFDerivWithinAt_nonpos hderiv.hasFDerivWithinAt hone
have hscalar :
((-scale * curve.dissipation s) -
(-rate * curve.energy s)) ≤ 0 := by
simpa using hnonpos
linarith
/-- Forward direction of Chewi, Theorem 1.2.21, between arbitrary times. -/Imports
- Mathlib.Analysis.Calculus.LocalExtr.Basic
- Mathlib.Analysis.ODE.Gronwall
Local dependencies
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.chewi_theorem_1_2_26_scalar_equivalence
theorem chewi_theorem_1_2_26_scalar_equivalence
{C : ℝ} (hC : 0 < C) (curve : DissipationCurve 1) :
(∀ s : ℝ,
curve.energy s ≤ (C / 2) * curve.dissipation s) ↔
(∀ s t : ℝ, 0 ≤ t →
curve.energy (s + t) ≤
curve.energy s * Real.exp (-(2 / C) * t)) := by
constructor
· intro hLSI s t ht
have h := chewi_theorem_1_2_26_forward_from
hC curve hLSI (show s ≤ s + t by linarith)
simpa using h
· exact chewi_theorem_1_2_26_backward hC curve
end
end SemigroupDecay
end FunctionalInequalities
end TechnicalLemmas
end AutoSamplingTheoryImports
- Mathlib.Analysis.Calculus.LocalExtr.Basic
- Mathlib.Analysis.ODE.Gronwall
Local dependencies
No Registry dependency inferred.
Downstream consumers
- entropy decay
- Langevin mixing in KL