Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Mean-Square Assembly of the Estimand Linearisation on the Synthetic Copy: Approximation of the Recentred Copy Endpoint by an Affine Function of the Parameter
lemmalem:copy-estimand-mean-square-assembly-2026bAnalysisProbabilityAdopt the setting, hypotheses (OC), (X), (W), (G), (G), (CL) and notation of Information Bound on the Synthetic Copy with Mean-Field Data: Prior Energy of the Profile, Observation Information Along the Profile Response, and the Non-Close Record Mass (and hence of…The Path-Closeness Event under the Cost Bound: Closeness of the Empirical State Measure to the Mean-Field Trajectory and of the Record-Frozen Control to the Mean-Field Control on an Event of Probability
lemmalem:path-closeness-event-cost-bound-2026aAnalysisProbabilityData. Adopt the setting, notation and standing hypotheses of the control- and flow-closeness lemma, and with them those of the asymptotic lower bound theorem for the recentred -agent cost: the common data, among them the affine-controlled transition-rate family…The Realized Control as the Record-Frozen Control at the Observation Record, and Measurability of the Path-and-Record Closeness Set
lemmalem:realized-control-record-frozen-closeness-set-2026aAnalysisProbabilityData. Adopt the setting of the realized-control lemma, with its transition-rate family specialised as follows: natural numbers , , and ; a real number and an affine-controlled transition-rate family on …Closeness of the Realized Control and the Realized Mean-Field Flow on a High-Probability Event under the Cost Bound
lemmalem:cost-bound-control-flow-closeness-2026aAnalysisProbabilityData. Adopt the setting, notation and standing hypotheses of the asymptotic lower bound theorem for the recentred -agent cost, and with them those of the ledger lemma and of the block cascade lemma on which it rests. In particular: the affine-controlled transition-rate family…The Observation Filtration of a Solution of the Controlled N-Agent Dynamics is Generated, up to Null Sets, by the Observation Record up to that Time
lemmalem:observation-filtration-equals-record-sigma-algebra-2026aProbabilityAdopt the setting and notation of the controlled -agent dynamics: natural numbers , , , ; a nonempty control set , assumed convex and compact for the topology determined by the Euclidean distance (as require…Factorisation of Random Variables Through a Measurable Map, the Variational Form of the Mean-Square Filtering Error, and Its Invariance Under the Joint Law
lemmalem:filtering-error-law-invariance-2026aAnalysisProbabilityLet be a probability space with expectation , let be a measurable space, and let be measurable with respect to and . Write for the…The Record-Frozen Control as a Measurable Map into the Weakly Metrized Control Set, and the Record-Frozen Mean-Field Flow: Joint Measurability, Flow Equation, and Measurability in the Record
lemmalem:record-frozen-control-measurable-flow-2026aAnalysisProbabilityAdopt the setting and notation of the flow stability lemma: an affine-controlled transition-rate family on states with control set (nonempty, convex and compact as part of those data) and Lipschitz constant ; its…Pathwise Estimand Linearisation of an Open-Loop Aggregate Solution Along a Comparison Pair: Cell-Count Coefficients from the Fundamental Solution and the Three Error Terms
lemmalem:open-loop-estimand-linearisation-pathwise-2026aAnalysisProbabilityAdopt the setting and notation of Linearisation of a Perturbed Controlled Aggregate Flow Along a Comparison Pair: Exact Variation-of-Constants Identity and Residual Bound: natural numbers , , the control set , real numbers a…Restriction of a Solution of the Controlled N-Agent Dynamics to a Shorter Horizon: the Truncated Policy, the Restricted Solution, Its Filtrations, and Its Record as the Prefix of the Record
lemmalem:n-agent-solution-horizon-restriction-2026aProbabilityAdopt the setting of the controlled -agent dynamics: natural numbers , , , , a nonempty control set in Euclidean space, a transition-rate family on states with control set and rate…Law Identity between the N-Agent Aggregate Path with Its Observation Record and the Synthetic Copy's Regularised Path with Its Record
lemmalem:n-agent-copy-record-law-identity-2026aProbabilityAdopt the setting and notation of The Synthetic Copy: Independent Cell Structure, Deterministic-Count Clocks, the Copy Measure, and the Smoothed Joint Density of Parameter and Observation Record, with the probability space of that lemma renamed…The Space of Piecewise Constant Paths in a Finite Set: Measurability of Evaluations, Restrictions, Left Limits, and Occupation Integrals
lemmalem:piecewise-constant-path-space-2026aAnalysisProbabilityLet be a real number and let be a nonempty finite set. Let be the set of maps for which there are a count , either or a natural number, and times such that is constant on , on …A Conditional Density Identity for Products Extends to Jointly Measurable Integrands
lemmalem:conditional-density-joint-integrand-2026aProbabilityLet be a probability space, let be a sub--algebra, let be a -finite measure space, and let be measurable with respect to and…Sections of Product-Measurable Sets and Maps Are Measurable, and Insertion Maps into Products Are Measurable
lemmalem:product-sections-measurable-2026aAnalysisProbabilityLet , , and be measurable spaces, and let denote the product -algebra on the Cartesian product , with the analogous notation for other pairs. For…Law Identity between the Reconstructed Record-Frozen Aggregate and the Aggregate Recursion Driven by the Same Control Path
lemmalem:record-frozen-aggregate-copy-law-identity-2026aProbabilityAdopt the setting and notation of Forward Equation on the Aggregate Lattice for the Reconstructed Record-Frozen N-Agent Dynamics with its fixed record : in particular the natural numbers , and , the control set…Forward Equation on the Aggregate Lattice for the Reconstructed Record-Frozen N-Agent Dynamics
lemmalem:n-agent-record-frozen-forward-equation-2026aProbabilityAdopt the setting and notation of Measurable Reconstruction of the Controlled N-Agent Dynamics from Observation Records: natural numbers , , , , a nonempty control set in Euclidean space, a…Forward Equation for the Aggregate Recursion Driven by Independent Poisson Clocks with a Horizon
lemmalem:aggregate-recursion-forward-equation-2026aProbabilityAdopt the setting and notation of Clock-Reading Bound for the Aggregate Recursion: the Recursion up to a Time Depends Only on the Clocks Below the Consumed Levels (that of Existence, Uniqueness, Causality, and Measurability of the Open-Loop Aggregate Solution): natural numbers…The Copy Clocks Are Independent Poisson Clocks with Horizon R, and Every Record Is Almost Surely Conflict-Free for Them
lemmalem:copy-clocks-independent-poisson-horizon-2026aProbabilityAdopt the setting and notation of The Synthetic Copy: Independent Cell Structure, Deterministic-Count Clocks, the Copy Measure, and the Smoothed Joint Density of Parameter and Observation Record, as recalled in…Clock-Reading Bound for the Aggregate Recursion: the Recursion up to a Time Depends Only on the Clocks Below the Consumed Levels
lemmalem:aggregate-recursion-clock-reading-bound-2026aProbabilityAdopt the setting and notation of Existence, Uniqueness, Causality, and Measurability of the Open-Loop Aggregate Solution: natural numbers , , , a nonempty subset of Euclidean space , real numbers and , a…- Let be a probability space and let be either a real number with or the symbol ; for a real number write for the smaller of and , with . A Poisson clock with horizon on…
Fresh-Start Property for Independent Poisson Clocks Read at Levels Satisfying a Clock-Reading Bound
lemmalem:poisson-clocks-fresh-start-2026aProbabilityLet be a probability space, let be a nonempty finite set (the clock labels), let be a -algebra (the initial data), let be either a real number with or , and for each…