Source Correspondence

Source

Every progressive process with finite probability-time L2 energy has an Ito integral that is an adapted continuous martingale, is characterized at each deterministic time by the restricted terminal L2 completion, and satisfies the Ito isometry.

ASTIS exposition

ASTIS constructs causal lagged-dyadic approximants, refines their grids, completes the terminal integral in L2, proves elementary martingale and Doob bounds, obtains a uniformly convergent continuous version by Borel-Cantelli, and identifies its value at every time through right-dyadic stopping.

Rigorous packet

The filtration usual conditions, progressive measurability, global product-space L2 integrability, Brownian motion relative to that filtration, almost-everywhere path continuity, fixed-time L2 representatives, and indistinguishability criterion are all explicit.

Lean

Source

At every deterministic time, the second moment of the Ito integral equals the probability-time L2 energy accumulated by the integrand up to that time.

ASTIS exposition

The fixed-time process is first identified almost everywhere with the L2 terminal completion of the restricted integrand. The terminal norm isometry and the product-space norm formula then give the displayed equality.

Rigorous packet

The theorem exposes the deterministic-time bound t <= T, the exact strict restriction representative, the fixed probability-time product measure, and the almost-everywhere identification needed to replace the process by its L2 class.

Lean

Source

The expected square of an elementary stochastic integral expands to the sum of its diagonal increment terms because distinct adapted Brownian increments are orthogonal.

ASTIS exposition

ASTIS proves the expectation identity after deriving L2 integrability and cross-term orthogonality from filtration-relative Brownian independence.

Rigorous packet

The filtration, left-endpoint measurability, Brownian future-increment independence, centered increment law, and product integrability are explicit.

Lean

Source

The second moment of the elementary Ito integral equals the expected time integral of the squared elementary integrand.

ASTIS exposition

ASTIS connects Brownian increment second moments to an exact evaluation of processL2Energy under the stopped nonnegative-time Lebesgue measure.

Rigorous packet

Coefficient integrability, clipped interval mass, time-cell disjointness, joint measurability, Tonelli, and the ENNReal energy representation are explicit.

Lean

Source

Localization permits progressive integrands whose squared time integral is finite almost surely, without requiring its expectation to be finite.

ASTIS exposition

The condition is ENNReal-valued and pathwise almost everywhere, so it is visibly weaker than finite expected process energy.

Rigorous packet

The finite time measure, nonnegative path energy, strict comparison with infinity, and probability almost-everywhere quantifier are explicit.

Lean

Source

The squared L2 norm of an integrand on the product probability-time space is the expectation of its squared time integral, and admissible integrands have finite value.

ASTIS exposition

ASTIS uses ENNReal for the energy so the finiteness condition is visible and proves the product-to-iterated identity with Mathlib Tonelli.

Rigorous packet

The finite nonnegative-time measure, product measure, joint a.e. measurability, nonnegative integral, and separate finiteness condition are explicit.

Lean

Source

An elementary adapted process is a finite sum of bounded left-endpoint measurable coefficients on half-open time intervals.

ASTIS exposition

The Lean structure keeps the strict grid, filtration measurability, and coefficient bounds as data rather than erasing the source regularity.

Rigorous packet

Finite indexing, strict endpoint order, left-endpoint strong measurability, boundedness, and the half-open interval convention are explicit.

Lean

Source

The Ito integral of an elementary process is defined by the finite sum of its adapted coefficients times Brownian increments stopped at the terminal time.

ASTIS exposition

This declaration is only the finite elementary integral; it does not claim the isometry, completion, or general stochastic integral.

Rigorous packet

The elementary-process contract supplies adapted bounded coefficients, and every Brownian increment is stopped by the same terminal time.

Lean

Source

Informally, a curve is absolutely continuous when its finite metric derivative exists almost everywhere.

ASTIS exposition

ASTIS formalizes exactly the source's informal criterion on a generic pseudometric space without introducing a tangent vector.

Rigorous packet

The a.e. time quantifier, punctured neighborhood, nonnegative finite speed, and real Lebesgue measure are explicit.

Lean

Source

A functional is alpha-geodesically convex when its value along each geodesic lies below endpoint interpolation minus the alpha quadratic distance correction.

ASTIS exposition

ASTIS chooses the first of the source's equivalent conditions and parameterizes the predicate selecting geodesics.

