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 167 research declarations. Search 10,000 more complete Mathlib declarations.
167 results
Clear filtersisLocallyBounded_of_isCadlag
Plain-language statement
A càdlàg function is locally bounded.
Source project: Brownian motion
Person-level attribution pending.
iteratedDerivWithin_eq_iteratedDeriv
Plain-language statement
Get rid of Within from iteratedDeriv for smooth functions
Source project: debate
Person-level attribution pending.
KLDiv_add_le_KLDiv_of_indep
Plain-language statement
If are independent -valued random variables, then
Source project: Polynomial Freiman-Ruzsa project
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.