Exact source context
[
{
"id": "chewi-1-1-theorem-1-1-8",
"chapter": 1,
"section": "1.1",
"edition": "2026-08-09",
"book_page": 6,
"pdf_page": 18,
"page": "book 6 / PDF 18",
"source_kind": "Theorem 1.1.8",
"source_url": "https://chewisinho.github.io/main.pdf#page=18",
"wording_status": "faithful paraphrase",
"source_summary": "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.",
"mathematical_exposition": "For a progressive square-integrable integrand \\(\\eta\\), elementary adapted stochastic integrals extend by \\(L^2\\) completion to a continuous martingale \\(I\\). At every \\(t\\in[0,T]\\), \\(I_t\\) is the completed integral of \\(\\eta\\) restricted to \\((0,t)\\), and any other continuous adapted version with these fixed-time representatives is indistinguishable from \\(I\\).",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoIntegralProcess.chewi_theorem_1_1_8"
],
"source_assumptions": [
"a complete right-continuous filtered probability space",
"a Brownian motion relative to the filtration",
"a progressive globally square-integrable integrand"
],
"formal_assumptions": [
"SatisfiesUsualConditions filtration mu",
"IsBrownianMotionWithFiltration B filtration mu",
"ProgressiveL2Integrand filtration mu T",
"positive finite construction horizon"
],
"downstream_consumers": [
"display (1.1.9)",
"localized Ito integration",
"Ito formula and SDE arguments"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "constructed adapted continuous Ito martingale with all-time restriction compatibility, isometry, linearity interfaces, and uniqueness up to indistinguishability",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-ito-progressive-density",
"label": "Causal elementary density in progressive L2",
"declarations": [
"progressiveL2_elementary_dense"
],
"dependencies": [
"tendsto_laggedDyadicApprox_toLp_clipped",
"tendsto_clipped_toLp"
],
"priority": 100,
"route_status": "compiled"
},
{
"node_id": "chapter1-ito-terminal-completion",
"label": "Grid-independent terminal L2 completion",
"declarations": [
"itoIntegralTerminal_norm"
],
"dependencies": [
"norm_terminal_sub_eq_process_sub",
"tendsto_terminal_of_tendsto_elementary"
],
"priority": 100,
"route_status": "compiled"
},
{
"node_id": "chapter1-ito-continuous-martingale",
"label": "Continuous martingale limit",
"declarations": [
"itoIntegralProcess_martingale",
"itoIntegralProcess_continuous_ae"
],
"dependencies": [
"elementaryItoProcess_martingale",
"doobL2_continuous",
"uniformBadSet_null"
],
"priority": 100,
"route_status": "compiled"
},
{
"node_id": "chapter1-ito-fixed-time-uniqueness",
"label": "Fixed-time identification and indistinguishability",
"declarations": [
"itoIntegralProcess_at_eq_terminal",
"itoIntegralProcess_unique",
"chewi_theorem_1_1_8"
],
"dependencies": [
"tendsto_stopAtRightApprox_toLp",
"itoIntegralProcess_continuous_ae"
],
"priority": 100,
"route_status": "compiled"
}
],
"latex_statement": "I_t(\\eta)=\\int_0^t \\eta_s\\,dB_s,\\qquad \\mathbb E[I_t(\\eta)^2]=\\mathbb E\\!\\left[\\int_0^t \\eta_s^2\\,ds\\right]"
},
{
"id": "chewi-1-1-display-1-1-9",
"chapter": 1,
"section": "1.1",
"edition": "2026-08-09",
"book_page": 6,
"pdf_page": 18,
"page": "book 6 / PDF 18",
"source_kind": "Displayed identity (1.1.9)",
"source_url": "https://chewisinho.github.io/main.pdf#page=18",
"wording_status": "faithful paraphrase",
"source_summary": "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.",
"mathematical_exposition": "For \\(t\\in[0,T]\\), the second moment \\(\\mathbb E[I_t(\\eta)^2]\\) equals \\(\\mathbb E[\\int_0^t\\eta_s^2\\,ds]\\). ASTIS represents the right side by restricting \\(\\eta\\) to \\((0,t)\\); changing an endpoint does not change the integral because singleton times are null.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoIntegralProcess.chewi_display_1_1_9"
],
"source_assumptions": [
"a complete right-continuous filtered probability space",
"a Brownian motion relative to the filtration",
"a progressive globally square-integrable integrand",
"a deterministic time in the construction horizon"
],
"formal_assumptions": [
"SatisfiesUsualConditions filtration mu",
"IsBrownianMotionWithFiltration B filtration mu",
"ProgressiveL2Integrand filtration mu T",
"t <= T"
],
"downstream_consumers": [
"localized stochastic integration",
"Ito formula energy estimates",
"SDE stability bounds"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "all-time Ito isometry compiled using the exact restricted product-space L2 representative",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-ito-restriction-isometry",
"label": "Restricted terminal identification and norm isometry",
"declarations": [
"chewi_display_1_1_9"
],
"dependencies": [
"itoIntegralProcess_at_eq_terminal",
"itoIntegralTerminal_norm",
"norm_sq_toLp_eq_integral_sq"
],
"priority": 100,
"route_status": "compiled"
}
],
"latex_statement": "\\mathbb E[I_t(\\eta)^2]=\\mathbb E\\!\\left[\\int_0^t \\eta_s^2\\,ds\\right]"
},
{
"id": "chewi-1-1-display-1-1-5",
"chapter": 1,
"section": "1.1",
"edition": "2026-08-09",
"book_page": 5,
"pdf_page": 17,
"page": "book 5 / PDF 17",
"source_kind": "Displayed identity (1.1.5)",
"source_url": "https://chewisinho.github.io/main.pdf#page=17",
"wording_status": "faithful paraphrase",
"source_summary": "The expected square of an elementary stochastic integral expands to the sum of its diagonal increment terms because distinct adapted Brownian increments are orthogonal.",
"mathematical_exposition": "Write \\(I_T(\\eta)=\\sum_i H_i\\Delta B_i\\). Expanding the square produces diagonal and cross terms; adaptedness and Brownian increment orthogonality make every cross term vanish in expectation.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoIsometry.chewi_display_1_1_5"
],
"source_assumptions": [
"an elementary adapted process",
"a Brownian motion relative to the filtration",
"a finite terminal time"
],
"formal_assumptions": [
"ElementaryAdaptedProcess",
"IsBrownianMotionWithFiltration",
"MemLp two for weighted increments"
],
"downstream_consumers": [
"display (1.1.6)",
"Theorem 1.1.8",
"display (1.1.9)"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "finite elementary stochastic-integral square expansion compiled with probabilistic cross-term orthogonality",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-elementary-ito-orthogonality",
"label": "Orthogonal adapted weighted increments",
"declarations": [
"chewi_display_1_1_5"
],
"dependencies": [
"IsBrownianMotionWithFiltration",
"integral_weightedIncrement_mul_eq_zero",
"integral_finsetSum"
],
"priority": 100,
"route_status": "compiled"
}
],
"latex_statement": "\\mathbb E\\!\\left[\\left(\\sum_i H_i\\Delta B_i\\right)^2\\right]=\\sum_i \\mathbb E[(H_i\\Delta B_i)^2]"
},
{
"id": "chewi-1-1-display-1-1-6",
"chapter": 1,
"section": "1.1",
"edition": "2026-08-09",
"book_page": 5,
"pdf_page": 17,
"page": "book 5 / PDF 17",
"source_kind": "Displayed identity (1.1.6)",
"source_url": "https://chewisinho.github.io/main.pdf#page=17",
"wording_status": "faithful paraphrase",
"source_summary": "The second moment of the elementary Ito integral equals the expected time integral of the squared elementary integrand.",
"mathematical_exposition": "The diagonal expansion is \\(\\sum_i\\mathbb E[H_i^2]\\,((t_{i+1}\\wedge T)-(t_i\\wedge T))\\), exactly the probability-time \\(L^2\\) energy of \\(\\eta\\) on \\([0,T]\\).",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoIsometry.chewi_display_1_1_6"
],
"source_assumptions": [
"an elementary adapted process",
"a Brownian motion relative to the filtration",
"a finite terminal time"
],
"formal_assumptions": [
"IsBrownianMotionWithFiltration",
"TimeMeasure.upTo",
"processTimeMeasure",
"processL2Energy"
],
"downstream_consumers": [
"Theorem 1.1.8",
"display (1.1.9)",
"general Ito integral by L2 completion"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "elementary-process Ito isometry compiled in the repository's nonnegative product-space energy representation",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-elementary-ito-isometry",
"label": "Elementary Ito isometry",
"declarations": [
"chewi_display_1_1_6"
],
"dependencies": [
"chewi_display_1_1_5",
"integral_weightedIncrement_sq",
"processL2Energy_value",
"TimeMeasure.upTo_Ioc"
],
"priority": 100,
"route_status": "compiled"
}
],
"latex_statement": "\\mathbb E\\!\\left[\\left(\\int_0^T \\eta_s\\,dB_s\\right)^2\\right]=\\mathbb E\\!\\left[\\int_0^T \\eta_s^2\\,ds\\right]"
},
{
"id": "chewi-1-1-display-1-1-10",
"chapter": 1,
"section": "1.1",
"edition": "2026-08-09",
"book_page": 6,
"pdf_page": 18,
"page": "book 6 / PDF 18",
"source_kind": "Displayed identity (1.1.10)",
"source_url": "https://chewisinho.github.io/main.pdf#page=18",
"wording_status": "faithful paraphrase",
"source_summary": "Localization permits progressive integrands whose squared time integral is finite almost surely, without requiring its expectation to be finite.",
"mathematical_exposition": "For almost every sample path \\(\\omega\\), the quadratic energy \\(\\int_0^T\\eta_s(\\omega)^2\\,ds\\) is finite. This is weaker than assuming finite expected energy.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoIntegral.chewi_display_1_1_10"
],
"source_assumptions": [
"a real stochastic integrand",
"a finite terminal time",
"a probability measure"
],
"formal_assumptions": [
"TimeMeasure.upTo T",
"ENNReal lintegral",
"Filter.Eventually under mu"
],
"downstream_consumers": [
"Proposition 1.1.13",
"display (1.1.14)",
"Proposition 1.1.16"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact almost-sure local square-integrability condition compiled; stopping-time construction remains separate",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-local-square-integrability",
"label": "Almost-sure finite path energy",
"declarations": [
"chewi_display_1_1_10"
],
"dependencies": [
"TimeMeasure.upTo",
"lintegral",
"Eventually"
],
"priority": 100,
"route_status": "compiled"
}
],
"latex_statement": "\\int_0^T \\eta_s(\\omega)^2\\,ds<\\infty\\quad\\text{for a.e. }\\omega"
},
{
"id": "chewi-1-1-display-1-1-7",
"chapter": 1,
"section": "1.1",
"edition": "2026-08-09",
"book_page": 5,
"pdf_page": 17,
"page": "book 5 / PDF 17",
"source_kind": "Displayed identity (1.1.7)",
"source_url": "https://chewisinho.github.io/main.pdf#page=17",
"wording_status": "faithful paraphrase",
"source_summary": "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.",
"mathematical_exposition": "Tonelli identifies the product integral of eta squared under P tensor m restricted to [0,T] with the iterated expectation and time integral.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoIntegral.chewi_display_1_1_7"
],
"source_assumptions": [
"a probability measure",
"a finite terminal time",
"a jointly measurable squared process"
],
"formal_assumptions": [
"TimeMeasure.upTo T",
"AEMeasurable squared process on processTimeMeasure",
"ENNReal lintegrals"
],
"downstream_consumers": [
"Theorem 1.1.8",
"display (1.1.9)",
"Definition 1.1.12"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "product-space L2 energy and Tonelli identity compiled; Ito isometry and stochastic-integral completion remain separate routes",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-process-l2-energy",
"label": "Product-space process L2 energy",
"declarations": [
"chewi_display_1_1_7"
],
"dependencies": [
"TimeMeasure.upTo",
"Measure.prod",
"lintegral_prod"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-1-display-1-1-2",
"chapter": 1,
"section": "1.1",
"edition": "2026-08-09",
"book_page": 4,
"pdf_page": 16,
"page": "book 4 / PDF 16",
"source_kind": "Displayed identity (1.1.2)",
"source_url": "https://chewisinho.github.io/main.pdf#page=16",
"wording_status": "faithful paraphrase",
"source_summary": "An elementary adapted process is a finite sum of bounded left-endpoint measurable coefficients on half-open time intervals.",
"mathematical_exposition": "For a strict grid t_0 < ... < t_n, eta_t is the sum of H_i times the indicator of t in (t_i,t_{i+1}].",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoIntegral.chewi_display_1_1_2"
],
"source_assumptions": [
"a filtered measurable sample space",
"a finite strict time grid",
"bounded left-endpoint measurable coefficients"
],
"formal_assumptions": [
"Mathlib Filtration at NNReal time",
"StrictMono grid on Fin (n + 1)",
"StronglyMeasurable coefficients",
"pointwise coefficient bounds"
],
"downstream_consumers": [
"display (1.1.3)",
"elementary Ito isometry"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact finite elementary-process identity compiled with source regularity stored in the structure",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-elementary-adapted-process",
"label": "Elementary adapted process finite sum",
"declarations": [
"chewi_display_1_1_2"
],
"dependencies": [
"Filtration",
"StronglyMeasurable",
"StrictMono",
"Finset.sum"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-1-display-1-1-3",
"chapter": 1,
"section": "1.1",
"edition": "2026-08-09",
"book_page": 5,
"pdf_page": 17,
"page": "book 5 / PDF 17",
"source_kind": "Displayed identity (1.1.3)",
"source_url": "https://chewisinho.github.io/main.pdf#page=17",
"wording_status": "faithful paraphrase",
"source_summary": "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.",
"mathematical_exposition": "I_[0,T](eta) is the sum of H_i times B_(t_(i+1) min T) minus B_(t_i min T).",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoIntegral.chewi_display_1_1_3"
],
"source_assumptions": [
"an elementary adapted process",
"a scalar Brownian path",
"a nonnegative terminal time"
],
"formal_assumptions": [
"the display (1.1.2) elementary-process structure",
"finite Fin-indexed summation",
"NNReal stopping by minimum"
],
"downstream_consumers": [
"display (1.1.5)",
"display (1.1.6)",
"Theorem 1.1.8"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact finite Brownian-increment definition compiled; isometry and L2 completion remain separate routes",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-elementary-ito-integral",
"label": "Elementary Ito integral finite sum",
"declarations": [
"chewi_display_1_1_3"
],
"dependencies": [
"chewi_display_1_1_2",
"Finset.sum",
"min"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-3-definition-1-3-16",
"chapter": 1,
"section": "1.3",
"edition": "2026-08-09",
"book_page": 26,
"pdf_page": 38,
"page": "book 26 / PDF 38",
"source_kind": "Definition 1.3.16",
"source_url": "https://chewisinho.github.io/main.pdf#page=38",
"wording_status": "faithful paraphrase",
"source_summary": "Informally, a curve is absolutely continuous when its finite metric derivative exists almost everywhere.",
"mathematical_exposition": "The metric derivative is the punctured-time limit of distance(curve(s),curve(t))/abs(s-t).",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.Geometry.MetricCurve.IsAbsolutelyContinuousMetricCurve"
],
"source_assumptions": [
"a curve in Wasserstein P2ac",
"the informal metric derivative criterion"
],
"formal_assumptions": [
"a PseudoMetricSpace",
"a real-time curve",
"a.e. existence of HasMetricDerivativeAt"
],
"downstream_consumers": [
"continuity equation",
"kinetic action",
"Wasserstein geodesics"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "the source's informal predicate is compiled; stronger AGS absolute continuity remains separate",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-metric-curve-absolute-continuity",
"label": "Almost-everywhere finite metric derivative",
"declarations": [
"IsAbsolutelyContinuousMetricCurve"
],
"dependencies": [
"HasMetricDerivativeAt",
"Tendsto",
"MeasureTheory.ae"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-3-definition-1-3-26",
"chapter": 1,
"section": "1.3",
"edition": "2026-08-09",
"book_page": 31,
"pdf_page": 43,
"page": "book 31 / PDF 43",
"source_kind": "Definition 1.3.26",
"source_url": "https://chewisinho.github.io/main.pdf#page=43",
"wording_status": "faithful paraphrase",
"source_summary": "A functional is alpha-geodesically convex when its value along each geodesic lies below endpoint interpolation minus the alpha quadratic distance correction.",
"mathematical_exposition": "For t in [0,1], F(p_t) is at most (1-t)F(p_0)+tF(p_1)-alpha t(1-t)d(p_0,p_1)^2/2.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.Geometry.GeodesicConvexity.IsAlphaGeodesicallyConvex"
],
"source_assumptions": [
"a Riemannian manifold",
"smooth functional",
"all geodesics"
],
"formal_assumptions": [
"a MetricSpace",
"an explicit geodesic predicate",
"real-valued functional"
],
"downstream_consumers": [
"Wasserstein KL convexity",
"gradient-flow convergence"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "source condition 1 compiled exactly; equivalence to gradient and Hessian forms remains separate",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-alpha-geodesic-convexity",
"label": "Alpha-geodesic convexity predicate",
"declarations": [
"IsAlphaGeodesicallyConvex"
],
"dependencies": [
"MetricSpace.dist",
"Set.Icc"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-4-display-1-4-7",
"chapter": 1,
"section": "1.4",
"edition": "2026-08-09",
"book_page": 34,
"pdf_page": 46,
"page": "book 34 / PDF 46",
"source_kind": "Displayed identity (1.4.7)",
"source_url": "https://chewisinho.github.io/main.pdf#page=46",
"wording_status": "faithful paraphrase",
"source_summary": "Geodesic alpha-convexity implies the first-order lower bound at the initial endpoint, with the derivative pairing and alpha times squared distance correction.",
"mathematical_exposition": "Apply the chord inequality at a positive interpolation time t, subtract the initial value, and divide by t. As t decreases to zero, the secant slope converges to the derivative along the geodesic and the correction converges to alpha times the squared endpoint distance divided by two.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.Geometry.GeodesicConvexity.firstOrder_geodesicConvexity"
],
"source_assumptions": [
"an alpha-geodesically convex smooth functional",
"a constant-speed geodesic from mu to nu",
"the Riemannian derivative-gradient pairing"
],
"formal_assumptions": [
"the compiled endpoint chord inequality on every selected geodesic",
"HasDerivAt of the functional along the selected path at zero"
],
"downstream_consumers": [
"gradient-flow contraction",
"Polyak-Lojasiewicz and quadratic-growth consequences"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact first-order convexity limit compiled; the concrete Wasserstein gradient-pairing identification remains an explicit upstream geometric interface",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-first-order-geodesic-convexity",
"label": "Chord alpha-convexity implies the first-order inequality",
"declarations": [
"firstOrder_geodesicConvexity"
],
"dependencies": [
"IsAlphaGeodesicallyConvex",
"HasDerivAt.tendsto_slope",
"le_of_tendsto_of_tendsto"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-2-theorem-1-2-14",
"chapter": 1,
"section": "1.2",
"edition": "2026-08-09",
"book_page": 14,
"pdf_page": 26,
"page": "book 14 / PDF 26",
"source_kind": "Theorem 1.2.14",
"source_url": "https://chewisinho.github.io/main.pdf#page=26",
"wording_status": "faithful paraphrase",
"source_summary": "For a stationary reversible generator, the two negative-generator pairings equal each other and the integrated carre du champ.",
"mathematical_exposition": "Integrating the definition of Gamma removes the L(fg) term by stationarity and identifies the remaining two terms by generator symmetry.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp.fundamental_integration_by_parts"
],
"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"
],
"downstream_consumers": [
"negative generator",
"Poincare inequality",
"Langevin Dirichlet form"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "source integral identity compiled from explicit stationarity and symmetry premises",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-fundamental-generator-ibp",
"label": "Fundamental generator integration by parts",
"declarations": [
"fundamental_integration_by_parts"
],
"dependencies": [
"carreDuChamp",
"dirichletForm",
"integral_sub",
"integral_const_mul"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-2-corollary-1-2-15",
"chapter": 1,
"section": "1.2",
"edition": "2026-08-09",
"book_page": 14,
"pdf_page": 26,
"page": "book 14 / PDF 26",
"source_kind": "Corollary 1.2.15",
"source_url": "https://chewisinho.github.io/main.pdf#page=26",
"wording_status": "faithful paraphrase",
"source_summary": "The negative generator of a reversible Markov semigroup has a nonnegative quadratic form.",
"mathematical_exposition": "The quadratic pairing integral f(-L)f equals integral Gamma(f,f), which is nonnegative.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp.negativeGenerator_quadratic_nonneg"
],
"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"
],
"downstream_consumers": [
"spectral gap",
"Poincare inequality"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "source quadratic-form conclusion compiled; Lemma 1.2.13 supplies Gamma positivity separately",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-negative-generator-nonnegative",
"label": "Negative generator quadratic nonnegativity",
"declarations": [
"negativeGenerator_quadratic_nonneg"
],
"dependencies": [
"fundamental_integration_by_parts",
"integral_nonneg_of_ae"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-3-definition-1-3-6",
"chapter": 1,
"section": "1.3",
"edition": "2026-08-09",
"book_page": 21,
"pdf_page": 33,
"page": "book 21 / PDF 33",
"source_kind": "Definition 1.3.6",
"source_url": "https://chewisinho.github.io/main.pdf#page=33",
"wording_status": "faithful paraphrase",
"source_summary": "The dual optimal transport value is the supremum of the two potential integrals over feasible integrable potential pairs.",
"mathematical_exposition": "Dual feasibility requires f(x)+g(y) to be at most the transport cost for mu-times-nu almost every pair.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.Measure.KantorovichDual.dualTransportValue"
],
"source_assumptions": [
"finite-second-moment probability marginals",
"quadratic cost"
],
"formal_assumptions": [
"measurable spaces and measures",
"integrable real potentials",
"product-a.e. dual constraint"
],
"downstream_consumers": [
"Kantorovich strong duality",
"optimal maps"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact dual optimization definition compiled; source-setting boundedness remains a theorem",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-kantorovich-dual-definition",
"label": "Kantorovich dual value",
"declarations": [
"dualTransportValue"
],
"dependencies": [
"DualFeasible",
"Integrable",
"Measure.prod",
"sSup"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-3-display-1-3-7",
"chapter": 1,
"section": "1.3",
"edition": "2026-08-09",
"book_page": 21,
"pdf_page": 33,
"page": "book 21 / PDF 33",
"source_kind": "Displayed identity (1.3.7)",
"source_url": "https://chewisinho.github.io/main.pdf#page=33",
"wording_status": "faithful paraphrase",
"source_summary": "The dual value is the supremum of integral f dmu plus integral g dnu over dual-feasible potentials.",
"mathematical_exposition": "This display expands the optimization objective and feasible set used by Definition 1.3.6.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.Measure.KantorovichDual.dualTransportValue_eq_sSup"
],
"source_assumptions": [
"Definition 1.3.6"
],
"formal_assumptions": [
"dualTransportValue and DualFeasible"
],
"downstream_consumers": [
"weak duality",
"strong duality"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact source display compiled by definitional equality",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-kantorovich-dual-display",
"label": "Dual feasible-potential supremum",
"declarations": [
"dualTransportValue_eq_sSup"
],
"dependencies": [
"dualTransportValue"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-2-definition-1-2-19",
"chapter": 1,
"section": "1.2",
"edition": "2026-08-09",
"book_page": 16,
"pdf_page": 28,
"page": "book 16 / PDF 28",
"source_kind": "Definition 1.2.19",
"source_url": "https://chewisinho.github.io/main.pdf#page=28",
"wording_status": "faithful paraphrase",
"source_summary": "A Markov process satisfies a Poincare inequality when variance is bounded by a constant times its generator Dirichlet energy.",
"mathematical_exposition": "For every observable in the generator form domain, Var_mu(f) is at most C times integral f(-L)f dmu.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Generator.SatisfiesPoincare"
],
"source_assumptions": [
"a stationary reversible Markov generator",
"observables in its form domain"
],
"formal_assumptions": [
"a probability measure",
"a real generator action",
"PoincareAdmissible finite integrals"
],
"downstream_consumers": [
"variance decay",
"chi-squared decay",
"spectral gap"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact source predicate compiled; concrete semigroup instantiation and decay remain separate",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-generator-poincare-definition",
"label": "Generator Poincare predicate",
"declarations": [
"SatisfiesPoincare"
],
"dependencies": [
"variance",
"dirichletForm",
"PoincareAdmissible"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-2-definition-1-2-25",
"chapter": 1,
"section": "1.2",
"edition": "2026-08-09",
"book_page": 18,
"pdf_page": 30,
"page": "book 18 / PDF 30",
"source_kind": "Definition 1.2.25",
"source_url": "https://chewisinho.github.io/main.pdf#page=30",
"wording_status": "faithful paraphrase",
"source_summary": "A Markov process satisfies an LSI when density entropy is bounded by C/2 times the Dirichlet form of the density and its logarithm.",
"mathematical_exposition": "For every density rho with respect to mu, KL(rho mu || mu) is at most (C/2) E(rho,log rho).",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Generator.SatisfiesLogSobolev"
],
"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"
],
"downstream_consumers": [
"KL decay",
"Fisher-information specialization"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact source predicate compiled; entropy dissipation and KL decay remain separate",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-generator-lsi-definition",
"label": "Generator log-Sobolev predicate",
"declarations": [
"SatisfiesLogSobolev"
],
"dependencies": [
"densityEntropy",
"dirichletForm",
"LogSobolevAdmissible"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-1-definition-1-1-1",
"chapter": 1,
"section": "1.1",
"edition": "2026-08-09",
"book_page": 4,
"pdf_page": 16,
"page": "book 4 / PDF 16",
"source_kind": "Definition 1.1.1",
"source_url": "https://chewisinho.github.io/main.pdf#page=16",
"wording_status": "faithful paraphrase",
"source_summary": "Standard Brownian motion starts at zero, has independent centered Gaussian increments with covariance proportional to elapsed time, and has almost surely continuous paths.",
"mathematical_exposition": "For every s<t, B_t-B_s is centered Gaussian with covariance (t-s)I; increments over disjoint intervals are jointly independent.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianMotion.IsStandardBrownianMotion"
],
"source_assumptions": [
"a probability space",
"a finite-dimensional Euclidean state space"
],
"formal_assumptions": [
"Borel measurable real Hilbert state space",
"HasLaw for every StrongDual projection",
"iIndepFun on disjoint intervals",
"a.e. Continuous paths"
],
"downstream_consumers": [
"Ito integration",
"Ito processes",
"Langevin SDE"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact source predicate compiled; existence of a process satisfying it is not claimed",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-standard-brownian-definition",
"label": "Standard Brownian motion predicate",
"declarations": [
"IsStandardBrownianMotion"
],
"dependencies": [
"HasLaw",
"gaussianReal",
"iIndepFun",
"Continuous"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-1-definition-1-1-12",
"chapter": 1,
"section": "1.1",
"edition": "2026-08-09",
"book_page": 6,
"pdf_page": 18,
"page": "book 6 / PDF 18",
"source_kind": "Definition 1.1.12",
"source_url": "https://chewisinho.github.io/main.pdf#page=18",
"wording_status": "faithful paraphrase",
"source_summary": "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.",
"mathematical_exposition": "Each stop makes the progressive integrand square-integrable on the finite time interval; monotone stops then exhaust that interval almost surely.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Localization.IsLocalizingSequence"
],
"source_assumptions": [
"a progressive process on a filtered probability space",
"a finite terminal time"
],
"formal_assumptions": [
"Mathlib ProgMeasurable",
"Mathlib IsStoppingTime",
"nonnegative-time Lebesgue measure",
"a.e. filter limit"
],
"downstream_consumers": [
"localized Ito integral",
"local martingales"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact source predicate compiled; canonical hitting-time construction remains Proposition 1.1.13",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-localizing-sequence-definition",
"label": "Localizing sequence predicate",
"declarations": [
"IsLocalizingSequence"
],
"dependencies": [
"ProgMeasurable",
"IsStoppingTime",
"lintegral",
"Tendsto"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-1-definition-1-1-15",
"chapter": 1,
"section": "1.1",
"edition": "2026-08-09",
"book_page": 7,
"pdf_page": 19,
"page": "book 7 / PDF 19",
"source_kind": "Definition 1.1.15",
"source_url": "https://chewisinho.github.io/main.pdf#page=19",
"wording_status": "faithful paraphrase",
"source_summary": "A local martingale is adapted and admits increasing stopping times tending almost surely to infinity for which every centered stopped process is a martingale.",
"mathematical_exposition": "Localization replaces global integrability by ordinary martingale behavior before each stop.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Localization.IsLocalMartingale"
],
"source_assumptions": [
"a filtered probability space",
"a real adapted process"
],
"formal_assumptions": [
"Mathlib Adapted",
"Mathlib stoppedProcess",
"Mathlib Martingale",
"a.e. atTop convergence"
],
"downstream_consumers": [
"localized Ito integral theorem",
"Ito processes"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact source predicate compiled; continuity and Ito-integral localization remain theorem routes",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-local-martingale-definition",
"label": "Local martingale predicate",
"declarations": [
"IsLocalMartingale"
],
"dependencies": [
"Adapted",
"IsStoppingTime",
"stoppedProcess",
"Martingale"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-2-definition-1-2-1",
"chapter": 1,
"section": "1.2",
"edition": "2026-08-09",
"book_page": 10,
"pdf_page": 22,
"page": "book 10 / PDF 22",
"source_kind": "Definition 1.2.1",
"source_url": "https://chewisinho.github.io/main.pdf#page=22",
"wording_status": "faithful paraphrase",
"source_summary": "The Markov operator sends an observable to its conditional expectation after elapsed time t, given the initial state.",
"mathematical_exposition": "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).",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.MarkovSemigroup.markovOperator"
],
"source_assumptions": [
"a time-homogeneous Markov process and its conditional transition laws"
],
"formal_assumptions": [
"a transition-kernel contract",
"measurable ENNReal observables"
],
"downstream_consumers": [
"semigroup property",
"Feller operators",
"generator theory"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "source conditional-law operator compiled at the transition-kernel level",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-markov-operator-definition",
"label": "Markov conditional-expectation operator",
"declarations": [
"markovOperator"
],
"dependencies": [
"Kernel",
"lintegral_kernel"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-3-definition-1-3-4",
"chapter": 1,
"section": "1.3",
"edition": "2026-08-09",
"book_page": 20,
"pdf_page": 32,
"page": "book 20 / PDF 32",
"source_kind": "Definition 1.3.4",
"source_url": "https://chewisinho.github.io/main.pdf#page=32",
"wording_status": "faithful paraphrase",
"source_summary": "The 2-Wasserstein distance is the positive square root of the optimal quadratic coupling cost.",
"mathematical_exposition": "W2(mu,nu) is the square root of the infimum over couplings of the integral of the squared Euclidean distance.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSpace.wassersteinDistance"
],
"source_assumptions": [
"probability measures on Euclidean space",
"quadratic transport cost"
],
"formal_assumptions": [
"measurable normed additive state space",
"compiled Kantorovich transportCost"
],
"downstream_consumers": [
"Wasserstein metric",
"geodesics",
"Langevin coupling"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact extended-real W2 value definition compiled; metric properties remain separate",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-wasserstein-distance-definition",
"label": "2-Wasserstein value",
"declarations": [
"wassersteinDistance"
],
"dependencies": [
"transportCost",
"quadraticCost",
"ENNReal.rpow"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-3-display-1-3-5",
"chapter": 1,
"section": "1.3",
"edition": "2026-08-09",
"book_page": 20,
"pdf_page": 32,
"page": "book 20 / PDF 32",
"source_kind": "Displayed identity (1.3.5)",
"source_url": "https://chewisinho.github.io/main.pdf#page=32",
"wording_status": "faithful paraphrase",
"source_summary": "The square of W2 equals the infimum of integrated squared distance over all couplings.",
"mathematical_exposition": "W2(mu,nu)^2 equals the quadratic Kantorovich transport cost.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSpace.wassersteinDistance_sq"
],
"source_assumptions": [
"the W2 and quadratic cost of Definition 1.3.4"
],
"formal_assumptions": [
"ENNReal rpow algebra"
],
"downstream_consumers": [
"Wasserstein estimates",
"metric-space route"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "source square identity compiled without an attainment assumption",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-wasserstein-square-display",
"label": "W2 squared coupling infimum",
"declarations": [
"wassersteinDistance_sq"
],
"dependencies": [
"ENNReal.rpow_two",
"ENNReal.rpow_mul"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-2-semigroup",
"chapter": 1,
"section": "1.2",
"edition": "2026-08-09",
"book_page": 10,
"pdf_page": 22,
"page": "book 10 / PDF 22",
"source_kind": "Supporting concrete Markov/Feller realization route",
"source_url": "https://chewisinho.github.io/main.pdf#page=22",
"wording_status": "faithful paraphrase",
"source_summary": "A Markov semigroup records how the law or observables evolve with time.",
"mathematical_exposition": "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.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.WeakGenerator.IntegratedSemigroupGeneratorContract",
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.WeakGenerator.isInvariantOn_of_integral_generator_eq_zero",
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.MarkovSemigroup.chewi_lemma_1_2_2",
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.MarkovSemigroup.markovOperator_const",
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.MarkovSemigroup.markovOperator_apply_mono",
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerSemigroup.norm_fellerOperator_apply_le",
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerSemigroup.fellerOperator_add",
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerSemigroup.continuousLinearSemigroupOfFeller",
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGeneratorDomain.StronglyContinuousSemigroup.tendsto_op_add"
],
"source_assumptions": [
"Markov evolution",
"time-homogeneous composition"
],
"formal_assumptions": [
"measurable state space",
"specified operator domain",
"chosen continuity topology"
],
"downstream_consumers": [
"generator domain",
"stationarity",
"mixing estimates"
],
"status": "partial",
"route_status": "partial",
"local_status": "compiled",
"semantic_status": "compiled transition-kernel algebra, Feller kernel-to-continuous-linear-operator bridge, and propagation of assumed strong continuity from zero to right-shifted abstract orbits; concrete diffusion kernels and strong continuity on a justified observable space remain open",
"remaining_obligations": [
"construct transition kernels from the intended concrete Markov or Langevin process",
"prove the Feller mapping property for the concrete process",
"prove strong continuity in time on the selected observable space"
],
"proof_leaves": [
{
"node_id": "chapter1_transition_kernel_semigroup",
"label": "Transition-kernel Markov semigroup laws",
"declarations": [
"TransitionKernelContract",
"markovOperator_zero",
"markovOperator_comp",
"markovOperator_comm",
"chewi_lemma_1_2_2"
],
"dependencies": [
"Kernel.lintegral_id'",
"Kernel.lintegral_comp"
],
"priority": 100,
"route_status": "partial"
},
{
"node_id": "chapter1_feller_continuous_linear_semigroup",
"label": "Feller kernels as contraction continuous-linear semigroup",
"declarations": [
"FellerTransitionKernelContract",
"fellerOperator",
"norm_fellerOperator_apply_le",
"fellerOperator_zero",
"fellerOperator_add",
"continuousLinearSemigroupOfFeller"
],
"dependencies": [
"Kernel.integral_comp",
"norm_integral_le_of_norm_le_const"
],
"priority": 95,
"route_status": "partial"
},
{
"node_id": "chapter1_abstract_strong_continuity",
"label": "Strong continuity at zero propagates along abstract semigroup orbits",
"declarations": [
"StronglyContinuousSemigroup",
"StronglyContinuousSemigroup.tendsto_op_add"
],
"dependencies": [
"ContinuousLinearSemigroup.op_add_apply",
"ContinuousLinearMap.continuous",
"Tendsto.comp"
],
"priority": 93,
"route_status": "partial"
}
]
},
{
"id": "chewi-1-2-lemma-1-2-2",
"chapter": 1,
"section": "1.2",
"edition": "2026-08-09",
"book_page": 10,
"pdf_page": 22,
"page": "book 10 / PDF 22",
"source_kind": "Lemma 1.2.2",
"source_url": "https://chewisinho.github.io/main.pdf#page=22",
"wording_status": "faithful paraphrase",
"source_summary": "Identity and Chapman-Kolmogorov transition-kernel laws induce the zero-time, composition, and commutation laws of Markov operators.",
"mathematical_exposition": "For 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.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.MarkovSemigroup.chewi_lemma_1_2_2"
],
"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"
],
"downstream_consumers": [
"Feller operator semigroup",
"infinitesimal generator",
"Kolmogorov equations"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "source semigroup law compiled from kernel integration",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-semigroup-property",
"label": "Markov semigroup property",
"declarations": [
"chewi_lemma_1_2_2"
],
"dependencies": [
"Kernel.lintegral_id'",
"Kernel.lintegral_comp",
"TransitionKernelContract"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-2-definition-1-2-3",
"chapter": 1,
"section": "1.2",
"edition": "2026-08-09",
"book_page": 11,
"pdf_page": 23,
"page": "book 11 / PDF 23",
"source_kind": "Definition 1.2.3",
"source_url": "https://chewisinho.github.io/main.pdf#page=23",
"wording_status": "faithful paraphrase",
"source_summary": "The infinitesimal generator is the right derivative at zero of the semigroup orbit on its convergence domain.",
"mathematical_exposition": "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.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator.HasRightGeneratorAt"
],
"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)"
],
"downstream_consumers": [
"generator domain",
"Kolmogorov backward equation",
"concrete Langevin generator identification"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact right-generator definition compiled in an explicit norm topology",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-generator-definition",
"label": "Norm-topology right generator",
"declarations": [
"HasRightGeneratorAt"
],
"dependencies": [
"rightDifferenceQuotient",
"Tendsto",
"ContinuousLinearSemigroup"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-2-proposition-1-2-5",
"chapter": 1,
"section": "1.2",
"edition": "2026-08-09",
"book_page": 12,
"pdf_page": 24,
"page": "book 12 / PDF 24",
"source_kind": "Proposition 1.2.5",
"source_url": "https://chewisinho.github.io/main.pdf#page=24",
"wording_status": "faithful paraphrase",
"source_summary": "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.",
"mathematical_exposition": "For 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.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator.kolmogorov_backward_right"
],
"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"
],
"downstream_consumers": [
"semigroup energy dissipation",
"Poincare and log-Sobolev decay",
"concrete Langevin backward equation"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "source backward equation compiled as a one-sided norm-limit theorem on the explicit generator domain",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-kolmogorov-backward",
"label": "Kolmogorov backward right derivative",
"declarations": [
"kolmogorov_backward_right"
],
"dependencies": [
"HasRightGeneratorAt.map",
"rightOrbitDifferenceQuotient_eq"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-2-generator",
"chapter": 1,
"section": "1.2",
"edition": "2026-08-09",
"book_page": 11,
"pdf_page": 23,
"page": "book 11 / PDF 23",
"source_kind": "Supporting generator and concrete-domain route",
"source_url": "https://chewisinho.github.io/main.pdf#page=23",
"wording_status": "faithful paraphrase",
"source_summary": "The generator is the derivative at time zero of the Markov semigroup.",
"mathematical_exposition": "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.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.WeakGenerator.weakGeneratorFromSampleDerivative",
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerSemigroup.continuousLinearSemigroupOfFeller",
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator.generatorDomain_map",
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator.kolmogorov_backward_right",
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGeneratorDomain.hasRightGeneratorAt_unique",
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGeneratorDomain.generatorDomainSubmodule",
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGeneratorDomain.rightGenerator",
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGeneratorDomain.rightGenerator_map",
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGeneratorDomain.kolmogorov_backward_right_generator"
],
"source_assumptions": [
"existence of the derivative of the semigroup"
],
"formal_assumptions": [
"explicit difference-quotient convergence",
"explicit observable and scalar field"
],
"downstream_consumers": [
"generator/semigroup domain packet",
"invariant Gibbs law"
],
"status": "partial",
"route_status": "partial",
"local_status": "compiled",
"semantic_status": "compiled norm-topology right-generator domain, uniqueness and linearity, bundled generator, domain invariance, semigroup commutation, and right backward equation; closedness and concrete differential-generator identification remain open",
"remaining_obligations": [
"identify the closed semigroup generator with the differential Langevin expression on a concrete core",
"prove the core/domain closure theorem for the concrete process",
"derive the concrete forward equation and connect it to Gibbs invariance"
],
"proof_leaves": [
{
"node_id": "chapter1_right_generator_domain",
"label": "Right generator domain and backward equation",
"declarations": [
"ContinuousLinearSemigroup",
"HasRightGeneratorAt",
"generatorDomain",
"generatorDomain_map",
"kolmogorov_backward_right",
"hasRightGeneratorAt_unique",
"generatorDomainSubmodule",
"rightGenerator",
"rightGenerator_map",
"kolmogorov_backward_right_generator"
],
"dependencies": [
"continuousLinearSemigroupOfFeller",
"ContinuousLinearMap.continuous",
"Tendsto.comp"
],
"priority": 90,
"route_status": "partial"
}
]
},
{
"id": "chewi-1-1-definition-1-1-4",
"chapter": 1,
"section": "1.1",
"edition": "2026-08-09",
"book_page": 5,
"pdf_page": 17,
"page": "book 5 / PDF 17",
"source_kind": "Definition 1.1.4",
"source_url": "https://chewisinho.github.io/main.pdf#page=17",
"wording_status": "faithful paraphrase",
"source_summary": "A martingale is an adapted integrable process whose conditional expectation at an earlier time equals its earlier value.",
"mathematical_exposition": "For s <= t, E[M_t | F_s] = M_s almost everywhere, and M_t is measurable with respect to F_t. Mathlib's predicate derives integrability from the fixed-point conditional-expectation law.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Martingale.IsChewiMartingale"
],
"source_assumptions": [
"a filtered probability space",
"an adapted integrable real process"
],
"formal_assumptions": [
"a Measure and Filtration indexed by NNReal",
"Mathlib StronglyAdapted process measurability",
"conditional expectation equality almost everywhere for s <= t"
],
"downstream_consumers": [
"Ito integral construction",
"local martingales",
"martingale increment orthogonality"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact source martingale predicate compiled through Mathlib conditional expectation",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-martingale-definition",
"label": "Continuous-time real martingale",
"declarations": [
"IsChewiMartingale"
],
"dependencies": [
"MeasureTheory.Martingale",
"MeasureTheory.Filtration",
"condExp"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-1-definition-1-1-11",
"chapter": 1,
"section": "1.1",
"edition": "2026-08-09",
"book_page": 6,
"pdf_page": 18,
"page": "book 6 / PDF 18",
"source_kind": "Definition 1.1.11",
"source_url": "https://chewisinho.github.io/main.pdf#page=18",
"wording_status": "faithful paraphrase",
"source_summary": "A stopping time is a random time whose occurrence by time t is measurable using the information available at time t.",
"mathematical_exposition": "For every nonnegative t, the event {omega | tau(omega) <= t} belongs to the filtration sigma-algebra F_t. Allowing tau = infinity represents paths that never stop.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.StoppingTime.IsChewiStoppingTime"
],
"source_assumptions": [
"a filtered measurable sample space",
"a nonnegative random time"
],
"formal_assumptions": [
"a Mathlib Filtration indexed by NNReal",
"tau maps into WithTop NNReal",
"each event tau <= t is measurable in the filtration at t"
],
"downstream_consumers": [
"localizing sequences",
"stopped stochastic integrals",
"local martingales"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact source predicate compiled through Mathlib's stopping-time API",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-stopping-time-definition",
"label": "Continuous-time stopping time",
"declarations": [
"IsChewiStoppingTime"
],
"dependencies": [
"MeasureTheory.Filtration",
"MeasureTheory.IsStoppingTime"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-2-definition-1-2-10",
"chapter": 1,
"section": "1.2",
"edition": "2026-08-09",
"book_page": 13,
"pdf_page": 25,
"page": "book 13 / PDF 25",
"source_kind": "Definition 1.2.10",
"source_url": "https://chewisinho.github.io/main.pdf#page=25",
"wording_status": "faithful paraphrase",
"source_summary": "A Markov semigroup is reversible when every time operator is symmetric in the L2 inner product of its stationary law.",
"mathematical_exposition": "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.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Reversibility.IsReversible"
],
"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"
],
"downstream_consumers": [
"generator symmetry",
"fundamental integration-by-parts identity",
"spectral-gap analysis"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact Hilbert-space source predicate compiled; concrete L2(pi) realization and Langevin reversibility remain separate routes",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-reversibility-definition",
"label": "Reversible semigroup predicate",
"declarations": [
"IsReversible"
],
"dependencies": [
"ContinuousLinearSemigroup",
"InnerProductSpace"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-2-display-1-2-11",
"chapter": 1,
"section": "1.2",
"edition": "2026-08-09",
"book_page": 13,
"pdf_page": 25,
"page": "book 13 / PDF 25",
"source_kind": "Displayed identity (1.2.11)",
"source_url": "https://chewisinho.github.io/main.pdf#page=25",
"wording_status": "faithful paraphrase",
"source_summary": "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.",
"mathematical_exposition": "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).",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerSemigroup.sq_fellerOperator_apply_le"
],
"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"
],
"downstream_consumers": [
"carre-du-champ non-negativity",
"Markov variance contraction"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact source Jensen display compiled for the kernel-induced Feller operator; concrete diffusion construction remains separate",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-markov-jensen-square",
"label": "Probability-kernel Jensen inequality for the square",
"declarations": [
"sq_fellerOperator_apply_le"
],
"dependencies": [
"FellerTransitionKernelContract",
"ConvexOn.map_integral_le",
"Even.convexOn_pow"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-2-definition-1-2-12",
"chapter": 1,
"section": "1.2",
"edition": "2026-08-09",
"book_page": 14,
"pdf_page": 26,
"page": "book 14 / PDF 26",
"source_kind": "Definition 1.2.12",
"source_url": "https://chewisinho.github.io/main.pdf#page=26",
"wording_status": "faithful paraphrase",
"source_summary": "The carre du champ is the bilinear defect between applying the generator after multiplication and multiplying after applying the generator.",
"mathematical_exposition": "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.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp.carreDuChamp"
],
"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"
],
"downstream_consumers": [
"carre-du-champ non-negativity",
"reversible integration by parts",
"iterated carre du champ"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact source definition compiled; positivity and concrete diffusion identification remain separate source items",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-carre-du-champ-definition",
"label": "Carre du champ definition",
"declarations": [
"carreDuChamp"
],
"dependencies": [
"LinearMap",
"pointwise multiplication"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-2-lemma-1-2-13",
"chapter": 1,
"section": "1.2",
"edition": "2026-08-09",
"book_page": 14,
"pdf_page": 26,
"page": "book 14 / PDF 26",
"source_kind": "Lemma 1.2.13",
"source_url": "https://chewisinho.github.io/main.pdf#page=26",
"wording_status": "faithful paraphrase",
"source_summary": "The carre du champ of a Markov generator is pointwise nonnegative on the diagonal.",
"mathematical_exposition": "Jensen'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.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp.carreDuChamp_nonneg_of_markov_jensen_rightGenerator"
],
"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"
],
"downstream_consumers": [
"non-negativity of the reversible generator",
"Dirichlet-form and functional-inequality arguments"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact Jensen-to-right-generator proof compiled; concrete semigroup construction and domain membership remain separate routes",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-carre-du-champ-nonnegative",
"label": "Markov Jensen gap converges to Gamma",
"declarations": [
"carreDuChamp_nonneg_of_markov_jensen_rightGenerator"
],
"dependencies": [
"carreDuChamp",
"Tendsto",
"isClosed_Ici"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-2-example-1-2-17",
"chapter": 1,
"section": "1.2",
"edition": "2026-08-09",
"book_page": 15,
"pdf_page": 27,
"page": "book 15 / PDF 27",
"source_kind": "Example 1.2.17",
"source_url": "https://chewisinho.github.io/main.pdf#page=27",
"wording_status": "faithful paraphrase",
"source_summary": "For the Langevin differential operator, the carre du champ is the gradient inner product, and on the diagonal it is the squared gradient norm.",
"mathematical_exposition": "The 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.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LangevinCarreDuChamp.langevinCarreDuChamp_eq_inner"
],
"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"
],
"downstream_consumers": [
"Langevin Dirichlet form",
"Poincare and log-Sobolev specializations",
"Bakry-Emery calculations"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact pointwise Langevin carre-du-champ calculation compiled; closed generator and semigroup realization remain separate source routes",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-langevin-carre-du-champ",
"label": "Langevin Gamma equals gradient inner product",
"declarations": [
"langevinCarreDuChamp_eq_inner"
],
"dependencies": [
"laplacian_mul",
"gradient_mul",
"LangevinGenerator.operator"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-2-definition-1-2-28",
"chapter": 1,
"section": "1.2",
"edition": "2026-08-09",
"book_page": 18,
"pdf_page": 30,
"page": "book 18 / PDF 30",
"source_kind": "Definition 1.2.28",
"source_url": "https://chewisinho.github.io/main.pdf#page=30",
"wording_status": "faithful paraphrase",
"source_summary": "The iterated carre du champ applies the generator to Gamma and subtracts the two mixed generator terms.",
"mathematical_exposition": "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.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp.iteratedCarreDuChamp"
],
"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"
],
"downstream_consumers": [
"Bakry-Emery curvature-dimension condition",
"Langevin curvature calculation"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact source definition compiled; no curvature inequality is inferred",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-iterated-carre-du-champ-definition",
"label": "Iterated carre du champ definition",
"declarations": [
"iteratedCarreDuChamp"
],
"dependencies": [
"carreDuChamp",
"LinearMap"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-2-definition-1-2-29",
"chapter": 1,
"section": "1.2",
"edition": "2026-08-09",
"book_page": 19,
"pdf_page": 31,
"page": "book 19 / PDF 31",
"source_kind": "Definition 1.2.29",
"source_url": "https://chewisinho.github.io/main.pdf#page=31",
"wording_status": "faithful paraphrase",
"source_summary": "The Bakry-Emery curvature-dimension condition requires positive alpha and the pointwise inequality Gamma_2(f) at least alpha Gamma(f).",
"mathematical_exposition": "CD(alpha,infinity) holds when alpha > 0 and alpha Gamma(f,f)(x) <= Gamma_2(f,f)(x) for every observable and state.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp.SatisfiesBakryEmery"
],
"source_assumptions": [
"a positive curvature constant",
"the pointwise Gamma_2 lower bound"
],
"formal_assumptions": [
"0 < alpha",
"the inequality holds for every observable and state"
],
"downstream_consumers": [
"Bakry-Emery criterion for Poincare and log-Sobolev inequalities",
"strongly convex Langevin potentials"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact source predicate compiled; the criterion and concrete Langevin verification remain separate theorem routes",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-bakry-emery-definition",
"label": "Bakry-Emery CD(alpha,infinity) predicate",
"declarations": [
"SatisfiesBakryEmery"
],
"dependencies": [
"carreDuChamp",
"iteratedCarreDuChamp"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-2-gronwall",
"chapter": 1,
"section": "1.2",
"edition": "2026-08-09",
"book_page": 16,
"pdf_page": 28,
"page": "book 16 / PDF 28",
"source_kind": "Lemma 1.2.20",
"source_url": "https://chewisinho.github.io/main.pdf#page=28",
"wording_status": "faithful paraphrase",
"source_summary": "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.",
"mathematical_exposition": "Differentiating 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.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.chewi_lemma_1_2_20"
],
"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"
],
"downstream_consumers": [
"Poincare variance and chi-squared decay",
"log-Sobolev KL decay",
"gradient-flow convergence inequalities"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "source-faithful differential Gronwall lemma compiled from Mathlib's one-sided comparison theorem",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-differential-gronwall",
"label": "Differential Gronwall on a finite interval",
"declarations": [
"chewi_lemma_1_2_20"
],
"dependencies": [
"le_gronwallBound_of_liminf_deriv_right_le",
"gronwallBound_ε0",
"DifferentiableAt.hasDerivAt"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-2-langevin-generator",
"chapter": 1,
"section": "1.2",
"edition": "2026-08-09",
"book_page": 11,
"pdf_page": 23,
"page": "book 11 / PDF 23",
"source_kind": "Example 1.2.4",
"source_url": "https://chewisinho.github.io/main.pdf#page=23",
"wording_status": "faithful paraphrase",
"source_summary": "For overdamped Langevin diffusion, Itô's formula displays the formal generator as a Laplacian minus a score-directional derivative.",
"mathematical_exposition": "Applying 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.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Langevin.finiteEuclidean_langevinGenerator_basisDisplay",
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Langevin.finiteEuclidean_langevinGenerator_coordinateDisplay",
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Langevin.finiteEuclidean_expNeg_lineDeriv_fderiv_coordinateSum_langevinGenerator_display",
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Langevin.finiteEuclidean_expNeg_lineDeriv_fderiv_coordinateSum_langevinGenerator_display_of_differentiableAt"
],
"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"
],
"downstream_consumers": [
"weighted integration by parts",
"formal symmetry",
"generator core"
],
"status": "partial"
},
{
"id": "chewi-1-2-weighted-ibp",
"chapter": 1,
"section": "1.2",
"edition": "2026-08-09",
"book_page": 13,
"pdf_page": 25,
"page": "book 13 / PDF 25",
"source_kind": "Example 1.2.8",
"source_url": "https://chewisinho.github.io/main.pdf#page=25",
"wording_status": "faithful paraphrase",
"source_summary": "A weighted integration-by-parts calculation makes the Langevin generator formally symmetric under its Gibbs weight.",
"mathematical_exposition": "With 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.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Langevin.weightedDivergence_gibbsWeight_langevinGenerator_algebra",
"AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff_hasCompactSupport",
"AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff_tendsto_one",
"AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.tendsto_integral_norm_fderiv_radialSmoothCutoff_comp_toLp_apply",
"AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.tendsto_integral_radialSmoothCutoff_comp_toLp_smul",
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Langevin.integral_expNeg_langevinGenerator_rhs_eq_zero_of_contDiff_of_hasCompactSupport"
],
"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"
],
"downstream_consumers": [
"whole-space weighted integration by parts",
"generator symmetry",
"Gibbs stationarity"
],
"status": "partial"
},
{
"id": "chewi-1-2-stationarity",
"chapter": 1,
"section": "1.2",
"edition": "2026-08-09",
"book_page": 13,
"pdf_page": 25,
"page": "book 13 / PDF 25",
"source_kind": "Corollary 1.2.9",
"source_url": "https://chewisinho.github.io/main.pdf#page=25",
"wording_status": "faithful paraphrase",
"source_summary": "The Gibbs measure is the stationary law suggested by the weighted generator identity.",
"mathematical_exposition": "The 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.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.Measure.Gibbs.isProbabilityMeasure_withDensity_normalized_gibbs",
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LangevinGenerator.integral_operator_normalizedGibbs_eq_zero_on_compactlySupportedC2",
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LangevinGenerator.isInvariantOn_normalizedGibbs_on_compactlySupportedC2"
],
"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"
],
"downstream_consumers": [
"equilibrium convergence",
"algorithmic sampling interpretation"
],
"status": "partial"
},
{
"id": "chewi-1-3-poincare",
"chapter": 1,
"section": "1.2",
"edition": "2026-08-09",
"book_page": 16,
"pdf_page": 28,
"page": "book 16 / PDF 28",
"source_kind": "Supporting Poincare-to-decay realization route",
"source_url": "https://chewisinho.github.io/main.pdf#page=28",
"wording_status": "faithful paraphrase",
"source_summary": "Variance is bounded by an energy involving the gradient.",
"mathematical_exposition": "A 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.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance",
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.dirichletEnergy",
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.Admissible",
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.Satisfies",
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance_nonneg",
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.dirichletEnergy_nonneg",
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.mono_constant",
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance_le",
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.mono_tests",
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.exponential_decay_of_scaled_dissipation",
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.chewi_theorem_1_2_21_forward",
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.chewi_theorem_1_2_22_forward",
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.exponential_decay_of_scaled_dissipation_from",
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.scaled_dissipation_of_exponential_decay",
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.chewi_theorem_1_2_21_scalar_equivalence",
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.chewi_theorem_1_2_22_scalar_equivalence"
],
"source_assumptions": [
"sufficiently regular functions"
],
"formal_assumptions": [
"explicit measure and scalar field",
"probability normalization",
"integrability/square-integrability",
"explicit Dirichlet form"
],
"downstream_consumers": [
"variance decay",
"spectral-gap estimates"
],
"status": "partial",
"route_status": "partial",
"local_status": "compiled",
"semantic_status": "compiled scalar equivalences between Poincare-style coercivity and shifted variance/chi-square exponential decay under an explicit exact dissipation curve; the concrete reversible semigroup, density realization, and core/domain extension remain open",
"remaining_obligations": [
"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"
],
"proof_leaves": [
{
"node_id": "chapter1-poincare-variance-decay-forward",
"label": "Poincare coercivity implies variance-style exponential decay",
"declarations": [
"exponential_decay_of_scaled_dissipation",
"chewi_theorem_1_2_21_forward"
],
"dependencies": [
"le_gronwallBound_of_liminf_deriv_right_le",
"gronwallBound_ε0"
],
"priority": 92,
"route_status": "partial"
},
{
"node_id": "chapter1-poincare-chi-square-decay-forward",
"label": "Poincare coercivity implies chi-square-style exponential decay",
"declarations": [
"exponential_decay_of_scaled_dissipation",
"chewi_theorem_1_2_22_forward"
],
"dependencies": [
"chewi_theorem_1_2_21_forward"
],
"priority": 90,
"route_status": "partial"
},
{
"node_id": "chapter1-poincare-shifted-decay-converse",
"label": "Shifted exponential decay recovers instantaneous Poincare coercivity",
"declarations": [
"scaled_dissipation_of_exponential_decay",
"chewi_theorem_1_2_21_scalar_equivalence",
"chewi_theorem_1_2_22_scalar_equivalence"
],
"dependencies": [
"IsLocalMaxOn.hasFDerivWithinAt_nonpos",
"one_mem_posTangentConeAt_iff_frequently"
],
"priority": 93,
"route_status": "partial"
}
]
},
{
"id": "chewi-1-3-log-sobolev",
"chapter": 1,
"section": "1.2",
"edition": "2026-08-09",
"book_page": 18,
"pdf_page": 30,
"page": "book 18 / PDF 30",
"source_kind": "Supporting log-Sobolev-to-decay realization route",
"source_url": "https://chewisinho.github.io/main.pdf#page=30",
"wording_status": "faithful paraphrase",
"source_summary": "Entropy is controlled by a Fisher-information or Dirichlet-form term.",
"mathematical_exposition": "A 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.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.Satisfies",
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.mono_constant",
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.mono_tests",
"AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainIntegralHandoffScalar",
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.exponential_decay_of_scaled_dissipation",
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.chewi_theorem_1_2_26_forward",
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.exponential_decay_of_scaled_dissipation_from",
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.scaled_dissipation_of_exponential_decay",
"AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.chewi_theorem_1_2_26_scalar_equivalence"
],
"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"
],
"downstream_consumers": [
"entropy decay",
"Langevin mixing in KL"
],
"status": "partial",
"route_status": "partial",
"local_status": "compiled",
"semantic_status": "compiled scalar equivalence between LSI-style coercivity and shifted KL exponential decay under an explicit KL/Fisher-information dissipation curve; the concrete density flow, entropy differentiation, and domain extension remain open",
"remaining_obligations": [
"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"
],
"proof_leaves": [
{
"node_id": "chapter1-lsi-kl-decay-forward",
"label": "Log-Sobolev coercivity implies KL exponential decay",
"declarations": [
"exponential_decay_of_scaled_dissipation",
"chewi_theorem_1_2_26_forward"
],
"dependencies": [
"le_gronwallBound_of_liminf_deriv_right_le",
"gronwallBound_ε0"
],
"priority": 94,
"route_status": "partial"
},
{
"node_id": "chapter1-lsi-shifted-decay-converse",
"label": "Shifted KL decay recovers instantaneous log-Sobolev coercivity",
"declarations": [
"scaled_dissipation_of_exponential_decay",
"chewi_theorem_1_2_26_scalar_equivalence"
],
"dependencies": [
"IsLocalMaxOn.hasFDerivWithinAt_nonpos",
"one_mem_posTangentConeAt_iff_frequently"
],
"priority": 95,
"route_status": "partial"
}
]
},
{
"id": "chewi-1-3-definition-1-3-12",
"chapter": 1,
"section": "1.3",
"edition": "2026-08-09",
"book_page": 25,
"pdf_page": 37,
"page": "book 25 / PDF 37",
"source_kind": "Definition 1.3.12",
"source_url": "https://chewisinho.github.io/main.pdf#page=37",
"wording_status": "faithful paraphrase",
"source_summary": "P2,ac consists of Euclidean probability laws with finite second moment that are absolutely continuous with respect to Lebesgue measure.",
"mathematical_exposition": "A measure belongs to P2,ac when it is a probability measure, its squared norm is integrable, and it is absolutely continuous with respect to volume.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSpace.IsAbsolutelyContinuousFiniteSecondMoment"
],
"source_assumptions": [
"a probability measure on Euclidean space",
"finite second moment",
"absolute continuity with respect to Lebesgue measure"
],
"formal_assumptions": [
"finite-dimensional real inner-product space",
"Borel measurable structure",
"IsProbabilityMeasure, absolute continuity, and Integrable squared norm"
],
"downstream_consumers": [
"Brenier optimal maps",
"Wasserstein tangent-space calculus",
"Langevin gradient-flow route"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact P2,ac measure-class definition compiled; metric and optimal-map structure remain separate source items",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-p2ac-definition",
"label": "Absolutely continuous finite-second-moment laws",
"declarations": [
"IsAbsolutelyContinuousFiniteSecondMoment"
],
"dependencies": [
"IsProbabilityMeasure",
"Measure.AbsolutelyContinuous",
"Integrable",
"volume"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-3-definition-1-3-25",
"chapter": 1,
"section": "1.3",
"edition": "2026-08-09",
"book_page": 30,
"pdf_page": 42,
"page": "book 30 / PDF 42",
"source_kind": "Definition 1.3.25",
"source_url": "https://chewisinho.github.io/main.pdf#page=42",
"wording_status": "faithful paraphrase",
"source_summary": "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.",
"mathematical_exposition": "If gamma is an optimal quadratic coupling of mu0 and mu1, the curve mu_t is the pushforward of gamma by (x0,x1) mapped to (1-t)x0+t x1 for t in [0,1].",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolation.IsWassersteinGeodesic"
],
"source_assumptions": [
"two P2,ac probability laws",
"an optimally coupled endpoint pair"
],
"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]"
],
"downstream_consumers": [
"geodesic convexity",
"Wasserstein gradient flows",
"McCann interpolation arguments"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact source definition and endpoint laws compiled; optimal-plan existence, constant speed, and uniqueness remain Theorem 1.3.23",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-displacement-interpolation-definition",
"label": "Optimal-coupling affine law curve",
"declarations": [
"IsWassersteinGeodesic"
],
"dependencies": [
"IsAbsolutelyContinuousFiniteSecondMoment",
"IsQuadraticOptimalCoupling",
"Measure.map"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-3-definition-1-3-1",
"chapter": 1,
"section": "1.3",
"edition": "2026-08-09",
"book_page": 20,
"pdf_page": 32,
"page": "book 20 / PDF 32",
"source_kind": "Definition 1.3.1",
"source_url": "https://chewisinho.github.io/main.pdf#page=32",
"wording_status": "faithful paraphrase",
"source_summary": "The Kantorovich transport cost is the infimum of expected cost over all joint probability laws with the prescribed marginals.",
"mathematical_exposition": "For an extended nonnegative cost c, T_c(mu,nu) is the infimum of the integrals of c against all couplings of mu and nu. The value is extended-real, so infinite transport cost remains representable.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.Measure.Transport.transportCost"
],
"source_assumptions": [
"probability measures on complete separable metric spaces",
"an extended nonnegative transport cost"
],
"formal_assumptions": [
"measurable state spaces",
"an ENNReal-valued cost",
"the exact coupling marginal predicate"
],
"downstream_consumers": [
"optimal-plan existence",
"2-Wasserstein distance",
"Kantorovich duality"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact extended-real Kantorovich value compiled; attainment and metric properties are separate source items",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-kantorovich-cost-definition",
"label": "Kantorovich transport cost",
"declarations": [
"transportCost"
],
"dependencies": [
"IsCoupling",
"lintegral",
"sInf"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-3-display-1-3-2",
"chapter": 1,
"section": "1.3",
"edition": "2026-08-09",
"book_page": 20,
"pdf_page": 32,
"page": "book 20 / PDF 32",
"source_kind": "Displayed identity (1.3.2)",
"source_url": "https://chewisinho.github.io/main.pdf#page=32",
"wording_status": "faithful paraphrase",
"source_summary": "The transport value expands as the infimum of the coupling lintegrals of the cost.",
"mathematical_exposition": "T_c(mu,nu) = inf over gamma in C(mu,nu) of the integral of c(x,y) against gamma.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.Measure.Transport.transportCost_eq_sInf"
],
"source_assumptions": [
"the Kantorovich feasible set and cost of Definition 1.3.1"
],
"formal_assumptions": [
"the compiled transportCost and couplingSet definitions"
],
"downstream_consumers": [
"optimal transport comparison arguments",
"Wasserstein cost specialization"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "exact definitional expansion compiled",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-kantorovich-cost-display",
"label": "Kantorovich infimum display",
"declarations": [
"transportCost_eq_sInf"
],
"dependencies": [
"transportCost"
],
"priority": 100,
"route_status": "compiled"
}
]
},
{
"id": "chewi-1-3-coupling",
"chapter": 1,
"section": "1.3",
"edition": "2026-08-09",
"book_page": 20,
"pdf_page": 32,
"page": "book 20 / PDF 32",
"source_kind": "Supporting coupling interface",
"source_url": "https://chewisinho.github.io/main.pdf#page=32",
"wording_status": "faithful paraphrase",
"source_summary": "A coupling is a joint probability law with two prescribed marginals.",
"mathematical_exposition": "For probability measures \\(\\mu\\) and \\(\\nu\\), a coupling \\(\\gamma\\) is a measure on the product space whose first marginal is \\(\\mu\\) and second marginal is \\(\\nu\\). The independent product \\(\\mu\\otimes\\nu\\) provides a canonical feasible coupling.",
"astis_exposition": "Samplinglib isolates the marginal contract from transport costs and proves the independent-product witness using Mathlib's product-measure marginal identities.",
"latex_statement": "\\Gamma(\\mu,\\nu)=\\{\\gamma\\in\\mathcal P(X\\times Y):(\\mathrm{proj}_X)_\\#\\gamma=\\mu,\\ (\\mathrm{proj}_Y)_\\#\\gamma=\\nu\\},\\qquad \\mu\\otimes\\nu\\in\\Gamma(\\mu,\\nu).",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.Measure.Transport.isProbabilityMeasure_of_isCoupling_left",
"AutoSamplingTheory.TechnicalLemmas.Measure.Transport.isCoupling_prod"
],
"dependencies": [
"Measure.fst_prod",
"Measure.snd_prod"
],
"source_assumptions": [
"probability measures on the two state spaces"
],
"formal_assumptions": [
"measurable spaces",
"probability-measure instances for both marginals"
],
"downstream_consumers": [
"optimal transport cost",
"Wasserstein distance",
"synchronous Langevin coupling",
"LMC coupling analysis"
],
"local_status": "compiled",
"semantic_status": "verified measure-theoretic core; topological transport layer remains open",
"route_status": "partial",
"remaining_obligations": [
"define measurable transport costs and the Kantorovich objective",
"connect the coupling interface to Wasserstein distance",
"formalize optimal-plan existence under the source's Polish-space hypotheses"
],
"proof_leaves": [
{
"node_id": "chapter1_product_coupling",
"label": "Independent product coupling witness",
"declarations": [
"IsCoupling",
"isProbabilityMeasure_of_isCoupling_left",
"isCoupling_prod"
],
"dependencies": [],
"priority": 70,
"route_status": "partial"
}
],
"status": "partial"
},
{
"id": "chewi-2-functional-inequalities-overview",
"chapter": 2,
"section": "2.1",
"edition": "2026-08-09",
"book_page": 48,
"pdf_page": 60,
"page": "book 48 / PDF 60",
"source_kind": "Section 2.1 overview",
"source_url": "https://chewisinho.github.io/main.pdf#page=60",
"wording_status": "faithful paraphrase",
"source_summary": "The chapter organizes Poincaré, log-Sobolev, transport, and concentration inequalities in a common measure-theoretic language.",
"mathematical_exposition": "The principal inequalities compare variance, entropy, transport distance, and boundary or tail behavior. Their implications and preservation rules provide reusable routes from geometric assumptions to quantitative sampling convergence.",
"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_declarations": [
"AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainIntegralHandoffScalar"
],
"source_assumptions": [
"probability reference law",
"regular test functions or densities"
],
"formal_assumptions": [
"explicit measure",
"probability normalization for the Poincare interface",
"finite entropy/energy terms",
"explicit function class"
],
"downstream_consumers": [
"semigroup convergence",
"sampling complexity"
],
"status": "partial"
},
{
"id": "chewi-3-girsanov",
"chapter": 3,
"section": "3.2",
"edition": "2026-08-09",
"book_page": 100,
"pdf_page": 112,
"page": "book 100 / PDF 112",
"source_kind": "Section 3.2",
"source_url": "https://chewisinho.github.io/main.pdf#page=112",
"wording_status": "faithful paraphrase",
"source_summary": "A change in drift can be represented by an exponential likelihood ratio.",
"mathematical_exposition": "Girsanov's theorem compares two path laws with the same diffusion coefficient by exponentiating a stochastic integral of their drift difference. A martingale condition is what promotes the local exponential to a genuine change of probability measure.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Girsanov.finiteGaussianGirsanovCylinderIntegral",
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Girsanov.finiteGaussianGirsanovCylinderMeasure_eq_withDensity"
],
"source_assumptions": [
"controlled drift change"
],
"formal_assumptions": [
"finite-dimensional Gaussian cylinder at the compiled layer",
"path-space martingale hypotheses still missing"
],
"downstream_consumers": [
"continuous-time comparison",
"LMC and ULMC discretization"
],
"status": "partial"
},
{
"id": "chewi-6-renyi",
"chapter": 6,
"section": "6.1",
"edition": "2026-08-09",
"book_page": 174,
"pdf_page": 186,
"page": "book 174 / PDF 186",
"source_kind": "Section 6.1",
"source_url": "https://chewisinho.github.io/main.pdf#page=186",
"wording_status": "faithful paraphrase",
"source_summary": "Rényi divergence packages a power integral of a density ratio.",
"mathematical_exposition": "At order q, Rényi divergence is the logarithm of a q-th power integral of the density ratio, scaled by 1/(q-1). The power weight changes both the dissipation term and the error estimates used in the LMC analysis.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.InformationTheory.Renyi.renyiIntegrand_pos",
"AutoSamplingTheory.TechnicalLemmas.InformationTheory.Renyi.measurable_renyiIntegrandENNReal",
"AutoSamplingTheory.TechnicalLemmas.InformationTheory.Renyi.lintegral_renyiIntegrandENNReal_ne_top_of_ae_le"
],
"source_assumptions": [
"density ratio",
"order parameter"
],
"formal_assumptions": [
"measurable nonnegative densities",
"explicit domination for finiteness"
],
"downstream_consumers": [
"warm-start comparison",
"discretization error conversion"
],
"status": "partial"
},
{
"id": "chewi-6-discretization",
"chapter": 6,
"section": "6.2",
"edition": "2026-08-09",
"book_page": 178,
"pdf_page": 190,
"page": "book 178 / PDF 190",
"source_kind": "Section 6.2",
"source_url": "https://chewisinho.github.io/main.pdf#page=190",
"wording_status": "faithful paraphrase",
"source_summary": "Continuous interpolation and change of measure convert local numerical error into sampling error.",
"mathematical_exposition": "An interpolation agrees with the discrete chain at grid times while freezing part of the drift between updates. Comparing this process with the target diffusion reduces the global law error to an integrated local drift mismatch.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Girsanov.finiteGaussianGirsanovCylinderMeasure_eq_withDensity"
],
"source_assumptions": [
"smooth drift",
"stable step size"
],
"formal_assumptions": [
"moment and path-law hypotheses not yet fully formalized"
],
"downstream_consumers": [
"LMC complexity",
"ULMC complexity"
],
"status": "partial"
},
{
"id": "chewi-8-proximal",
"chapter": 8,
"section": "8.1",
"edition": "2026-08-09",
"book_page": 215,
"pdf_page": 227,
"page": "book 215 / PDF 227",
"source_kind": "Section 8.1",
"source_url": "https://chewisinho.github.io/main.pdf#page=227",
"wording_status": "faithful paraphrase",
"source_summary": "A Gaussian augmentation creates alternating conditional distributions with the target as a marginal.",
"mathematical_exposition": "The proximal sampler augments the target with a Gaussian coupling between x and y, then alternates the two conditional laws. The x-marginal remains the original target, while the conditional structure exposes a restricted Gaussian oracle.",
"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_declarations": [],
"source_assumptions": [
"well-defined conditional samplers"
],
"formal_assumptions": [
"kernel measurability",
"finite conditional normalizers",
"joint-law marginal identity"
],
"downstream_consumers": [
"proximal sampler convergence",
"structured sampling"
],
"status": "todo"
},
{
"id": "chewi-11-fisher-stationarity",
"chapter": 11,
"section": "11.1",
"edition": "2026-08-09",
"book_page": 272,
"pdf_page": 284,
"page": "book 272 / PDF 284",
"source_kind": "Section 11.1",
"source_url": "https://chewisinho.github.io/main.pdf#page=284",
"wording_status": "faithful paraphrase",
"source_summary": "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.",
"mathematical_exposition": "Relative Fisher information measures the squared difference between the current score and the target score. Integrating entropy dissipation over time yields a bound for a randomized or averaged output even when global mixing is computationally inaccessible.",
"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_declarations": [
"AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainIntegralHandoffScalar"
],
"source_assumptions": [
"absolutely continuous time marginals",
"finite initial relative entropy"
],
"formal_assumptions": [
"chosen score representative",
"finite Fisher-information terms",
"justified entropy-dissipation identity",
"measurable randomized output time"
],
"downstream_consumers": [
"non-log-concave stationarity bounds",
"algorithmic Fisher-information estimates"
],
"status": "partial"
},
{
"id": "chewi-12-score",
"chapter": 12,
"section": "12.1",
"edition": "2026-08-09",
"book_page": 283,
"pdf_page": 295,
"page": "book 283 / PDF 295",
"source_kind": "Section 12.1",
"source_url": "https://chewisinho.github.io/main.pdf#page=295",
"wording_status": "faithful paraphrase",
"source_summary": "The reverse-time drift uses the score of the forward marginal, and approximation errors become drift errors.",
"mathematical_exposition": "A forward diffusion transports data toward a tractable reference law. Under suitable marginal regularity, the reverse SDE contains the time-dependent score \\(\\nabla\\log\\pi_t\\); replacing that score and discretizing time create distinct error terms.",
"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_declarations": [
"AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainIntegralHandoffScalar"
],
"source_assumptions": [
"regular time marginals",
"available score approximation"
],
"formal_assumptions": [
"score representative",
"time-reversal regularity",
"law under which score error is controlled"
],
"downstream_consumers": [
"diffusion generative models"
],
"status": "partial"
},
{
"id": "chewi-proposition-1-1-13",
"chapter": 1,
"section": "1.1",
"edition": "2026-08-09",
"book_page": 7,
"pdf_page": 19,
"page": "book 7 / PDF 19",
"source_kind": "Proposition 1.1.13",
"source_url": "https://chewisinho.github.io/main.pdf#page=19",
"wording_status": "faithful paraphrase",
"source_summary": "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.",
"mathematical_exposition": "Complete the null exceptional set, form the continuous accumulated-energy path, stop at equality level n+1, use continuity to rule out overshoot, characterize the threshold event to prove the stopping-time property, and use finite terminal energy to show the localizers exhaust the horizon.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalLocalizationTheorem.chewi_proposition_1_1_13"
],
"source_assumptions": [
"a complete right-continuous filtered probability space",
"a progressive integrand whose squared time integral is finite almost surely on the finite horizon"
],
"formal_assumptions": [
"SatisfiesUsualConditions filtration mu",
"IsProbabilityMeasure mu",
"LocalProgressiveL2Integrand filtration mu T"
],
"downstream_consumers": [
"display (1.1.14)",
"Proposition 1.1.16"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "source-facing canonical localization theorem compiled with stopping-time, monotonicity, horizon exhaustion, and stopped-energy bound",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-source-1-1-13",
"label": "Chewi Proposition 1.1.13",
"declarations": [
"chewi_proposition_1_1_13"
],
"dependencies": [
"continuous_completedEnergy",
"canonicalEnergyLocalizer_le_iff",
"canonicalLocalizingTime_isChewiStoppingTime",
"integral_energyStoppedIntegrand_sq_le"
],
"priority": 100,
"route_status": "compiled"
}
],
"source_mapping_id": "chewi-chapter1-statement-1-1-13",
"latex_statement": "\\tau_n:=\\inf\\{t\\le T:A_t=n+1\\}\\ \\text{(fallback }T\\text{)},\\qquad \\tau_n\\uparrow T"
},
{
"id": "chewi-1-1-display-1-1-14",
"chapter": 1,
"section": "1.1",
"edition": "2026-08-09",
"book_page": 7,
"pdf_page": 19,
"page": "book 7 / PDF 19",
"source_kind": "Displayed identity (1.1.14)",
"source_url": "https://chewisinho.github.io/main.pdf#page=19",
"wording_status": "faithful paraphrase",
"source_summary": "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.",
"mathematical_exposition": "Proposition 1.1.13 turns the locally square-integrable integrand into a globally L2 stopped integrand. Applying the existing global Ito map gives a continuous martingale, and each deterministic-time value agrees almost surely with the terminal completed Ito integral of the stopped integrand restricted up to that time.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalStoppedItoIntegral.chewi_display_1_1_14"
],
"source_assumptions": [
"the canonical localizing sequence of Proposition 1.1.13",
"a Brownian motion relative to the filtration",
"a positive finite horizon"
],
"formal_assumptions": [
"SatisfiesUsualConditions filtration mu",
"IsProbabilityMeasure mu",
"LocalProgressiveL2Integrand filtration mu T",
"0 < T",
"IsBrownianMotionWithFiltration B filtration mu"
],
"downstream_consumers": [
"Proposition 1.1.16"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "source-facing stopped-Ito display compiled as a continuous martingale with deterministic-time restriction compatibility",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-source-1-1-14",
"label": "Chewi Displayed identity (1.1.14)",
"declarations": [
"chewi_display_1_1_14"
],
"dependencies": [
"chewi_proposition_1_1_13",
"canonicalStoppedProgressiveL2",
"itoIntegralProcess_martingale",
"itoIntegralProcess_continuous_ae"
],
"priority": 100,
"route_status": "compiled"
}
],
"source_mapping_id": "chewi-chapter1-displayed-identity-1-1-14"
},
{
"id": "chewi-proposition-1-1-16",
"chapter": 1,
"section": "1.1",
"edition": "2026-08-09",
"book_page": 7,
"pdf_page": 19,
"page": "book 7 / PDF 19",
"source_kind": "Proposition 1.1.16",
"source_url": "https://chewisinho.github.io/main.pdf#page=19",
"wording_status": "faithful paraphrase",
"source_summary": "The Ito integral of a progressive locally square-integrable integrand has a continuous version that is a local martingale.",
"mathematical_exposition": "Use canonical energy localizers to obtain globally L2 stopped integrands. Prove stochastic integration commutes with those random stops first on grid-valued stopping times, pass by dyadic approximation in L2 and along continuous paths, prove cross-horizon consistency, glue the finite-horizon processes pathwise, and use localizers tending to infinity almost surely.",
"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_declarations": [
"AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ChewiProposition1_1_16.chewi_proposition_1_1_16"
],
"source_assumptions": [
"a complete right-continuous filtered probability space",
"a Brownian motion relative to the filtration",
"a progressive integrand with almost-sure locally finite squared energy"
],
"formal_assumptions": [
"SatisfiesUsualConditions filtration mu",
"IsProbabilityMeasure mu",
"GlobalLocalProgressiveL2Integrand filtration mu",
"IsBrownianMotionWithFiltration B filtration mu"
],
"downstream_consumers": [
"Definition 1.1.17 (Ito process)",
"Ito formula and SDE localization"
],
"status": "compiled",
"route_status": "compiled",
"local_status": "compiled",
"semantic_status": "source-facing local-Ito continuous-local-martingale theorem compiled with random-stopping and cross-horizon gluing",
"remaining_obligations": [],
"proof_leaves": [
{
"node_id": "chapter1-source-1-1-16",
"label": "Chewi Proposition 1.1.16",
"declarations": [
"chewi_proposition_1_1_16"
],
"dependencies": [
"elementaryItoIntegral_stop_gridValued",
"tendsto_rightApproxTime_stoppingValue",
"processTimeMeasure_stoppingGraph_zero",
"globalStoppedItoProcess_overlap_pathwise_ae",
"globalItoProcess_isLocalMartingale"
],
"priority": 100,
"route_status": "compiled"
}
],
"source_mapping_id": "chewi-chapter1-statement-1-1-16",
"latex_statement": "M_t=\\int_0^t \\eta_s\\,dB_s,\\qquad M_{t\\wedge\\tau_n}=\\int_0^t \\eta_s\\mathbf 1_{\\{s\\le\\tau_n\\}}\\,dB_s"
}
]