Rigorous packet

The ambient metric, complete path, geodesic selection, interval membership, coefficient normalization, and endpoint distance are explicit.

Lean

Source

Geodesic alpha-convexity implies the first-order lower bound at the initial endpoint, with the derivative pairing and alpha times squared distance correction.

ASTIS exposition

ASTIS formalizes the positive-time secant limit with HasDerivAt.tendsto_slope and transports the eventual inequality through both limits using the closed order on the reals.

Rigorous packet

A selected geodesic must satisfy the compiled chord formulation, and the path composition t maps to F(path t) must have derivative gradientPairing at zero. In a Wasserstein application, the separate geometric identification sets this scalar to the source inner product with the optimal displacement.

Lean

Source

For a stationary reversible generator, the two negative-generator pairings equal each other and the integrated carre du champ.

ASTIS exposition

ASTIS performs this integral algebra and exposes integrability for L(fg), f Lg, and g Lf separately.

Rigorous packet

Stationarity and symmetry are concrete hypotheses produced by the semigroup route; they are not inferred from an algebraic generator display.

Lean

Source

The negative generator of a reversible Markov semigroup has a nonnegative quadratic form.

ASTIS exposition

ASTIS invokes the compiled integration-by-parts theorem and Mathlib integral nonnegativity.

Rigorous packet

The theorem consumes pointwise Gamma nonnegativity and the stationary generator identity instead of assuming the desired quadratic conclusion.

Lean

Source

The dual optimal transport value is the supremum of the two potential integrals over feasible integrable potential pairs.

ASTIS exposition

ASTIS keeps both integrability requirements and the product-measure a.e. constraint in the feasible predicate.

Rigorous packet

The generic real-cost definition does not silently assume strong duality, boundedness, or attainment.

Lean

Source

The dual value is the supremum of integral f dmu plus integral g dnu over dual-feasible potentials.

ASTIS exposition

The source display is a proved definitional expansion rather than an assumed primal-dual theorem.

Rigorous packet

Only the dual value is expanded; equality to one half W2 squared is not claimed here.

Lean

Source

A Markov process satisfies a Poincare inequality when variance is bounded by a constant times its generator Dirichlet energy.

ASTIS exposition

ASTIS separates this general generator definition from the gradient-energy identity special to Langevin diffusion.

Rigorous packet

Probability normalization, positivity of C, finite mean/variance, and integrability of f Lf are explicit.

Lean

Source

A Markov process satisfies an LSI when density entropy is bounded by C/2 times the Dirichlet form of the density and its logarithm.

ASTIS exposition

ASTIS exposes positivity, unit mass, entropy integrability, and generator-energy integrability instead of relying on totalized integrals.

Rigorous packet

The zero-density log convention, normalization, probability reference law, positive constant, and both finite integrals are explicit.

Lean

Source

Standard Brownian motion starts at zero, has independent centered Gaussian increments with covariance proportional to elapsed time, and has almost surely continuous paths.

ASTIS exposition

ASTIS expresses the vector Gaussian law by every continuous-linear projection, matching Mathlib's coordinate-free Gaussian API.

Rigorous packet

Zero start, finite-family independent increments, all projected Gaussian laws, and a.e. path continuity are separate conjuncts.

Lean

Source

A localizing sequence is an increasing stopping-time sequence whose stopped integrands have finite L2 norm and which converges almost surely to the terminal time.

ASTIS exposition

ASTIS records the iterated nonnegative integral before finiteness, so no totalized real integral hides the L2 side condition.

Rigorous packet

Progressive measurability, stopping-time measurability, monotonicity, finite expected time integral, and the almost-sure limit are separate conjuncts.

Lean

Source

A local martingale is adapted and admits increasing stopping times tending almost surely to infinity for which every centered stopped process is a martingale.

ASTIS exposition

ASTIS reuses Mathlib's stoppedProcess and Martingale predicates and leaves every quantifier visible.

Rigorous packet

Adaptedness, stopping-time measurability, monotonicity, a.s. divergence, initial centering, and the martingale property are all required.

Lean

Source

The Markov operator sends an observable to its conditional expectation after elapsed time t, given the initial state.

ASTIS exposition

ASTIS uses a measurable transition-kernel family and defines the conditional-expectation operator by kernel lintegration.

