Standalone Lean project
A probability-theory development constructing and studying Brownian motion in Lean.
Flagship declarations
continuousWithinAt_Iio_indicator_Ioc
Plain-language statement
The indicator of a half-open interval Ioc a b with constant value c is left-continuous: when approached from the left it is eventually constant, so it is continuous within Iio t at t for every t.
Source project: Brownian motion
Person-level attribution pending.
Dense.comap_val_nhdsWithin_Iio_neBot
Plain-language statement
This is the dual of Dense.comap_val_nhdsWithin_Ioi_neBot.
Source project: Brownian motion
Person-level attribution pending.
Dense.comap_val_nhdsWithin_Ioi_neBot
Project documentation
This is an auxillary lemma used to prove Dense.monotone_of_isRightContinuous. It is saying that if D is a dense set and a, b are two points such that a < b, then the comap of 𝓝[Set.Ioi a] a under the inclusion D → α is nontrivial. Note that a < b is necessary as this is clearly not true if a is a top element.
Source project: Brownian motion
Person-level attribution pending.
Dense.monotone_of_isRightContinuous
Project documentation
If f is monotone on a dense set D and is right continuous, then f is monotone. We prove under the assumption that α has a top element ⊤ and ⊤ ∈ D, which is a necessary assumption because otherwise it is possible that ⊤ is an isolated point. This theorem should be also true when α satisfies NoTopOrder α.
Source project: Brownian motion
Person-level attribution pending.
equation4
Project documentation
Apply the optional stopping theorem to get equation 4. Note that T1 Space is needed to make sure that mesh ι n has order topology.
Source project: Brownian motion
Person-level attribution pending.
InfClosed.mem_countableInfClosure_iff
Plain-language statement
If the set is inf-closed, elements of countablInfClosure can be written as countable intersections of antitone sequences of sets.
Source project: Brownian motion
Person-level attribution pending.
Project index
Showing 8 of 64 additional declarations. Use project search for the complete index.
IsCadlag.not_accPt_largeLeftJumpSet
Plain-language statement
The set of large left jump times has no accumulation points. TODO: maybe to_dual can be extended to simplify this proof as the proof of the second part is very similar to the first part.
Source project: Brownian motion
Person-level attribution pending.
IsCompactSystem.equiv
Plain-language statement
Transport a compact system along an equivalence of types.
Source project: Brownian motion
Person-level attribution pending.
IsCompactSystem.finsetCoe
Plain-language statement
The set of Finset coercions forms a compact system.
Source project: Brownian motion
Person-level attribution pending.
isLocallyBounded_of_isCadlag
Plain-language statement
A càdlàg function is locally bounded.
Source project: Brownian motion
Person-level attribution pending.
le_liminf_of_eventually_monotone_of_tendsto_on_dense
Plain-language statement
This is the dual of limsup_le_of_eventually_monotone_of_tendsto_on_dense.
Source project: Brownian motion
Person-level attribution pending.
limsup_le_of_eventually_monotone_of_tendsto_on_dense
Plain-language statement
Convergence on a dense set of a collection of monotone function controls the limsup at a point if f is right continuous at a. We prove this under the assumption that α has both a bottom element and a top element. The bottom element is needed because otherwise limsup evaluated at the bottome element may give a junk value to break the inequality.
Source project: Brownian motion
Person-level attribution pending.
MeasureTheory.eLpNorm_indicator_tail_eq_setIntegral_norm
Project documentation
A helper lemma for uniformIntegrable_iff_tendsto_iSup_setIntegral_norm.
Source project: Brownian motion
Person-level attribution pending.
MeasureTheory.eLpNorm_indicator_tail_eq_setIntegral_of_nonneg
Project documentation
A helper lemma for uniformIntegrable_iff_tendsto_iSup_setIntegral_of_nonneg.
Source project: Brownian motion
Person-level attribution pending.