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,711 to 1,716 of 2,569 results.
MeasureTheory.dLpNorm_translate
Mathematical statement
Translation preserves the discrete normalized norm: for every group element , .
Source project: Arithmetic Progressions Almost Periodicity
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.
MeasureTheory.IsPavingAnalyticFor.fst
Mathematical statement
The projection of an analytic set is analytic.
Source project: Brownian motion
Person-level attribution pending.
MeasureTheory.IsPavingAnalyticFor.isCapacitable
Project documentation
Choquet's capacitability theorem.
Source project: Brownian motion
Person-level attribution pending.
MeasureTheory.isStoppingTime_debut
Mathematical statement
Debut Theorem: The debut of a progressively measurable set E is a stopping time.
Source project: Brownian motion
Person-level attribution pending.