Rigorous packet

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.

Lean

Source

The 2-Wasserstein distance is the positive square root of the optimal quadratic coupling cost.

ASTIS exposition

ASTIS specializes the compiled Kantorovich value to an ENNReal squared-norm cost and takes its positive ENNReal rpow one half.

Rigorous packet

The state space is a measurable real normed additive group, the cost is ENNReal.ofReal of squared norm, and infinite values remain representable.

Lean

Source

The square of W2 equals the infimum of integrated squared distance over all couplings.

ASTIS exposition

The equality is proved by ENNReal rpow multiplication, not stored as an axiom.

Rigorous packet

The theorem remains valid at infinite transport cost and does not require an optimal coupling witness.

Lean

Source

A Markov semigroup records how the law or observables evolve with time.

ASTIS exposition

ASTIS separates the algebraic semigroup laws from measurability, continuity, and the choice of function space on which the operators act.

Rigorous packet

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.

Lean

Source

Identity and Chapman-Kolmogorov transition-kernel laws induce the zero-time, composition, and commutation laws of Markov operators.

ASTIS exposition

ASTIS derives the operator identities from transition kernels instead of storing the desired semigroup conclusion as an operator assumption.

Rigorous packet

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.

Lean

Source

The infinitesimal generator is the right derivative at zero of the semigroup orbit on its convergence domain.

ASTIS exposition

ASTIS resolves the source's stated technical ambiguity by fixing a real normed observable space, norm convergence, and the one-sided positive-time filter.

Rigorous packet

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.

Lean

Source

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.

ASTIS exposition

The proof uses semigroup commutation and continuity of each P_t to transport the generator limit; no formal differentiation symbol is left uninterpreted.

Rigorous packet

The observable has an actual right-generator witness, and all limits are taken in the selected norm topology through positive time increments.

Lean

Source

The generator is the derivative at time zero of the Markov semigroup.

ASTIS exposition

The formal differential expression and the closed infinitesimal generator are different objects. ASTIS keeps the analytic domain as an explicit red node.

Rigorous packet

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.

Lean

Source

A martingale is an adapted integrable process whose conditional expectation at an earlier time equals its earlier value.

ASTIS exposition

ASTIS uses Mathlib's real-valued Martingale predicate at NNReal time so conditional expectation, stopped-process, and filtration lemmas remain available.

Rigorous packet

The sample space has a measure and filtration, the process is strongly adapted, and the conditional-expectation equality is an almost-everywhere equality for every ordered pair of times.

Lean

Source

A stopping time is a random time whose occurrence by time t is measurable using the information available at time t.

ASTIS exposition

ASTIS uses Mathlib's native Filtration and IsStoppingTime predicate with nonnegative continuous time, preserving all later stopped-process APIs.

Rigorous packet

The sample space carries an ambient measurable structure, the filtration is monotone and subordinate to it, and tau takes values in extended nonnegative time.

Lean

Source

A Markov semigroup is reversible when every time operator is symmetric in the L2 inner product of its stationary law.

ASTIS exposition

The predicate isolates self-adjointness from construction of the concrete L2 semigroup and from proof that pi is invariant.

Rigorous packet

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.

Lean

Source

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.

ASTIS exposition

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.

Rigorous packet

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.

Lean

Source

The carre du champ is the bilinear defect between applying the generator after multiplication and multiplying after applying the generator.

ASTIS exposition

ASTIS records the exact generator formula without building positivity, reversibility, or a concrete Langevin process into the definition.

Rigorous packet

The generator is a real linear map on real observables. The definition is pointwise and leaves domain closure and analytic regularity to downstream interfaces.

Lean

Source

The carre du champ of a Markov generator is pointwise nonnegative on the diagonal.

ASTIS exposition

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.

Rigorous packet

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.

Lean

Source

For the Langevin differential operator, the carre du champ is the gradient inner product, and on the diagonal it is the squared gradient norm.

ASTIS exposition

ASTIS proves the missing Laplacian product rule from second Frechet derivatives and an orthonormal-basis expansion, then performs the concrete Langevin cancellation.

Rigorous packet

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.

Lean

Source

The iterated carre du champ applies the generator to Gamma and subtracts the two mixed generator terms.

ASTIS exposition

The definition reuses the same generator and the compiled Gamma interface, exposing a shared node for curvature and functional-inequality routes.

