Skip to main content

Source-pinned research

Research proof index

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.

All topics

Showing 1,345 to 1,350 of 2,569 results.

Project-declaredLean 4.8.0

Hoeffdings lemma

hoeffdings_lemma

Project documentation

The Beroulli case of Hoeffding's lemma

probabilitycomplexity theoryinteractive protocols

Source project: debate

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Holder van der corput

holder_van_der_corput

Mathematical statement

If φ\varphi is supported in the ball B(z,R)B(z,R), then the oscillatory integral with phase difference fgf-g satisfies

ei(f(x)g(x))φ(x)dxC(a)μ(B(z,R))φHol,τ;B(z,2R)(1+dz,R(f,g))1/(2a2+a3).\left\lVert\int e^{i(f(x)-g(x))}\varphi(x)\,dx\right\rVert \le C(a)\,\mu(B(z,R))\,\lVert\varphi\rVert_{\mathrm{Hol},\tau;B(z,2R)}\,(1+d_{z,R}(f,g))^{-1/(2a^2+a^3)}.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Holder On With of i Hol ENorm ne top

HolderOnWith.of_iHolENorm_ne_top

Mathematical statement

If the project’s inhomogeneous tt-Hölder norm of φ\varphi on the ball B(z,R)B(z,R) is finite and t0t\ge0, then φ\varphi is tt-Hölder on that ball. A valid Hölder constant is the finite normalized norm divided by RtR^t.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

Homomorphism pfr

homomorphism_pfr

Project documentation

Let f:GGf: G \to G' be a function, and let SS denote the set S:={f(x+y)f(x)f(y):x,yG}. S := \{ f(x+y)-f(x)-f(y): x,y \in G \}. Then there exists a homomorphism ϕ:GG\phi: G \to G' such that {f(x)ϕ(x)}S10.|\{f(x) - \phi(x)\}| \leq |S|^{10}.

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record
Project-declaredLean 4.28.0

Funext pos trace

HPMap.funext_pos_trace

Mathematical statement

Two maps are equal if they agree on all positive inputs with trace one

quantum informationentropyquantum channels

Source project: quantumInfo

Person-level attribution pending.

View proof record
Project-declaredLean 4.28.0

Hₛ le log d

Hₛ_le_log_d

Mathematical statement

Shannon entropy of a distribution is at most ln d.

quantum informationentropyquantum channels

Source project: quantumInfo

Person-level attribution pending.

View proof record