WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Random walk

Revision #1524 → #2186 · back to history

modifiedRandom walk602e307e0b5c
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no general random-walk definition; only Brownian motion and CLT-style stochastic objects exist.
status—not_formalized
modifiedElementary random walk on the integers5742d0c016ea
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No formalization of the integer-line random walk exists in Mathlib.
status—not_formalized
modifiedLattice random walk5cfec166b2cd
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no lattice random walk definition.
status—not_formalized
modifiedSimple random walk2670f857a2aa
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No simple-random-walk definition in Mathlib.
status—not_formalized
modifiedSimple symmetric random walk1fcfdcbf8381
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib lacks any symmetric random walk definition.
status—not_formalized
modifiedSimple bordered symmetric random walkd85682e17305
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No bordered symmetric random walk in Mathlib.
status—not_formalized
modifiedOne-dimensional random walk83657580d51e
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized in Mathlib.
status—not_formalized
modifiedSimple random walk on Zcfbfefff2cce
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Simple random walk on Z has no Mathlib definition.
status—not_formalized
modifiedExpected position is zero6ee327c93111
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Mathlib statement about expected position of a simple random walk.
status—not_formalized
modifiedExpected translation distance order sqrt(n)766ee1fd0351
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No √n diffusive scaling result for random walks in Mathlib.
status—not_formalized
modifiedRecurrence of simple random walk on Zf48c5df4f947
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib does not contain the recurrence theorem for the simple random walk on Z.
status—not_formalized
modifiedExpected hitting time and hitting probabilities2cc782844a97
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No gambler's-ruin hitting time formula in Mathlib.
status—not_formalized
modifiedCounting walks via Pascal's triangle01f5d878da02
FieldFrom #1524To #2186
mathlib.decl—Nat.sum_range_choose
mathlib.match_kind—generalization
mathlib.module—Mathlib.Data.Nat.Choose.Sum
note—The underlying identity ∑ C(n,k) = 2^n is in Mathlib, but the random-walk counting interpretation is not.
status—partial
modifiedCentral limit theorem for simple random walksfe316e343ab2
FieldFrom #1524To #2186
mathlib.decl—ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum_sub
mathlib.match_kind—generalization
mathlib.module—Mathlib.Probability.CentralLimitTheorem
note—Mathlib has the 1D CLT for iid sums (a generalization), but no law of the iterated logarithm and no random-walk specialization.
status—partial
modifiedCLT and large deviations on crystal lattices98440d5b3e24
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No large deviations / crystal-lattice CLT in Mathlib.
status—not_formalized
modifiedRandom walk as a Markov chainf6d71f32005c
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has Markov kernels but no Markov-chain wrapping of the simple random walk.
status—not_formalized
modifiedHeterogeneous random walk3888faa5490a
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized in Mathlib.
status—not_formalized
modifiedTrajectory is a discrete fractalbb0b02a83f40
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No statement about discrete fractality of random walk trajectories in Mathlib.
status—not_formalized
modifiedTwo-dimensional random walk on a city grid76e179aebc47
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Illustrative example with no Mathlib counterpart.
status—not_formalized
modifiedPólya's recurrence theoremaaa112129894
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Pólya's recurrence theorem is not in Mathlib.
status—not_formalized
modifiedMeeting of two independent random walks928c6ae8f294
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized in Mathlib.
status—not_formalized
modifiedErdős–Taylor intersection theorem2de454a52611
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Erdős–Taylor intersection result is absent from Mathlib.
status—not_formalized
modifiedRayleigh distribution asymptotic for 2D random walkaffbf2f1f190
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no Rayleigh distribution or this asymptotic.
status—not_formalized
modifiedWiener process3b30363a41e6
FieldFrom #1524To #2186
mathlib.decl—ProbabilityTheory.IsBrownianReal
mathlib.match_kind—exact
mathlib.module—Mathlib.Probability.BrownianMotion.Basic
note—Brownian motion (synonymous with Wiener process) is formalized as IsBrownianReal.
status—formalized
modifiedWiener process as scaling limitcf1408d5ad46
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Scaling-limit theorem (Donsker-type) is not in Mathlib.
status—not_formalized
modifiedAverage steps to hit a circlee6aab8096e27
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized in Mathlib.
status—not_formalized
modifiedHausdorff dimension of Wiener trajectoryb23514abe104
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Hausdorff dimension is in Mathlib but not applied to Brownian sample paths.
status—not_formalized
modifiedBoundary of Wiener trajectory has dimension 4/34e589ae22f41
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Lawler–Schramm–Werner result is not in Mathlib.
status—not_formalized
modifiedSkorokhod embedding and KMT coupling35db14942cf1
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Neither Skorokhod embedding nor KMT coupling is formalized.
status—not_formalized
modifiedDonsker's theorema56b9c70e4ad
FieldFrom #1524To #2186
mathlib.decl—ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum_sub
mathlib.match_kind—special_case
mathlib.module—Mathlib.Probability.CentralLimitTheorem
note—Mathlib has the finite-dimensional CLT but not the functional Donsker invariance principle.
status—partial
modifiedGaussian random walkbb87ac1273cc
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Gaussian-step random walk is not defined in Mathlib.
status—not_formalized
modifiedExpected value of Gaussian random walk04ee801cc32a
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized in Mathlib.
status—not_formalized
modifiedDistribution of translation distance after n steps336133a33f00
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized in Mathlib.
status—not_formalized
modifiedRoot mean square translation distancefd2a2a86a988
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized in Mathlib.
status—not_formalized
modified68.27% and 50% probability intervals5bf63c60393c
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized in Mathlib.
status—not_formalized
modifiedNumber of distinct sites visited8e09a3698bbe
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Range of a random walk is not defined in Mathlib.
status—not_formalized
modifiedQuadratic rate distortion function4efcf903169f
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No rate distortion theory in Mathlib.
status—not_formalized
modifiedRandom walk on a graph6fb34a0f5447
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has combinatorial SimpleGraph.Walk but no probabilistic random walk on a graph.
status—not_formalized
modifiedTransience and resistance to infinitye333e2a6cc37
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Electric-network / transience theory is absent from Mathlib.
status—not_formalized
modifiedReversibility of random walk on graph659678d17252
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No reversibility statement for graph random walks in Mathlib.
status—not_formalized
modifiedRandom walk in random environment275b3c405104
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized in Mathlib.
status—not_formalized
modifiedMaximal entropy random walk8ca81f77601f
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—MERW is not in Mathlib.
status—not_formalized
modifiedSelf-avoiding walk5411408308ea
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Self-avoiding walks are not formalized in Mathlib.
status—not_formalized
modifiedMaximal entropy random walk (section)d234b9b1639e
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized in Mathlib.
status—not_formalized
modifiedCorrelated random walks19f0180415af
FieldFrom #1524To #2186
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized in Mathlib.
status—not_formalized
addedVariance of position after n stepseff0604b60c4
addedGambler's ruin interpretation2a3424493797
addedProbability of S_n = k via binomial coefficient7826eb5aef0b
addedGaussian limit via Stirling's formula1d0e628e40d9
addedProbability of recurrence in d dimensions75c17109dcea
addedTrajectory of a random walk02c711054bb2
addedVariance of random walk position grows linearly in time0984ddf51eab
addedLoop-erased random walk0d68d5e4d895
addedReinforced random walk54766552edaf
addedRandom walk hypothesis in financial economics598c39febbe3
addedPólya's question on meeting of two walkersd3ed36c98203