Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 2,569 research declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,963 to 1,968 of 2,569 results.
ProbabilityTheory.HasIndepIncrements.isGaussianProcess
Mathematical statement
A stochastic process X with independent increments and such that X t is gaussian for all t is a Gaussian process.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.iIndepFun.sum_elim
Mathematical statement
Two internally independent families remain jointly independent after they are combined over a disjoint union, provided the two family-valued random variables are independent of one another.
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
ProbabilityTheory.integral_sum_weight_increments_mem_Icc
Mathematical statement
Two-sided expectation bound for adapted {0,1}-weighted increment sums of X, from the boundedness of elementary stochastic integrals at time t. The lower bound uses the complementary weights 1 - W.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.IsBrownianReal.indep_zero
Mathematical statement
Blumenthal's zero-one law: Let 𝓕 be the canonical filtration associated to a Brownian motion. Then the σ-algebra ⨅ s > 0, 𝓕 s is trivial.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.IsLocallySquareIntegrable.isLocalSubmartingale_sq_norm
Mathematical statement
A locally square-integrable martingale has locally submartingale squared norm.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.IsLocalSubmartingale.locally_classD
Mathematical statement
A nonnegative local submartingale is locally of class D.
Source project: Brownian motion
Person-level attribution pending.