Chapter 1 · source-complete audit

Chapter 1 Completion Matrix

Every numbered statement, numbered displayed identity, and exercise in the August 9, 2026 source edition. Local compilation and full mathematical-route completion are tracked separately.

67numbered statements

37displayed identities

21exercises

49items with compiled local evidence

Status rule. A blue local declaration does not turn a theorem route blue. Concrete process construction, topology, domains, regularity, or source-level consumers remain visible in the blocker column.

Source	Faithful summary	Local status	Route status	Rigor boundary
Definition 1.1.1book 4 / PDF 16	Standard Brownian motion	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions Borel measurable real Hilbert state space HasLaw for every StrongDual projection iIndepFun on disjoint intervals a.e. Continuous paths
Definition 1.1.4book 5 / PDF 17	Martingale with respect to a filtration	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions a Measure and Filtration indexed by NNReal Mathlib StronglyAdapted process measurability conditional expectation equality almost everywhere for s <= t
Theorem 1.1.8book 6 / PDF 18	Definition of the Ito integral and Ito isometry	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions SatisfiesUsualConditions filtration mu IsBrownianMotionWithFiltration B filtration mu ProgressiveL2Integrand filtration mu T positive finite construction horizon almost-everywhere representatives and path continuity
Definition 1.1.11book 6 / PDF 18	Stopping time	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions a Mathlib Filtration indexed by NNReal tau maps into WithTop NNReal each event tau <= t is measurable in the filtration at t
Definition 1.1.12book 6 / PDF 18	Localizing sequence	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions Mathlib ProgMeasurable Mathlib IsStoppingTime nonnegative-time Lebesgue measure a.e. filter limit
Proposition 1.1.13book 7 / PDF 19	Canonical localizing sequence for a progressive integrand	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions SatisfiesUsualConditions filtration mu IsProbabilityMeasure mu LocalProgressiveL2Integrand filtration mu T
Definition 1.1.15book 7 / PDF 19	Local martingale	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions Mathlib Adapted Mathlib stoppedProcess Mathlib Martingale a.e. atTop convergence
Proposition 1.1.16book 7 / PDF 19	A localized Ito integral is a continuous local martingale	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions SatisfiesUsualConditions filtration mu IsProbabilityMeasure mu GlobalLocalProgressiveL2Integrand filtration mu IsBrownianMotionWithFiltration B filtration mu
Definition 1.1.17book 8 / PDF 20	Ito process	Planned No exact local mapping yet	Planned	Exact blocker formalize or port the required filtered-space stochastic integral, localization, and Ito-calculus interface Formal assumptions explicit filtration and adaptedness joint/progressive measurability Bochner or stochastic integrability almost-everywhere representatives stopping-time measurability where localization is used
Theorem 1.1.19book 9 / PDF 21	Ito formula	Planned No exact local mapping yet	Planned	Exact blocker formalize or port the required filtered-space stochastic integral, localization, and Ito-calculus interface Formal assumptions explicit filtration and adaptedness joint/progressive measurability Bochner or stochastic integrability almost-everywhere representatives stopping-time measurability where localization is used
Theorem 1.1.22book 10 / PDF 22	Existence and uniqueness of SDE solutions	Planned No exact local mapping yet	Planned	Exact blocker formalize or port the required filtered-space stochastic integral, localization, and Ito-calculus interface Formal assumptions explicit filtration and adaptedness joint/progressive measurability Bochner or stochastic integrability almost-everywhere representatives stopping-time measurability where localization is used
Definition 1.2.1book 10 / PDF 22	Markov semigroup	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions a transition-kernel contract measurable ENNReal observables
Lemma 1.2.2book 10 / PDF 22	Semigroup property	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions Markov transition kernels at NNReal times identity at zero Chapman-Kolmogorov kernel composition
Definition 1.2.3book 11 / PDF 23	Infinitesimal generator	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions a real normed observable space a continuous-linear semigroup Tendsto through nhdsWithin 0 (Ioi 0)
Example 1.2.4book 11 / PDF 23	Generator of the Langevin diffusion	Compiled 4 Registry declarations	Partial	Exact blocker connect the abstract compiled leaves to a concrete strongly continuous Langevin semigroup and its closed generator domain Formal assumptions finite-dimensional Euclidean index type explicit Fréchet derivatives pointwise differentiability hypotheses where genuine derivatives are used
Proposition 1.2.5book 12 / PDF 24	Kolmogorov backward equation	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions ContinuousLinearSemigroup HasRightGeneratorAt S f g NNReal evaluation time
Proposition 1.2.6book 12 / PDF 24	Kolmogorov forward equation	Planned No exact local mapping yet	Planned	Exact blocker connect the abstract compiled leaves to a concrete strongly continuous Langevin semigroup and its closed generator domain Formal assumptions measurable transition kernels a specified observable space and topology explicit generator domain integrability and domain closure concrete process-level realization when Langevin is claimed
Proposition 1.2.7book 12 / PDF 24	Equivalent formulations of stationarity	Planned No exact local mapping yet	Planned	Exact blocker connect the abstract compiled leaves to a concrete strongly continuous Langevin semigroup and its closed generator domain Formal assumptions measurable transition kernels a specified observable space and topology explicit generator domain integrability and domain closure concrete process-level realization when Langevin is claimed
Example 1.2.8book 13 / PDF 25	Langevin adjoint and weighted integration by parts	Compiled 6 Registry declarations	Partial	Exact blocker connect the abstract compiled leaves to a concrete strongly continuous Langevin semigroup and its closed generator domain 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
Corollary 1.2.9book 13 / PDF 25	Stationary Gibbs law for Langevin diffusion	Compiled 3 Registry declarations	Partial	Exact blocker connect the abstract compiled leaves to a concrete strongly continuous Langevin semigroup and its closed generator domain Formal assumptions probability normalization whole-space weighted integration by parts generator/semigroup domain well-posed Markov evolution
Definition 1.2.10book 13 / PDF 25	Reversible Markov semigroup	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions a real inner-product space a nonnegative-time continuous-linear semigroup the symmetry equality for every time and pair of observables
Definition 1.2.12book 14 / PDF 26	Carre du champ	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions a real linear map on real-valued observables pointwise multiplication of observables
Lemma 1.2.13book 14 / PDF 26	Non-negativity of the carre du champ	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. 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
Theorem 1.2.14book 14 / PDF 26	Fundamental integration-by-parts identity	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions three explicit Integrable terms zero integral of L(fg) symmetric generator pairing
Corollary 1.2.15book 14 / PDF 26	Non-negativity of minus the reversible generator	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions integrability of L(f squared) and f Lf stationarity pointwise Gamma nonnegativity
Example 1.2.17book 15 / PDF 27	Carre du champ and Dirichlet form for Langevin	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions finite-dimensional real Euclidean state space global ContDiff R 2 hypotheses for both observables
Definition 1.2.19book 16 / PDF 28	Poincare inequality	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions a probability measure a real generator action PoincareAdmissible finite integrals
Lemma 1.2.20book 16 / PDF 28	Differential Gronwall lemma	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. 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
Theorem 1.2.21book 16 / PDF 28	Poincare inequality and variance decay	Compiled 16 Registry declarations	Partial	Exact blocker instantiate the scalar variance curve from the concrete reversible Markov or Langevin semigroup and prove its -2 Dirichlet-energy derivative identity; instantiate the chi-square curve from an evolving Radon-Nikodym density and justify its dissipation identity; extend the scalar/core equivalence to the intended closed L2 generator domain Formal assumptions explicit measure and scalar field probability normalization integrability/square-integrability explicit Dirichlet form
Theorem 1.2.22book 17 / PDF 29	Poincare inequality and chi-squared decay	Compiled 16 Registry declarations	Partial	Exact blocker instantiate the scalar variance curve from the concrete reversible Markov or Langevin semigroup and prove its -2 Dirichlet-energy derivative identity; instantiate the chi-square curve from an evolving Radon-Nikodym density and justify its dissipation identity; extend the scalar/core equivalence to the intended closed L2 generator domain Formal assumptions explicit measure and scalar field probability normalization integrability/square-integrability explicit Dirichlet form
Example 1.2.23book 17 / PDF 29	Poincare inequality for Langevin diffusion	Planned No exact local mapping yet	Planned	Exact blocker connect the abstract compiled leaves to a concrete strongly continuous Langevin semigroup and its closed generator domain Formal assumptions measurable transition kernels a specified observable space and topology explicit generator domain integrability and domain closure concrete process-level realization when Langevin is claimed
Definition 1.2.25book 18 / PDF 30	Log-Sobolev inequality	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions a probability measure LogSobolevAdmissible density generator Dirichlet form
Theorem 1.2.26book 18 / PDF 30	Log-Sobolev inequality and KL decay	Compiled 9 Registry declarations	Partial	Exact blocker construct the concrete KL/Fisher-information curve for the reversible Langevin or Markov semigroup; justify KL differentiation and the entropy-dissipation identity under explicit density and integrability hypotheses; extend the scalar/core equivalence to the intended entropy domain Formal assumptions nonnegative measurable density normalization finite entropy and energy terms in the handoff
Example 1.2.27book 18 / PDF 30	Log-Sobolev inequality for Langevin diffusion	Planned No exact local mapping yet	Planned	Exact blocker connect the abstract compiled leaves to a concrete strongly continuous Langevin semigroup and its closed generator domain Formal assumptions measurable transition kernels a specified observable space and topology explicit generator domain integrability and domain closure concrete process-level realization when Langevin is claimed
Definition 1.2.28book 18 / PDF 30	Iterated carre du champ	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions a real linear generator on real-valued observables the compiled carreDuChamp definition
Definition 1.2.29book 19 / PDF 31	Bakry-Emery curvature-dimension criterion	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions 0 < alpha the inequality holds for every observable and state
Theorem 1.2.30book 19 / PDF 31	Bakry-Emery criterion implies functional inequalities	Planned No exact local mapping yet	Planned	Exact blocker connect the abstract compiled leaves to a concrete strongly continuous Langevin semigroup and its closed generator domain Formal assumptions measurable transition kernels a specified observable space and topology explicit generator domain integrability and domain closure concrete process-level realization when Langevin is claimed
Theorem 1.2.31book 19 / PDF 31	Curvature-dimension condition for Langevin	Planned No exact local mapping yet	Planned	Exact blocker connect the abstract compiled leaves to a concrete strongly continuous Langevin semigroup and its closed generator domain Formal assumptions measurable transition kernels a specified observable space and topology explicit generator domain integrability and domain closure concrete process-level realization when Langevin is claimed
Definition 1.3.1book 20 / PDF 32	Kantorovich primal transport problem	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions measurable state spaces an ENNReal-valued cost the exact coupling marginal predicate
Theorem 1.3.3book 20 / PDF 32	Existence of an optimal transport plan	Planned No exact local mapping yet	Planned	Exact blocker build the Wasserstein metric, optimal-plan existence, gluing, geodesic, and continuity-equation chain without assuming the desired transport theorem Formal assumptions measurable marginals and couplings finite second moments tightness/lower semicontinuity for existence absolute continuity for transport maps weak continuity-equation regularity
Definition 1.3.4book 20 / PDF 32	2-Wasserstein distance	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions measurable normed additive state space compiled Kantorovich transportCost
Definition 1.3.6book 21 / PDF 33	Dual quadratic optimal transport problem	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions measurable spaces and measures integrable real potentials product-a.e. dual constraint
Theorem 1.3.8book 22 / PDF 34	Fundamental theorem of optimal transport	Planned No exact local mapping yet	Planned	Exact blocker build the Wasserstein metric, optimal-plan existence, gluing, geodesic, and continuity-equation chain without assuming the desired transport theorem Formal assumptions measurable marginals and couplings finite second moments tightness/lower semicontinuity for existence absolute continuity for transport maps weak continuity-equation regularity
Definition 1.3.12book 25 / PDF 37	Absolutely continuous finite-second-moment laws	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions finite-dimensional real inner-product space Borel measurable structure IsProbabilityMeasure, absolute continuity, and Integrable squared norm
Lemma 1.3.13book 25 / PDF 37	Gluing lemma	Planned No exact local mapping yet	Planned	Exact blocker build the Wasserstein metric, optimal-plan existence, gluing, geodesic, and continuity-equation chain without assuming the desired transport theorem Formal assumptions measurable marginals and couplings finite second moments tightness/lower semicontinuity for existence absolute continuity for transport maps weak continuity-equation regularity
Proposition 1.3.14book 25 / PDF 37	Wasserstein distance is a metric	Planned No exact local mapping yet	Planned	Exact blocker build the Wasserstein metric, optimal-plan existence, gluing, geodesic, and continuity-equation chain without assuming the desired transport theorem Formal assumptions measurable marginals and couplings finite second moments tightness/lower semicontinuity for existence absolute continuity for transport maps weak continuity-equation regularity
Proposition 1.3.15book 26 / PDF 38	Completeness, separability, and convergence in Wasserstein space	Planned No exact local mapping yet	Planned	Exact blocker build the Wasserstein metric, optimal-plan existence, gluing, geodesic, and continuity-equation chain without assuming the desired transport theorem Formal assumptions measurable marginals and couplings finite second moments tightness/lower semicontinuity for existence absolute continuity for transport maps weak continuity-equation regularity
Definition 1.3.16book 26 / PDF 38	Absolutely continuous curve in Wasserstein space	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions a PseudoMetricSpace a real-time curve a.e. existence of HasMetricDerivativeAt
Theorem 1.3.17book 26 / PDF 38	Continuity equation generated by a velocity field	Planned No exact local mapping yet	Planned	Exact blocker build the Wasserstein metric, optimal-plan existence, gluing, geodesic, and continuity-equation chain without assuming the desired transport theorem Formal assumptions measurable marginals and couplings finite second moments tightness/lower semicontinuity for existence absolute continuity for transport maps weak continuity-equation regularity
Remark 1.3.19book 27 / PDF 39	Regularity boundary for the continuity equation	Planned No exact local mapping yet	Planned	Exact blocker build the Wasserstein metric, optimal-plan existence, gluing, geodesic, and continuity-equation chain without assuming the desired transport theorem Formal assumptions measurable marginals and couplings finite second moments tightness/lower semicontinuity for existence absolute continuity for transport maps weak continuity-equation regularity
Theorem 1.3.20book 27 / PDF 39	Curves of measures as fluid flows	Planned No exact local mapping yet	Planned	Exact blocker build the Wasserstein metric, optimal-plan existence, gluing, geodesic, and continuity-equation chain without assuming the desired transport theorem Formal assumptions measurable marginals and couplings finite second moments tightness/lower semicontinuity for existence absolute continuity for transport maps weak continuity-equation regularity
Theorem 1.3.23book 30 / PDF 42	Wasserstein geodesics	Planned No exact local mapping yet	Planned	Exact blocker build the Wasserstein metric, optimal-plan existence, gluing, geodesic, and continuity-equation chain without assuming the desired transport theorem Formal assumptions measurable marginals and couplings finite second moments tightness/lower semicontinuity for existence absolute continuity for transport maps weak continuity-equation regularity
Definition 1.3.25book 30 / PDF 42	Wasserstein geodesic and displacement interpolation	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions a finite-dimensional real inner-product Borel space P2,ac endpoint predicates a coupling attaining the quadratic transport cost the affine pushforward identity on [0,1]
Definition 1.3.26book 31 / PDF 43	Geodesic alpha-convexity	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions a MetricSpace an explicit geodesic predicate real-valued functional
Theorem 1.4.1book 32 / PDF 44	Wasserstein gradient from the first variation	Planned No exact local mapping yet	Planned	Exact blocker formalize first variations and the weak Wasserstein gradient-flow chain with the regularity needed for differentiation Formal assumptions density positivity and integrability weak continuity equation differentiability along Wasserstein curves tangent-space membership geodesic convexity with explicit domain
Example 1.4.2book 32 / PDF 44	Langevin diffusion as the KL Wasserstein gradient flow	Planned No exact local mapping yet	Planned	Exact blocker formalize first variations and the weak Wasserstein gradient-flow chain with the regularity needed for differentiation Formal assumptions density positivity and integrability weak continuity equation differentiability along Wasserstein curves tangent-space membership geodesic convexity with explicit domain
Theorem 1.4.5book 34 / PDF 46	Geodesic convexity of KL divergence	Planned No exact local mapping yet	Planned	Exact blocker formalize first variations and the weak Wasserstein gradient-flow chain with the regularity needed for differentiation Formal assumptions density positivity and integrability weak continuity equation differentiability along Wasserstein curves tangent-space membership geodesic convexity with explicit domain
Theorem 1.4.6book 34 / PDF 46	Wasserstein gradient of squared distance	Planned No exact local mapping yet	Planned	Exact blocker formalize first variations and the weak Wasserstein gradient-flow chain with the regularity needed for differentiation Formal assumptions density positivity and integrability weak continuity equation differentiability along Wasserstein curves tangent-space membership geodesic convexity with explicit domain
Theorem 1.4.12book 36 / PDF 48	Contractivity of the Langevin diffusion	Planned No exact local mapping yet	Planned	Exact blocker formalize first variations and the weak Wasserstein gradient-flow chain with the regularity needed for differentiation Formal assumptions density positivity and integrability weak continuity equation differentiability along Wasserstein curves tangent-space membership geodesic convexity with explicit domain
Lemma 1.5.1book 37 / PDF 49	Comparison between TV, KL, and chi-squared divergences	Planned No exact local mapping yet	Planned	Exact blocker formalize the divergence comparisons, initialization bounds, data processing, variational principle, and conditional KL chain rule Formal assumptions Radon-Nikodym representatives finite divergence terms kernel measurability initialization normalizers and moment bounds
Lemma 1.5.2book 37 / PDF 49	Chi-squared divergence at initialization	Planned No exact local mapping yet	Planned	Exact blocker formalize the divergence comparisons, initialization bounds, data processing, variational principle, and conditional KL chain rule Formal assumptions Radon-Nikodym representatives finite divergence terms kernel measurability initialization normalizers and moment bounds
Lemma 1.5.3book 37 / PDF 49	Wasserstein distance at initialization	Planned No exact local mapping yet	Planned	Exact blocker formalize the divergence comparisons, initialization bounds, data processing, variational principle, and conditional KL chain rule Formal assumptions Radon-Nikodym representatives finite divergence terms kernel measurability initialization normalizers and moment bounds
Definition 1.5.4book 38 / PDF 50	Total variation distance	Planned No exact local mapping yet	Planned	Exact blocker formalize the divergence comparisons, initialization bounds, data processing, variational principle, and conditional KL chain rule Formal assumptions Radon-Nikodym representatives finite divergence terms kernel measurability initialization normalizers and moment bounds
Definition 1.5.5book 39 / PDF 51	f-divergence	Planned No exact local mapping yet	Planned	Exact blocker formalize the divergence comparisons, initialization bounds, data processing, variational principle, and conditional KL chain rule Formal assumptions Radon-Nikodym representatives finite divergence terms kernel measurability initialization normalizers and moment bounds
Theorem 1.5.6book 39 / PDF 51	Data-processing inequality	Planned No exact local mapping yet	Planned	Exact blocker formalize the divergence comparisons, initialization bounds, data processing, variational principle, and conditional KL chain rule Formal assumptions Radon-Nikodym representatives finite divergence terms kernel measurability initialization normalizers and moment bounds
Theorem 1.5.7book 40 / PDF 52	Donsker-Varadhan variational principle	Planned No exact local mapping yet	Planned	Exact blocker formalize the divergence comparisons, initialization bounds, data processing, variational principle, and conditional KL chain rule Formal assumptions Radon-Nikodym representatives finite divergence terms kernel measurability initialization normalizers and moment bounds
Lemma 1.5.8book 40 / PDF 52	Chain rule for KL divergence	Planned No exact local mapping yet	Planned	Exact blocker formalize the divergence comparisons, initialization bounds, data processing, variational principle, and conditional KL chain rule Formal assumptions Radon-Nikodym representatives finite divergence terms kernel measurability initialization normalizers and moment bounds
Displayed identity (1.0.1)book 3 / PDF 15	Overdamped Langevin SDE	Planned No exact local mapping yet	Planned	Exact blocker construct the concrete Langevin process and connect its integral equation, transition law, and regularity Formal assumptions finite-dimensional measurable Euclidean state space adapted Brownian motion measurable and integrable drift existence of the stochastic integrals
Displayed identity (1.1.2)book 4 / PDF 16	Elementary adapted process	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions a Mathlib Filtration indexed by NNReal StrictMono endpoint map on Fin (n + 1) StronglyMeasurable coefficients in the left-endpoint sigma-algebra a pointwise bound for every coefficient
Displayed identity (1.1.3)book 5 / PDF 17	Ito integral for an elementary process	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions the certified elementary-process structure from display (1.1.2) finite Fin-indexed summation NNReal minimum for stopping each increment at the terminal time
Displayed identity (1.1.5)book 5 / PDF 17	Orthogonal martingale-increment expansion	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions IsBrownianMotionWithFiltration bounded left-endpoint strongly measurable coefficients MemLp two for every weighted increment filtration-level independence and centered future increments
Displayed identity (1.1.6)book 5 / PDF 17	Elementary-process Ito isometry	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions IsBrownianMotionWithFiltration bounded left-endpoint strongly measurable coefficients the stopped NNReal time measure product-space processL2Energy in ENNReal
Displayed identity (1.1.7)book 5 / PDF 17	Square-integrability condition for an integrand	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions finite pulled-back Lebesgue measure on NNReal time up to T AEMeasurable squared process on the product measure ENNReal product and iterated lintegrals so finiteness remains explicit
Displayed identity (1.1.9)book 6 / PDF 18	Ito isometry	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions SatisfiesUsualConditions filtration mu IsBrownianMotionWithFiltration B filtration mu ProgressiveL2Integrand filtration mu T deterministic time t <= T strict time restriction as an endpoint-null representative of the integral over [0,t]
Displayed identity (1.1.10)book 6 / PDF 18	Almost-sure local square-integrability	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions TimeMeasure.upTo T ENNReal time lintegral MeasureTheory almost-everywhere quantification
Displayed identity (1.1.14)book 7 / PDF 19	Stopped Ito integral	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions SatisfiesUsualConditions filtration mu IsProbabilityMeasure mu LocalProgressiveL2Integrand filtration mu T 0 < T IsBrownianMotionWithFiltration B filtration mu
Displayed identity (1.1.18)book 8 / PDF 20	Differential notation for an Ito process	Planned No exact local mapping yet	Planned	Exact blocker formalize or port the required filtered-space stochastic integral, localization, and Ito-calculus interface Formal assumptions explicit filtration and adaptedness joint/progressive measurability Bochner or stochastic integrability almost-everywhere representatives stopping-time measurability where localization is used
Displayed identity (1.1.20)book 9 / PDF 21	Integral Ito formula	Planned No exact local mapping yet	Planned	Exact blocker formalize or port the required filtered-space stochastic integral, localization, and Ito-calculus interface Formal assumptions explicit filtration and adaptedness joint/progressive measurability Bochner or stochastic integrability almost-everywhere representatives stopping-time measurability where localization is used
Displayed identity (1.1.21)book 9 / PDF 21	Differential Ito formula	Planned No exact local mapping yet	Planned	Exact blocker formalize or port the required filtered-space stochastic integral, localization, and Ito-calculus interface Formal assumptions explicit filtration and adaptedness joint/progressive measurability Bochner or stochastic integrability almost-everywhere representatives stopping-time measurability where localization is used
Displayed identity (1.2.11)book 13 / PDF 25	Markov-semigroup Jensen inequality	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions a Feller transition-kernel contract a bounded continuous real observable
Displayed identity (1.2.16)book 15 / PDF 27	Relative-density Fokker-Planck equation	Planned No exact local mapping yet	Planned	Exact blocker connect the abstract compiled leaves to a concrete strongly continuous Langevin semigroup and its closed generator domain Formal assumptions measurable transition kernels a specified observable space and topology explicit generator domain integrability and domain closure concrete process-level realization when Langevin is claimed
Displayed identity (1.2.18)book 15 / PDF 27	Langevin negative generator as weighted gradient adjoint	Planned No exact local mapping yet	Planned	Exact blocker connect the abstract compiled leaves to a concrete strongly continuous Langevin semigroup and its closed generator domain Formal assumptions measurable transition kernels a specified observable space and topology explicit generator domain integrability and domain closure concrete process-level realization when Langevin is claimed
Displayed identity (1.2.24)book 17 / PDF 29	KL dissipation through the Dirichlet form	Planned No exact local mapping yet	Planned	Exact blocker connect the abstract compiled leaves to a concrete strongly continuous Langevin semigroup and its closed generator domain Formal assumptions measurable transition kernels a specified observable space and topology explicit generator domain integrability and domain closure concrete process-level realization when Langevin is claimed
Displayed identity (1.3.2)book 20 / PDF 32	Kantorovich primal value	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions the compiled transportCost and couplingSet definitions
Displayed identity (1.3.5)book 20 / PDF 32	Quadratic transport cost	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions ENNReal rpow algebra
Displayed identity (1.3.7)book 21 / PDF 33	Kantorovich dual value	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions dualTransportValue and DualFeasible
Displayed identity (1.3.9)book 22 / PDF 34	Quadratic-cost dual constraint	Planned No exact local mapping yet	Planned	Exact blocker build the Wasserstein metric, optimal-plan existence, gluing, geodesic, and continuity-equation chain without assuming the desired transport theorem Formal assumptions measurable marginals and couplings finite second moments tightness/lower semicontinuity for existence absolute continuity for transport maps weak continuity-equation regularity
Displayed identity (1.3.10)book 22 / PDF 34	Convex-potential dual form	Planned No exact local mapping yet	Planned	Exact blocker build the Wasserstein metric, optimal-plan existence, gluing, geodesic, and continuity-equation chain without assuming the desired transport theorem Formal assumptions measurable marginals and couplings finite second moments tightness/lower semicontinuity for existence absolute continuity for transport maps weak continuity-equation regularity
Displayed identity (1.3.11)book 23 / PDF 35	Optimal-map gradient relation	Planned No exact local mapping yet	Planned	Exact blocker build the Wasserstein metric, optimal-plan existence, gluing, geodesic, and continuity-equation chain without assuming the desired transport theorem Formal assumptions measurable marginals and couplings finite second moments tightness/lower semicontinuity for existence absolute continuity for transport maps weak continuity-equation regularity
Displayed identity (1.3.18)book 26 / PDF 38	Continuity equation	Planned No exact local mapping yet	Planned	Exact blocker build the Wasserstein metric, optimal-plan existence, gluing, geodesic, and continuity-equation chain without assuming the desired transport theorem Formal assumptions measurable marginals and couplings finite second moments tightness/lower semicontinuity for existence absolute continuity for transport maps weak continuity-equation regularity
Displayed identity (1.3.21)book 27 / PDF 39	Kinetic action of a measure curve	Planned No exact local mapping yet	Planned	Exact blocker build the Wasserstein metric, optimal-plan existence, gluing, geodesic, and continuity-equation chain without assuming the desired transport theorem Formal assumptions measurable marginals and couplings finite second moments tightness/lower semicontinuity for existence absolute continuity for transport maps weak continuity-equation regularity
Displayed identity (1.3.22)book 29 / PDF 41	Riemannian distance as the infimum of path length	Planned No exact local mapping yet	Planned	Exact blocker build the Wasserstein metric, optimal-plan existence, gluing, geodesic, and continuity-equation chain without assuming the desired transport theorem Formal assumptions measurable marginals and couplings finite second moments tightness/lower semicontinuity for existence absolute continuity for transport maps weak continuity-equation regularity
Displayed identity (1.3.24)book 30 / PDF 42	Benamou-Brenier dynamic formulation	Planned No exact local mapping yet	Planned	Exact blocker build the Wasserstein metric, optimal-plan existence, gluing, geodesic, and continuity-equation chain without assuming the desired transport theorem Formal assumptions measurable marginals and couplings finite second moments tightness/lower semicontinuity for existence absolute continuity for transport maps weak continuity-equation regularity
Displayed identity (1.4.3)book 34 / PDF 46	Entropy under displacement interpolation	Planned No exact local mapping yet	Planned	Exact blocker formalize first variations and the weak Wasserstein gradient-flow chain with the regularity needed for differentiation Formal assumptions density positivity and integrability weak continuity equation differentiability along Wasserstein curves tangent-space membership geodesic convexity with explicit domain
Displayed identity (1.4.4)book 34 / PDF 46	Entropy Hessian along a Wasserstein geodesic	Planned No exact local mapping yet	Planned	Exact blocker formalize first variations and the weak Wasserstein gradient-flow chain with the regularity needed for differentiation Formal assumptions density positivity and integrability weak continuity equation differentiability along Wasserstein curves tangent-space membership geodesic convexity with explicit domain
Displayed identity (1.4.7)book 34 / PDF 46	First-order geodesic-convexity inequality	Compiled 1 Registry declarations	Compiled	Exact blocker None for this source item. Formal assumptions the compiled endpoint chord inequality on every selected geodesic HasDerivAt of the functional along the selected path at zero
Displayed identity (1.4.8)book 35 / PDF 47	Gradient-flow function-value rate	Planned No exact local mapping yet	Planned	Exact blocker formalize first variations and the weak Wasserstein gradient-flow chain with the regularity needed for differentiation Formal assumptions density positivity and integrability weak continuity equation differentiability along Wasserstein curves tangent-space membership geodesic convexity with explicit domain
Displayed identity (1.4.9)book 35 / PDF 47	Gradient-flow energy dissipation	Planned No exact local mapping yet	Planned	Exact blocker formalize first variations and the weak Wasserstein gradient-flow chain with the regularity needed for differentiation Formal assumptions density positivity and integrability weak continuity equation differentiability along Wasserstein curves tangent-space membership geodesic convexity with explicit domain
Displayed identity (1.4.10)book 35 / PDF 47	Wasserstein Polyak-Lojasiewicz inequality	Planned No exact local mapping yet	Planned	Exact blocker formalize first variations and the weak Wasserstein gradient-flow chain with the regularity needed for differentiation Formal assumptions density positivity and integrability weak continuity equation differentiability along Wasserstein curves tangent-space membership geodesic convexity with explicit domain
Displayed identity (1.4.11)book 35 / PDF 47	Quadratic growth inequality	Planned No exact local mapping yet	Planned	Exact blocker formalize first variations and the weak Wasserstein gradient-flow chain with the regularity needed for differentiation Formal assumptions density positivity and integrability weak continuity equation differentiability along Wasserstein curves tangent-space membership geodesic convexity with explicit domain
Displayed identity (1.4.13)book 36 / PDF 48	Sharp KL convergence under strong convexity	Planned No exact local mapping yet	Planned	Exact blocker formalize first variations and the weak Wasserstein gradient-flow chain with the regularity needed for differentiation Formal assumptions density positivity and integrability weak continuity equation differentiability along Wasserstein curves tangent-space membership geodesic convexity with explicit domain
Displayed identity (1.4.14)book 36 / PDF 48	Convex KL convergence rate	Planned No exact local mapping yet	Planned	Exact blocker formalize first variations and the weak Wasserstein gradient-flow chain with the regularity needed for differentiation Formal assumptions density positivity and integrability weak continuity equation differentiability along Wasserstein curves tangent-space membership geodesic convexity with explicit domain
Displayed identity (1.4.15)book 36 / PDF 48	LSI as Wasserstein gradient domination	Planned No exact local mapping yet	Planned	Exact blocker formalize first variations and the weak Wasserstein gradient-flow chain with the regularity needed for differentiation Formal assumptions density positivity and integrability weak continuity equation differentiability along Wasserstein curves tangent-space membership geodesic convexity with explicit domain
Displayed identity (1.4.16)book 36 / PDF 48	Talagrand T2 inequality	Planned No exact local mapping yet	Planned	Exact blocker formalize first variations and the weak Wasserstein gradient-flow chain with the regularity needed for differentiation Formal assumptions density positivity and integrability weak continuity equation differentiability along Wasserstein curves tangent-space membership geodesic convexity with explicit domain
Exercise 1.1book 41 / PDF 53	Orthogonality of martingale increments	Planned No exact local mapping yet	Planned	Exact blocker decompose the exercise into dependency-ready Lean leaves and map every cited theorem Formal assumptions all measurability, integrability, topology, and domain conditions needed by the cited route
Exercise 1.2book 42 / PDF 54	Explosion of ODEs	Planned No exact local mapping yet	Planned	Exact blocker decompose the exercise into dependency-ready Lean leaves and map every cited theorem Formal assumptions all measurability, integrability, topology, and domain conditions needed by the cited route
Exercise 1.3book 42 / PDF 54	Ornstein-Uhlenbeck process	Planned No exact local mapping yet	Planned	Exact blocker decompose the exercise into dependency-ready Lean leaves and map every cited theorem Formal assumptions all measurability, integrability, topology, and domain conditions needed by the cited route
Exercise 1.4book 42 / PDF 54	Generator for general SDEs	Planned No exact local mapping yet	Planned	Exact blocker decompose the exercise into dependency-ready Lean leaves and map every cited theorem Formal assumptions all measurability, integrability, topology, and domain conditions needed by the cited route
Exercise 1.5book 42 / PDF 54	Basic properties of the Markov semigroup	Planned No exact local mapping yet	Planned	Exact blocker decompose the exercise into dependency-ready Lean leaves and map every cited theorem Formal assumptions all measurability, integrability, topology, and domain conditions needed by the cited route
Exercise 1.6book 42 / PDF 54	Functional inequalities and exponential decay	Planned No exact local mapping yet	Planned	Exact blocker decompose the exercise into dependency-ready Lean leaves and map every cited theorem Formal assumptions all measurability, integrability, topology, and domain conditions needed by the cited route
Exercise 1.7book 43 / PDF 55	Log-Sobolev implies Poincare	Planned No exact local mapping yet	Planned	Exact blocker decompose the exercise into dependency-ready Lean leaves and map every cited theorem Formal assumptions all measurability, integrability, topology, and domain conditions needed by the cited route
Exercise 1.8book 43 / PDF 55	Mixing of the Ornstein-Uhlenbeck process	Planned No exact local mapping yet	Planned	Exact blocker decompose the exercise into dependency-ready Lean leaves and map every cited theorem Formal assumptions all measurability, integrability, topology, and domain conditions needed by the cited route
Exercise 1.9book 43 / PDF 55	Optimal transport between Gaussians	Planned No exact local mapping yet	Planned	Exact blocker decompose the exercise into dependency-ready Lean leaves and map every cited theorem Formal assumptions all measurability, integrability, topology, and domain conditions needed by the cited route
Exercise 1.10book 43 / PDF 55	Optimal transport with other costs	Planned No exact local mapping yet	Planned	Exact blocker decompose the exercise into dependency-ready Lean leaves and map every cited theorem Formal assumptions all measurability, integrability, topology, and domain conditions needed by the cited route
Exercise 1.11book 44 / PDF 56	Dynamical formulations of optimal transport	Planned No exact local mapping yet	Planned	Exact blocker decompose the exercise into dependency-ready Lean leaves and map every cited theorem Formal assumptions all measurability, integrability, topology, and domain conditions needed by the cited route
Exercise 1.12book 45 / PDF 57	Wasserstein space has non-negative curvature	Planned No exact local mapping yet	Planned	Exact blocker decompose the exercise into dependency-ready Lean leaves and map every cited theorem Formal assumptions all measurability, integrability, topology, and domain conditions needed by the cited route
Exercise 1.13book 46 / PDF 58	Reconciling the SDE and Wasserstein perspectives	Planned No exact local mapping yet	Planned	Exact blocker decompose the exercise into dependency-ready Lean leaves and map every cited theorem Formal assumptions all measurability, integrability, topology, and domain conditions needed by the cited route
Exercise 1.14book 46 / PDF 58	Wasserstein calculus for f-divergences	Planned No exact local mapping yet	Planned	Exact blocker decompose the exercise into dependency-ready Lean leaves and map every cited theorem Formal assumptions all measurability, integrability, topology, and domain conditions needed by the cited route
Exercise 1.15book 46 / PDF 58	Smoothness along Wasserstein geodesics	Planned No exact local mapping yet	Planned	Exact blocker decompose the exercise into dependency-ready Lean leaves and map every cited theorem Formal assumptions all measurability, integrability, topology, and domain conditions needed by the cited route
Exercise 1.16book 46 / PDF 58	Otto-Villani theorem	Planned No exact local mapping yet	Planned	Exact blocker decompose the exercise into dependency-ready Lean leaves and map every cited theorem Formal assumptions all measurability, integrability, topology, and domain conditions needed by the cited route
Exercise 1.17book 47 / PDF 59	Contraction of the Langevin diffusion	Planned No exact local mapping yet	Planned	Exact blocker decompose the exercise into dependency-ready Lean leaves and map every cited theorem Formal assumptions all measurability, integrability, topology, and domain conditions needed by the cited route
Exercise 1.18book 47 / PDF 59	Sharp KL convergence	Planned No exact local mapping yet	Planned	Exact blocker decompose the exercise into dependency-ready Lean leaves and map every cited theorem Formal assumptions all measurability, integrability, topology, and domain conditions needed by the cited route
Exercise 1.19book 47 / PDF 59	Divergences at initialization	Planned No exact local mapping yet	Planned	Exact blocker decompose the exercise into dependency-ready Lean leaves and map every cited theorem Formal assumptions all measurability, integrability, topology, and domain conditions needed by the cited route
Exercise 1.20book 47 / PDF 59	First moment of an exponential distribution	Planned No exact local mapping yet	Planned	Exact blocker decompose the exercise into dependency-ready Lean leaves and map every cited theorem Formal assumptions all measurability, integrability, topology, and domain conditions needed by the cited route
Exercise 1.21book 47 / PDF 59	Sharpness of the initialization bounds	Planned No exact local mapping yet	Planned	Exact blocker decompose the exercise into dependency-ready Lean leaves and map every cited theorem Formal assumptions all measurability, integrability, topology, and domain conditions needed by the cited route

Chapter 1 Completion Matrix

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions

Formal assumptions