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 research declarations. Search 10,000 more complete Mathlib declarations.

All topics

Showing 457 to 462 of 2,569 results.

Project-declaredLean 4.8.0

Chernoff count le

chernoff_count_le

Project documentation

Weak Chernoff's theorem for the Bernoulli case

probabilitycomplexity theoryinteractive protocols

Source project: debate

Person-level attribution pending.

View proof record
Project-declaredLean 4.8.0

Chernoff estimate abs le

chernoff_estimate_abs_le

Mathematical statement

Chernoff symmetric bound for estimate

probabilitycomplexity theoryinteractive protocols

Source project: debate

Person-level attribution pending.

View proof record
Project-declaredLean 4.8.0

Chernoff le count

chernoff_le_count

Mathematical statement

Chernoff lower bound

probabilitycomplexity theoryinteractive protocols

Source project: debate

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Rows linearly independent

CKMMatrix.rows_linearly_independent

Mathematical statement

The rows of a CKM matrix are linearly independent.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

VAbs sum sq row eq one

CKMMatrix.VAbs_sum_sq_row_eq_one

Mathematical statement

The absolute value squared of any row of a CKM matrix is 1, in terms of Vabs.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Classical carleson

classical_carleson

Mathematical statement

For every continuous, 2π2\pi-periodic function f:RCf : \mathbb{R} \to \mathbb{C}, the symmetric partial Fourier sums SNf(x)S_N f(x) converge to f(x)f(x) for almost every xRx \in \mathbb{R}.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record