Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Stopped Completion of Squares on a Cascade Block
lemmalem:fluctuation-block-completion-squares-2026aProbabilityAdopt the setting, notation and hypotheses of the completion-of-squares theorem for the fluctuation cost: the fluctuation processes , of a solution with regular event , empirical state measure , control and system…The Tracked Energy Bound for the Block Cascade under Local Joint Coercivity
lemmalem:fluctuation-tracked-energy-2026aProbabilityAdopt simultaneously the settings and notation of the block cascade lemma, of the anchored pre-stopping envelope lemma, of the localized joint coercivity lemma and of the post-exit comparison lemma, all formed for one and the same data: the…Localized Joint Coercivity of the Recentred N-Agent Cost Integrand under a Positive-Definite Fluctuation Hessian
lemmalem:fluctuation-local-joint-coercivity-2026aAnalysisAdopt the setting and notation of the first-order expansion lemma for the recentred -agent cost: the transition-rate family on states with control set and rate bound ; the observation-rate family ; the horizon…The Block Cascade of Anchored Good-Set Clocks: Adapted Good Sets, Matched Escape Bounds, and the Energy Ledger
lemmalem:fluctuation-block-cascade-2026aProbabilityAdopt the setting, notation and conventions of the extended good-set stopping-time lemma: the affine-controlled transition-rate family on states with compact convex control set , its transition-rate family wi…Post-Exit Comparison at a Stopping Time for the Recentred N-Agent Cost under To-Go Value Regularity
lemmalem:n-agent-post-exit-comparison-2026aProbabilityAdopt the setting, hypotheses and notation of the pathwise tracking lemma: the affine-controlled transition-rate family on states with control set , its transition-rate family with rate bound ,…Quadratic Expansion Bounds for the Mean-Field To-Go Value along a Stationary Mean-Field Triple
lemmalem:mean-field-togo-comparison-2026aAnalysisAdopt the setting, hypotheses and notation of the time-shift lemma for the mean-field control problem: the affine-controlled transition-rate family on states — whose control set is nonempty, compact and convex as pa…Time Shift of the Mean-Field Control Problem: Restriction of a Stationary Triple, Cost Splitting, and the Dynamic Programming Principle
lemmalem:mean-field-togo-shift-2026aAnalysisAdopt the setting, hypotheses and notation of the definition of the optimal value, controls and trajectories of the mean-field problem — in particular: the affine-controlled transition-rate family on states with control set…Anchored Pre-Stopping Envelope and Restricted Moment Bounds for the State Fluctuation Process
lemmalem:fluctuation-anchored-envelope-2026aProbabilityAdopt the setting, notation, hypotheses and definitions of the pre-stopping envelope lemma: the affine-controlled transition-rate family on states with compact convex control set , its transition-rate family with r…Anchored Good-Set Clocks on a Subinterval and the Block Escape Bound
lemmalem:anchored-good-set-clocks-2026aProbabilityAdopt the setting, notation and definitions of the extended good-set stopping-time lemma: the affine-controlled transition-rate family on states with compact convex control set , its transition-rate family with rat…First-Order Expansion of the Recentred N-Agent Cost about a Stationary Mean-Field Triple and Its Coercive Lower Bound
lemmalem:n-agent-cost-first-order-identity-2026aProbabilityAdopt the setting of the fluctuation processes of the controlled -agent dynamics: a transition-rate family on states with control set , a nonempty subset of Euclidean space , and rate bound ; an observation-rate family ;…Pre-Stopping-Time Envelope and Restricted Moment Bounds for the State Fluctuation Process
lemmalem:fluctuation-pre-stopping-envelope-2026aProbabilityAdopt the setting, notation and definitions of the extended good-set stopping-time lemma: the affine-controlled transition-rate family on states with compact convex control set , its transition-rate family with rat…The Extended Good-Set Stopping Time of the Realized Control: Clipped-Out Time and Energy Hitting Bounds
lemmalem:extended-good-set-stopping-time-2026aProbabilityAdopt the setting and notation of the good-set stopping-time lemma, together with those of the progressive measurability lemma for the realized control and of the causality and adaptedness lemma for the realized mean-field flow on which it rests: the…Stopped Weighted Second-Moment Evolution of the State Fluctuation Process
lemmalem:fluctuation-weighted-second-moment-stopped-2026aProbabilityAdopt the setting of the weighted second-moment evolution lemma for the state fluctuation process: the fluctuation processes of the controlled -agent dynamics — a transition-rate family on states with control set , a nonempty subset of Euclidean space…Stopped Covariation Identities for the Martingale Part of the Empirical State Measure
lemmalem:n-agent-martingale-stopped-covariation-2026aProbabilityAdopt the setting of the martingale decomposition theorem for the controlled -agent dynamics with agents, states, observation channels, and control dimension : a transition-rate family with control set , a nonempty subset of…The Pre-Stopping-Time Indicator and Stopped Time Integrals
lemmalem:stopped-time-integral-2026aProbabilityLet be a probability space, let be a real number, let be a filtration on with time index restricted to , and let be a stopping time of .…The Good-Set Stopping Time of the Realized Control: Flow Deviation and Control Energy
lemmalem:good-set-stopping-time-2026aProbabilityAdopt the setting and notation of claims 3 and 4 of the adaptedness lemma for the realized mean-field flow, together with those of the progressive measurability lemma for the realized control on which it rests: the affine-controlled transition-rate family with compact convex cont…Causality of the Mean-Field Flow and Observation-Adaptedness of the Realized Mean-Field Flow
lemmalem:realized-mean-field-flow-adapted-2026aProbabilityAdopt the setting and notation of the flow stability lemma: an affine-controlled transition-rate family on states with control set , its transition-rate family with rate bound , state-Lipschitz constant…Progressive Measurability of the Realized Control with Respect to the Observation Filtration
lemmalem:realized-control-observation-progressive-2026aProbabilityAdopt the setting, hypotheses and notation of the realized-control lemma: natural numbers , , , ; a nonempty convex subset of Euclidean space which is compact for the topology determined by the Euclidean distance, w…Conditional Mean-Square Optimality Restricted to an Event of the Conditioning Sigma-Algebra
lemmalem:conditional-mean-square-optimality-restricted-2026aProbabilityAdopt the setting and notation of the conditional mean-square optimality lemma: a probability space , a sub--algebra of , a natural number , a tuple of square-integrable random variables, a fixe…Fourth-Moment Maximal Inequality for Bounded Right-Continuous Martingales on a Compact Time Interval
theoremthm:doob-l4-right-continuous-2026aProbabilityLet be a probability space, let and be real numbers, let be a filtration on with time index restricted to , and let be a square-integrable martingale with resp…