Rigorous packet

The pointwise algebraic definition is compiled independently of the diffusion chain rule or any Hessian representation.

Lean

Source

The Bakry-Emery curvature-dimension condition requires positive alpha and the pointwise inequality Gamma_2(f) at least alpha Gamma(f).

ASTIS exposition

ASTIS keeps positivity of alpha inside the predicate and does not identify the condition with strong convexity until a separate Langevin theorem proves it.

Rigorous packet

The predicate quantifies over every real observable and state for the selected linear generator; domain restrictions for unbounded generators remain a downstream refinement.

Lean

Source

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.

ASTIS exposition

ASTIS derives the exact textbook statement from Mathlib's more general right-slope Gronwall theorem, preserving the source interval, differentiability, constant, and exponential factor.

Rigorous packet

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.

Lean

Source

For overdamped Langevin diffusion, Itô's formula displays the formal generator as a Laplacian minus a score-directional derivative.

ASTIS exposition

ASTIS owns algebraic, basis, coordinate, and differentiability-aware display lemmas. None of these alone identifies a closed generator domain.

Rigorous packet

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.

Lean

Source

A weighted integration-by-parts calculation makes the Langevin generator formally symmetric under its Gibbs weight.

ASTIS exposition

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.

Rigorous packet

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.

Lean

Source

The Gibbs measure is the stationary law suggested by the weighted generator identity.

ASTIS exposition

ASTIS marks this as red. A formal density calculation does not by itself prove invariance for the Markov semigroup.

Rigorous packet

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.

Lean

Source

Variance is bounded by an energy involving the gradient.

ASTIS exposition

The ASTIS layer makes the measure, function class, integrability, and gradient representation visible.

Rigorous packet

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.

Lean

Source

Entropy is controlled by a Fisher-information or Dirichlet-form term.

ASTIS exposition

ASTIS records the scalar handoff from a square-root density form to a KL/Fisher-information chain, while retaining all finiteness requirements.

Rigorous packet

The density, logarithm convention at zero, square-root derivative, and absolute continuity all need stated representatives and integrability.

Lean

Source

P2,ac consists of Euclidean probability laws with finite second moment that are absolutely continuous with respect to Lebesgue measure.

ASTIS exposition

ASTIS packages the three measure-theoretic conditions without importing any optimal-map or Wasserstein metric conclusion.

Rigorous packet

The ambient space is a finite-dimensional real inner-product Borel space, so Mathlib volume represents Lebesgue measure and the real squared norm defines the second moment.

Lean

Source

The Wasserstein geodesic between two P2,ac laws is the law of the affine interpolation of an optimally coupled endpoint pair; it is also called displacement or McCann interpolation.

ASTIS exposition

ASTIS represents the joint endpoint law directly as a coupling measure, avoiding an unnecessary auxiliary probability space while preserving the exact law construction.

Rigorous packet

Both endpoints satisfy the compiled P2,ac predicate. The coupling has the requested marginals and attains the quadratic Kantorovich infimum. The curve agrees with its measurable affine pushforward throughout [0,1].

Lean

Source

The Kantorovich transport cost is the infimum of expected cost over all joint probability laws with the prescribed marginals.

ASTIS exposition

ASTIS defines the coupling feasible set and its ENNReal infimum directly; lower semicontinuity is reserved for the later minimizer-existence theorem.

Rigorous packet

The two state spaces are measurable, the cost is ENNReal-valued, and the feasible measures have exactly the requested marginals. Probability normalization follows from probability marginals.

Lean

Source

The transport value expands as the infimum of the coupling lintegrals of the cost.

ASTIS exposition

The source-facing theorem unfolds the ASTIS definition without claiming that the infimum is attained.

Rigorous packet

The equality uses an ENNReal sInf and an ENNReal lintegral over the exact coupling set.

Lean

Source

A coupling is a joint probability law with two prescribed marginals.

ASTIS exposition

Samplinglib isolates the marginal contract from transport costs and proves the independent-product witness using Mathlib's product-measure marginal identities.

Rigorous packet

The source works with probability measures on complete separable metric spaces. The coupling contract itself is measure-theoretic; topology and cost measurability enter only when defining and minimizing the transport objective.

Lean

Source

