therefore
Sign up
Open navigation

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

1 topic

2 results

Clear filters
Project-declaredLean 4.33.0-rc1

Multi Tau min sum le

multiTau_min_sum_le

Plain-language statement

If (Xi)1≤i≤m(X_i)_{1 \leq i \leq m} is a τ\tau-minimizer, then ∑i=1md[Xi;X0]≤2mηd[X0;X0]\sum_{i=1}^m d[X_i; X^0] \leq \frac{2m}{\eta} d[X^0; X^0].

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

Sub cond Multi Distance le

sub_condMultiDistance_le

Project documentation

If (Xi)1≤i≤m(X_i)_{1 \leq i \leq m} is a τ\tau-minimizer, and k:=D[(Xi)1≤i≤m]k := D[(X_i)_{1 \leq i \leq m}], then for any other tuples (Xi′)1≤i≤m(X'_i)_{1 \leq i \leq m} and (Yi)1≤i≤m(Y_i)_{1 \leq i \leq m} with the Xi′X'_i G$-valued, one has k−D[(Xi′)1≤i≤m∣(Yi)1≤i≤m]≤η∑i=1md[Xi;Xi′∣Yi]. k - D[(X'_i)_{1 \leq i \leq m} | (Y_i)_{1 \leq i \leq m}] \leq \eta \sum_{i=1}^m d[X_i; X'_i|Y_i].

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record