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 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,723 to 1,728 of 2,569 results.
MeasureTheory.ringHaarChar_padic
Mathematical statement
The distributive Haar character of the action of ℚ_[p]ˣ on ℚ_[p] is the usual p-adic norm. This means that volume (x • s) = ‖x‖ * volume s for all x : ℚ_[p] and s : Set ℚ_[p]. See Padic.volume_padic_smul
Source project: Fermat's Last Theorem
Person-level attribution pending.
MeasureTheory.Submartingale.classDL
Mathematical statement
A nonnegative right-continuous submartingale is of class DL.
Source project: Brownian motion
Person-level attribution pending.
MeasureTheory.Submartingale.integrableOn_const_tauMesh_lt_top
Mathematical statement
The constant c is integrable on the event where τₙ(c) hits before the top element.
Source project: Brownian motion
Person-level attribution pending.
MeasureTheory.Submartingale.iSup_ofReal_ne_top
Mathematical statement
Alternative form of Submartingale.ae_bddAbove.
Source project: Brownian motion
Person-level attribution pending.
MeasureTheory.Submartingale.monotone_predictablePart_ae
Mathematical statement
For a submartingale indexed by a countable type, the predictable part is monotone a.e.
Source project: Brownian motion
Person-level attribution pending.
MeasureTheory.Submartingale.tauMesh_lt_top_eq_lt_predictableSeqTop
Mathematical statement
{τₙ(c) < 1} = {c < Aⁿ₁}.
Source project: Brownian motion
Person-level attribution pending.