The chapter organizes Poincaré, log-Sobolev, transport, and concentration inequalities in a common measure-theoretic language.

ASTIS exposition

ASTIS separates the probability-law and density prerequisites from the analytic inequality and its semigroup consumers.

Rigorous packet

Each inequality needs an explicit function class and finite terms; extension beyond a smooth compactly supported core requires a closure or density argument.

Lean

Source

A change in drift can be represented by an exponential likelihood ratio.

ASTIS exposition

ASTIS currently owns finite Gaussian cylinder identities. The path-space theorem remains a separate red boundary.

Rigorous packet

A full result requires adapted drift differences, a stochastic integral, a martingale criterion, and identification of the changed path law.

Lean

Source

Rényi divergence packages a power integral of a density ratio.

ASTIS exposition

ASTIS first establishes positivity, measurability, finite lintegral transfer, and calculus for the scalar integrand.

Rigorous packet

Absolute continuity and the extended-value behavior of the density ratio cannot be suppressed.

Lean

Source

Continuous interpolation and change of measure convert local numerical error into sampling error.

ASTIS exposition

The website exposes the compiled divergence and Girsanov leaves, while the full stochastic interpolation chain remains red.

Rigorous packet

Prove adaptedness, moment bounds, integrated drift error, absolute continuity of path laws, and the terminal-time data-processing step independently.

Lean

Source

A Gaussian augmentation creates alternating conditional distributions with the target as a marginal.

ASTIS exposition

ASTIS treats kernel measurability, normalization, Fubini/Tonelli, and marginal preservation as independent reusable roots.

Rigorous packet

Before composing kernels, both conditional normalizers must be measurable, positive, and finite.

Lean

Source

Relative Fisher information is used as a first-order stationarity measure for non-log-concave sampling, and entropy dissipation supplies an averaged finite-time bound.

ASTIS exposition

ASTIS exposes the density, score-representative, absolute-continuity, entropy-dissipation, and randomized-time interfaces separately.

Rigorous packet

Define the relative score almost everywhere, prove Fisher-information measurability and finiteness where used, justify entropy dissipation on a stated domain, then add discretization and oracle errors.

Lean

Source

The reverse-time drift uses the score of the forward marginal, and approximation errors become drift errors.

ASTIS exposition

ASTIS exposes Fisher-information roots but does not yet claim a reverse-time SDE theorem.

Rigorous packet

Choose a density representative, establish spatial and temporal regularity, state the time-reversal theorem, and only then analyze learned-score and discretization errors.

Lean

Source

The pathwise local-square-integrability condition admits an increasing canonical sequence of stopping times approaching the horizon such that each stopped integrand has finite global L2 energy.

ASTIS exposition

ASTIS compiles exceptional-set completion, equality-level first hitting, the intermediate-value step, stopping-time measurability, exact stopped-energy control, monotonicity, and terminal exhaustion rather than treating localization as a black box.

Rigorous packet

Usual filtration conditions, completion of null sets, progressive measurability, pathwise energy continuity, stopping-time measurability, no overshoot, and the probability-space product-L2 consequence are explicit.

Lean

Source

Each canonical energy truncation is globally square-integrable, so its Ito integral is an adapted continuous martingale with the deterministic-time restriction representation used in the localization proof.

ASTIS exposition

ASTIS reuses the global Ito map from Theorem 1.1.8 and proves adaptedness, martingality, continuity, and deterministic-time restriction compatibility in one source-facing display theorem. Random-time stopping is deliberately discharged later in Proposition 1.1.16.

Rigorous packet

The stopped-integrand L2 bound, Brownian/filtration contract, positive horizon, continuous process representative, and distinction between deterministic restriction and random stopping are explicit.

Lean

Source

The Ito integral of a progressive locally square-integrable integrand has a continuous version that is a local martingale.

ASTIS exposition

ASTIS compiles the coefficient-level stopping identity, the entire elementary-Ito finite-sum identity, right-dyadic random-time convergence, stopped-integrand L2 contraction, stopping-graph nullity, horizon overlap, localized martingale coherence, and final pathwise gluing into the source-facing proposition.

Rigorous packet

Strict-versus-closed stopping differs only on a product-measure-zero stopping graph; finite-horizon Ito versions are proved compatible before gluing; and the localizers are proved monotone and tending to infinity almost surely.

Lean